let V, A be set ; :: thesis: for a, b, z being Element of V
for x, y being object
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))
let a, b, z be Element of V; :: thesis: for x, y being object
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))
let x, y be object ; :: thesis: for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))
let x0, y0 be Nat; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) implies <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A)) )
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
set Dz = denaming (V,A,z);
set e = Equality (A,a,b);
set i = gcd_inv (V,A,a,b,x0,y0);
set p = valid_gcd_input (V,A,x,y,x0,y0);
set q = PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)));
set r = valid_gcd_output (V,A,z,x0,y0);
set f = gcd_main_part (V,A,a,b,x,y);
set g = SC_assignment ((denaming (V,A,a)),z);
set P = PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))));
assume that
A1: ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y ) and
A2: A is complex-containing and
A3: for d being TypeSCNominativeData of V,A holds a is_complex_on d and
A4: for d being TypeSCNominativeData of V,A holds b is_complex_on d ; :: thesis: <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))
A5: for d being TypeSCNominativeData of V,A holds a is_a_value_on d by A2, A3, Th7;
A6: for d being TypeSCNominativeData of V,A holds b is_a_value_on d by A2, A4, Th7;
A7: <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A)) by A1, A2, A3, A4, Th24;
A8: <*(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((denaming (V,A,a)),z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A)) by A1, A5, A6, Th25;
<*(PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))),(SC_assignment ((denaming (V,A,a)),z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A)) by A2, A3, A4, Th26;
hence <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_program (V,A,a,b,x,y,z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A)) by A7, A8, NOMIN_3:25; :: thesis: verum