:: Partial correctness of an algorithm computing Lucas sequences
:: by Adrian Jaszczak
::
:: Received October 25, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

registration

let n be Nat;
let f be n -element FinSequence;

reduce f | (Seg n) to f;

reducibility
f | (Seg n) = f

proof 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
<*f1,f2,f3,f4,f5,f6*> is PFuncs (A,B) -valued

proof 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
<*f1,f2,f3,f4,f5,f6*> is FPrg (ND (V,A)) -valued ;

end;

registration

let a1, a2, a3, a4, a5, a6 be object ;

reduce <*a1,a2,a3,a4,a5,a6*> . 1 to a1;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 1 = a1 by AOFA_A00:20;

reduce <*a1,a2,a3,a4,a5,a6*> . 2 to a2;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 2 = a2 by AOFA_A00:20;

reduce <*a1,a2,a3,a4,a5,a6*> . 3 to a3;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 3 = a3 by AOFA_A00:20;

reduce <*a1,a2,a3,a4,a5,a6*> . 4 to a4;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 4 = a4 by AOFA_A00:20;

reduce <*a1,a2,a3,a4,a5,a6*> . 5 to a5;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 5 = a5 by AOFA_A00:20;

reduce <*a1,a2,a3,a4,a5,a6*> . 6 to a6;

reducibility
<*a1,a2,a3,a4,a5,a6*> . 6 = a6 by AOFA_A00:20;

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 :: NOMIN_9:def 1
<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>;

coherence
<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*> is FinSequence ;

end;

:: deftheorem defines <* NOMIN_9:def 1 :
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = <*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>;

theorem Th1: :: NOMIN_9:1

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 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
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> is 9 -element ;

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
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 1 = a1 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 2 to a2;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 2 = a2 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 3 to a3;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 3 = a3 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 4 to a4;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 4 = a4 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 5 to a5;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 5 = a5 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 6 to a6;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 6 = a6 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 7 to a7;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 7 = a7 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 8 to a8;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 8 = a8 by Th1;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 9 to a9;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 9 = a9 by Th1;

end;

theorem Th2: :: NOMIN_9:2

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 end;

definition

let X be non empty set ;
let a1, a2, a3, a4, a5, a6, a7, a8, a9 be Element of X;
:: original: <*
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence of X;
coherence
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> is FinSequence of X

proof 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 :: NOMIN_9:def 2
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> ^ <*a10*>;

coherence
<*a1,a2,a3,a4,a5,a6,a7,a8,a9*> ^ <*a10*> is FinSequence ;

end;

:: deftheorem defines <* NOMIN_9:def 2 :
for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object holds <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> ^ <*a10*>;

theorem Th3: :: NOMIN_9:3

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 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
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> is 10 -element ;

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
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 1 = a1 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 2 to a2;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 2 = a2 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 3 to a3;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 3 = a3 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 4 to a4;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 4 = a4 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 5 to a5;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 5 = a5 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 6 to a6;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 6 = a6 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 7 to a7;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 7 = a7 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 8 to a8;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 8 = a8 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 9 to a9;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 9 = a9 by Th3;

reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 10 to a10;

reducibility
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . 10 = a10 by Th3;

end;

theorem :: NOMIN_9:4

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 end;

definition

let X be non empty set ;
let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be Element of X;
:: original: <*
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence of X;
coherence
<*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> is FinSequence of X

proof end;

end;

definition

let i, j be Integer;
:: original: [
redefine func [i,j] -> Element of [:INT,INT:];
coherence
[i,j] is Element of [:INT,INT:]

proof end;

end;

definition

let x, y, P, Q be Integer;
deffunc H₁( set , Element of [:INT,INT:]) -> 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: :: NOMIN_9:def 3
( it . 0 = [x,y] & ( for n being Nat holds it . (n + 1) = [((it . n) `2),((P * ((it . n) `2)) - (Q * ((it . n) `1)))] ) );

existence
ex b₁ being sequence of [:INT,INT:] st
( b₁ . 0 = [x,y] & ( for n being Nat holds b₁ . (n + 1) = [((b₁ . n) `2),((P * ((b<sub>1</sub> . n) `2)) - (Q * ((b₁ . n) `1)))] ) )

proof end;

uniqueness
for b₁, b₂ being sequence of [:INT,INT:] st b₁ . 0 = [x,y] & ( for n being Nat holds b₁ . (n + 1) = [((b₁ . n) `2),((P * ((b<sub>1</sub> . n) `2)) - (Q * ((b₁ . n) `1)))] ) & b<sub>2</sub> . 0 = [x,y] & ( for n being Nat holds b<sub>2</sub> . (n + 1) = [((b<sub>2</sub> . n) `2),((P * ((b₂ . n) `2)) - (Q * ((b<sub>2</sub> . n) `1)))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Lucas_Sequence NOMIN_9:def 3 :
for x, y, P, Q being Integer
for b₅ being sequence of [:INT,INT:] holds
( b₅ = Lucas_Sequence (x,y,P,Q) iff ( b₅ . 0 = [x,y] & ( for n being Nat holds b₅ . (n + 1) = [((b₅ . n) `2),((P * ((b<sub>5</sub> . n) `2)) - (Q * ((b₅ . n) `1)))] ) ) );

definition

let x, y, P, Q be Integer;
let n be Nat;

func Lucas (x,y,P,Q,n) -> Element of INT equals :: NOMIN_9:def 4
((Lucas_Sequence (x,y,P,Q)) . n) `1 ;

coherence
((Lucas_Sequence (x,y,P,Q)) . n) `1 is Element of INT ;

end;

:: deftheorem defines Lucas NOMIN_9:def 4 :
for x, y, P, Q being Integer
for n being Nat holds Lucas (x,y,P,Q,n) = ((Lucas_Sequence (x,y,P,Q)) . n) `1 ;

theorem Th5: :: NOMIN_9:5

for x, y, P, Q being Integer holds
( Lucas (x,y,P,Q,0) = x & Lucas (x,y,P,Q,1) = y & ( for n being Nat holds Lucas (x,y,P,Q,(n + 2)) = (P * (Lucas (x,y,P,Q,(n + 1)))) - (Q * (Lucas (x,y,P,Q,n))) ) )

proof end;

theorem Th6: :: NOMIN_9:6

Lucas_Sequence (0,1,1,(- 1)) = Fib

proof end;

theorem :: NOMIN_9:7

for n being Nat holds Lucas (0,1,1,(- 1),n) = Fib n by Th6;

theorem Th8: :: NOMIN_9:8

for a, b being Nat holds Lucas_Sequence (a,b,1,(- 1)) = GenFib (a,b)

proof end;

theorem :: NOMIN_9:9

for a, b, n being Nat holds Lucas (a,b,1,(- 1),n) = GenFib (a,b,n) by Th8;

theorem Th10: :: NOMIN_9:10

Lucas_Sequence (2,1,1,(- 1)) = Lucas

proof end;

theorem :: NOMIN_9:11

for n being Nat holds Lucas (2,1,1,(- 1),n) = Lucas n by Th10;

:: 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: :: NOMIN_9:12

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st Seg 10 c= dom loc & loc is_valid_wrt d1 holds
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1

proof end;

definition

let V, A be set ;
let loc be V -valued Function;

func Lucas_loop_body (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_9:def 5
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
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)))) is SCBinominativeFunction of V,A ;

end;

:: deftheorem defines Lucas_loop_body NOMIN_9:def 5 :
for V, A being set
for loc being b₁ -valued Function holds Lucas_loop_body (A,loc) = 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))));

definition

let V, A be set ;
let loc be V -valued Function;

func Lucas_main_loop (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_9:def 6
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Lucas_loop_body (A,loc)));

coherence
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Lucas_loop_body (A,loc))) is SCBinominativeFunction of V,A ;

end;

:: deftheorem defines Lucas_main_loop NOMIN_9:def 6 :
for V, A being set
for loc being b₁ -valued Function holds Lucas_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Lucas_loop_body (A,loc)));

definition

let V, A be set ;
let loc be V -valued Function;
let val be Function;

func Lucas_main_part (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_9:def 7
PP_composition ((initial_assignments (A,loc,val,10)),(Lucas_main_loop (A,loc)));

coherence
PP_composition ((initial_assignments (A,loc,val,10)),(Lucas_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

end;

:: deftheorem defines Lucas_main_part NOMIN_9:def 7 :
for V, A being set
for loc being b₁ -valued Function
for val being Function holds Lucas_main_part (A,loc,val) = PP_composition ((initial_assignments (A,loc,val,10)),(Lucas_main_loop (A,loc)));

definition

let V, A be set ;
let loc be V -valued Function;
let val be Function;
let z be Element of V;

func Lucas_program (A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_9:def 8
PP_composition ((Lucas_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));

coherence
PP_composition ((Lucas_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z))) is SCBinominativeFunction of V,A ;

end;

:: deftheorem defines Lucas_program NOMIN_9:def 8 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for z being Element of V holds Lucas_program (A,loc,val,z) = PP_composition ((Lucas_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));

definition

let x0, y0, p0, q0 be Integer;
let n0 be Nat;

func Lucas_input (x0,y0,p0,q0,n0) -> FinSequence equals :: NOMIN_9:def 9
<*0,1,n0,x0,y0,x0,p0,q0,0,0*>;

coherence
<*0,1,n0,x0,y0,x0,p0,q0,0,0*> is FinSequence ;

end;

:: deftheorem defines Lucas_input NOMIN_9:def 9 :
for x0, y0, p0, q0 being Integer
for n0 being Nat holds Lucas_input (x0,y0,p0,q0,n0) = <*0,1,n0,x0,y0,x0,p0,q0,0,0*>;

registration

let x0, y0, p0, q0 be Integer;
let n0 be Nat;

cluster Lucas_input (x0,y0,p0,q0,n0) -> 10 -element ;

coherence
Lucas_input (x0,y0,p0,q0,n0) is 10 -element ;

end;

definition

let V, A be set ;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
let d be object ;
let val be FinSequence;

pred valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d means :: NOMIN_9:def 10
Lucas_input (x0,y0,p0,q0,n0) is_valid_input V,A,val,d;

end;

:: deftheorem defines valid_Lucas_input_pred NOMIN_9:def 10 :
for V, A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object
for val being FinSequence holds
( valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d iff Lucas_input (x0,y0,p0,q0,n0) is_valid_input V,A,val,d );

definition

let V, A be set ;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
let val be FinSequence;
defpred S₁[ 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 :: NOMIN_9:def 11
valid_input (V,A,val,(Lucas_input (x0,y0,p0,q0,n0)));

coherence
valid_input (V,A,val,(Lucas_input (x0,y0,p0,q0,n0))) is SCPartialNominativePredicate of V,A ;

end;

:: deftheorem defines valid_Lucas_input NOMIN_9:def 11 :
for V, A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being FinSequence holds valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) = valid_input (V,A,val,(Lucas_input (x0,y0,p0,q0,n0)));

registration

let V, A be set ;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
let val be FinSequence;

cluster valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) -> total ;

coherence
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) is total ;

end;

definition

let V, A be set ;
let z be Element of V;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
let d be object ;

pred valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d means :: NOMIN_9:def 12
<*(Lucas (x0,y0,p0,q0,n0))*> is_valid_output V,A,<*z*>,d;

end;

:: deftheorem defines valid_Lucas_output_pred NOMIN_9:def 12 :
for V, A being set
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object holds
( valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d iff <*(Lucas (x0,y0,p0,q0,n0))*> is_valid_output V,A,<*z*>,d );

definition

let V, A be set ;
let z be Element of V;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;

func valid_Lucas_output (A,z,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V,A equals :: NOMIN_9:def 13
valid_output (V,A,z,(Lucas (x0,y0,p0,q0,n0)));

coherence
valid_output (V,A,z,(Lucas (x0,y0,p0,q0,n0))) is SCPartialNominativePredicate of V,A ;

end;

:: deftheorem defines valid_Lucas_output NOMIN_9:def 13 :
for V, A being set
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat holds valid_Lucas_output (A,z,x0,y0,p0,q0,n0) = valid_output (V,A,z,(Lucas (x0,y0,p0,q0,n0)));

definition

let V, A be set ;
let loc be V -valued Function;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
let d be object ;

pred Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d means :: NOMIN_9:def 14
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;

:: deftheorem defines Lucas_inv_pred NOMIN_9:def 14 :
for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object holds
( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d iff 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)) ) ) );

definition

let V, A be set ;
let loc be V -valued Function;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;
defpred S₁[ 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: :: NOMIN_9:def 15
( 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
ex b₁ being SCPartialNominativePredicate of V,A st
( dom b₁ = ND (V,A) & ( for d being object st d in dom b₁ holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₁ . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₁ . d = FALSE ) ) ) )

proof end;

uniqueness
for b₁, b₂ being SCPartialNominativePredicate of V,A st dom b₁ = ND (V,A) & ( for d being object st d in dom b₁ holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₁ . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₁ . d = FALSE ) ) ) & dom b₂ = ND (V,A) & ( for d being object st d in dom b₂ holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₂ . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₂ . d = FALSE ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Lucas_inv NOMIN_9:def 15 :
for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for b₉ being SCPartialNominativePredicate of V,A holds
( b₉ = Lucas_inv (A,loc,x0,y0,p0,q0,n0) iff ( dom b₉ = ND (V,A) & ( for d being object st d in dom b₉ holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₉ . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₉ . d = FALSE ) ) ) ) );

registration

let V, A be set ;
let loc be V -valued Function;
let x0, y0, p0, q0 be Integer;
let n0 be Nat;

cluster Lucas_inv (A,loc,x0,y0,p0,q0,n0) -> total ;

coherence
Lucas_inv (A,loc,x0,y0,p0,q0,n0) is total by Def15;

end;

theorem Th13: :: NOMIN_9:13

for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))))

proof end;

theorem Th14: :: NOMIN_9:14

for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))

proof end;

theorem Th15: :: NOMIN_9:15

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st not V is 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 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 ) ) holds
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 end;

theorem Th16: :: NOMIN_9:16

for A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₇ -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))

proof end;

theorem Th17: :: NOMIN_9:17

for A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₇ -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_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 end;

theorem Th18: :: NOMIN_9:18

for A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₇ -valued 10 -element FinSequence
for val being 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 & loc,val are_different_wrt 10 holds
<*(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 end;

theorem Th19: :: NOMIN_9:19

for V, A being set
for loc being b₁ -valued Function
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))) ||= SC_Psuperpos ((valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),(denaming (V,A,(loc /. 4))),z)

proof end;

theorem Th20: :: NOMIN_9:20

for V, A being set
for loc being b₁ -valued Function
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))

proof end;

theorem Th21: :: NOMIN_9:21

for V, A being set
for loc being b₁ -valued Function
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(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 end;

:: Partial correctness of a Lucas algorithm

theorem :: NOMIN_9:22

for A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₇ -valued 10 -element FinSequence
for val being 10 -element FinSequence
for z being Element of V 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 /. 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 holds
<*(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 end;