thus card GCD-Algorithm = (card (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) + (card (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))) by SCMPDS_4:45
.= ((card ((GBP := 0 ) ';' (GBP ,3 := GBP ,1))) + 1) + (card (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))) by SCMP_GCD:8
.= (2 + 1) + 9 by Lm13, SCMP_GCD:9
.= 12 ; :: thesis: verum