let A be set ; for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b6 -valued 10 -element FinSequence 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 /. 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 holds
<*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let x0, y0, p0, q0 be Integer; for n0 being Nat
for V being non empty set
for loc being b2 -valued 10 -element FinSequence 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 /. 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 holds
<*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; for V being non empty set
for loc being b1 -valued 10 -element FinSequence 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 /. 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 holds
<*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let V be non empty set ; for loc being V -valued 10 -element FinSequence 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 /. 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 holds
<*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let loc be V -valued 10 -element FinSequence; ( 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 /. 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 implies <*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,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;
assume that
A1:
A is complex-containing
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 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 )
; ( not loc is one-to-one or <*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) )
assume A4:
loc is one-to-one
; <*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
A5:
Seg 10 = dom loc
by FINSEQ_1:89;
A6:
loc | (Seg 10) = loc
;
set D = ND (V,A);
set EN = {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)};
set inv = Lucas_inv (A,loc,x0,y0,p0,q0,n0);
set B = Lucas_loop_body (A,loc);
set Di = denaming (V,A,(loc /. 1));
set Dj = denaming (V,A,(loc /. 2));
set Dn = denaming (V,A,(loc /. 3));
set Ds = denaming (V,A,(loc /. 4));
set Db = denaming (V,A,(loc /. 5));
set Dc = denaming (V,A,(loc /. 6));
set Dp = denaming (V,A,(loc /. 7));
set Dq = denaming (V,A,(loc /. 8));
set Dps = denaming (V,A,(loc /. 9));
set Dqc = denaming (V,A,(loc /. 10));
set Aij = addition (A,(loc /. 1),(loc /. 2));
set Mps = multiplication (A,(loc /. 7),(loc /. 4));
set Mqc = multiplication (A,(loc /. 8),(loc /. 6));
set Scs = subtraction (A,(loc /. 9),(loc /. 10));
set AS1 = SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6));
set AS2 = SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4));
set AS3 = SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9));
set AS4 = SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10));
set AS5 = SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5));
set AS6 = SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1));
now for d being TypeSCNominativeData of V,A st d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) & (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . d = TRUE & d in dom (Lucas_loop_body (A,loc)) & (Lucas_loop_body (A,loc)) . d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) holds
(Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . ((Lucas_loop_body (A,loc)) . d) = TRUE let d be
TypeSCNominativeData of
V,
A;
( d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) & (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . d = TRUE & d in dom (Lucas_loop_body (A,loc)) & (Lucas_loop_body (A,loc)) . d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) implies (Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . ((Lucas_loop_body (A,loc)) . d) = TRUE )assume that A7:
d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0))
and A8:
(Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . d = TRUE
and A9:
d in dom (Lucas_loop_body (A,loc))
and A10:
(Lucas_loop_body (A,loc)) . d in dom (Lucas_inv (A,loc,x0,y0,p0,q0,n0))
;
(Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . ((Lucas_loop_body (A,loc)) . d) = TRUE
Lucas_inv_pred A,
loc,
x0,
y0,
p0,
q0,
n0,
d
by A7, A8, Def15;
then consider d1 being
NonatomicND of
V,
A such that A11:
d = d1
and A12:
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1
and A13:
d1 . (loc /. 2) = 1
and A14:
d1 . (loc /. 3) = n0
and A15:
d1 . (loc /. 7) = p0
and A16:
d1 . (loc /. 8) = q0
and A17:
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)) )
;
A18:
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;
A19:
loc /. 2
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;
A20:
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;
A21:
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;
A22:
loc /. 5
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;
A23:
loc /. 7
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;
A24:
loc /. 8
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;
consider I being
Nat such that A25:
I = d1 . (loc /. 1)
and A26:
d1 . (loc /. 4) = Lucas (
x0,
y0,
p0,
q0,
I)
and A27:
d1 . (loc /. 5) = Lucas (
x0,
y0,
p0,
q0,
(I + 1))
by A17;
set prg =
<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>;
set pos =
<*6,4,9,10,5,1*>;
reconsider prg =
<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> as non
empty FPrg (ND (V,A)) -valued FinSequence ;
set PS =
PrgLocalOverlapSeq (
A,
loc,
d1,
prg,
<*6,4,9,10,5,1*>);
A28:
len prg = 6
by AOFA_A00:20;
A29:
len (PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) = len prg
by NOMIN_8:def 14;
A30:
(
prg . 1
= denaming (
V,
A,
(loc /. 4)) &
<*6,4,9,10,5,1*> . 1
= 6 )
;
A31:
(
prg . 2
= denaming (
V,
A,
(loc /. 5)) &
<*6,4,9,10,5,1*> . 2
= 4 )
;
A32:
(
prg . 3
= multiplication (
A,
(loc /. 7),
(loc /. 4)) &
<*6,4,9,10,5,1*> . 3
= 9 )
;
A33:
(
prg . 4
= multiplication (
A,
(loc /. 8),
(loc /. 6)) &
<*6,4,9,10,5,1*> . 4
= 10 )
;
A34:
(
prg . 5
= subtraction (
A,
(loc /. 9),
(loc /. 10)) &
<*6,4,9,10,5,1*> . 5
= 5 )
;
A35:
(
prg . 6
= addition (
A,
(loc /. 1),
(loc /. 2)) &
<*6,4,9,10,5,1*> . 6
= 1 )
;
rng loc c= {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)}
proof
let y be
object ;
TARSKI:def 3 ( not y in rng loc or y in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} )
assume
y in rng loc
;
y in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)}
then consider w being
object such that A36:
w in dom loc
and A37:
loc . w = y
by FUNCT_1:def 3;
A38:
not not
w = 1 & ... & not
w = 10
by A5, A36, FINSEQ_1:91;
1
in Seg 10 & ... & 10
in Seg 10
;
then
loc . 1
= loc /. 1 & ... &
loc . 10
= loc /. 10
by A5, PARTFUN1:def 6;
hence
y in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)}
by A37, A38, ENUMSET1:def 8;
verum
end; then
rng loc c= dom d1
by A12;
then A39:
loc is_valid_wrt d1
;
A40:
dom (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = dom (denaming (V,A,(loc /. 4)))
by NOMIN_2:def 7;
A41:
dom (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) = dom (denaming (V,A,(loc /. 5)))
by NOMIN_2:def 7;
PP_composition (
(PP_composition ((PP_composition ((PP_composition ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))),(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) =
PP_composition (
(PP_composition ((PP_composition (((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))),(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))))
by PARTPR_2:def 1
.=
PP_composition (
(PP_composition (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))))
by PARTPR_2:def 1
.=
PP_composition (
((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))),
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))))
by PARTPR_2:def 1
.=
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))
by PARTPR_2:def 1
;
then A42:
Lucas_loop_body (
A,
loc)
= (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))))
by PARTPR_2:def 1;
A43:
((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) =
(((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36
.=
((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by RELAT_1:36
.=
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))
by RELAT_1:36
;
A44:
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) =
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by RELAT_1:36
.=
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36
;
A45:
(((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) =
((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36
.=
(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by RELAT_1:36
;
A46:
(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) = (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36;
A47:
((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36;
Lucas_loop_body (
A,
loc) =
(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))
by A42, RELAT_1:36
.=
(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by RELAT_1:36
.=
(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36
;
then A48:
d in dom (((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A9, FUNCT_1:11;
then A49:
d in dom ((((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A43, A44, FUNCT_1:11;
then
d in dom (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A45, A46, FUNCT_1:11;
then A50:
d in dom ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A47, FUNCT_1:11;
then A51:
((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) . d = (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d)
by FUNCT_1:12;
A52:
dom (denaming (V,A,(loc /. 1))) = { d where d is NonatomicND of V,A : loc /. 1 in dom d }
by NOMIN_1:def 18;
A53:
dom (denaming (V,A,(loc /. 2))) = { d where d is NonatomicND of V,A : loc /. 2 in dom d }
by NOMIN_1:def 18;
A54:
dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d }
by NOMIN_1:def 18;
A55:
dom (denaming (V,A,(loc /. 5))) = { d where d is NonatomicND of V,A : loc /. 5 in dom d }
by NOMIN_1:def 18;
A56:
dom (denaming (V,A,(loc /. 6))) = { d where d is NonatomicND of V,A : loc /. 6 in dom d }
by NOMIN_1:def 18;
A57:
dom (denaming (V,A,(loc /. 7))) = { d where d is NonatomicND of V,A : loc /. 7 in dom d }
by NOMIN_1:def 18;
A58:
dom (denaming (V,A,(loc /. 8))) = { d where d is NonatomicND of V,A : loc /. 8 in dom d }
by NOMIN_1:def 18;
A59:
dom (denaming (V,A,(loc /. 9))) = { d where d is NonatomicND of V,A : loc /. 9 in dom d }
by NOMIN_1:def 18;
A60:
dom (denaming (V,A,(loc /. 10))) = { d where d is NonatomicND of V,A : loc /. 10 in dom d }
by NOMIN_1:def 18;
A61:
d in dom (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))
by A48, FUNCT_1:11;
then reconsider Ad =
(denaming (V,A,(loc /. 4))) . d1 as
TypeSCNominativeData of
V,
A by A40, A11, PARTFUN1:4, NOMIN_1:39;
reconsider L1 =
local_overlapping (
V,
A,
d1,
Ad,
(loc /. 6)) as
NonatomicND of
V,
A by NOMIN_2:9;
A62:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 1
= L1
by A28, A30, NOMIN_8:def 14;
A63:
(SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d = L1
by A11, A61, NOMIN_2:def 7;
then A64:
L1 in dom (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))
by A50, FUNCT_1:11;
then reconsider DbL1 =
(denaming (V,A,(loc /. 5))) . L1 as
TypeSCNominativeData of
V,
A by A41, PARTFUN1:4, NOMIN_1:39;
reconsider L2 =
local_overlapping (
V,
A,
L1,
DbL1,
(loc /. 4)) as
NonatomicND of
V,
A by NOMIN_2:9;
A65:
( 2
= 1
+ 1 & 3
= 2
+ 1 & 4
= 3
+ 1 & 5
= 4
+ 1 & 6
= 5
+ 1 )
;
A66:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 2
= L2
by A65, A28, A29, A31, A62, NOMIN_8:def 14;
A67:
(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . L1 = L2
by A64, NOMIN_2:def 7;
A68:
dom L1 = {(loc /. 6)} \/ (dom d1)
by A2, NOMIN_4:4;
A69:
dom L2 = {(loc /. 4)} \/ (dom L1)
by A2, NOMIN_4:4;
A70:
d1 in dom (denaming (V,A,(loc /. 4)))
by A12, A21, A54;
A71:
dom (PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) = dom prg
by A29, FINSEQ_3:29;
A72:
loc /. 4
in dom L2
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A66, NOMIN_8:25;
then A73:
L2 in dom (denaming (V,A,(loc /. 4)))
by A54;
A74:
loc /. 7
in dom L1
by A12, A23, A68, XBOOLE_0:def 3;
then A75:
loc /. 7
in dom L2
by A69, XBOOLE_0:def 3;
then
L2 in dom (denaming (V,A,(loc /. 7)))
by A57;
then
L2 in (dom (denaming (V,A,(loc /. 4)))) /\ (dom (denaming (V,A,(loc /. 7))))
by A73, XBOOLE_0:def 4;
then A76:
L2 in dom <:(denaming (V,A,(loc /. 7))),(denaming (V,A,(loc /. 4))):>
by FUNCT_3:def 7;
then A77:
<:(denaming (V,A,(loc /. 7))),(denaming (V,A,(loc /. 4))):> . L2 = [((denaming (V,A,(loc /. 7))) . L2),((denaming (V,A,(loc /. 4))) . L2)]
by FUNCT_3:def 7;
A78:
dom (multiplication A) = [:A,A:]
by A1, FUNCT_2:def 1;
(
loc /. 7
is_a_value_on L2 &
loc /. 4
is_a_value_on L2 )
by A3;
then
[((denaming (V,A,(loc /. 7))) . L2),((denaming (V,A,(loc /. 4))) . L2)] in [:A,A:]
by ZFMISC_1:87;
then A79:
L2 in dom (multiplication (A,(loc /. 7),(loc /. 4)))
by A76, A78, A77, FUNCT_1:11;
then reconsider MpsL2 =
(multiplication (A,(loc /. 7),(loc /. 4))) . L2 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L3 =
local_overlapping (
V,
A,
L2,
MpsL2,
(loc /. 9)) as
NonatomicND of
V,
A by NOMIN_2:9;
A80:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 3
= L3
by A65, A28, A29, A32, A66, NOMIN_8:def 14;
A81:
dom L3 = {(loc /. 9)} \/ (dom L2)
by A2, NOMIN_4:4;
A82:
loc /. 4
in dom L3
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A80, NOMIN_8:25;
A83:
loc /. 8
in dom L1
by A12, A24, A68, XBOOLE_0:def 3;
then A84:
loc /. 8
in dom L2
by A69, XBOOLE_0:def 3;
then A85:
loc /. 8
in dom L3
by A81, XBOOLE_0:def 3;
A86:
loc /. 6
in dom L1
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A62, NOMIN_8:25;
A87:
loc /. 6
in dom L2
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A66, NOMIN_8:25;
A88:
loc /. 6
in dom L3
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A80, NOMIN_8:25;
A89:
L3 in dom (denaming (V,A,(loc /. 8)))
by A85, A58;
L3 in dom (denaming (V,A,(loc /. 6)))
by A88, A56;
then
L3 in (dom (denaming (V,A,(loc /. 8)))) /\ (dom (denaming (V,A,(loc /. 6))))
by A89, XBOOLE_0:def 4;
then A90:
L3 in dom <:(denaming (V,A,(loc /. 8))),(denaming (V,A,(loc /. 6))):>
by FUNCT_3:def 7;
then A91:
<:(denaming (V,A,(loc /. 8))),(denaming (V,A,(loc /. 6))):> . L3 = [((denaming (V,A,(loc /. 8))) . L3),((denaming (V,A,(loc /. 6))) . L3)]
by FUNCT_3:def 7;
(
loc /. 8
is_a_value_on L3 &
loc /. 6
is_a_value_on L3 )
by A3;
then
[((denaming (V,A,(loc /. 8))) . L3),((denaming (V,A,(loc /. 6))) . L3)] in [:A,A:]
by ZFMISC_1:87;
then A92:
L3 in dom (multiplication (A,(loc /. 8),(loc /. 6)))
by A90, A78, A91, FUNCT_1:11;
then reconsider MqcL3 =
(multiplication (A,(loc /. 8),(loc /. 6))) . L3 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L4 =
local_overlapping (
V,
A,
L3,
MqcL3,
(loc /. 10)) as
NonatomicND of
V,
A by NOMIN_2:9;
A93:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 4
= L4
by A65, A28, A29, A33, A80, NOMIN_8:def 14;
A94:
dom L4 = {(loc /. 10)} \/ (dom L3)
by A2, NOMIN_4:4;
A95:
loc /. 10
in dom L4
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A33, A93, NOMIN_8:25;
A96:
loc /. 9
in dom L3
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A80, NOMIN_8:25;
A97:
loc /. 9
in dom L4
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A93, NOMIN_8:25;
A98:
loc /. 5
in dom L1
by A12, A22, A68, XBOOLE_0:def 3;
A99:
L4 in dom (denaming (V,A,(loc /. 9)))
by A97, A59;
L4 in dom (denaming (V,A,(loc /. 10)))
by A95, A60;
then
L4 in (dom (denaming (V,A,(loc /. 9)))) /\ (dom (denaming (V,A,(loc /. 10))))
by A99, XBOOLE_0:def 4;
then A100:
L4 in dom <:(denaming (V,A,(loc /. 9))),(denaming (V,A,(loc /. 10))):>
by FUNCT_3:def 7;
then A101:
<:(denaming (V,A,(loc /. 9))),(denaming (V,A,(loc /. 10))):> . L4 = [((denaming (V,A,(loc /. 9))) . L4),((denaming (V,A,(loc /. 10))) . L4)]
by FUNCT_3:def 7;
A102:
dom (subtraction A) = [:A,A:]
by A1, FUNCT_2:def 1;
(
loc /. 9
is_a_value_on L4 &
loc /. 10
is_a_value_on L4 )
by A3;
then
[((denaming (V,A,(loc /. 9))) . L4),((denaming (V,A,(loc /. 10))) . L4)] in [:A,A:]
by ZFMISC_1:87;
then A103:
L4 in dom (subtraction (A,(loc /. 9),(loc /. 10)))
by A100, A102, A101, FUNCT_1:11;
then reconsider ScsL4 =
(subtraction (A,(loc /. 9),(loc /. 10))) . L4 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L5 =
local_overlapping (
V,
A,
L4,
ScsL4,
(loc /. 5)) as
NonatomicND of
V,
A by NOMIN_2:9;
A104:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 5
= L5
by A65, A28, A29, A34, A93, NOMIN_8:def 14;
A105:
dom L5 = {(loc /. 5)} \/ (dom L4)
by A2, NOMIN_4:4;
A106:
loc /. 1
in dom L1
by A12, A18, A68, XBOOLE_0:def 3;
then A107:
loc /. 1
in dom L2
by A69, XBOOLE_0:def 3;
then A108:
loc /. 1
in dom L3
by A81, XBOOLE_0:def 3;
then A109:
loc /. 1
in dom L4
by A94, XBOOLE_0:def 3;
then A110:
loc /. 1
in dom L5
by A105, XBOOLE_0:def 3;
then A111:
L5 in dom (denaming (V,A,(loc /. 1)))
by A52;
A112:
loc /. 2
in dom L1
by A12, A19, A68, XBOOLE_0:def 3;
then A113:
loc /. 2
in dom L2
by A69, XBOOLE_0:def 3;
then A114:
loc /. 2
in dom L3
by A81, XBOOLE_0:def 3;
then A115:
loc /. 2
in dom L4
by A94, XBOOLE_0:def 3;
then A116:
loc /. 2
in dom L5
by A105, XBOOLE_0:def 3;
then A117:
L5 in dom (denaming (V,A,(loc /. 2)))
by A53;
L5 in (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 2))))
by A111, A117, XBOOLE_0:def 4;
then A118:
L5 in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):>
by FUNCT_3:def 7;
then A119:
<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):> . L5 = [((denaming (V,A,(loc /. 1))) . L5),((denaming (V,A,(loc /. 2))) . L5)]
by FUNCT_3:def 7;
A120:
dom (addition A) = [:A,A:]
by A1, FUNCT_2:def 1;
(
loc /. 1
is_a_value_on L5 &
loc /. 2
is_a_value_on L5 )
by A3;
then
[((denaming (V,A,(loc /. 1))) . L5),((denaming (V,A,(loc /. 2))) . L5)] in [:A,A:]
by ZFMISC_1:87;
then A121:
L5 in dom (addition (A,(loc /. 1),(loc /. 2)))
by A120, A118, A119, FUNCT_1:11;
then reconsider AijL5 =
(addition (A,(loc /. 1),(loc /. 2))) . L5 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L6 =
local_overlapping (
V,
A,
L5,
AijL5,
(loc /. 1)) as
NonatomicND of
V,
A by NOMIN_2:9;
A122:
(PrgLocalOverlapSeq (A,loc,d1,prg,<*6,4,9,10,5,1*>)) . 6
= L6
by A28, A29, A35, A104, NOMIN_8:def 14;
A123:
dom L6 = {(loc /. 1)} \/ (dom L5)
by A2, NOMIN_4:4;
A124:
d in dom ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by A45, A49, FUNCT_1:11;
then
L2 in dom (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))
by A51, A63, A67, FUNCT_1:11;
then A125:
(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) . L2 = L3
by NOMIN_2:def 7;
A126:
((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) . d = (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) . (((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) . d)
by A124, FUNCT_1:12;
then
L3 in dom (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))
by A49, A45, A125, A67, A51, A63, FUNCT_1:11;
then A127:
(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) . L3 = L4
by NOMIN_2:def 7;
A128:
((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) . d = (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) . (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) . d)
by A49, A45, FUNCT_1:12;
then
L4 in dom (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))
by A43, A48, A127, A125, A67, A63, A126, A51, FUNCT_1:11;
then A129:
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) . L4 = L5
by NOMIN_2:def 7;
A130:
((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))) . d = (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) . (((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) . d)
by A43, A48, FUNCT_1:12;
Lucas_loop_body (
A,
loc) =
((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))
by A42, RELAT_1:36
.=
(((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by RELAT_1:36
.=
((((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36
.=
(((((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))
by RELAT_1:36
;
then
(SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d in dom (((((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))
by A9, FUNCT_1:11;
then
(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . L1 in dom ((((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))))
by A63, FUNCT_1:11;
then
(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) . L2 in dom (((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))
by A67, FUNCT_1:11;
then
(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) . L3 in dom ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))))
by A125, FUNCT_1:11;
then
(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) . L4 in dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1)))
by A127, FUNCT_1:11;
then A131:
L6 =
(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . L5
by A129, NOMIN_2:def 7
.=
(Lucas_loop_body (A,loc)) . d
by A129, A127, A125, A67, A63, A51, A130, A128, A126, A9, A42, FUNCT_1:12
;
Lucas_inv_pred A,
loc,
x0,
y0,
p0,
q0,
n0,
L6
proof
take
L6
;
NOMIN_9:def 14 ( L6 = L6 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom L6 & L6 . (loc /. 2) = 1 & L6 . (loc /. 3) = n0 & L6 . (loc /. 7) = p0 & L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus
L6 = L6
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom L6 & L6 . (loc /. 2) = 1 & L6 . (loc /. 3) = n0 & L6 . (loc /. 7) = p0 & L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
A132:
loc /. 1
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A35, A122, NOMIN_8:25;
A133:
loc /. 2
in dom L6
by A116, A123, XBOOLE_0:def 3;
A134:
loc /. 3
in dom L1
by A12, A20, A68, XBOOLE_0:def 3;
then A135:
loc /. 3
in dom L2
by A69, XBOOLE_0:def 3;
then A136:
loc /. 3
in dom L3
by A81, XBOOLE_0:def 3;
then A137:
loc /. 3
in dom L4
by A94, XBOOLE_0:def 3;
then A138:
loc /. 3
in dom L5
by A105, XBOOLE_0:def 3;
then A139:
loc /. 3
in dom L6
by A123, XBOOLE_0:def 3;
A140:
loc /. 4
in dom L4
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A93, NOMIN_8:25;
A141:
loc /. 4
in dom L5
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A104, NOMIN_8:25;
A142:
loc /. 4
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A122, NOMIN_8:25;
A143:
loc /. 5
in dom L5
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A34, A104, NOMIN_8:25;
A144:
loc /. 5
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A34, A122, NOMIN_8:25;
A145:
loc /. 6
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A30, A28, A122, NOMIN_8:25;
A146:
loc /. 7
in dom L3
by A75, A81, XBOOLE_0:def 3;
then A147:
loc /. 7
in dom L4
by A94, XBOOLE_0:def 3;
then A148:
loc /. 7
in dom L5
by A105, XBOOLE_0:def 3;
then A149:
loc /. 7
in dom L6
by A123, XBOOLE_0:def 3;
A150:
loc /. 8
in dom L4
by A85, A94, XBOOLE_0:def 3;
then A151:
loc /. 8
in dom L5
by A105, XBOOLE_0:def 3;
then A152:
loc /. 8
in dom L6
by A123, XBOOLE_0:def 3;
A153:
loc /. 9
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A122, NOMIN_8:25;
loc /. 10
in dom L6
by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A33, A122, NOMIN_8:25;
hence
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom L6
by A132, A133, A139, A142, A144, A145, A149, A152, A153, ENUMSET1:def 8;
( L6 . (loc /. 2) = 1 & L6 . (loc /. 3) = n0 & L6 . (loc /. 7) = p0 & L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
A154:
L5 . (loc /. 2) =
L4 . (loc /. 2)
by A2, A4, A5, A6, A115, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 2)
by A2, A4, A5, A6, A114, NOMIN_5:3, NOMIN_7:1
.=
L2 . (loc /. 2)
by A2, A4, A5, A6, A113, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 2)
by A2, A4, A5, A6, A112, NOMIN_5:3, NOMIN_7:1
.=
1
by A2, A4, A5, A6, A12, A13, A19, NOMIN_5:3, NOMIN_7:1
;
hence
L6 . (loc /. 2) = 1
by A2, A4, A5, A6, A116, NOMIN_5:3, NOMIN_7:1;
( L6 . (loc /. 3) = n0 & L6 . (loc /. 7) = p0 & L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus L6 . (loc /. 3) =
L5 . (loc /. 3)
by A2, A4, A5, A6, A138, NOMIN_5:3, NOMIN_7:1
.=
L4 . (loc /. 3)
by A2, A4, A5, A6, A137, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 3)
by A2, A4, A5, A6, A136, NOMIN_5:3, NOMIN_7:1
.=
L2 . (loc /. 3)
by A2, A4, A5, A6, A135, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 3)
by A2, A4, A5, A6, A134, NOMIN_5:3, NOMIN_7:1
.=
n0
by A2, A4, A5, A6, A12, A14, A20, NOMIN_5:3, NOMIN_7:1
;
( L6 . (loc /. 7) = p0 & L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus L6 . (loc /. 7) =
L5 . (loc /. 7)
by A2, A4, A5, A6, A148, NOMIN_5:3, NOMIN_7:1
.=
L4 . (loc /. 7)
by A2, A4, A5, A6, A147, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 7)
by A2, A4, A5, A6, A146, NOMIN_5:3, NOMIN_7:1
.=
L2 . (loc /. 7)
by A2, A4, A5, A6, A75, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 7)
by A2, A4, A5, A6, A74, NOMIN_5:3, NOMIN_7:1
.=
p0
by A2, A4, A5, A6, A12, A15, A23, NOMIN_5:3, NOMIN_7:1
;
( L6 . (loc /. 8) = q0 & ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) )
thus L6 . (loc /. 8) =
L5 . (loc /. 8)
by A2, A4, A5, A6, A151, NOMIN_5:3, NOMIN_7:1
.=
L4 . (loc /. 8)
by A2, A4, A5, A6, A150, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 8)
by A2, A4, A5, A6, A85, NOMIN_5:3, NOMIN_7:1
.=
L2 . (loc /. 8)
by A2, A4, A5, A6, A84, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 8)
by A2, A4, A5, A6, A83, NOMIN_5:3, NOMIN_7:1
.=
q0
by A2, A4, A5, A6, A12, A16, A24, NOMIN_5:3, NOMIN_7:1
;
ex I being Nat st
( I = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) )
take I1 =
I + 1;
( I1 = L6 . (loc /. 1) & L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I1) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I1 + 1)) )
A155:
L5 . (loc /. 1) =
L4 . (loc /. 1)
by A2, A4, A5, A6, A109, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 1)
by A2, A4, A5, A6, A108, NOMIN_5:3, NOMIN_7:1
.=
L2 . (loc /. 1)
by A2, A4, A5, A6, A107, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 1)
by A2, A4, A5, A6, A106, NOMIN_5:3, NOMIN_7:1
.=
I
by A2, A4, A5, A6, A12, A18, A25, NOMIN_5:3, NOMIN_7:1
;
thus L6 . (loc /. 1) =
(addition (A,(loc /. 1),(loc /. 2))) . L5
by NOMIN_2:10
.=
I1
by A1, A121, A110, A116, A154, A155, NOMIN_5:4
;
( L6 . (loc /. 4) = Lucas (x0,y0,p0,q0,I1) & L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I1 + 1)) )
A156:
L1 in dom (denaming (V,A,(loc /. 5)))
by A55, A98;
A157:
L2 . (loc /. 4) =
(denaming (V,A,(loc /. 5))) . L1
by NOMIN_2:10
.=
denaming (
(loc /. 5),
L1)
by A156, NOMIN_1:def 18
.=
L1 . (loc /. 5)
by A98, NOMIN_1:def 12
.=
Lucas (
x0,
y0,
p0,
q0,
I1)
by A2, A4, A5, A6, A27, A12, A22, NOMIN_5:3, NOMIN_7:1
;
thus L6 . (loc /. 4) =
L5 . (loc /. 4)
by A2, A4, A5, A6, A141, NOMIN_5:3, NOMIN_7:1
.=
L4 . (loc /. 4)
by A2, A4, A5, A6, A140, NOMIN_5:3, NOMIN_7:1
.=
L3 . (loc /. 4)
by A2, A4, A5, A6, A82, NOMIN_5:3, NOMIN_7:1
.=
Lucas (
x0,
y0,
p0,
q0,
I1)
by A2, A4, A5, A6, A72, A157, NOMIN_5:3, NOMIN_7:1
;
L6 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I1 + 1))
A158:
L2 . (loc /. 7) =
L1 . (loc /. 7)
by A2, A4, A5, A6, A74, NOMIN_5:3, NOMIN_7:1
.=
p0
by A2, A4, A5, A6, A12, A15, A23, NOMIN_5:3, NOMIN_7:1
;
A159:
L4 . (loc /. 9) =
L3 . (loc /. 9)
by A2, A4, A5, A6, A96, NOMIN_5:3, NOMIN_7:1
.=
(multiplication (A,(loc /. 7),(loc /. 4))) . L2
by NOMIN_2:10
.=
p0 * (Lucas (x0,y0,p0,q0,I1))
by A1, A79, A75, A72, A157, A158, NOMIN_5:5
;
A160:
L3 . (loc /. 8) =
L2 . (loc /. 8)
by A2, A4, A5, A6, A84, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 8)
by A2, A4, A5, A6, A83, NOMIN_5:3, NOMIN_7:1
.=
q0
by A2, A4, A5, A6, A12, A16, A24, NOMIN_5:3, NOMIN_7:1
;
A161:
L3 . (loc /. 6) =
L2 . (loc /. 6)
by A2, A4, A5, A6, A87, NOMIN_5:3, NOMIN_7:1
.=
L1 . (loc /. 6)
by A2, A4, A5, A6, A86, NOMIN_5:3, NOMIN_7:1
.=
(denaming (V,A,(loc /. 4))) . d1
by NOMIN_2:10
.=
denaming (
(loc /. 4),
d1)
by A70, NOMIN_1:def 18
.=
Lucas (
x0,
y0,
p0,
q0,
I)
by A12, A21, A26, NOMIN_1:def 12
;
A162:
L4 . (loc /. 10) =
(multiplication (A,(loc /. 8),(loc /. 6))) . L3
by NOMIN_2:10
.=
q0 * (Lucas (x0,y0,p0,q0,I))
by A1, A92, A88, A85, A160, A161, NOMIN_5:5
;
A163:
I1 + 1
= I + 2
;
thus L6 . (loc /. 5) =
L5 . (loc /. 5)
by A2, A4, A5, A6, A143, NOMIN_7:1, NOMIN_5:3
.=
(subtraction (A,(loc /. 9),(loc /. 10))) . L4
by NOMIN_2:10
.=
(p0 * (Lucas (x0,y0,p0,q0,I1))) - (q0 * (Lucas (x0,y0,p0,q0,I)))
by A1, A103, A97, A95, A159, A162, NOMIN_4:15
.=
Lucas (
x0,
y0,
p0,
q0,
(I1 + 1))
by Th5, A163
;
verum
end; hence
(Lucas_inv (A,loc,x0,y0,p0,q0,n0)) . ((Lucas_loop_body (A,loc)) . d) = TRUE
by A10, A131, Def15;
verum end;
hence
<*(Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(Lucas_loop_body (A,loc)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:28; verum