:: Partial correctness of an algorithm computing Lucas sequences
:: by Adrian Jaszczak
::
:: Received October 25, 2020
:: Copyright (c) 2020-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NOMIN_1, NUMBERS, ZFMISC_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1,
FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NOMIN_3, NOMIN_4,
XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, NOMIN_5, CARD_1, PRE_FF, NOMIN_7,
XXREAL_0, ARYTM_1, INT_1, MCART_1, NOMIN_8, FIB_NUM3, ORDINAL4, NOMIN_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS,
DOMAIN_1, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, CARD_1,
FINSEQ_1, BINOP_1, XXREAL_0, XCMPLX_0, INT_1, NAT_1, FUNCT_3, AOFA_A00,
PRE_FF, NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5,
NOMIN_7, FIB_NUM3, NOMIN_8;
constructors RELSET_1, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5, NOMIN_6, NOMIN_7,
PRE_FF, DOMAIN_1, FIB_NUM3, AOFA_A00, FINSEQ_4, NOMIN_8;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, INT_1, NOMIN_1, NUMBERS,
NAT_1, XXREAL_0, XREAL_0, CARD_1, FINSEQ_1, FINSEQ_4, NEWTON04, NOMIN_4,
NOMIN_7, AOFA_A00, SUBSET_1, PARTPR_2, XTUPLE_0, NOMIN_8;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, RELAT_1, FUNCT_1, NOMIN_3, NOMIN_7, NOMIN_8;
equalities NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_4, XBOOLEAN, PRE_FF,
FIB_NUM3, BINOP_1, NOMIN_5, NOMIN_6, NOMIN_7, AOFA_A00, FINSEQ_1,
NOMIN_8;
expansions TARSKI, PARTFUN1, NOMIN_4, NOMIN_7, NOMIN_8;
theorems XBOOLE_0, NOMIN_1, PARTPR_1, NOMIN_2, NOMIN_3, NOMIN_4, FUNCT_1,
FUNCT_3, PARTFUN1, TARSKI, PARTPR_2, ENUMSET1, NOMIN_5, INT_1, XXREAL_0,
FINSEQ_3, NAT_1, FINSEQ_1, RELAT_1, ZFMISC_1, FUNCT_2, NOMIN_7, CARD_1,
PRE_FF, FIB_NUM3, AOFA_A00, NOMIN_8;
schemes PARTPR_2, NAT_1;
begin :: Introduction about finite sequences
registration
let n be Nat;
let f be n-element FinSequence;
reduce f | Seg n to f;
reducibility
proof
len f = n by CARD_1:def 7;
then f|n = f;
hence thesis;
end;
end;
registration
let A,B be set;
let f1,f2,f3,f4,f5,f6 be PartFunc of A,B;
cluster <*f1,f2,f3,f4,f5,f6*> -> PFuncs(A,B)-valued;
coherence
proof
{f1,f2,f3,f4,f5,f6} c= PFuncs(A,B)
proof
let x be object;
assume x in {f1,f2,f3,f4,f5,f6};
then x = f1 or x = f2 or x = f3 or x = f4 or x = f5 or x = f6
by ENUMSET1:def 4;
hence thesis by PARTFUN1:45;
end;
hence rng <*f1,f2,f3,f4,f5,f6*> c= PFuncs(A,B) by AOFA_A00:21;
end;
end;
registration
let V,A be set;
let f1,f2,f3,f4,f5,f6 be SCBinominativeFunction of V,A;
cluster <*f1,f2,f3,f4,f5,f6*> -> FPrg(ND(V,A))-valued;
coherence;
end;
definition
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence equals
<*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>;
coherence;
end;
theorem Th1:
for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object
for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> iff
len f = 9 &
f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7 &
f.8 = a8 & f.9 = a9
proof
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
let f be FinSequence;
set AS1 = <*a9*>;
set AS8 = <*a1,a2,a3,a4,a5,a6,a7,a8*>;
set AS9 = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>;
A1: now
let f be FinSequence;
assume
A2: f = AS9;
hence len f = len AS8+ len AS1 by FINSEQ_1:22
.= 8 + len AS1 by AOFA_A00:24
.= 8 + 1 by FINSEQ_1:39
.= 9;
dom AS8 = Seg 8 by FINSEQ_1:89;
then
1 in dom AS8 & 2 in dom AS8 & 3 in dom AS8 & 4 in dom AS8 &
5 in dom AS8 & 6 in dom AS8 & 7 in dom AS8 & 8 in dom AS8;
then f.1 = AS8.1 & f.2 = AS8.2 & f.3 = AS8.3 & f.4 = AS8.4 &
f.5 = AS8.5 & f.6 = AS8.6 & f.7 = AS8.7 & f.8 = AS8.8
by A2, FINSEQ_1:def 7;
hence f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 &
f.6 = a6 & f.7 = a7 & f.8 = a8;
len AS8 = 8 by AOFA_A00:24;
hence f.9 = a9 by A2;
end;
hence f = AS9 implies len f = 9 &
f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 &
f.7 = a7 & f.8 = a8 & f.9 = a9;
assume
A3: len f = 9;
len AS9 = 9 by A1;
then
A4: dom f = Seg 9 & dom AS9 = Seg 9 by A3,FINSEQ_1:def 3;
assume
A5: f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6
& f.7 = a7 & f.8 = a8 & f.9 = a9;
now let x be object;
assume x in Seg 9; then
x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or
x = 6 or x = 7 or x = 8 or x = 9 by AOFA_A00:27,ENUMSET1:def 7;
hence f.x = AS9.x by A1,A5;
end;
hence f = AS9 by A4, FUNCT_1:2;
end;
registration
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
cluster <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> 9-element;
coherence;
end;
registration
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.1 to a1;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.2 to a2;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.3 to a3;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.4 to a4;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.5 to a5;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.6 to a6;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.7 to a7;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.8 to a8;
reducibility by Th1;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.9 to a9;
reducibility by Th1;
end;
theorem Th2:
for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds
rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = {a1,a2,a3,a4,a5,a6,a7,a8,a9}
proof
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
thus rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>
= rng <*a1,a2,a3,a4,a5,a6,a7,a8*> \/ rng <*a9*> by FINSEQ_1:31
.= {a1,a2,a3,a4,a5,a6,a7,a8} \/ rng <*a9*> by AOFA_A00:25
.= {a1,a2,a3,a4,a5,a6,a7,a8} \/ {a9} by FINSEQ_1:38
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9} by ENUMSET1:84;
end;
definition
let X be non empty set;
let a1,a2,a3,a4,a5,a6,a7,a8,a9 be Element of X;
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence of X; :: redefines <* (NOMIN_9, definition)
coherence
proof
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = <*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>;
hence thesis;
end;
end;
definition
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence equals
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*>^<*a10*>;
coherence;
end;
theorem Th3:
for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object
for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> iff
len f = 10 &
f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7 &
f.8 = a8 & f.9 = a9 & f.10 = a10
proof
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
let f be FinSequence;
set AS1 = <*a10*>;
set AS9 = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>;
set AS10 = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>;
A1: now
let f be FinSequence;
assume
A2: f = AS10;
hence len f = len AS9+ len AS1 by FINSEQ_1:22
.= 9 + len AS1 by Th1
.= 9 + 1 by FINSEQ_1:39
.= 10;
dom AS9 = Seg 9 by FINSEQ_1:89;
then
1 in dom AS9 & 2 in dom AS9 & 3 in dom AS9 & 4 in dom AS9 &
5 in dom AS9 & 6 in dom AS9 & 7 in dom AS9 & 8 in dom AS9 & 9 in dom AS9;
then f.1 = AS9.1 & f.2 = AS9.2 & f.3 = AS9.3 & f.4 = AS9.4 &
f.5 = AS9.5 & f.6 = AS9.6 & f.7 = AS9.7 & f.8 = AS9.8 & f.9 = AS9.9
by A2, FINSEQ_1:def 7;
hence f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 &
f.6 = a6 & f.7 = a7 & f.8 = a8 & f.9 = a9;
len AS9 = 9 by Th1;
hence f.10 = a10 by A2;
end;
hence f = AS10 implies len f = 10 &
f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 &
f.7 = a7 & f.8 = a8 & f.9 = a9 & f.10 = a10;
assume
A3: len f = 10;
len AS10 = 10 by A1;
then
A4: dom f = Seg 10 & dom AS10 = Seg 10 by A3,FINSEQ_1:def 3;
assume
A5: f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6
& f.7 = a7 & f.8 = a8 & f.9 = a9 & f.10 = a10;
now let x be object;
assume x in Seg 10; then
x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or
x = 6 or x = 7 or x = 8 or x = 9 or x = 10
by AOFA_A00:28,ENUMSET1:def 8;
hence f.x = AS10.x by A1,A5;
end;
hence f = AS10 by A4, FUNCT_1:2;
end;
registration
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
cluster <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> 10-element;
coherence;
end;
registration
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.1 to a1;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.2 to a2;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.3 to a3;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.4 to a4;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.5 to a5;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.6 to a6;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.7 to a7;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.8 to a8;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.9 to a9;
reducibility by Th3;
reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.10 to a10;
reducibility by Th3;
end;
theorem
for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object holds
rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}
proof
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
thus rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>
= rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> \/ rng <*a10*> by FINSEQ_1:31
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9} \/ rng <*a10*> by Th2
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9} \/ {a10} by FINSEQ_1:38
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} by ENUMSET1:85;
end;
definition
let X be non empty set;
let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be Element of X;
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence of X; :: redefines <* (NOMIN_9, definition)
coherence
proof
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> =
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*>^<*a10*>;
hence thesis;
end;
end;
begin :: Lucas Sequences
definition
let i,j be Integer;
redefine func [i,j] -> Element of [:INT,INT:]; :: redefines [ (TARSKI, definition)
coherence
proof
reconsider i,j as Element of INT by INT_1:def 2;
[i,j] is Element of [:INT,INT:];
hence thesis;
end;
end;
reserve x,y,P,Q for Integer;
reserve a,b,n for Nat;
reserve V,A for set;
reserve val for Function;
reserve loc for V-valued Function;
reserve d1 for NonatomicND of V,A;
reserve p for SCPartialNominativePredicate of V,A;
reserve d for object;
reserve z for Element of V;
reserve T for TypeSCNominativeData of V,A;
reserve size for non zero Nat;
reserve x0, y0, p0, q0 for Integer;
reserve n0 for Nat;
definition
let x,y,P,Q;
deffunc F(set,Element of [:INT,INT:]) = [ $2`2, P*$2`2 - Q*$2`1 ];
func Lucas_Sequence(x,y,P,Q) -> sequence of [:INT,INT:] means :Def3:
it.0 = [x,y] &
for n being Nat holds it.(n+1) = [ (it.n)`2, P*(it.n)`2 - Q*(it.n)`1 ];
existence
proof
ex L being sequence of [:INT,INT:] st
L.0 = [x,y] & for n being Nat holds L.(n+1) = F(n,L.n) from NAT_1:sch 12;
hence thesis;
end;
uniqueness
proof
let L1,L2 be sequence of [:INT,INT:] such that
A1: L1.0 = [x,y] and
A2: for n being Nat holds L1.(n+1) = F(n,L1.n) and
A3: L2.0 = [x,y] and
A4: for n being Nat holds L2.(n+1) = F(n,L2.n);
thus L1 = L2 from NAT_1:sch 16(A1,A2,A3,A4);
end;
end;
definition
let x,y,P,Q,n;
func Lucas(x,y,P,Q,n) -> Element of INT equals
(Lucas_Sequence(x,y,P,Q).n)`1;
coherence;
end;
theorem Th5:
Lucas(x,y,P,Q,0) = x & Lucas(x,y,P,Q,1) = y &
for n holds Lucas(x,y,P,Q,n+2) = P*Lucas(x,y,P,Q,n+1)-Q*Lucas(x,y,P,Q,n)
proof
set L = Lucas_Sequence(x,y,P,Q);
thus Lucas(x,y,P,Q,0) = [x,y]`1 by Def3
.= x;
thus Lucas(x,y,P,Q,1) = (L.(0+1))`1
.= ([(L.0)`2, P*(L.0)`2-Q*(L.0)`1])`1 by Def3
.= [x,y]`2 by Def3
.= y;
let n;
A1: (L.(n+1))`1 = [(L.n)`2, P*(L.n)`2-Q*(L.n)`1]`1 by Def3
.= (L.n)`2;
n+2 = n+1+1;
hence Lucas(x,y,P,Q,n+2) = [(L.(n+1))`2, P*(L.(n+1))`2-Q*(L.(n+1))`1]`1
by Def3
.= [(L.n)`2, P*(L.n)`2-Q*(L.n)`1]`2 by Def3
.= P*Lucas(x,y,P,Q,n+1)-Q*Lucas(x,y,P,Q,n) by A1;
end;
theorem Th6:
Lucas_Sequence(0,1,1,-1) = Fib
proof
set L = Lucas_Sequence(0,1,1,-1);
set F = Fib;
dom F = NAT & dom L = NAT by FUNCT_2:def 1;
hence dom L = dom F;
let n be object such that
A1: n in dom L;
defpred P[Nat] means L.$1 = F.$1;
L.0 = [0,1] by Def3;
then
A2: P[0] by PRE_FF:def 1;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
thus L.(k+1) = [ (L.k)`2, 1*(L.k)`2 - (-1)*(L.k)`1 ] by Def3
.= [ (F.k)`2, (F.k)`1 + (F.k)`2 ] by A4
.= F.(k+1) by PRE_FF:def 1;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
theorem
Lucas(0,1,1,-1,n) = Fib(n) by Th6;
theorem Th8:
Lucas_Sequence(a,b,1,-1) = GenFib(a,b)
proof
set L = Lucas_Sequence(a,b,1,-1);
set F = GenFib(a,b);
dom F = NAT & dom L = NAT by FUNCT_2:def 1;
hence dom L = dom F;
let n be object such that
A1: n in dom L;
defpred P[Nat] means L.$1 = F.$1;
L.0 = [a,b] by Def3;
then
A2: P[0] by FIB_NUM3:def 3;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
thus L.(k+1) = [ (L.k)`2, 1*(L.k)`2 - (-1)*(L.k)`1 ] by Def3
.= [ (F.k)`2, (F.k)`1 + (F.k)`2 ] by A4
.= F.(k+1) by FIB_NUM3:def 3;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
theorem
Lucas(a,b,1,-1,n) = GenFib(a,b,n) by Th8;
theorem Th10:
Lucas_Sequence(2,1,1,-1) = Lucas
proof
set L = Lucas_Sequence(2,1,1,-1);
set F = Lucas;
dom F = NAT & dom L = NAT by FUNCT_2:def 1;
hence dom L = dom F;
let n be object such that
A1: n in dom L;
defpred P[Nat] means L.$1 = F.$1;
L.0 = [2,1] by Def3;
then
A2: P[0] by FIB_NUM3:def 1;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
thus L.(k+1) = [ (L.k)`2, 1*(L.k)`2 - (-1)*(L.k)`1 ] by Def3
.= [ (F.k)`2, (F.k)`1 + (F.k)`2 ] by A4
.= F.(k+1) by FIB_NUM3:def 1;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
theorem
Lucas(2,1,1,-1,n) = Lucas(n) by Th10;
begin :: Main algorithm
:: Pseudocode of Lucas(x,y,p,q,n)
::
:: i := val.1 :: counter
:: j := val.2 :: constant 1
:: n := val.3 :: index of searched element
:: s := val.4 :: result
:: b := val.5
:: c := val.6
:: p := val.7 :: constant P
:: q := val.8 :: constant Q
:: ps := val.9
:: qc := val.10
::
:: { s == Lucas(i) && b == Lucas(i+1) &&
:: p == p0 && q == q0 }
:: while ( i <> n )
:: c := s
:: s := b
:: ps := p*s
:: qc := q*c
:: b := ps - qc
:: i := i + j
:: return s
:: { n == i && s == Lucas(i) && b == Lucas(i+1) &&
:: p == p0 && q == q0 }
::
:: where
:: val.1 = 0,
:: val.2 = 1,
:: val.3 - the number n the Lucas of which we compute,
:: val.4 = x
:: val.5 = y
:: val.6 = x
:: val.7 = p
:: val.8 = q
:: val.9 = 0
:: val.10 = 0
:: are input data from the environment,
:: and loc/.1 = i, loc/.2 = j, loc/.3 = n, loc/.4 = s, loc/.5 = b, loc/.6 = c,
:: loc/.7 = p, loc/.8 = q, loc/.9 = ps, loc/.10 = qc
theorem Th12:
Seg 10 c= dom loc & loc is_valid_wrt d1 implies
{ loc/.1, loc/.2, loc/.3, loc/.4, loc/.5,
loc/.6, loc/.7, loc/.8, loc/.9, loc/.10 } c= dom d1
proof
assume that
A1: Seg 10 c= dom loc and
A2: rng loc c= dom d1;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
let x be object;
assume x in {i,j,n,s,b,c,p,q,ps,qc};
then
A3: x = i or x = j or x = n or x = s or x = b or x = c or x = p or x = q
or x = ps or x = qc by ENUMSET1:def 8;
A4: 1 in Seg 10 & ... & 10 in Seg 10;
then
A5: loc.1 in rng loc & ... & loc.10 in rng loc by A1,FUNCT_1:def 3;
loc.1 = loc/.1 & ... & loc.10 = loc/.10 by A1,A4,PARTFUN1:def 6;
hence thesis by A2,A3,A5;
end;
definition
let V,A,loc;
func Lucas_loop_body(A,loc) -> SCBinominativeFunction of V,A equals
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),
SC_assignment(addition(A,loc/.1,loc/.2),loc/.1)
);
coherence;
end;
definition
let V,A,loc;
func Lucas_main_loop(A,loc) -> SCBinominativeFunction of V,A equals
PP_while(PP_not(Equality(A,loc/.1,loc/.3)),Lucas_loop_body(A,loc));
coherence;
end;
definition
let V,A,loc,val;
func Lucas_main_part(A,loc,val)
-> SCBinominativeFunction of V,A equals
PP_composition(
initial_assignments(A,loc,val,10),
Lucas_main_loop(A,loc)
);
coherence;
end;
definition
let V,A,loc,val,z;
func Lucas_program(A,loc,val,z)
-> SCBinominativeFunction of V,A equals
PP_composition(
Lucas_main_part(A,loc,val),
SC_assignment(denaming(V,A,loc/.4),z)
);
coherence;
end;
definition
let x0,y0,p0,q0,n0;
func Lucas_input(x0,y0,p0,q0,n0) -> FinSequence equals
<*0,1,n0,x0,y0,x0,p0,q0,0,0*>;
coherence;
end;
registration
let x0,y0,p0,q0,n0;
cluster Lucas_input(x0,y0,p0,q0,n0) -> 10-element;
coherence;
end;
definition
let V,A,x0,y0,p0,q0,n0,d;
let val be FinSequence;
pred valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d means
Lucas_input(x0,y0,p0,q0,n0) is_valid_input V,A,val,d;
end;
definition
let V,A,x0,y0,p0,q0,n0;
let val be FinSequence;
defpred P[object] means valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,$1;
func valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0)
-> SCPartialNominativePredicate of V,A equals
valid_input(V,A,val,Lucas_input(x0,y0,p0,q0,n0));
coherence;
end;
registration
let V,A,x0,y0,p0,q0,n0;
let val be FinSequence;
cluster valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0) -> total;
coherence;
end;
definition
let V,A,z,x0,y0,p0,q0,n0,d;
pred valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d means
<*Lucas(x0,y0,p0,q0,n0)*> is_valid_output V,A,<*z*>,d;
end;
definition
let V,A,z,x0,y0,p0,q0,n0;
func valid_Lucas_output(A,z,x0,y0,p0,q0,n0) ->
SCPartialNominativePredicate of V,A equals
valid_output(V,A,z,Lucas(x0,y0,p0,q0,n0));
coherence;
end;
definition
let V,A,loc,x0,y0,p0,q0,n0,d;
pred Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d means
ex d1 being NonatomicND of V,A st
d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4, loc/.5,
loc/.6, loc/.7, loc/.8, loc/.9, loc/.10 } c= dom d1 &
d1.(loc/.2) = 1 & d1.(loc/.3) = n0 &
d1.(loc/.7) = p0 & d1.(loc/.8) = q0 &
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);
end;
definition
let V,A,loc,x0,y0,p0,q0,n0;
defpred P[object] means Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,$1;
func Lucas_inv(A,loc,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V,A
means
:Def15:
dom it = ND(V,A) &
for d being object st d in dom it holds
(Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies it.d = TRUE) &
(not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies it.d = FALSE);
existence
proof
A1: ND(V,A) c= ND(V,A);
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = ND(V,A) & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
registration
let V,A,loc,x0,y0,p0,q0,n0;
cluster Lucas_inv(A,loc,x0,y0,p0,q0,n0) -> total;
coherence by Def15;
end;
theorem Th13:
for val being 10-element FinSequence holds
V is non 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))
proof
let val be 10-element FinSequence;
set size = 10;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4, b1 = val.5, c1 = val.6;
set p1 = val.7, q1 = val.8, ps1 = val.9, qc1 = val.10;
set EN = {i1,j1,n1,s1,b1,c1,p1,q1,ps1,qc1};
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,inv);
set Q1 = SC_Psuperpos(SE.8,DS.2,j);
set P1 = SC_Psuperpos(Q1,DS.1,i);
set inp = Lucas_input(x0,y0,p0,q0,n0);
assume that
A1: V is non 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;
A6: Seg 10 = dom val by FINSEQ_1:89;
A7: len val = 10 by CARD_1:def 7;
A8: len SE = len val by NOMIN_8:def 9;
A9: len inp = 10 by CARD_1:def 7;
A10: len DS = 10 by NOMIN_8:def 8,A7;
A11: DS.1 = denaming(V,A,val.1) by NOMIN_8:def 8,A10;
A12: DS.2 = denaming(V,A,val.2) by NOMIN_8:def 8,A10;
A13: DS.9 = denaming(V,A,val.9) by NOMIN_8:def 8,A10;
A14: DS.10 = denaming(V,A,val.10) by NOMIN_8:def 8,A10;
A15: SE.(8+1) =
SC_Psuperpos(SE.8,denaming(V,A,val.(len val-8)),loc/.(len val-8))
by A7,A8,NOMIN_8:def 9
.= Q1 by NOMIN_8:def 8,A10,A7;
A16: SE.(9+1) =
SC_Psuperpos(SE.9,denaming(V,A,val.(len val-9)),loc/.(len val-9))
by A7,A8,NOMIN_8:def 9
.= P1 by NOMIN_8:def 8,A10,A7,A15;
let d be Element of D;
assume d in dom I & I.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 <= len inp holds d1.(val.n) = inp.n;
A20: d1.i1 = inp.1 by A9,A19
.= 0;
A21: d1.j1 = inp.2 by A9,A19
.= 1;
A22: d1.n1 = inp.3 by A9,A19
.= n0;
A23: d1.s1 = inp.4 by A9,A19
.= x0;
A24: d1.b1 = inp.5 by A9,A19
.= y0;
A25: d1.p1 = inp.7 by A9,A19
.= p0;
A26: d1.q1 = inp.8 by A9,A19
.= q0;
set F = LocalOverlapSeq(A,loc,val,d1,size);
A27: len F = size by NOMIN_7:def 4;
then
A28: loc,val,size are_correct_wrt d1 by A1,A2,A6,A18,FINSEQ_1:def 3;
A29: dom(DS.1) = {d where d is NonatomicND of V,A: i1 in dom d}
by A11,NOMIN_1:def 18;
A30: dom P1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,DS.1.d,i) in dom Q1 & d in dom(DS.1)}
by NOMIN_2:def 11;
A31: dom Q1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,DS.2.d,j) in dom(SE.8) & d in dom(DS.2)}
by NOMIN_2:def 11;
1 in dom val by A6;
then i1 in rng val by FUNCT_1:def 3;
then
A32: d1 in dom(DS.1) by A18,A29;
A33: F.1 is NonatomicND of V,A by A27,NOMIN_7:def 6;
reconsider Lqc = F.10 as NonatomicND of V,A by A27,NOMIN_7:def 6;
A34: F.1 = local_overlapping(V,A,d1,DS.1.d1,i) by A11,NOMIN_7:def 4;
A35: F.(1+1) = local_overlapping(V,A,F.1,DS.2.(F.1),j)
by A12,A27,NOMIN_7:def 4;
A36: F.1 in dom(DS.2) by A12,A27,A28,NOMIN_8:15;
A37: dom inv = D by Def15;
then
A38: Lqc in dom inv;
A39: size-8-1 = 1;
A40: 8+1 < size;
local_overlapping(V,A,F.(size-1),denaming(V,A,val.len val).(F.(size-1)),
loc/.len val) in dom inv by A37;
then F.2 in dom(SE.8) by A12,A7,A28,A35,A39,A40,NOMIN_8:16;
then
A41: F.1 in dom Q1 by A35,A31,A33,A36;
hence d in dom(SE.len SE) by A34,A17,A30,A32,A7,A8,A16;
A42: Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,Lqc
proof
take Lqc;
thus Lqc = Lqc;
thus {i,j,n,s,b,c,p,q,ps,qc} c= dom Lqc
proof
A43: i in dom Lqc by A28,NOMIN_7:9;
A44: j in dom Lqc by A28,NOMIN_7:9;
A45: n in dom Lqc by A28,NOMIN_7:9;
A46: s in dom Lqc by A28,NOMIN_7:9;
A47: b in dom Lqc by A28,NOMIN_7:9;
A48: c in dom Lqc by A28,NOMIN_7:9;
A49: p in dom Lqc by A28,NOMIN_7:9;
A50: q in dom Lqc by A28,NOMIN_7:9;
A51: ps in dom Lqc by A28,NOMIN_7:9;
qc in dom Lqc by A28,NOMIN_7:9;
hence {i,j,n,s,b,c,p,q,ps,qc} c= dom Lqc
by A43,A44,A45,A46,A47,A48,A49,A50,A51,ENUMSET1:def 8;
end;
thus Lqc.j = d1.j1 by A3,A4,A5,A28,NOMIN_7:13
.= 1 by A21;
thus Lqc.n = d1.n1 by A3,A4,A5,A28,NOMIN_7:13
.= n0 by A22;
thus Lqc.p = d1.p1 by A3,A4,A5,A28,NOMIN_7:13
.= p0 by A25;
thus Lqc.q = d1.q1 by A3,A4,A5,A28,NOMIN_7:13
.= q0 by A26;
take 0;
thus Lqc.i = d1.i1 by A3,A4,A5,A28,NOMIN_7:13
.= 0 by A20;
thus Lqc.s = d1.s1 by A3,A4,A5,A28,NOMIN_7:13
.= x0 by A23
.= Lucas(x0,y0,p0,q0,0) by Th5;
thus Lqc.b = d1.b1 by A3,A4,A5,A28,NOMIN_7:13
.= y0 by A24
.= Lucas(x0,y0,p0,q0,0+1) by Th5;
end;
A52: 10-9 = 1 & 10-1 = 9;
A53: 8+1 = 9 & 8 = 10-2;
A54: local_overlapping(V,A,F.9,DS.10.(F.9),qc) in dom inv by A37;
set dy = local_overlapping(V,A,F.8,DS.9.(F.8),ps);
A55: local_overlapping(V,A,dy,DS.10.dy,qc) in dom inv by A37;
thus (SE.len SE).d = Q1.(F.1)
by A11,A12,A14,A7,A15,A17,A28,A34,A41,A52,A53,A54,NOMIN_8:19
.= SE.1.(F.9) by A14,A7,A15,A28,A52,A54,NOMIN_8:17
.= inv.Lqc by A13,A14,A7,A28,A52,A53,A54,A55,NOMIN_8:18
.= TRUE by A38,A42,Def15;
end;
theorem Th14:
for val being 10-element FinSequence holds
V is non 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),
initial_assignments(A,loc,val,10),
Lucas_inv(A,loc,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A)
proof
let val be 10-element FinSequence;
set size = 10;
set G = initial_assignments_Seq(A,loc,val,size);
A1: G.1 = SC_assignment(denaming(V,A,val.1),loc/.1) by NOMIN_7:def 8;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4, b1 = val.5, c1 = val.6;
set p1 = val.7, q1 = val.8, ps1 = val.9, qc1 = val.10;
set EN = {i1,j1,n1,s1,b1,c1,p1,q1,ps1,qc1};
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 asi = SC_assignment(DS.1,i);
set asj = SC_assignment(DS.2,j);
set asn = SC_assignment(DS.3,n);
set ass = SC_assignment(DS.4,s);
set asb = SC_assignment(DS.5,b);
set asc = SC_assignment(DS.6,c);
set asp = SC_assignment(DS.7,p);
set asq = SC_assignment(DS.8,q);
set asps = SC_assignment(DS.9,ps);
set asqc = SC_assignment(DS.10,qc);
set SE = SC_Psuperpos_Seq(loc,val,inv);
assume that
A2: V is non empty and
A3: A is_without_nonatomicND_wrt V and
A4: Seg 10 c= dom loc and
A5: loc|Seg 10 is one-to-one and
A6: loc,val are_different_wrt 10;
A7: len val = 10 by CARD_1:def 7;
A8: len SE = 10 by NOMIN_8:def 9,A7;
A9: len DS = 10 by NOMIN_8:def 8,A7;
A10: 2=1+1 & 3=2+1 & 4=3+1 & 5=4+1 & 6=5+1 & 7=6+1 & 8=7+1 & 9=8+1 & 10=9+1;
A11: SE.1 = SC_Psuperpos(inv,denaming(V,A,val.(len val)),loc/.(len val))
by NOMIN_8:def 9;
A12: SE.2 = SC_Psuperpos(SE.1,denaming(V,A,val.(len val-1)),loc/.(len val-1))
by A10,A8,NOMIN_8:def 9;
A13: SE.3 = SC_Psuperpos(SE.2,denaming(V,A,val.(len val-2)),loc/.(len val-2))
by A10,A8,NOMIN_8:def 9;
A14: SE.4 = SC_Psuperpos(SE.3,denaming(V,A,val.(len val-3)),loc/.(len val-3))
by A10,A8,NOMIN_8:def 9;
A15: SE.5 = SC_Psuperpos(SE.4,denaming(V,A,val.(len val-4)),loc/.(len val-4))
by A10,A8,NOMIN_8:def 9;
A16: SE.6 = SC_Psuperpos(SE.5,denaming(V,A,val.(len val-5)),loc/.(len val-5))
by A10,A8,NOMIN_8:def 9;
A17: SE.7 = SC_Psuperpos(SE.6,denaming(V,A,val.(len val-6)),loc/.(len val-6))
by A10,A8,NOMIN_8:def 9;
A18: SE.8 = SC_Psuperpos(SE.7,denaming(V,A,val.(len val-7)),loc/.(len val-7))
by A10,A8,NOMIN_8:def 9;
A19: SE.9 = SC_Psuperpos(SE.8,denaming(V,A,val.(len val-8)),loc/.(len val-8))
by A10,A8,NOMIN_8:def 9;
A20: SE.10 = SC_Psuperpos(SE.9,denaming(V,A,val.(len val-9)),loc/.(len val-9))
by A10,A8,NOMIN_8:def 9;
A21: DS.1 = denaming(V,A,val.1) by NOMIN_8:def 8,A9;
A22: DS.2 = denaming(V,A,val.2) by NOMIN_8:def 8,A9;
A23: DS.3 = denaming(V,A,val.3) by NOMIN_8:def 8,A9;
A24: DS.4 = denaming(V,A,val.4) by NOMIN_8:def 8,A9;
A25: DS.5 = denaming(V,A,val.5) by NOMIN_8:def 8,A9;
A26: DS.6 = denaming(V,A,val.6) by NOMIN_8:def 8,A9;
A27: DS.7 = denaming(V,A,val.7) by NOMIN_8:def 8,A9;
A28: DS.8 = denaming(V,A,val.8) by NOMIN_8:def 8,A9;
A29: DS.9 = denaming(V,A,val.9) by NOMIN_8:def 8,A9;
A30: DS.10 = denaming(V,A,val.10) by NOMIN_8:def 8,A9;
A31: <*SE.1,asqc,inv*> is SFHT of D by A7,A11,A30,NOMIN_3:29;
A32: <*SE.2,asps,SE.1*> is SFHT of D by A7,A12,A29,NOMIN_3:29;
A33: <*SE.3,asq,SE.2*> is SFHT of D by A7,A13,A28,NOMIN_3:29;
A34: <*SE.4,asp,SE.3*> is SFHT of D by A7,A14,A27,NOMIN_3:29;
A35: <*SE.5,asc,SE.4*> is SFHT of D by A7,A15,A26,NOMIN_3:29;
A36: <*SE.6,asb,SE.5*> is SFHT of D by A7,A16,A25,NOMIN_3:29;
A37: <*SE.7,ass,SE.6*> is SFHT of D by A7,A17,A24,NOMIN_3:29;
A38: <*SE.8,asn,SE.7*> is SFHT of D by A7,A18,A23,NOMIN_3:29;
A39: <*SE.9,asj,SE.8*> is SFHT of D by A7,A19,A22,NOMIN_3:29;
A40: <*SE.10,asi,SE.9*> is SFHT of D by A7,A20,A21,NOMIN_3:29;
A41: G.2 = PP_composition(asi,asj) by A10,A21,A22,A1,NOMIN_7:def 8;
A42: G.3 = PP_composition(G.2,asn) by A10,A23,NOMIN_7:def 8;
A43: G.4 = PP_composition(G.3,ass) by A10,A24,NOMIN_7:def 8;
A44: G.5 = PP_composition(G.4,asb) by A10,A25,NOMIN_7:def 8;
A45: G.6 = PP_composition(G.5,asc) by A10,A26,NOMIN_7:def 8;
A46: G.7 = PP_composition(G.6,asp) by A10,A27,NOMIN_7:def 8;
A47: G.8 = PP_composition(G.7,asq) by A10,A28,NOMIN_7:def 8;
A48: G.9 = PP_composition(G.8,asps) by A10,A29,NOMIN_7:def 8;
A49: initial_assignments(A,loc,val,10) =
PP_composition(asi,asj,asn,ass,asb,asc,asp,asq,asps,asqc)
by A10,A30,A41,A42,A43,A44,A45,A46,A47,A48,NOMIN_7:def 8;
I ||= SE.10 by A2,A3,A4,A5,A6,A8,Th13;
then
A50: <*I,asi,SE.9*> is SFHT of D by A40,NOMIN_3:15;
A51: <*PP_inversion(SE.9),asj,SE.8*> is SFHT of D by A7,A19,A22,NOMIN_4:16;
A52: <*PP_inversion(SE.8),asn,SE.7*> is SFHT of D by A7,A18,A23,NOMIN_4:16;
A53: <*PP_inversion(SE.7),ass,SE.6*> is SFHT of D by A7,A17,A24,NOMIN_4:16;
A54: <*PP_inversion(SE.6),asb,SE.5*> is SFHT of D by A7,A16,A25,NOMIN_4:16;
A55: <*PP_inversion(SE.5),asc,SE.4*> is SFHT of D by A7,A15,A26,NOMIN_4:16;
A56: <*PP_inversion(SE.4),asp,SE.3*> is SFHT of D by A7,A14,A27,NOMIN_4:16;
A57: <*PP_inversion(SE.3),asq,SE.2*> is SFHT of D by A7,A13,A28,NOMIN_4:16;
A58: <*PP_inversion(SE.2),asps,SE.1*> is SFHT of D by A7,A12,A29,NOMIN_4:16;
<*PP_inversion(SE.1),asqc,inv*> is SFHT of D by A7,A11,A30,NOMIN_4:16;
hence thesis by A49,A32,A31,A33,A34,A35,A36,A37,A38,A39,A50,A51,A52,A53,
A54,A55,A56,A57,A58,NOMIN_8:4;
end;
theorem Th15:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
d1 in dom Lucas_loop_body(A,loc) & loc is_valid_wrt d1 & Seg 10 c= dom loc &
(for T 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)
implies
prg_doms_of loc,d1,
<*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)*>,
<*6,4,9,10,5,1*>
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set B = Lucas_loop_body(A,loc);
assume that
A1: V is non empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: d1 in dom B and
A5: loc is_valid_wrt d1 and
A6: Seg 10 c= dom loc and
A7: for T holds i is_a_value_on T & j is_a_value_on T & s is_a_value_on T &
c is_a_value_on T & p is_a_value_on T & q is_a_value_on T &
ps is_a_value_on T & qc is_a_value_on T;
set D = ND(V,A);
set EN = {i,j,n,s,b,c,p,q,ps,qc};
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set Db = denaming(V,A,b);
set Dc = denaming(V,A,c);
set Dp = denaming(V,A,p);
set Dq = denaming(V,A,q);
set Dps = denaming(V,A,ps);
set Dqc = denaming(V,A,qc);
set Aij = addition(A,i,j);
set Mps = multiplication(A,p,s);
set Mqc = multiplication(A,q,c);
set Scs = subtraction(A,ps,qc);
set AS1 = SC_assignment(Ds,c);
set AS2 = SC_assignment(Db,s);
set AS3 = SC_assignment(Mps,ps);
set AS4 = SC_assignment(Mqc,qc);
set AS5 = SC_assignment(Scs,b);
set AS6 = SC_assignment(Aij,i);
set prg = <*Ds,Db,Mps,Mqc,Scs,Aij*>;
set pos = <*6,4,9,10,5,1*>;
set PS = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
A8: EN c= dom d1 by A5,A6,Th12;
A9: i in EN by ENUMSET1:def 8;
A10: j in EN by ENUMSET1:def 8;
A11: b in EN by ENUMSET1:def 8;
A12: p in EN by ENUMSET1:def 8;
A13: q in EN by ENUMSET1:def 8;
A14: len prg = 6 by AOFA_A00:20;
A15: len PS = len prg by NOMIN_8:def 14;
A16: prg.1 = Ds & pos.1 = 6;
A17: prg.2 = Db & pos.2 = 4;
A18: prg.3 = Mps & pos.3 = 9;
A19: prg.4 = Mqc & pos.4 = 10;
A20: prg.5 = Scs & pos.5 = 5;
A21: dom AS1 = dom Ds by NOMIN_2:def 7;
A22: dom AS2 = dom Db by NOMIN_2:def 7;
PP_composition(PP_composition(PP_composition(PP_composition(AS1,AS2),
AS3),AS4),AS5) = PP_composition(PP_composition(PP_composition(
AS2*AS1,AS3),AS4),AS5) by PARTPR_2:def 1
.= PP_composition(PP_composition(AS3*(AS2*AS1),AS4),AS5)
by PARTPR_2:def 1
.= PP_composition(AS4*(AS3*(AS2*AS1)),AS5) by PARTPR_2:def 1
.= AS5*(AS4*(AS3*(AS2*AS1))) by PARTPR_2:def 1;
then
A23: B = AS6*(AS5*(AS4*(AS3*(AS2*AS1)))) by PARTPR_2:def 1;
A24: AS5*AS4*AS3*AS2*AS1 = AS5*AS4*AS3*(AS2*AS1) by RELAT_1:36
.= AS5*AS4*(AS3*(AS2*AS1)) by RELAT_1:36
.= AS5*(AS4*(AS3*(AS2*AS1))) by RELAT_1:36;
A25: AS5*(AS4*(AS3*(AS2*AS1))) = AS5*(AS4*AS3*(AS2*AS1)) by RELAT_1:36
.= AS5*(AS4*AS3*AS2*AS1) by RELAT_1:36;
A26: AS4*AS3*AS2*AS1 = AS4*AS3*(AS2*AS1) by RELAT_1:36
.= AS4*(AS3*(AS2*AS1)) by RELAT_1:36;
A27: AS4*(AS3*(AS2*AS1)) = AS4*(AS3*AS2*AS1) by RELAT_1:36;
A28: AS3*AS2*AS1 = AS3*(AS2*AS1) by RELAT_1:36;
B = AS6*(AS5*AS4*(AS3*(AS2*AS1))) by A23,RELAT_1:36
.= AS6*(AS5*AS4*AS3*(AS2*AS1)) by RELAT_1:36
.= AS6*(AS5*AS4*AS3*AS2*AS1) by RELAT_1:36;
then
A29: d1 in dom(AS5*AS4*AS3*AS2*AS1) by A4,FUNCT_1:11;
then d1 in dom(AS4*AS3*AS2*AS1) by A24,A25,FUNCT_1:11;
then d1 in dom(AS3*AS2*AS1) by A26,A27,FUNCT_1:11;
then
A30: d1 in dom(AS2*AS1) by A28,FUNCT_1:11;
A31: dom Di = {d where d is NonatomicND of V,A: i in dom d}
by NOMIN_1:def 18;
A32: dom Dj = {d where d is NonatomicND of V,A: j in dom d}
by NOMIN_1:def 18;
A33: dom Ds = {d where d is NonatomicND of V,A: s in dom d}
by NOMIN_1:def 18;
A34: dom Db = {d where d is NonatomicND of V,A: b in dom d}
by NOMIN_1:def 18;
A35: dom Dc = {d where d is NonatomicND of V,A: c in dom d}
by NOMIN_1:def 18;
A36: dom Dp = {d where d is NonatomicND of V,A: p in dom d}
by NOMIN_1:def 18;
A37: dom Dq = {d where d is NonatomicND of V,A: q in dom d}
by NOMIN_1:def 18;
A38: dom Dps = {d where d is NonatomicND of V,A: ps in dom d}
by NOMIN_1:def 18;
A39: dom Dqc = {d where d is NonatomicND of V,A: qc in dom d}
by NOMIN_1:def 18;
A40: d1 in dom Ds by A21,A29,FUNCT_1:11;
then reconsider Ad = Ds.d1 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L1 = local_overlapping(V,A,d1,Ad,c) as NonatomicND of V,A
by NOMIN_2:9;
AS1.d1 = L1 by A21,A40,NOMIN_2:def 7;
then L1 in dom AS2 by A30,FUNCT_1:11;
then reconsider DbL1 = Db.L1 as TypeSCNominativeData of V,A
by A22,PARTFUN1:4,NOMIN_1:39;
reconsider L2 = local_overlapping(V,A,L1,DbL1,s) as NonatomicND of V,A
by NOMIN_2:9;
A41: dom L1 = {c} \/ dom d1 by A3,A1,NOMIN_4:4;
A42: dom L2 = {s} \/ dom L1 by A3,A1,NOMIN_4:4;
s in {s} by TARSKI:def 1;
then
s in dom L2 by A42,XBOOLE_0:def 3;
then
A43: L2 in dom Ds by A33;
p in dom L1 by A8,A12,A41,XBOOLE_0:def 3;
then p in dom L2 by A42,XBOOLE_0:def 3;
then L2 in dom Dp by A36;
then L2 in dom Ds /\ dom Dp by A43,XBOOLE_0:def 4;
then
A44: L2 in dom <:Dp,Ds:> by FUNCT_3:def 7;
then
A45: <:Dp,Ds:>.L2 = [Dp.L2,Ds.L2] by FUNCT_3:def 7;
A46: dom(multiplication(A)) = [:A,A:] by A2,FUNCT_2:def 1;
p is_a_value_on L2 & s is_a_value_on L2 by A7;
then [Dp.L2,Ds.L2] in [:A,A:] by ZFMISC_1:87;
then
A47: L2 in dom Mps by A44,A46,A45,FUNCT_1:11;
then reconsider MpsL2 = Mps.L2 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L3 = local_overlapping(V,A,L2,MpsL2,ps) as NonatomicND of V,A
by NOMIN_2:9;
A48: dom L3 = {ps} \/ dom L2 by A1,A3,NOMIN_4:4;
q in dom L1 by A8,A13,A41,XBOOLE_0:def 3;
then q in dom L2 by A42,XBOOLE_0:def 3;
then
A49: q in dom L3 by A48,XBOOLE_0:def 3;
c in {c} by TARSKI:def 1;
then c in dom L1 by A41,XBOOLE_0:def 3;
then c in dom L2 by A42,XBOOLE_0:def 3;
then
A50: c in dom L3 by A48,XBOOLE_0:def 3;
A51: L3 in dom Dq by A49,A37;
L3 in dom Dc by A50,A35;
then L3 in dom Dq /\ dom Dc by A51,XBOOLE_0:def 4;
then
A52: L3 in dom <:Dq,Dc:> by FUNCT_3:def 7;
then
A53: <:Dq,Dc:>.L3 = [Dq.L3,Dc.L3] by FUNCT_3:def 7;
q is_a_value_on L3 & c is_a_value_on L3 by A7;
then [Dq.L3,Dc.L3] in [:A,A:] by ZFMISC_1:87;
then
A54: L3 in dom Mqc by A52,A46,A53,FUNCT_1:11;
then reconsider MqcL3 = Mqc.L3 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L4 = local_overlapping(V,A,L3,MqcL3,qc) as NonatomicND of V,A
by NOMIN_2:9;
A55: dom L4 = {qc} \/ dom L3 by A1,A3,NOMIN_4:4;
qc in {qc} by TARSKI:def 1;
then
A56: qc in dom L4 by A55,XBOOLE_0:def 3;
ps in {ps} by TARSKI:def 1;
then ps in dom L3 by A48,XBOOLE_0:def 3;
then
A57: ps in dom L4 by A55,XBOOLE_0:def 3;
A58: b in dom L1 by A8,A11,A41,XBOOLE_0:def 3;
A59: L4 in dom Dps by A57,A38;
L4 in dom Dqc by A56,A39;
then L4 in dom Dps /\ dom Dqc by A59,XBOOLE_0:def 4;
then
A60: L4 in dom <:Dps,Dqc:> by FUNCT_3:def 7;
then
A61: <:Dps,Dqc:>.L4 = [Dps.L4,Dqc.L4] by FUNCT_3:def 7;
A62: dom(subtraction(A)) = [:A,A:] by A2,FUNCT_2:def 1;
ps is_a_value_on L4 & qc is_a_value_on L4 by A7;
then [Dps.L4,Dqc.L4] in [:A,A:] by ZFMISC_1:87;
then
A63: L4 in dom Scs by A60,A62,A61,FUNCT_1:11;
then reconsider ScsL4 = Scs.L4 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L5 = local_overlapping(V,A,L4,ScsL4,b) as NonatomicND of V,A
by NOMIN_2:9;
A64: dom L5 = {b} \/ dom L4 by A1,A3,NOMIN_4:4;
i in dom L1 by A8,A9,A41,XBOOLE_0:def 3;
then i in dom L2 by A42,XBOOLE_0:def 3;
then i in dom L3 by A48,XBOOLE_0:def 3;
then i in dom L4 by A55,XBOOLE_0:def 3;
then i in dom L5 by A64,XBOOLE_0:def 3;
then
A65: L5 in dom Di by A31;
j in dom L1 by A8,A10,A41,XBOOLE_0:def 3;
then j in dom L2 by A42,XBOOLE_0:def 3;
then j in dom L3 by A48,XBOOLE_0:def 3;
then j in dom L4 by A55,XBOOLE_0:def 3;
then j in dom L5 by A64,XBOOLE_0:def 3;
then
A66: L5 in dom Dj by A32;
L5 in dom Di /\ dom Dj by A65,A66,XBOOLE_0:def 4;
then
A67: L5 in dom <:Di,Dj:> by FUNCT_3:def 7;
then
A68: <:Di,Dj:>.L5 = [Di.L5,Dj.L5] by FUNCT_3:def 7;
A69: dom(addition(A)) = [:A,A:] by A2,FUNCT_2:def 1;
i is_a_value_on L5 & j is_a_value_on L5 by A7;
then [Di.L5,Dj.L5] in [:A,A:] by ZFMISC_1:87;
then
A70: L5 in dom Aij by A69,A67,A68,FUNCT_1:11;
A71: 2=1+1 & 3=2+1 & 4=3+1 & 5=4+1 & 6=5+1;
A72: PS.1 = L1 by A14,A16,NOMIN_8:def 14;
A73: PS.2 = L2 by A71,A14,A15,A17,A72,NOMIN_8:def 14;
A74: PS.3 = L3 by A71,A14,A15,A18,A73,NOMIN_8:def 14;
A75: PS.4 = L4 by A71,A14,A15,A19,A74,NOMIN_8:def 14;
let y be Nat;
assume
A76: 1 <= y;
assume y < len prg;
then y+1-1 <= 6-1 by A14,NAT_1:13;
then y = 1+0 or ... or y = 1+4 by A76,NAT_1:62;
then per cases;
suppose y = 1;
hence thesis by A72,A34,A58;
end;
suppose y = 2;
hence thesis by A47,A71,A14,A15,A17,A72,NOMIN_8:def 14;
end;
suppose y = 3;
hence thesis by A54,A71,A14,A15,A18,A73,NOMIN_8:def 14;
end;
suppose y = 4;
hence thesis by A63,A71,A14,A15,A19,A74,NOMIN_8:def 14;
end;
suppose y = 5;
hence thesis by A70,A71,A14,A15,A20,A75,NOMIN_8:def 14;
end;
end;
theorem Th16:
for V being non empty set
for loc being V-valued 10-element FinSequence holds
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)
proof
let V be non empty set;
let loc be V-valued 10-element FinSequence;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, 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 i is_a_value_on T & j is_a_value_on T & s is_a_value_on T &
c is_a_value_on T & p is_a_value_on T & q is_a_value_on T &
ps is_a_value_on T & qc is_a_value_on T;
assume
A4: loc is one-to-one;
A5: Seg 10 = dom loc by FINSEQ_1:89;
A6: loc|Seg 10 = loc;
set D = ND(V,A);
set EN = {i,j,n,s,b,c,p,q,ps,qc};
set inv = Lucas_inv(A,loc,x0,y0,p0,q0,n0);
set B = Lucas_loop_body(A,loc);
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set Db = denaming(V,A,b);
set Dc = denaming(V,A,c);
set Dp = denaming(V,A,p);
set Dq = denaming(V,A,q);
set Dps = denaming(V,A,ps);
set Dqc = denaming(V,A,qc);
set Aij = addition(A,i,j);
set Mps = multiplication(A,p,s);
set Mqc = multiplication(A,q,c);
set Scs = subtraction(A,ps,qc);
set AS1 = SC_assignment(Ds,c);
set AS2 = SC_assignment(Db,s);
set AS3 = SC_assignment(Mps,ps);
set AS4 = SC_assignment(Mqc,qc);
set AS5 = SC_assignment(Scs,b);
set AS6 = SC_assignment(Aij,i);
now
let d be TypeSCNominativeData of V,A such that
A7: d in dom inv and
A8: inv.d = TRUE and
A9: d in dom B and
A10: B.d in dom inv;
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: EN c= dom d1 and
A13: d1.j = 1 and
A14: d1.n = n0 and
A15: d1.p = p0 and
A16: d1.q = q0 and
A17: ex I being Nat st I = d1.i & d1.s = Lucas(x0,y0,p0,q0,I) &
d1.b = Lucas(x0,y0,p0,q0,I+1);
A18: i in EN by ENUMSET1:def 8;
A19: j in EN by ENUMSET1:def 8;
A20: n in EN by ENUMSET1:def 8;
A21: s in EN by ENUMSET1:def 8;
A22: b in EN by ENUMSET1:def 8;
A23: p in EN by ENUMSET1:def 8;
A24: q in EN by ENUMSET1:def 8;
consider I being Nat such that
A25: I = d1.i and
A26: d1.s = Lucas(x0,y0,p0,q0,I) and
A27: d1.b = Lucas(x0,y0,p0,q0,I+1) by A17;
set prg = <*Ds,Db,Mps,Mqc,Scs,Aij*>;
set pos = <*6,4,9,10,5,1*>;
reconsider prg as non empty FPrg(ND(V,A))-valued FinSequence;
set PS = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
A28: len prg = 6 by AOFA_A00:20;
A29: len PS = len prg by NOMIN_8:def 14;
A30: prg.1 = Ds & pos.1 = 6;
A31: prg.2 = Db & pos.2 = 4;
A32: prg.3 = Mps & pos.3 = 9;
A33: prg.4 = Mqc & pos.4 = 10;
A34: prg.5 = Scs & pos.5 = 5;
A35: prg.6 = Aij & pos.6 = 1;
rng loc c= EN
proof
let y be object;
assume y in rng loc;
then consider w being object such that
A36: w in dom loc and
A37: loc.w = y by FUNCT_1:def 3;
A38: w = 1 or ... or 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 thesis by A37,A38,ENUMSET1:def 8;
end;
then rng loc c= dom d1 by A12;
then
A39: loc is_valid_wrt d1;
A40: dom AS1 = dom Ds by NOMIN_2:def 7;
A41: dom AS2 = dom Db by NOMIN_2:def 7;
PP_composition(PP_composition(PP_composition(PP_composition(AS1,AS2),
AS3),AS4),AS5) = PP_composition(PP_composition(PP_composition(
AS2*AS1,AS3),AS4),AS5) by PARTPR_2:def 1
.= PP_composition(PP_composition(AS3*(AS2*AS1),AS4),AS5)
by PARTPR_2:def 1
.= PP_composition(AS4*(AS3*(AS2*AS1)),AS5) by PARTPR_2:def 1
.= AS5*(AS4*(AS3*(AS2*AS1))) by PARTPR_2:def 1;
then
A42: B = AS6*(AS5*(AS4*(AS3*(AS2*AS1)))) by PARTPR_2:def 1;
A43: AS5*AS4*AS3*AS2*AS1 = AS5*AS4*AS3*(AS2*AS1) by RELAT_1:36
.= AS5*AS4*(AS3*(AS2*AS1)) by RELAT_1:36
.= AS5*(AS4*(AS3*(AS2*AS1))) by RELAT_1:36;
A44: AS5*(AS4*(AS3*(AS2*AS1))) = AS5*(AS4*AS3*(AS2*AS1)) by RELAT_1:36
.= AS5*(AS4*AS3*AS2*AS1) by RELAT_1:36;
A45: AS4*AS3*AS2*AS1 = AS4*AS3*(AS2*AS1) by RELAT_1:36
.= AS4*(AS3*(AS2*AS1)) by RELAT_1:36;
A46: AS4*(AS3*(AS2*AS1)) = AS4*(AS3*AS2*AS1) by RELAT_1:36;
A47: AS3*AS2*AS1 = AS3*(AS2*AS1) by RELAT_1:36;
B = AS6*(AS5*AS4*(AS3*(AS2*AS1))) by A42,RELAT_1:36
.= AS6*(AS5*AS4*AS3*(AS2*AS1)) by RELAT_1:36
.= AS6*(AS5*AS4*AS3*AS2*AS1) by RELAT_1:36;
then
A48: d in dom(AS5*AS4*AS3*AS2*AS1) by A9,FUNCT_1:11;
then
A49: d in dom(AS4*AS3*AS2*AS1) by A43,A44,FUNCT_1:11;
then d in dom(AS3*AS2*AS1) by A45,A46,FUNCT_1:11;
then
A50: d in dom(AS2*AS1) by A47,FUNCT_1:11;
then
A51: (AS2*AS1).d = AS2.(AS1.d) by FUNCT_1:12;
A52: dom Di = {d where d is NonatomicND of V,A: i in dom d}
by NOMIN_1:def 18;
A53: dom Dj = {d where d is NonatomicND of V,A: j in dom d}
by NOMIN_1:def 18;
A54: dom Ds = {d where d is NonatomicND of V,A: s in dom d}
by NOMIN_1:def 18;
A55: dom Db = {d where d is NonatomicND of V,A: b in dom d}
by NOMIN_1:def 18;
A56: dom Dc = {d where d is NonatomicND of V,A: c in dom d}
by NOMIN_1:def 18;
A57: dom Dp = {d where d is NonatomicND of V,A: p in dom d}
by NOMIN_1:def 18;
A58: dom Dq = {d where d is NonatomicND of V,A: q in dom d}
by NOMIN_1:def 18;
A59: dom Dps = {d where d is NonatomicND of V,A: ps in dom d}
by NOMIN_1:def 18;
A60: dom Dqc = {d where d is NonatomicND of V,A: qc in dom d}
by NOMIN_1:def 18;
A61: d in dom AS1 by A48,FUNCT_1:11;
then reconsider Ad = Ds.d1 as TypeSCNominativeData of V,A
by A40,A11,PARTFUN1:4,NOMIN_1:39;
reconsider L1 = local_overlapping(V,A,d1,Ad,c) as NonatomicND of V,A
by NOMIN_2:9;
A62: PS.1 = L1 by A28,A30,NOMIN_8:def 14;
A63: AS1.d = L1 by A11,A61,NOMIN_2:def 7;
then
A64: L1 in dom AS2 by A50,FUNCT_1:11;
then reconsider DbL1 = Db.L1 as TypeSCNominativeData of V,A
by A41,PARTFUN1:4,NOMIN_1:39;
reconsider L2 = local_overlapping(V,A,L1,DbL1,s) 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: PS.2 = L2 by A65,A28,A29,A31,A62,NOMIN_8:def 14;
A67: AS2.L1 = L2 by A64,NOMIN_2:def 7;
A68: dom L1 = {c} \/ dom d1 by A2,NOMIN_4:4;
A69: dom L2 = {s} \/ dom L1 by A2,NOMIN_4:4;
A70: d1 in dom Ds by A12,A21,A54;
A71: dom PS = dom prg by A29,FINSEQ_3:29;
A72: s 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 Ds by A54;
A74: p in dom L1 by A12,A23,A68,XBOOLE_0:def 3;
then
A75: p in dom L2 by A69,XBOOLE_0:def 3;
then L2 in dom Dp by A57;
then L2 in dom Ds /\ dom Dp by A73,XBOOLE_0:def 4;
then
A76: L2 in dom <:Dp,Ds:> by FUNCT_3:def 7;
then
A77: <:Dp,Ds:>.L2 = [Dp.L2,Ds.L2] by FUNCT_3:def 7;
A78: dom(multiplication(A)) = [:A,A:] by A1,FUNCT_2:def 1;
p is_a_value_on L2 & s is_a_value_on L2 by A3;
then [Dp.L2,Ds.L2] in [:A,A:] by ZFMISC_1:87;
then
A79: L2 in dom Mps by A76,A78,A77,FUNCT_1:11;
then reconsider MpsL2 = Mps.L2 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L3 = local_overlapping(V,A,L2,MpsL2,ps) as NonatomicND of V,A
by NOMIN_2:9;
A80: PS.3 = L3 by A65,A28,A29,A32,A66,NOMIN_8:def 14;
A81: dom L3 = {ps} \/ dom L2 by A2,NOMIN_4:4;
A82: s in dom L3
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A31,A80,NOMIN_8:25;
A83: q in dom L1 by A12,A24,A68,XBOOLE_0:def 3;
then
A84: q in dom L2 by A69,XBOOLE_0:def 3;
then
A85: q in dom L3 by A81,XBOOLE_0:def 3;
A86: c in dom L1
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A62,NOMIN_8:25;
A87: c in dom L2
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A66,NOMIN_8:25;
A88: c in dom L3
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A80,NOMIN_8:25;
A89: L3 in dom Dq by A85,A58;
L3 in dom Dc by A88,A56;
then L3 in dom Dq /\ dom Dc by A89,XBOOLE_0:def 4;
then
A90: L3 in dom <:Dq,Dc:> by FUNCT_3:def 7;
then
A91: <:Dq,Dc:>.L3 = [Dq.L3,Dc.L3] by FUNCT_3:def 7;
q is_a_value_on L3 & c is_a_value_on L3 by A3;
then [Dq.L3,Dc.L3] in [:A,A:] by ZFMISC_1:87;
then
A92: L3 in dom Mqc by A90,A78,A91,FUNCT_1:11;
then reconsider MqcL3 = Mqc.L3 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L4 = local_overlapping(V,A,L3,MqcL3,qc) as NonatomicND of V,A
by NOMIN_2:9;
A93: PS.4 = L4 by A65,A28,A29,A33,A80,NOMIN_8:def 14;
A94: dom L4 = {qc} \/ dom L3 by A2,NOMIN_4:4;
A95: qc in dom L4
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A33,A93,NOMIN_8:25;
A96: ps in dom L3
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A32,A80,NOMIN_8:25;
A97: ps in dom L4
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A32,A93,NOMIN_8:25;
A98: b in dom L1 by A12,A22,A68,XBOOLE_0:def 3;
A99: L4 in dom Dps by A97,A59;
L4 in dom Dqc by A95,A60;
then L4 in dom Dps /\ dom Dqc by A99,XBOOLE_0:def 4;
then
A100: L4 in dom <:Dps,Dqc:> by FUNCT_3:def 7;
then
A101: <:Dps,Dqc:>.L4 = [Dps.L4,Dqc.L4] by FUNCT_3:def 7;
A102: dom(subtraction(A)) = [:A,A:] by A1,FUNCT_2:def 1;
ps is_a_value_on L4 & qc is_a_value_on L4 by A3;
then [Dps.L4,Dqc.L4] in [:A,A:] by ZFMISC_1:87;
then
A103: L4 in dom Scs by A100,A102,A101,FUNCT_1:11;
then reconsider ScsL4 = Scs.L4 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L5 = local_overlapping(V,A,L4,ScsL4,b) as NonatomicND of V,A
by NOMIN_2:9;
A104: PS.5 = L5 by A65,A28,A29,A34,A93,NOMIN_8:def 14;
A105: dom L5 = {b} \/ dom L4 by A2,NOMIN_4:4;
A106: i in dom L1 by A12,A18,A68,XBOOLE_0:def 3;
then
A107: i in dom L2 by A69,XBOOLE_0:def 3;
then
A108: i in dom L3 by A81,XBOOLE_0:def 3;
then
A109: i in dom L4 by A94,XBOOLE_0:def 3;
then
A110: i in dom L5 by A105,XBOOLE_0:def 3;
then
A111: L5 in dom Di by A52;
A112: j in dom L1 by A12,A19,A68,XBOOLE_0:def 3;
then
A113: j in dom L2 by A69,XBOOLE_0:def 3;
then
A114: j in dom L3 by A81,XBOOLE_0:def 3;
then
A115: j in dom L4 by A94,XBOOLE_0:def 3;
then
A116: j in dom L5 by A105,XBOOLE_0:def 3;
then
A117: L5 in dom Dj by A53;
L5 in dom Di /\ dom Dj by A111,A117,XBOOLE_0:def 4;
then
A118: L5 in dom <:Di,Dj:> by FUNCT_3:def 7;
then
A119: <:Di,Dj:>.L5 = [Di.L5,Dj.L5] by FUNCT_3:def 7;
A120: dom(addition(A)) = [:A,A:] by A1,FUNCT_2:def 1;
i is_a_value_on L5 & j is_a_value_on L5 by A3;
then [Di.L5,Dj.L5] in [:A,A:] by ZFMISC_1:87;
then
A121: L5 in dom Aij by A120,A118,A119,FUNCT_1:11;
then reconsider AijL5 = Aij.L5 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39;
reconsider L6 = local_overlapping(V,A,L5,AijL5,i) as NonatomicND of V,A
by NOMIN_2:9;
A122: PS.6 = L6 by A28,A29,A35,A104,NOMIN_8:def 14;
A123: dom L6 = {i} \/ dom L5 by A2,NOMIN_4:4;
A124: d in dom(AS3*(AS2*AS1)) by A45,A49,FUNCT_1:11;
then L2 in dom AS3 by A51,A63,A67,FUNCT_1:11;
then
A125: AS3.L2 = L3 by NOMIN_2:def 7;
A126: (AS3*(AS2*AS1)).d = AS3.((AS2*AS1).d) by A124,FUNCT_1:12;
then L3 in dom AS4 by A49,A45,A125,A67,A51,A63,FUNCT_1:11;
then
A127: AS4.L3 = L4 by NOMIN_2:def 7;
A128: (AS4*(AS3*(AS2*AS1))).d = AS4.((AS3*(AS2*AS1)).d) by A49,A45,FUNCT_1:12;
then L4 in dom AS5 by A43,A48,A127,A125,A67,A63,A126,A51,FUNCT_1:11;
then
A129: AS5.L4 = L5 by NOMIN_2:def 7;
A130: (AS5*(AS4*(AS3*(AS2*AS1)))).d = AS5.((AS4*(AS3*(AS2*AS1))).d)
by A43,A48,FUNCT_1:12;
B = AS6*AS5*(AS4*(AS3*(AS2*AS1))) by A42,RELAT_1:36
.= AS6*AS5*AS4*(AS3*(AS2*AS1)) by RELAT_1:36
.= AS6*AS5*AS4*AS3*(AS2*AS1) by RELAT_1:36
.= AS6*AS5*AS4*AS3*AS2*AS1 by RELAT_1:36;
then AS1.d in dom(AS6*AS5*AS4*AS3*AS2) by A9,FUNCT_1:11;
then AS2.L1 in dom(AS6*AS5*AS4*AS3) by A63,FUNCT_1:11;
then AS3.L2 in dom(AS6*AS5*AS4) by A67,FUNCT_1:11;
then AS4.L3 in dom(AS6*AS5) by A125,FUNCT_1:11;
then AS5.L4 in dom AS6 by A127,FUNCT_1:11;
then
A131: L6 = AS6.L5 by A129,NOMIN_2:def 7
.= B.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;
thus L6 = L6;
A132: i in dom L6 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A35,A122,
NOMIN_8:25;
A133: j in dom L6 by A116,A123,XBOOLE_0:def 3;
A134: n in dom L1 by A12,A20,A68,XBOOLE_0:def 3;
then
A135: n in dom L2 by A69,XBOOLE_0:def 3;
then
A136: n in dom L3 by A81,XBOOLE_0:def 3;
then
A137: n in dom L4 by A94,XBOOLE_0:def 3;
then
A138: n in dom L5 by A105,XBOOLE_0:def 3;
then
A139: n in dom L6 by A123,XBOOLE_0:def 3;
A140: s in dom L4 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A31,A93,
NOMIN_8:25;
A141: s in dom L5 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A31,A104,
NOMIN_8:25;
A142: s in dom L6 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A31,A122,
NOMIN_8:25;
A143: b in dom L5 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A34,A104,
NOMIN_8:25;
A144: b in dom L6 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A34,A122,
NOMIN_8:25;
A145: c in dom L6
by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A30,A28,A122,NOMIN_8:25;
A146: p in dom L3 by A75,A81,XBOOLE_0:def 3;
then
A147: p in dom L4 by A94,XBOOLE_0:def 3;
then
A148: p in dom L5 by A105,XBOOLE_0:def 3;
then
A149: p in dom L6 by A123,XBOOLE_0:def 3;
A150: q in dom L4 by A85,A94,XBOOLE_0:def 3;
then
A151: q in dom L5 by A105,XBOOLE_0:def 3;
then
A152: q in dom L6 by A123,XBOOLE_0:def 3;
A153: ps in dom L6 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A32,A122,
NOMIN_8:25;
qc in dom L6 by A1,A2,A3,A5,A9,A11,Th15,A39,A71,A70,A28,A30,A33,A122,
NOMIN_8:25;
hence EN c= dom L6
by A132,A133,A139,A142,A144,A145,A149,A152,A153,ENUMSET1:def 8;
A154: L5.j = L4.j by A2,A4,A5,A6,A115,NOMIN_5:3,NOMIN_7:1
.= L3.j by A2,A4,A5,A6,A114,NOMIN_5:3,NOMIN_7:1
.= L2.j by A2,A4,A5,A6,A113,NOMIN_5:3,NOMIN_7:1
.= L1.j 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.j = 1 by A2,A4,A5,A6,A116,NOMIN_5:3,NOMIN_7:1;
thus L6.n = L5.n by A2,A4,A5,A6,A138,NOMIN_5:3,NOMIN_7:1
.= L4.n by A2,A4,A5,A6,A137,NOMIN_5:3,NOMIN_7:1
.= L3.n by A2,A4,A5,A6,A136,NOMIN_5:3,NOMIN_7:1
.= L2.n by A2,A4,A5,A6,A135,NOMIN_5:3,NOMIN_7:1
.= L1.n 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;
thus L6.p = L5.p by A2,A4,A5,A6,A148,NOMIN_5:3,NOMIN_7:1
.= L4.p by A2,A4,A5,A6,A147,NOMIN_5:3,NOMIN_7:1
.= L3.p by A2,A4,A5,A6,A146,NOMIN_5:3,NOMIN_7:1
.= L2.p by A2,A4,A5,A6,A75,NOMIN_5:3,NOMIN_7:1
.= L1.p 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;
thus L6.q = L5.q by A2,A4,A5,A6,A151,NOMIN_5:3,NOMIN_7:1
.= L4.q by A2,A4,A5,A6,A150,NOMIN_5:3,NOMIN_7:1
.= L3.q by A2,A4,A5,A6,A85,NOMIN_5:3,NOMIN_7:1
.= L2.q by A2,A4,A5,A6,A84,NOMIN_5:3,NOMIN_7:1
.= L1.q 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;
take I1 = I+1;
A155: L5.i = L4.i by A2,A4,A5,A6,A109,NOMIN_5:3,NOMIN_7:1
.= L3.i by A2,A4,A5,A6,A108,NOMIN_5:3,NOMIN_7:1
.= L2.i by A2,A4,A5,A6,A107,NOMIN_5:3,NOMIN_7:1
.= L1.i 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.i = Aij.L5 by NOMIN_2:10
.= I1 by A1,A121,A110,A116,A154,A155,NOMIN_5:4;
A156: L1 in dom Db by A55,A98;
A157: L2.s = Db.L1 by NOMIN_2:10
.= denaming(b,L1) by A156,NOMIN_1:def 18
.= L1.b 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.s = L5.s by A2,A4,A5,A6,A141,NOMIN_5:3,NOMIN_7:1
.= L4.s by A2,A4,A5,A6,A140,NOMIN_5:3,NOMIN_7:1
.= L3.s 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;
A158: L2.p = L1.p 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.ps = L3.ps by A2,A4,A5,A6,A96,NOMIN_5:3,NOMIN_7:1
.= Mps.L2 by NOMIN_2:10
.= p0*Lucas(x0,y0,p0,q0,I1) by A1,A79,A75,A72,A157,A158,NOMIN_5:5;
A160: L3.q = L2.q by A2,A4,A5,A6,A84,NOMIN_5:3,NOMIN_7:1
.= L1.q 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.c = L2.c by A2,A4,A5,A6,A87,NOMIN_5:3,NOMIN_7:1
.= L1.c by A2,A4,A5,A6,A86,NOMIN_5:3,NOMIN_7:1
.= Ds.d1 by NOMIN_2:10
.= denaming(s,d1) by A70,NOMIN_1:def 18
.= Lucas(x0,y0,p0,q0,I) by A12,A21,A26,NOMIN_1:def 12;
A162: L4.qc = Mqc.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.b = L5.b by A2,A4,A5,A6,A143,NOMIN_7:1,NOMIN_5:3
.= Scs.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;
end;
hence inv.(B.d) = TRUE by A10,A131,Def15;
end;
hence thesis by NOMIN_3:28;
end;
theorem Th17:
for V being non empty set
for loc being V-valued 10-element FinSequence holds
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_main_loop(A,loc),
PP_and(Equality(A,loc/.1,loc/.3),Lucas_inv(A,loc,x0,y0,p0,q0,n0)) *>
is SFHT of ND(V,A)
proof
let V be non empty set;
let loc be V-valued 10-element FinSequence;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set D = ND(V,A);
set inv = Lucas_inv(A,loc,x0,y0,p0,q0,n0);
set B = Lucas_loop_body(A,loc);
set E = Equality(A,i,n);
set N = PP_inversion(inv);
assume A is complex-containing &
A is_without_nonatomicND_wrt V &
(for T being TypeSCNominativeData of V,A
holds i is_a_value_on T & j is_a_value_on T &
s is_a_value_on T & c is_a_value_on T & p is_a_value_on T &
q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T) &
loc is one-to-one;
then <*inv,B,inv*> is SFHT of D by Th16;
then
A1: <*PP_and(PP_not(E),inv),B,inv*> is SFHT of D by NOMIN_3:3,15;
<*N,B,inv*> is SFHT of D by NOMIN_3:19;
then <*PP_and(PP_not(E),N),B,inv*> is SFHT of D by NOMIN_3:3,15;
hence thesis by A1,NOMIN_3:26;
end;
theorem Th18:
for V being non empty set
for loc being V-valued 10-element FinSequence holds
for val being 10-element FinSequence holds
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 & loc,val are_different_wrt 10
implies
<* 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)
proof
let V be non empty set;
let loc be V-valued 10-element FinSequence;
let val be 10-element FinSequence;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4, b1 = val.5, c1 = val.6;
set p1 = val.7, q1 = val.8, ps1 = val.9, qc1 = val.10;
set D = ND(V,A);
set P = valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0);
set f = initial_assignments(A,loc,val,10);
set g = Lucas_main_loop(A,loc);
set Q = Lucas_inv(A,loc,x0,y0,p0,q0,n0);
set R = PP_and(Equality(A,i,n),Lucas_inv(A,loc,x0,y0,p0,q0,n0));
assume that
A1: A is complex-containing & A is_without_nonatomicND_wrt V &
(for T being TypeSCNominativeData of V,A
holds i is_a_value_on T & j is_a_value_on T &
s is_a_value_on T & c is_a_value_on T & p is_a_value_on T &
q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T) and
A2: loc is one-to-one and
A3: loc,val are_different_wrt 10;
A4: Seg 10 c= dom loc by FINSEQ_1:89;
loc|Seg 10 is one-to-one by A2;
then
A5: <*P,f,Q*> is SFHT of D by A1,A3,A4,Th14;
A6: <*Q,g,R*> is SFHT of D by A1,A2,Th17;
<*PP_inversion(Q),g,R*> is SFHT of D by NOMIN_3:19;
hence thesis by A5,A6,NOMIN_3:25;
end;
theorem Th19:
V is non empty & A is_without_nonatomicND_wrt V &
(for T 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)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, 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,i);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set Dz = denaming(V,A,z);
set ass = SC_assignment(Ds,z);
set out = valid_Lucas_output(A,z,x0,y0,p0,q0,n0);
set F = SC_Psuperpos(out,Ds,z);
set E = Equality(A,i,n);
set EM = {i,j,n,s,b,c,p,q,ps,qc};
assume that
A1: V is non empty & A is_without_nonatomicND_wrt V and
A2: for T holds i is_a_value_on T & n is_a_value_on T;
let d be Element of D such that
A3: d in dom PP_and(E,inv) and
A4: (PP_and(E,inv)).d = TRUE;
A5: dom F = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Ds.d,z) in dom out & d in dom Ds}
by NOMIN_2:def 11;
A6: dom out = {d where d is TypeSCNominativeData of V,A: d in dom Dz}
by NOMIN_8:def 13;
A7: dom Ds = {d where d is NonatomicND of V,A: s in dom d} by NOMIN_1:def 18;
A8: dom Dz = {d where d is NonatomicND of V,A: z in dom d} by NOMIN_1:def 18;
A9: d in dom E by A3,A4,PARTPR_1:23;
A10: d in dom inv by A3,A4,PARTPR_1:23;
A11: dom E = dom Di /\ dom Dn by A2,NOMIN_4:11;
then
A12: d in dom Di by A9,XBOOLE_0:def 4;
inv.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: EM c= dom d1 and
d1.j = 1 and
A15: d1.n = n0 and
d1.p = p0 and
d1.q = q0 and
A16: ex I being Nat st I = d1.i & d1.s = Lucas(x0,y0,p0,q0,I) &
d1.b = Lucas(x0,y0,p0,q0,I+1);
A17: i in EM by ENUMSET1:def 8;
A18: n in EM by ENUMSET1:def 8;
A19: s in EM by ENUMSET1:def 8;
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set L = local_overlapping(V,A,dd,Ds.dd,z);
A20: dd in dom Ds by A7,A13,A14,A19;
then Ds.d1 in D by A13,PARTFUN1:4;
then
A21: ex d2 being TypeSCNominativeData of V,A st Ds.d1 = d2;
then
A22: L in dom Dz by A1,A13,NOMIN_4:6;
then
A23: L in dom out by A6;
hence
A24: d in dom F by A5,A20;
valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,L
proof
consider I being Nat such that
A25: I = d1.i and
A26: d1.s = Lucas(x0,y0,p0,q0,I) and
d1.b = Lucas(x0,y0,p0,q0,I+1) by A16;
A27: ex d being NonatomicND of V,A st L = d & z in dom d by A8,A22;
then reconsider dlo = L as NonatomicND of V,A;
take dlo;
thus L = dlo;
rng <*z*> = {z} by FINSEQ_1:38;
hence rng <*z*> c= dom dlo by A27,ZFMISC_1:31;
let nn be Nat such that
A28: 1 <= nn and
A29: nn <= len <*z*>;
len <*z*> = 1 by FINSEQ_1:39;
then
A30: nn = 1 by A28,A29,XXREAL_0:1;
A31: i is_a_value_on dd by A2;
A32: n is_a_value_on dd by A2;
A33: dom <:Di,Dn:> = dom Di /\ dom Dn by FUNCT_3:def 7;
d in dom <:Di,Dn:> by A9,A11,FUNCT_3:def 7;
then
A34: E.d = (Equality(A)).(<:Di,Dn:>.d) by FUNCT_1:13;
A35: d in dom Dn by A9,A11,XBOOLE_0:def 4;
A36: <:Di,Dn:>.d = [Di.d,Dn.d] by A9,A11,A33,FUNCT_3:def 7;
A37: Di.d = denaming(i,d1) by A13,A12,NOMIN_1:def 18
.= d1.i by A14,A17,NOMIN_1:def 12;
A38: Dn.d = denaming(n,d1) by A13,A35,NOMIN_1:def 18
.= d1.n by A14,A18,NOMIN_1:def 12;
A39: Ds.d = denaming(s,d1) by A20,A13,NOMIN_1:def 18
.= d1.s by A14,A19,NOMIN_1:def 12;
(Equality(A)).(Di.d,Dn.d) <> FALSE by A3,A4,A34,A36,PARTPR_1:23;
then Di.d = Dn.d by A31,A32,NOMIN_4:def 9;
hence thesis by A1,A13,A15,A30,A21,A25,A26,A37,A38,A39,NOMIN_2:10;
end;
hence TRUE = out.L by A23,NOMIN_8:def 13
.= F.d by A24,NOMIN_2:35;
end;
theorem Th20:
V is non empty & A is_without_nonatomicND_wrt V &
(for T 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_assignment(denaming(V,A,loc/.4),z),
valid_Lucas_output(A,z,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A)
proof
set s = loc/.4;
<*SC_Psuperpos(valid_Lucas_output(A,z,x0,y0,p0,q0,n0),denaming(V,A,s),z),
SC_assignment(denaming(V,A,s),z),
valid_Lucas_output(A,z,x0,y0,p0,q0,n0)*> is SFHT
of ND(V,A) by NOMIN_3:29;
hence thesis by Th19,NOMIN_3:15;
end;
theorem Th21:
(for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
implies
<* 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)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set D = ND(V,A);
set inv = Lucas_inv(A,loc,x0,y0,p0,q0,n0);
set O = valid_Lucas_output(A,z,x0,y0,p0,q0,n0);
set Di = denaming(V,A,i);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set E = Equality(A,i,n);
set F = PP_and(E,inv);
set G = SC_assignment(Ds,z);
set N = PP_inversion(F);
assume
A1: for T holds i is_a_value_on T & n is_a_value_on T;
now
let d be TypeSCNominativeData of V,A such that
A2: d in dom N and
N.d = TRUE and
d in dom G and
G.d in dom O;
A3: dom F = {d where d is Element of D:
d in dom E & E.d = FALSE or d in dom inv & inv.d = FALSE
or d in dom E & E.d = TRUE & d in dom inv & inv.d = TRUE} by PARTPR_1:16;
A4: dom Di = {d where d is NonatomicND of V,A: i in dom d} by NOMIN_1:def 18;
A5: dom Dn = {d where d is NonatomicND of V,A: n in dom d} by NOMIN_1:def 18;
A6: dom E = dom Di /\ dom Dn by A1,NOMIN_4:11;
A7: not d in dom F by A2,PARTPR_2:9;
dom E c= dom F by PARTPR_2:3;
then not d in dom E by A2,PARTPR_2:9;
then
A8: not d in dom Di or not d in dom Dn by A6,XBOOLE_0:def 4;
dom inv = D by Def15;
then
A9: d in dom inv;
then inv.d <> FALSE by A3,A7;
then Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d by A9,Def15;
then consider d1 being NonatomicND of V,A such that
A10: d = d1 and
A11: {i,j,n,s,b,c,p,q,ps,qc} c= dom d1 and
d1.j = 1 & d1.n = n0 & d1.p = p0 & d1.q = q0 &
ex I being Nat st I = d1.i &
d1.s = Lucas(x0,y0,p0,q0,I) &
d1.b = Lucas(x0,y0,p0,q0,I+1);
i in {i,j,n,s,b,c,p,q,ps,qc} & n in {i,j,n,s,b,c,p,q,ps,qc}
by ENUMSET1:def 8;
hence O.(G.d) = TRUE by A4,A5,A8,A10,A11;
end;
hence thesis by NOMIN_3:28;
end;
::$N Partial correctness of a Lucas algorithm
theorem
for V being non empty set
for loc being V-valued 10-element FinSequence
for val being 10-element FinSequence
for z being Element of V holds
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)
proof
let V be non empty set;
let loc be V-valued 10-element FinSequence;
let val be 10-element FinSequence;
let z be Element of V;
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4, b = loc/.5, c = loc/.6;
set p = loc/.7, q = loc/.8, ps = loc/.9, qc = loc/.10;
set i1 = val.1, j1 = val.2, n1 = val.3, 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,s),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,i,n);
assume that
A1: A is complex-containing & A is_without_nonatomicND_wrt V
and
A2: for T being TypeSCNominativeData of V,A
holds i is_a_value_on T & j is_a_value_on T & n is_a_value_on T &
s is_a_value_on T & c is_a_value_on T & p is_a_value_on T &
q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T;
assume loc is one-to-one & loc,val are_different_wrt 10;
then
A3: <*P,F,PP_and(E,inv)*> is SFHT of D by A1,A2,Th18;
A4: <*PP_and(E,inv),G,Q*> is SFHT of D by A1,A2,Th20;
<*PP_inversion(PP_and(E,inv)),G,Q*> is SFHT of D by A2,Th21;
hence thesis by A3,A4,NOMIN_3:25;
end;