let V, A be set ; :: thesis: for loc being V -valued Function
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)
let loc be V -valued Function; :: thesis: for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)
let z be Element of V; :: thesis: for x0, y0, p0, q0 being Integer
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)
let x0, y0, p0, q0 be Integer; :: thesis: for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)
let n0 be Nat; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) implies PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z) )
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 D = ND (V,A);
set res = Lucas (x0,y0,p0,q0,n0);
set inv = Lucas_inv (A,loc,x0,y0,p0,q0,n0);
set Di = denaming (V,A,(loc /. 1));
set Dn = denaming (V,A,(loc /. 3));
set Ds = denaming (V,A,(loc /. 4));
set Dz = denaming (V,A,z);
set ass = SC_assignment ((denaming (V,A,(loc /. 4))),z);
set out = valid_Lucas_output (A,z,x0,y0,p0,q0,n0);
set F = SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z);
set E = Equality (A,(loc /. 1),(loc /. 3));
set EM = {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)};
assume that
A1: ( not V is empty & A is_without_nonatomicND_wrt V ) and
A2: for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ; :: thesis: PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)
let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis: ( not d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) or not (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . d = TRUE or ( d in dom (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE ) )
assume that
A3: d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) and
A4: (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . d = TRUE ; :: thesis: ( d in dom (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE )
A5: dom (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(loc /. 4))) . d),z) in dom (valid_Lucas_output (A,z,x0,y0,p0,q0,n0)) & d in dom (denaming (V,A,(loc /. 4))) ) } by NOMIN_2:def 11;
A6: dom (valid_Lucas_output (A,z,x0,y0,p0,q0,n0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } by NOMIN_8:def 13;
A7: dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d } by NOMIN_1:def 18;
A8: dom (denaming (V,A,z)) = { d where d is NonatomicND of V,A : z in dom d } by NOMIN_1:def 18;
A9: d in dom (Equality (A,(loc /. 1),(loc /. 3))) by A3, A4, PARTPR_1:23;
A10: d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) by A3, A4, PARTPR_1:23;
A11: dom (Equality (A,(loc /. 1),(loc /. 3))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by A2, NOMIN_4:11;
then A12: d in dom (denaming (V,A,(loc /. 1))) by A9, XBOOLE_0:def 4;
(Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . d = TRUE by A3, A4, PARTPR_1:23;
then Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d by A10, Def15;
then consider d1 being NonatomicND of V,A such that
A13: d = d1 and
A14: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1 and
d1 . (loc /. 2) = 1 and
A15: d1 . (loc /. 3) = n0 and
d1 . (loc /. 7) = p0 and
d1 . (loc /. 8) = q0 and
A16: ex I being Nat st
( I = d1 . (loc /. 1) & d1 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & d1 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) ;
A17: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A18: loc /. 3 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A19: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set L = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z);
A20: dd in dom (denaming (V,A,(loc /. 4))) by A7, A13, A14, A19;
then (denaming (V,A,(loc /. 4))) . d1 in ND (V,A) by A13, PARTFUN1:4;
then A21: ex d2 being TypeSCNominativeData of V,A st (denaming (V,A,(loc /. 4))) . d1 = d2 ;
then A22: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (denaming (V,A,z)) by A1, A13, NOMIN_4:6;
then A23: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (valid_Lucas_output (A,z,x0,y0,p0,q0,n0)) by A6;
hence A24: d in dom (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) by A5, A20; :: thesis: (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE
valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0, local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)

proof

consider I being Nat such that
A25: I = d1 . (loc /. 1) and
A26: d1 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) and
d1 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) by A16;
A27: ex d being NonatomicND of V,A st
( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = d & z in dom d ) by A8, A22;
then reconsider dlo = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) as NonatomicND of V,A ;
take dlo ; :: according to NOMIN_8:def 12,NOMIN_9:def 12 :: thesis: ( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo & <*z*> is_valid_wrt dlo & ( for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len <*z*> or dlo . (<*z*> . b₁) = <*(Lucas (x0,y0,p0,q0,n0))*> . b₁ ) ) )
thus local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo ; :: thesis: ( <*z*> is_valid_wrt dlo & ( for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len <*z*> or dlo . (<*z*> . b₁) = <*(Lucas (x0,y0,p0,q0,n0))*> . b₁ ) ) )
rng <*z*> = {z} by FINSEQ_1:38;
hence rng <*z*> c= dom dlo by A27, ZFMISC_1:31; :: according to NOMIN_7:def 1 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len <*z*> or dlo . (<*z*> . b₁) = <*(Lucas (x0,y0,p0,q0,n0))*> . b₁ )
let nn be Nat; :: thesis: ( not 1 <= nn or not nn <= len <*z*> or dlo . (<*z*> . nn) = <*(Lucas (x0,y0,p0,q0,n0))*> . nn )
assume that
A28: 1 <= nn and
A29: nn <= len <*z*> ; :: thesis: dlo . (<*z*> . nn) = <*(Lucas (x0,y0,p0,q0,n0))*> . nn
len <*z*> = 1 by FINSEQ_1:39;
then A30: nn = 1 by A28, A29, XXREAL_0:1;
A31: loc /. 1 is_a_value_on dd by A2;
A32: loc /. 3 is_a_value_on dd by A2;
A33: dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by FUNCT_3:def 7;
d in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> by A9, A11, FUNCT_3:def 7;
then A34: (Equality (A,(loc /. 1),(loc /. 3))) . d = (Equality A) . (<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d) by FUNCT_1:13;
A35: d in dom (denaming (V,A,(loc /. 3))) by A9, A11, XBOOLE_0:def 4;
A36: <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d = [((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)] by A9, A11, A33, FUNCT_3:def 7;
A37: (denaming (V,A,(loc /. 1))) . d = denaming ((loc /. 1),d1) by A13, A12, NOMIN_1:def 18
.= d1 . (loc /. 1) by A14, A17, NOMIN_1:def 12 ;
A38: (denaming (V,A,(loc /. 3))) . d = denaming ((loc /. 3),d1) by A13, A35, NOMIN_1:def 18
.= d1 . (loc /. 3) by A14, A18, NOMIN_1:def 12 ;
A39: (denaming (V,A,(loc /. 4))) . d = denaming ((loc /. 4),d1) by A20, A13, NOMIN_1:def 18
.= d1 . (loc /. 4) by A14, A19, NOMIN_1:def 12 ;
(Equality A) . (((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)) <> FALSE by A3, A4, A34, A36, PARTPR_1:23;
then (denaming (V,A,(loc /. 1))) . d = (denaming (V,A,(loc /. 3))) . d by A31, A32, NOMIN_4:def 9;
hence dlo . (<*z*> . nn) = <*(Lucas (x0,y0,p0,q0,n0))*> . nn by A1, A13, A15, A30, A21, A25, A26, A37, A38, A39, NOMIN_2:10; :: thesis: verum

end;

hence TRUE = (valid_Lucas_output (A,z,x0,y0,p0,q0,n0)) . (local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)) by A23, NOMIN_8:def 13
.= (SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)) . d by A24, NOMIN_2:35 ;
:: thesis: verum