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:8
.= ((card (x1 ';' x2)) + 1) + 1 by SCMP_GCD:8
.= (2 + 1) + 1 by SCMP_GCD:9
.= 4 ; :: thesis: verum