thus card ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))) =
(card (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0)))) + (card (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))
by AFINSQ_1:17
.=
4 + (card (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))
by Th4
.=
4 + (((card ((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1))))) + (card (Load ((GBP,7) := 0)))) + 2)
by SCMPDS_6:65
.=
4 + ((2 + (card (Load ((GBP,7) := 0)))) + 2)
by SCMP_GCD:5
.=
4 + ((2 + 1) + 2)
by COMPOS_1:54
.=
9
; verum