let x1, x2, x3, x4 be Instruction of SCMPDS; :: thesis: card (((x1 ';' x2) ';' x3) ';' x4) = 4
thus card (((x1 ';' x2) ';' x3) ';' x4) = (card ((x1 ';' x2) ';' x3)) + 1 by SCMP_GCD:4
.= ((card (x1 ';' x2)) + 1) + 1 by SCMP_GCD:4
.= (2 + 1) + 1 by SCMP_GCD:5
.= 4 ; :: thesis: verum