thus card (while>0 GBP ,5,(((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 ))))) ';' (while>0 GBP ,7,(((((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 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))) = 29 + 2 by Lm17, SCMPDS_8:17
.= 31 ; :: thesis: verum