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 AFINSQ_1:17
.=
((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:4
.=
(2 + 1) + 9
by Lm11, SCMP_GCD:5
.=
12
; verum