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

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

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 via foxmail