let V, A be set ; :: thesis: for z being Element of V
for loc being V -valued Function
for n0 being Nat
for val being 6 -element FinSequence 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 /. 3 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 & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
let z be Element of V; :: thesis: for loc being V -valued Function
for n0 being Nat
for val being 6 -element FinSequence 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 /. 3 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 & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; :: thesis: for n0 being Nat
for val being 6 -element FinSequence 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 /. 3 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 & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: for val being 6 -element FinSequence 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 /. 3 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 & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
let val be 6 -element FinSequence; :: 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 /. 3 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 & loc,val are_different_wrt 6 implies <*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A)) )
set D = ND (V,A);
set p = valid_Fibonacci_input (V,A,val,n0);
set f = Fibonacci_main_part (A,loc,val);
set g = SC_assignment ((denaming (V,A,(loc /. 4))),z);
set q = valid_Fibonacci_output (A,z,n0);
set inv = Fibonacci_inv (A,loc,n0);
set E = Equality (A,(loc /. 1),(loc /. 3));
assume that
A1: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V ) and
A2: for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 3 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ; :: thesis: ( not Seg 6 c= dom loc or not loc | (Seg 6) is one-to-one or not loc,val are_different_wrt 6 or <*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A)) )
assume that
A3: Seg 6 c= dom loc and
A4: loc | (Seg 6) is one-to-one and
A5: loc,val are_different_wrt 6 ; :: thesis: <*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
A6: <*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) by A1, A2, A3, A4, A5, Th19;
A7: <*(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0)))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A)) by A1, A2, Th21;
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A)) by A2, Th22;
hence <*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A)) by A6, A7, NOMIN_3:25; :: thesis: verum