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