:: deftheorem defines gcd_main_loop NOMIN_4:def 19 :
for V, A being set
for a, b being Element of V holds gcd_main_loop (V,A,a,b) = PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b)));