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