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