thus card Partition = (card (((((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (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))))))) ';' (GBP ,6 := (intpos 4),0 )) ';' ((intpos 4),0 := (intpos 2),0 ))) + 1 by SCMP_GCD:8
.= ((card ((((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (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))))))) ';' (GBP ,6 := (intpos 4),0 ))) + 1) + 1 by SCMP_GCD:8
.= (((card (((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (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)))))))) + 1) + 1) + 1 by SCMP_GCD:8
.= ((((card ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1))) + (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)))))))) + 1) + 1) + 1 by SCMPDS_4:45
.= (((4 + 31) + 1) + 1) + 1 by Lm18, Th4
.= 38 ; :: thesis: verum