let i1, i2, i3 be Instruction of SCM+FSA ; :: thesis: card ((i1 ';' i2) ';' i3) = 6
thus card ((i1 ';' i2) ';' i3) = (card (i1 ';' i2)) + (card (Macro i3)) by SCMFSA6A:61
.= (card (i1 ';' i2)) + 2 by SCMFSA7B:6
.= ((card (Macro i1)) + (card (Macro i2))) + 2 by SCMFSA6A:61
.= (2 + (card (Macro i2))) + 2 by SCMFSA7B:6
.= (2 + 2) + 2 by SCMFSA7B:6
.= 6 ; :: thesis: verum