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 ))))) ';' (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))))) = (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 ))))) ';' (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 ))))))) + (card (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))))) by SCMPDS_4:45
.= (11 + 11) + (card (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))))) by Lm11, Lm13, SCMPDS_4:45
.= 22 + ((card ((((((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)))) + 1) by SCMPDS_6:89
.= 22 + (((card (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1))) + 1) + 1) by SCMP_GCD:8
.= 22 + ((((card ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2)))) + 1) + 1) + 1) by SCMP_GCD:8
.= 22 + (((((card (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6))) + 1) + 1) + 1) + 1) by SCMP_GCD:8
.= 22 + ((((((card ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 ))) + 1) + 1) + 1) + 1) + 1) by SCMP_GCD:8
.= 22 + (((((2 + 1) + 1) + 1) + 1) + 1) by SCMP_GCD:9
.= 29 ; :: thesis: verum