let V, A be set ; :: thesis: for loc being V -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
let loc be V -valued Function; :: thesis: for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one implies <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set b = loc /. 5;
set c = loc /. 6;
set D = ND (V,A);
set inv = Fibonacci_inv (A,loc,n0);
set B = Fibonacci_loop_body (A,loc);
set E = Equality (A,(loc /. 1),(loc /. 3));
set N = PP_inversion (Fibonacci_inv (A,loc,n0));
assume that
A1: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ) ) and
A2: Seg 6 c= dom loc and
A3: loc | (Seg 6) is one-to-one ; :: thesis: <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by A1, A2, A3, Th17;
then A4: <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_inv (A,loc,n0)))),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:3, NOMIN_3:15;
<*(PP_inversion (Fibonacci_inv (A,loc,n0))),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:19;
then <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(PP_inversion (Fibonacci_inv (A,loc,n0))))),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:3, NOMIN_3:15;
hence <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) by A4, NOMIN_3:26; :: thesis: verum