thus card (((((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 )))) = (card ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 ))) + (card (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))) by SCMPDS_4:45
.= 4 + (card (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))) by Th4
.= 4 + (((card ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1)))) + (card (Load (GBP ,5 := 0 )))) + 2) by SCMPDS_6:79
.= 4 + ((2 + (card (Load (GBP ,5 := 0 )))) + 2) by SCMP_GCD:9
.= 4 + ((2 + 1) + 2) by SCMPDS_5:6
.= 9 ; :: thesis: verum