:: Partial correctness of an algorithm computing Lucas sequences
::
:: 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 ;
coherence
[i,j] is Element of
proof end;
end;

definition
let x, y, P, Q be Integer;
deffunc H1( set , Element of ) -> Element of = [($2 2),((P * ($2 2)) - (Q * ($2 1)))]; func Lucas_Sequence (x,y,P,Q) -> sequence of 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 b1 being sequence of st ( b1 . 0 = [x,y] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) 2),((P * ((b1 . n) 2)) - (Q * ((b1 . n) 1)))] ) ) proof end; uniqueness for b1, b2 being sequence of st b1 . 0 = [x,y] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) 2),((P * ((b1 . n) 2)) - (Q * ((b1 . n) 1)))] ) & b2 . 0 = [x,y] & ( for n being Nat holds b2 . (n + 1) = [((b2 . n) 2),((P * ((b2 . n) 2)) - (Q * ((b2 . n) 1)))] ) holds b1 = b2 proof end; end; :: deftheorem Def3 defines Lucas_Sequence NOMIN_9:def 3 : for x, y, P, Q being Integer for b5 being sequence of holds ( b5 = Lucas_Sequence (x,y,P,Q) iff ( b5 . 0 = [x,y] & ( for n being Nat holds b5 . (n + 1) = [((b5 . n) 2),((P * ((b5 . n) 2)) - (Q * ((b5 . 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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 S1[ 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 b1 -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 S1[ 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 b1 being SCPartialNominativePredicate of V,A st
( dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b1 . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b1 . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b2 . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Lucas_inv NOMIN_9:def 15 :
for V, A being set
for loc being b1 -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for b9 being SCPartialNominativePredicate of V,A holds
( b9 = Lucas_inv (A,loc,x0,y0,p0,q0,n0) iff ( dom b9 = ND (V,A) & ( for d being object st d in dom b9 holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b9 . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b9 . 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 b1 -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 b1 -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 b1 -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 b7 -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 b7 -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 b7 -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 b1 -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 b1 -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 b1 -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 b7 -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;