:: deftheorem defines gcd_conditional_step NOMIN_4:def 17 :
for V, A being set
for a, b being Element of V holds gcd_conditional_step (V,A,a,b) = PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A))));