let V, A be set ; for loc being V -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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)))))
let loc be V -valued Function; for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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)))))
let x0, y0, p0, q0 be Integer; for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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)))))
let n0 be Nat; for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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)))))
let val be 10 -element FinSequence; ( not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 implies valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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))))) )
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
; valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (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)))))
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); NOMIN_3:def 3 ( not d in dom (valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) or not (valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) . d = TRUE or ( 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)))))) & ((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 = TRUE ) )
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 )
; ( 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)))))) & ((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 = TRUE )
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; ((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 = TRUE
A42:
Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,Lqc
proof
take
Lqc
;
NOMIN_9:def 14 ( Lqc = Lqc & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom Lqc & Lqc . (loc /. 2) = 1 & Lqc . (loc /. 3) = n0 & Lqc . (loc /. 7) = p0 & Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus
Lqc = Lqc
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom Lqc & Lqc . (loc /. 2) = 1 & Lqc . (loc /. 3) = n0 & Lqc . (loc /. 7) = p0 & Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom Lqc
( Lqc . (loc /. 2) = 1 & Lqc . (loc /. 3) = n0 & Lqc . (loc /. 7) = p0 & Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )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;
verum
end;
thus Lqc . (loc /. 2) =
d1 . (val . 2)
by A3, A4, A5, A28, NOMIN_7:13
.=
1
by A21
;
( Lqc . (loc /. 3) = n0 & Lqc . (loc /. 7) = p0 & Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus Lqc . (loc /. 3) =
d1 . (val . 3)
by A3, A4, A5, A28, NOMIN_7:13
.=
n0
by A22
;
( Lqc . (loc /. 7) = p0 & Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus Lqc . (loc /. 7) =
d1 . (val . 7)
by A3, A4, A5, A28, NOMIN_7:13
.=
p0
by A25
;
( Lqc . (loc /. 8) = q0 & ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus Lqc . (loc /. 8) =
d1 . (val . 8)
by A3, A4, A5, A28, NOMIN_7:13
.=
q0
by A26
;
ex I being Nat st
( I = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) )
take
0
;
( 0 = Lqc . (loc /. 1) & Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,0) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(0 + 1)) )
thus Lqc . (loc /. 1) =
d1 . (val . 1)
by A3, A4, A5, A28, NOMIN_7:13
.=
0
by A20
;
( Lqc . (loc /. 4) = Lucas (x0,y0,p0,q0,0) & Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(0 + 1)) )
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
;
Lqc . (loc /. 5) = Lucas (x0,y0,p0,q0,(0 + 1))
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
;
verum
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
; verum