thus card (while>0 GBP ,5,(((((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 ))))) = 9 + 2 by Lm7, SCMPDS_8:17
.= 11 ; :: thesis: verum