[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] A problem about proving of "if"



Hi,
 
A state in the proving prodedure in PVS is like:
 
IF v1 >= 0 THEN v0 = v1 ELSE v0 = -v1 ENDIF AND v2 = v0
 
I hope it can be converted into the form like:
 
IF v1 >= 0 THEN v0 = v1 AND v2 = v0 ELSE v0 = -v1 AND v2 = v0 ENDIF
 
Which command can I use?
 
Really appreciate!
Thank you!
 
Huangchao

huangchao via foxmail