...antecedents 
PVS requires only that one consequent be proved, in order to prove the sequent
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.