let A be set ; :: thesis: for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₆ -valued 10 -element FinSequence
for val being 10 -element FinSequence
for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let x0, y0, p0, q0 be Integer; :: thesis: for n0 being Nat
for V being non empty set
for loc being b₂ -valued 10 -element FinSequence
for val being 10 -element FinSequence
for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: for V being non empty set
for loc being b₁ -valued 10 -element FinSequence
for val being 10 -element FinSequence
for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let V be non empty set ; :: thesis: for loc being V -valued 10 -element FinSequence
for val being 10 -element FinSequence
for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let loc be V -valued 10 -element FinSequence; :: thesis: for val being 10 -element FinSequence
for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let val be 10 -element FinSequence; :: thesis: for z being Element of V st 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let z be Element of V; :: thesis: ( 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) & loc is one-to-one & loc,val are_different_wrt 10 implies <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,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 p = loc /. 7;
set q = loc /. 8;
set ps = loc /. 9;
set qc = loc /. 10;
set i1 = val . 1;
set j1 = val . 2;
set n1 = val . 3;
set s1 = val . 4;
set D = ND (V,A);
set P = valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0);
set F = Lucas_main_part (A,loc,val);
set G = SC_assignment ((denaming (V,A,(loc /. 4))),z);
set Q = valid_Lucas_output (A,z,x0,y0,p0,q0,n0);
set inv = Lucas_inv (A,loc,x0,y0,p0,q0,n0);
set E = Equality (A,(loc /. 1),(loc /. 3));
assume that
A1: ( 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 & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ; :: thesis: ( not loc is one-to-one or not loc,val are_different_wrt 10 or <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) )
assume ( loc is one-to-one & loc,val are_different_wrt 10 ) ; :: thesis: <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
then A3: <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))))*> is SFHT of (ND (V,A)) by A1, A2, Th18;
A4: <*(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A1, A2, Th20;
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A2, Th21;
hence <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_program (A,loc,val,z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A3, A4, NOMIN_3:25; :: thesis: verum