let V, A be set ; :: thesis: for a, b being Element of V
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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
<*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_loop_body (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
let a, b be Element of V; :: thesis: for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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
<*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_loop_body (V,A,a,b)),(gcd_inv (V,A,a,b,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 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 <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_loop_body (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) )
assume A1: ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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 ) ) ; :: thesis: <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_loop_body (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
set f = gcd_conditional_step (V,A,a,b);
set g = gcd_conditional_step (V,A,b,a);
set i = gcd_inv (V,A,a,b,x0,y0);
set p = PP_inversion (gcd_inv (V,A,a,b,x0,y0));
A2: PP_inversion (gcd_inv (V,A,a,b,x0,y0)) ||= PP_False (ND (V,A)) by PARTPR_2:10;
<*(PP_False (ND (V,A))),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by NOMIN_3:18;
then A3: <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by A2, NOMIN_3:15;
A4: <*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,b,a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by A1, Th20;
<*(PP_False (ND (V,A))),(gcd_conditional_step (V,A,b,a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by NOMIN_3:18;
then <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_conditional_step (V,A,b,a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by A2, NOMIN_3:15;
then <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)))),(PP_or ((gcd_inv (V,A,a,b,x0,y0)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A)) by A3, A4, NOMIN_3:24;
hence <*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_loop_body (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) ; :: thesis: verum