thus card (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) = (card ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 ))) + (card (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) by SCMPDS_4:45
.= 2 + (card (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) by SCMP_GCD:9
.= 2 + (((card (((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1)))) + (card (Load (GBP ,6 := 0 )))) + 2) by SCMPDS_6:79
.= 2 + ((((card ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1)))) + 1) + (card (Load (GBP ,6 := 0 )))) + 2) by SCMP_GCD:8
.= 2 + (((((card (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5))) + 1) + 1) + (card (Load (GBP ,6 := 0 )))) + 2) by SCMP_GCD:8
.= 2 + ((((((card ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 ))) + 1) + 1) + 1) + (card (Load (GBP ,6 := 0 )))) + 2) by SCMP_GCD:8
.= 2 + (((((2 + 1) + 1) + 1) + (card (Load (GBP ,6 := 0 )))) + 2) by SCMP_GCD:9
.= 2 + (((((2 + 1) + 1) + 1) + 1) + 2) by SCMPDS_5:6
.= 10 ; :: thesis: verum