let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let x0, y0, p0, q0 be Integer; :: thesis:
let n0 be Nat; :: thesis:
let val be 10 -element FinSequence; :: thesis:
set size = 10;
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 b1 = val . 5;
set c1 = val . 6;
set p1 = val . 7;
set q1 = val . 8;
set ps1 = val . 9;
set qc1 = val . 10;
set EN = {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6),(val . 7),(val . 8),(val . 9),(val . 10)};
set D = ND (V,A);
set I = valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0);
set inv = Lucas_inv (A,loc,x0,y0,p0,q0,n0);
set DS = denamingSeq (V,A,val);
set SE = SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)));
set Q1 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2));
set P1 = SC_Psuperpos ((SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))),((denamingSeq (V,A,val)) . 1),(loc /. 1));
set inp = Lucas_input (x0,y0,p0,q0,n0);
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: Seg 10 c= dom loc and
A4: loc | (Seg 10) is one-to-one and
A5: loc,val are_different_wrt 10 ; :: thesis:
A6: Seg 10 = dom val by FINSEQ_1:89;
A7: len val = 10 by CARD_1:def 7;
A8: len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) = len val by NOMIN_8:def 9;
A9: len (Lucas_input (x0,y0,p0,q0,n0)) = 10 by CARD_1:def 7;
A10: len (denamingSeq (V,A,val)) = 10 by NOMIN_8:def 8, A7;
A11: (denamingSeq (V,A,val)) . 1 = denaming (V,A,(val . 1)) by NOMIN_8:def 8, A10;
A12: (denamingSeq (V,A,val)) . 2 = denaming (V,A,(val . 2)) by NOMIN_8:def 8, A10;
A13: (denamingSeq (V,A,val)) . 9 = denaming (V,A,(val . 9)) by NOMIN_8:def 8, A10;
A14: (denamingSeq (V,A,val)) . 10 = denaming (V,A,(val . 10)) by NOMIN_8:def 8, A10;
A15: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (8 + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),(denaming (V,A,(val . ((len val) - 8)))),(loc /. ((len val) - 8))) by A7, A8, NOMIN_8:def 9
.= SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2)) by NOMIN_8:def 8, A10, A7 ;
A16: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (9 + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9),(denaming (V,A,(val . ((len val) - 9)))),(loc /. ((len val) - 9))) by A7, A8, NOMIN_8:def 9
.= SC_Psuperpos ((SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))),((denamingSeq (V,A,val)) . 1),(loc /. 1)) by NOMIN_8:def 8, A10, A7, A15 ;
let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis:
assume ( d in dom (valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) & (valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) . d = TRUE ) ; :: thesis:
then Lucas_input (x0,y0,p0,q0,n0) is_valid_input V,A,val,d by NOMIN_8:def 11;
then consider d1 being NonatomicND of V,A such that
A17: d = d1 and
A18: val is_valid_wrt d1 and
A19: for n being Nat st 1 <= n & n <= len (Lucas_input (x0,y0,p0,q0,n0)) holds
d1 . (val . n) = (Lucas_input (x0,y0,p0,q0,n0)) . n ;
A20: d1 . (val . 1) = (Lucas_input (x0,y0,p0,q0,n0)) . 1 by A9, A19
.= 0 ;
A21: d1 . (val . 2) = (Lucas_input (x0,y0,p0,q0,n0)) . 2 by A9, A19
.= 1 ;
A22: d1 . (val . 3) = (Lucas_input (x0,y0,p0,q0,n0)) . 3 by A9, A19
.= n0 ;
A23: d1 . (val . 4) = (Lucas_input (x0,y0,p0,q0,n0)) . 4 by A9, A19
.= x0 ;
A24: d1 . (val . 5) = (Lucas_input (x0,y0,p0,q0,n0)) . 5 by A9, A19
.= y0 ;
A25: d1 . (val . 7) = (Lucas_input (x0,y0,p0,q0,n0)) . 7 by A9, A19
.= p0 ;
A26: d1 . (val . 8) = (Lucas_input (x0,y0,p0,q0,n0)) . 8 by A9, A19
.= q0 ;
set F = LocalOverlapSeq (A,loc,val,d1,10);
A27: len (LocalOverlapSeq (A,loc,val,d1,10)) = 10 by NOMIN_7:def 4;
then A28: loc,val,10 are_correct_wrt d1 by A1, A2, A6, A18, FINSEQ_1:def 3;
A29: dom ((denamingSeq (V,A,val)) . 1) = { d where d is NonatomicND of V,A : val . 1 in dom d } by A11, NOMIN_1:def 18;
A30: dom (SC_Psuperpos ((SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))),((denamingSeq (V,A,val)) . 1),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(((denamingSeq (V,A,val)) . 1) . d),(loc /. 1)) in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))) & d in dom ((denamingSeq (V,A,val)) . 1) ) } by NOMIN_2:def 11;
A31: dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(((denamingSeq (V,A,val)) . 2) . d),(loc /. 2)) in dom ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8) & d in dom ((denamingSeq (V,A,val)) . 2) ) } by NOMIN_2:def 11;
1 in dom val by A6;
then val . 1 in rng val by FUNCT_1:def 3;
then A32: d1 in dom ((denamingSeq (V,A,val)) . 1) by A18, A29;
A33: (LocalOverlapSeq (A,loc,val,d1,10)) . 1 is NonatomicND of V,A by A27, NOMIN_7:def 6;
reconsider Lqc = (LocalOverlapSeq (A,loc,val,d1,10)) . 10 as NonatomicND of V,A by A27, NOMIN_7:def 6;
A34: (LocalOverlapSeq (A,loc,val,d1,10)) . 1 = local_overlapping (V,A,d1,(((denamingSeq (V,A,val)) . 1) . d1),(loc /. 1)) by A11, NOMIN_7:def 4;
A35: (LocalOverlapSeq (A,loc,val,d1,10)) . (1 + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . 1),(((denamingSeq (V,A,val)) . 2) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 1)),(loc /. 2)) by A12, A27, NOMIN_7:def 4;
A36: (LocalOverlapSeq (A,loc,val,d1,10)) . 1 in dom ((denamingSeq (V,A,val)) . 2) by A12, A27, A28, NOMIN_8:15;
A37: dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) = ND (V,A) by Def15;
then A38: Lqc in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) ;
A39: (10 - 8) - 1 = 1 ;
A40: 8 + 1 < 10 ;
local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . (10 - 1)),((denaming (V,A,(val . (len val)))) . ((LocalOverlapSeq (A,loc,val,d1,10)) . (10 - 1))),(loc /. (len val))) in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) by A37;
then (LocalOverlapSeq (A,loc,val,d1,10)) . 2 in dom ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8) by A12, A7, A28, A35, A39, A40, NOMIN_8:16;
then A41: (LocalOverlapSeq (A,loc,val,d1,10)) . 1 in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))) by A35, A31, A33, A36;
hence d in dom ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))))) by A34, A17, A30, A32, A7, A8, A16; :: thesis:
A42: Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,Lqc

proof

take Lqc ; :: according to NOMIN_9:def 14 :: thesis:
thus Lqc = Lqc ; :: thesis:
thus {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom Lqc :: thesis:

proof

A43: loc /. 1 in dom Lqc by A28, NOMIN_7:9;
A44: loc /. 2 in dom Lqc by A28, NOMIN_7:9;
A45: loc /. 3 in dom Lqc by A28, NOMIN_7:9;
A46: loc /. 4 in dom Lqc by A28, NOMIN_7:9;
A47: loc /. 5 in dom Lqc by A28, NOMIN_7:9;
A48: loc /. 6 in dom Lqc by A28, NOMIN_7:9;
A49: loc /. 7 in dom Lqc by A28, NOMIN_7:9;
A50: loc /. 8 in dom Lqc by A28, NOMIN_7:9;
A51: loc /. 9 in dom Lqc by A28, NOMIN_7:9;
loc /. 10 in dom Lqc by A28, NOMIN_7:9;
hence {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom Lqc by A43, A44, A45, A46, A47, A48, A49, A50, A51, ENUMSET1:def 8; :: thesis:

end;

thus Lqc . (loc /. 2) = d1 . (val . 2) by A3, A4, A5, A28, NOMIN_7:13
.= 1 by A21 ; :: thesis:
thus Lqc . (loc /. 3) = d1 . (val . 3) by A3, A4, A5, A28, NOMIN_7:13
.= n0 by A22 ; :: thesis:
thus Lqc . (loc /. 7) = d1 . (val . 7) by A3, A4, A5, A28, NOMIN_7:13
.= p0 by A25 ; :: thesis:
thus Lqc . (loc /. 8) = d1 . (val . 8) by A3, A4, A5, A28, NOMIN_7:13
.= q0 by A26 ; :: thesis:
take 0 ; :: thesis:
thus Lqc . (loc /. 1) = d1 . (val . 1) by A3, A4, A5, A28, NOMIN_7:13
.= 0 by A20 ; :: thesis:
thus Lqc . (loc /. 4) = d1 . (val . 4) by A3, A4, A5, A28, NOMIN_7:13
.= x0 by A23
.= Lucas (x0,y0,p0,q0,0) by Th5 ; :: thesis:
thus Lqc . (loc /. 5) = d1 . (val . 5) by A3, A4, A5, A28, NOMIN_7:13
.= y0 by A24
.= Lucas (x0,y0,p0,q0,(0 + 1)) by Th5 ; :: thesis:

end;

A52: ( 10 - 9 = 1 & 10 - 1 = 9 ) ;
A53: ( 8 + 1 = 9 & 8 = 10 - 2 ) ;
A54: local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . 9),(((denamingSeq (V,A,val)) . 10) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 9)),(loc /. 10)) in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) by A37;
set dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . 8),(((denamingSeq (V,A,val)) . 9) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 8)),(loc /. 9));
A55: local_overlapping (V,A,(local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . 8),(((denamingSeq (V,A,val)) . 9) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 8)),(loc /. 9))),(((denamingSeq (V,A,val)) . 10) . (local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,10)) . 8),(((denamingSeq (V,A,val)) . 9) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 8)),(loc /. 9)))),(loc /. 10)) in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) by A37;
thus ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))))) . d = (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),((denamingSeq (V,A,val)) . 2),(loc /. 2))) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 1) by A11, A12, A14, A7, A15, A17, A28, A34, A41, A52, A53, A54, NOMIN_8:19
.= ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1) . ((LocalOverlapSeq (A,loc,val,d1,10)) . 9) by A14, A7, A15, A28, A52, A54, NOMIN_8:17
.= (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . Lqc by A13, A14, A7, A28, A52, A53, A54, A55, NOMIN_8:18
.= TRUE by A38, A42, Def15 ; :: thesis: