let i, j be Instruction of SCMPDS ; :: thesis: card (i ';' j) = 2
thus card (i ';' j) = card ((Load i) ';' (Load j)) by SCMPDS_4:def 6
.= (card (Load i)) + (card (Load j)) by SCMPDS_4:45
.= 1 + (card (Load j)) by SCMPDS_5:6
.= 1 + 1 by SCMPDS_5:6
.= 2 ; :: thesis: verum