:: deftheorem defines gcd_program NOMIN_4:def 22 :
for V, A being set
for a, b being Element of V
for x, y being object
for z being Element of V holds gcd_program (V,A,a,b,x,y,z) = PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z)));