...antecedents 

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

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.