:: deftheorem defines gcd_loop_body NOMIN_4:def 18 :
for V, A being set
for a, b being Element of V holds gcd_loop_body (V,A,a,b) = PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)));