:: Partial Correctness of a Fibonacci Algorithm
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2020-2021 Association of Mizar Users

definition
let R1, R2 be Relation;
pred R1 is_valid_wrt R2 means :Def1: :: NOMIN_7:def 1
rng R1 c= dom R2;
end;

:: deftheorem Def1 defines is_valid_wrt NOMIN_7:def 1 :
for R1, R2 being Relation holds
( R1 is_valid_wrt R2 iff rng R1 c= dom R2 );

definition
let V be set ;
let loc be V -valued Function;
let val be Function;
let N be Nat;
pred loc,val are_different_wrt N means :: NOMIN_7:def 2
for m, n being Nat st 1 <= m & m <= N & 1 <= n & n <= N holds
val . m <> loc /. n;
end;

:: deftheorem defines are_different_wrt NOMIN_7:def 2 :
for V being set
for loc being b1 -valued Function
for val being Function
for N being Nat holds
( loc,val are_different_wrt N iff for m, n being Nat st 1 <= m & m <= N & 1 <= n & n <= N holds
val . m <> loc /. n );

theorem Th1: :: NOMIN_7:1
for N being Nat
for V being set
for loc being b2 -valued Function st loc | (Seg N) is one-to-one & Seg N c= dom loc holds
for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j
proof end;

theorem Th2: :: NOMIN_7:2
for v being object
for V, A being set
for z being Element of V
for d1 being NonatomicND of V,A st not V is empty & v in dom d1 holds
(local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v
proof end;

definition
let D be non empty set ;
let f1, f2, f3, f4, f5, f6 be BinominativeFunction of D;
func PP_composition (f1,f2,f3,f4,f5,f6) -> BinominativeFunction of D equals :: NOMIN_7:def 3
PP_composition ((PP_composition (f1,f2,f3,f4,f5)),f6);
coherence
PP_composition ((PP_composition (f1,f2,f3,f4,f5)),f6) is BinominativeFunction of D
;
end;

:: deftheorem defines PP_composition NOMIN_7:def 3 :
for D being non empty set
for f1, f2, f3, f4, f5, f6 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6) = PP_composition ((PP_composition (f1,f2,f3,f4,f5)),f6);

:: Unconditional composition rule for 6 programs
theorem Th3: :: NOMIN_7:3
for D being non empty set
for f1, f2, f3, f4, f5, f6 being BinominativeFunction of D
for p1, p2, p3, p4, p5, p6, p7 being PartialPredicate of D st <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*(),f2,p3*> is SFHT of D & <*(),f3,p4*> is SFHT of D & <*(),f4,p5*> is SFHT of D & <*(),f5,p6*> is SFHT of D & <*(),f6,p7*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p7*> is SFHT of D
proof end;

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
let d1 be NonatomicND of V,A;
let size be Nat;
assume A1: size > 0 ;
defpred S1[ Nat, object , object ] means $3 = local_overlapping (V,A,$2,((denaming (V,A,(val . ($1 + 1)))) .$2),(loc /. ($1 + 1))); set X = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)); func LocalOverlapSeq (A,loc,val,d1,size) -> FinSequence of ND (V,A) means :Def4: :: NOMIN_7:def 4 ( len it = size & it . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len it holds it . (n + 1) = local_overlapping (V,A,(it . n),((denaming (V,A,(val . (n + 1)))) . (it . n)),(loc /. (n + 1))) ) ); existence ex b1 being FinSequence of ND (V,A) st ( len b1 = size & b1 . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b1 holds b1 . (n + 1) = local_overlapping (V,A,(b1 . n),((denaming (V,A,(val . (n + 1)))) . (b1 . n)),(loc /. (n + 1))) ) ) proof end; uniqueness for b1, b2 being FinSequence of ND (V,A) st len b1 = size & b1 . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b1 holds b1 . (n + 1) = local_overlapping (V,A,(b1 . n),((denaming (V,A,(val . (n + 1)))) . (b1 . n)),(loc /. (n + 1))) ) & len b2 = size & b2 . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b2 holds b2 . (n + 1) = local_overlapping (V,A,(b2 . n),((denaming (V,A,(val . (n + 1)))) . (b2 . n)),(loc /. (n + 1))) ) holds b1 = b2 proof end; end; :: deftheorem Def4 defines LocalOverlapSeq NOMIN_7:def 4 : for V, A being set for loc being b1 -valued Function for val being Function for d1 being NonatomicND of V,A for size being Nat st size > 0 holds for b7 being FinSequence of ND (V,A) holds ( b7 = LocalOverlapSeq (A,loc,val,d1,size) iff ( len b7 = size & b7 . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b7 holds b7 . (n + 1) = local_overlapping (V,A,(b7 . n),((denaming (V,A,(val . (n + 1)))) . (b7 . n)),(loc /. (n + 1))) ) ) ); definition let V, A be set ; let f be Function; attr f is V,A -NonatomicND-yielding means :: NOMIN_7:def 5 for n being object st n in dom f holds f . n is NonatomicND of V,A; end; :: deftheorem defines -NonatomicND-yielding NOMIN_7:def 5 : for V, A being set for f being Function holds ( f is V,A -NonatomicND-yielding iff for n being object st n in dom f holds f . n is NonatomicND of V,A ); definition let V, A be set ; let f be FinSequence; redefine attr f is V,A -NonatomicND-yielding means :Def6: :: NOMIN_7:def 6 for n being Nat st 1 <= n & n <= len f holds f . n is NonatomicND of V,A; compatibility ( f is V,A -NonatomicND-yielding iff for n being Nat st 1 <= n & n <= len f holds f . n is NonatomicND of V,A ) proof end; end; :: deftheorem Def6 defines -NonatomicND-yielding NOMIN_7:def 6 : for V, A being set for f being FinSequence holds ( f is V,A -NonatomicND-yielding iff for n being Nat st 1 <= n & n <= len f holds f . n is NonatomicND of V,A ); registration let V, A be set ; let d1 be NonatomicND of V,A; cluster <*d1*> -> V,A -NonatomicND-yielding ; coherence <*d1*> is V,A -NonatomicND-yielding proof end; end; registration let V, A be set ; existence ex b1 being FinSequence st b1 is V,A -NonatomicND-yielding proof end; end; theorem :: NOMIN_7:4 for n being Nat for V, A being set for f being b2,b3 -NonatomicND-yielding FinSequence st n in dom f holds f . n is NonatomicND of V,A proof end; registration let V, A be set ; let loc be V -valued Function; let val be Function; let d1 be NonatomicND of V,A; let size be non zero Nat; cluster LocalOverlapSeq (A,loc,val,d1,size) -> V,A -NonatomicND-yielding ; coherence LocalOverlapSeq (A,loc,val,d1,size) is V,A -NonatomicND-yielding proof end; end; registration let V, A be set ; let loc be V -valued Function; let val be Function; let d1 be NonatomicND of V,A; let size be non zero Nat; let n be Nat; cluster (LocalOverlapSeq (A,loc,val,d1,size)) . n -> Relation-like Function-like ; coherence ( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like ) proof end; end; theorem Th5: :: NOMIN_7:5 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) proof end; theorem Th6: :: NOMIN_7:6 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) proof end; definition let V, A be set ; let loc be V -valued Function; let val be Function; let d1 be NonatomicND of V,A; let size be non zero Nat; pred loc,val,size are_correct_wrt d1 means :: NOMIN_7:def 7 ( not V is empty & A is_without_nonatomicND_wrt V & val is_valid_wrt d1 & dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val ); end; :: deftheorem defines are_correct_wrt NOMIN_7:def 7 : for V, A being set for loc being b1 -valued Function for val being Function for d1 being NonatomicND of V,A for size being non zero Nat holds ( loc,val,size are_correct_wrt d1 iff ( not V is empty & A is_without_nonatomicND_wrt V & val is_valid_wrt d1 & dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val ) ); theorem Th7: :: NOMIN_7:7 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds for n being Nat st 1 <= n & n <= size holds dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) proof end; theorem Th8: :: NOMIN_7:8 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds for m, n being Nat st 1 <= n & n <= m & m <= size holds dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) proof end; theorem Th9: :: NOMIN_7:9 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds for m, n being Nat st 1 <= n & n <= m & m <= size holds loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) proof end; theorem Th10: :: NOMIN_7:10 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) proof end; theorem Th11: :: NOMIN_7:11 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 & loc,val are_different_wrt size holds for j, m, n being Nat st 1 <= n & n <= m & m < j & j <= size holds ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (val . j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (val . j) proof end; theorem Th12: :: NOMIN_7:12 for size being non zero Nat for V, A being set for val being Function for loc being b2 -valued Function for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j) proof end; theorem Th13: :: NOMIN_7:13 for size being non zero Nat for V, A being set for loc being b2 -valued Function for d1 being NonatomicND of V,A for val being b1 -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds for m, n being Nat st 1 <= n & n <= m & m <= size holds ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n) proof end; theorem Th14: :: NOMIN_7:14 for size being non zero Nat for V, A being set for loc being b2 -valued Function for d1 being NonatomicND of V,A for val being b1 -element FinSequence st loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds for m, n being Nat st 1 <= m & m <= size & 1 <= n & n <= size holds ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (val . n) = d1 . (val . n) proof end; theorem :: NOMIN_7:15 for size being non zero Nat for V, A being set for loc being b2 -valued Function for d1 being NonatomicND of V,A for val being b1 -element FinSequence st loc,val,size are_correct_wrt d1 & Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size holds for j, m, n being Nat st 1 <= j & j < m & m <= n & n <= size holds ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. m) = ((LocalOverlapSeq (A,loc,val,d1,size)) . j) . (val . m) proof end; definition let V, A be set ; let loc be V -valued Function; let val be Function; let size be Nat; assume A1: 0 < size ; set D = PFuncs ((ND (V,A)),(ND (V,A))); reconsider X = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) as Element of PFuncs ((ND (V,A)),(ND (V,A))) by PARTFUN1:45; defpred S1[ Nat, object , object ] means ex f being PartFunc of (ND (V,A)),(ND (V,A)) st ( f =$2 & $3 = PP_composition (f,(SC_assignment ((denaming (V,A,(val . ($1 + 1)))),(loc /. ($1 + 1))))) ); func initial_assignments_Seq (A,loc,val,size) -> FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) means :Def8: :: NOMIN_7:def 8 ( len it = size & it . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds it . (n + 1) = PP_composition ((it . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) ); existence ex b1 being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st ( len b1 = size & b1 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds b1 . (n + 1) = PP_composition ((b1 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) ) proof end; uniqueness for b1, b2 being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st len b1 = size & b1 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds b1 . (n + 1) = PP_composition ((b1 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) & len b2 = size & b2 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds b2 . (n + 1) = PP_composition ((b2 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) holds b1 = b2 proof end; end; :: deftheorem Def8 defines initial_assignments_Seq NOMIN_7:def 8 : for V, A being set for loc being b1 -valued Function for val being Function for size being Nat st 0 < size holds for b6 being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) holds ( b6 = initial_assignments_Seq (A,loc,val,size) iff ( len b6 = size & b6 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds b6 . (n + 1) = PP_composition ((b6 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) ) ); definition let V, A be set ; let loc be V -valued Function; let val be Function; let size be Nat; func initial_assignments (A,loc,val,size) -> SCBinominativeFunction of V,A equals :: NOMIN_7:def 9 (initial_assignments_Seq (A,loc,val,size)) . size; coherence (initial_assignments_Seq (A,loc,val,size)) . size is SCBinominativeFunction of V,A ; end; :: deftheorem defines initial_assignments NOMIN_7:def 9 : for V, A being set for loc being b1 -valued Function for val being Function for size being Nat holds initial_assignments (A,loc,val,size) = (initial_assignments_Seq (A,loc,val,size)) . size; :: Pseudocode of Fibonacci(n) :: :: i := val.1 :: counter :: j := val.2 :: constant 1 :: n := val.3 :: input :: s := val.4 :: result :: b := val.5 :: c := val.6 :: { s == Fibonacci(i) && b == Fibonacci(i+1) } :: while ( i <> n ) :: c := s :: s := b :: b := c + s :: i := i + j :: return s :: { n == i && s == Fibonacci(i) && b == Fibonacci(i+1) } :: :: where :: val.1 = 0, :: val.2 = 1, :: val.3 - the number n the Fibonacci of which we compute, :: val.4 = 0 :: val.5 = 1 :: val.6 = 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 definition let V, A be set ; let loc be V -valued Function; func Fibonacci_loop_body (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_7:def 10 PP_composition ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))),(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(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 ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))),(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1)))) is SCBinominativeFunction of V,A ; end; :: deftheorem defines Fibonacci_loop_body NOMIN_7:def 10 : for V, A being set for loc being b1 -valued Function holds Fibonacci_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 ((addition (A,(loc /. 6),(loc /. 4))),(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 Fibonacci_main_loop (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_7:def 11 PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_loop_body (A,loc))); coherence PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_loop_body (A,loc))) is SCBinominativeFunction of V,A ; end; :: deftheorem defines Fibonacci_main_loop NOMIN_7:def 11 : for V, A being set for loc being b1 -valued Function holds Fibonacci_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_loop_body (A,loc))); definition let V, A be set ; let loc be V -valued Function; let val be Function; func Fibonacci_main_part (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_7:def 12 PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_main_loop (A,loc))); coherence PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_main_loop (A,loc))) is SCBinominativeFunction of V,A ; end; :: deftheorem defines Fibonacci_main_part NOMIN_7:def 12 : for V, A being set for loc being b1 -valued Function for val being Function holds Fibonacci_main_part (A,loc,val) = PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_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 Fibonacci_program (A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_7:def 13 PP_composition ((Fibonacci_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z))); coherence PP_composition ((Fibonacci_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z))) is SCBinominativeFunction of V,A ; end; :: deftheorem defines Fibonacci_program NOMIN_7:def 13 : for V, A being set for loc being b1 -valued Function for val being Function for z being Element of V holds Fibonacci_program (A,loc,val,z) = PP_composition ((Fibonacci_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z))); definition let V, A be set ; let val be Function; let n0 be Nat; let d be object ; pred valid_Fibonacci_input_pred V,A,val,n0,d means :: NOMIN_7:def 14 ex d1 being NonatomicND of V,A st ( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = n0 & d1 . (val . 4) = 0 & d1 . (val . 5) = 1 & d1 . (val . 6) = 0 ); end; :: deftheorem defines valid_Fibonacci_input_pred NOMIN_7:def 14 : for V, A being set for val being Function for n0 being Nat for d being object holds ( valid_Fibonacci_input_pred V,A,val,n0,d iff ex d1 being NonatomicND of V,A st ( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = n0 & d1 . (val . 4) = 0 & d1 . (val . 5) = 1 & d1 . (val . 6) = 0 ) ); definition let V, A be set ; let val be Function; let n0 be Nat; defpred S1[ object ] means valid_Fibonacci_input_pred V,A,val,n0,$1;
func valid_Fibonacci_input (V,A,val,n0) -> SCPartialNominativePredicate of V,A means :Def15: :: NOMIN_7:def 15
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( valid_Fibonacci_input_pred V,A,val,n0,d implies it . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,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
( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b1 . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,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
( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b1 . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b2 . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines valid_Fibonacci_input NOMIN_7:def 15 :
for V, A being set
for val being Function
for n0 being Nat
for b5 being SCPartialNominativePredicate of V,A holds
( b5 = valid_Fibonacci_input (V,A,val,n0) iff ( dom b5 = ND (V,A) & ( for d being object st d in dom b5 holds
( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b5 . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b5 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let val be Function;
let n0 be Nat;
cluster valid_Fibonacci_input (V,A,val,n0) -> total ;
coherence
valid_Fibonacci_input (V,A,val,n0) is total
by Def15;
end;

definition
let V, A be set ;
let z be Element of V;
let n0 be Nat;
let d be object ;
pred valid_Fibonacci_output_pred A,z,n0,d means :: NOMIN_7:def 16
ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = Fib n0 );
end;

:: deftheorem defines valid_Fibonacci_output_pred NOMIN_7:def 16 :
for V, A being set
for z being Element of V
for n0 being Nat
for d being object holds
( valid_Fibonacci_output_pred A,z,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = Fib n0 ) );

definition
let V, A be set ;
let z be Element of V;
let n0 be Nat;
set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ;
defpred S1[ object ] means valid_Fibonacci_output_pred A,z,n0,$1; func valid_Fibonacci_output (A,z,n0) -> SCPartialNominativePredicate of V,A means :Def17: :: NOMIN_7:def 17 ( dom it = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom it holds ( ( valid_Fibonacci_output_pred A,z,n0,d implies it . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies it . d = FALSE ) ) ) ); existence ex b1 being SCPartialNominativePredicate of V,A st ( dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds ( ( valid_Fibonacci_output_pred A,z,n0,d implies b1 . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b1 . d = FALSE ) ) ) ) proof end; uniqueness for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds ( ( valid_Fibonacci_output_pred A,z,n0,d implies b1 . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b2 holds ( ( valid_Fibonacci_output_pred A,z,n0,d implies b2 . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b2 . d = FALSE ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def17 defines valid_Fibonacci_output NOMIN_7:def 17 : for V, A being set for z being Element of V for n0 being Nat for b5 being SCPartialNominativePredicate of V,A holds ( b5 = valid_Fibonacci_output (A,z,n0) iff ( dom b5 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b5 holds ( ( valid_Fibonacci_output_pred A,z,n0,d implies b5 . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b5 . d = FALSE ) ) ) ) ); definition let V, A be set ; let loc be V -valued Function; let n0 be Nat; let d be object ; pred Fibonacci_inv_pred A,loc,n0,d means :: NOMIN_7:def 18 ex d1 being NonatomicND of V,A st ( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & ex I being Nat st ( I = d1 . (loc /. 1) & d1 . (loc /. 4) = Fib I & d1 . (loc /. 5) = Fib (I + 1) ) ); end; :: deftheorem defines Fibonacci_inv_pred NOMIN_7:def 18 : for V, A being set for loc being b1 -valued Function for n0 being Nat for d being object holds ( Fibonacci_inv_pred A,loc,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)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & ex I being Nat st ( I = d1 . (loc /. 1) & d1 . (loc /. 4) = Fib I & d1 . (loc /. 5) = Fib (I + 1) ) ) ); definition let V, A be set ; let loc be V -valued Function; let n0 be Nat; defpred S1[ object ] means Fibonacci_inv_pred A,loc,n0,$1;
func Fibonacci_inv (A,loc,n0) -> SCPartialNominativePredicate of V,A means :Def19: :: NOMIN_7:def 19
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( Fibonacci_inv_pred A,loc,n0,d implies it . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,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
( ( Fibonacci_inv_pred A,loc,n0,d implies b1 . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,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
( ( Fibonacci_inv_pred A,loc,n0,d implies b1 . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( Fibonacci_inv_pred A,loc,n0,d implies b2 . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Fibonacci_inv NOMIN_7:def 19 :
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for b5 being SCPartialNominativePredicate of V,A holds
( b5 = Fibonacci_inv (A,loc,n0) iff ( dom b5 = ND (V,A) & ( for d being object st d in dom b5 holds
( ( Fibonacci_inv_pred A,loc,n0,d implies b5 . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b5 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
cluster Fibonacci_inv (A,loc,n0) -> total ;
coherence
Fibonacci_inv (A,loc,n0) is total
by Def19;
end;

theorem Th16: :: NOMIN_7:16
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for val being 6 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
proof end;

theorem Th17: :: NOMIN_7:17
for V, A being set
for loc being b1 -valued Function
for n0 being Nat st not V is empty & 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
proof end;

theorem Th18: :: NOMIN_7:18
for V, A being set
for loc being b1 -valued Function
for n0 being Nat st not V is empty & 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
proof end;

theorem Th19: :: NOMIN_7:19
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for val being 6 -element FinSequence st not V is empty & 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
proof end;

theorem Th20: :: NOMIN_7:20
for V, A being set
for z being Element of V
for loc being b1 -valued Function
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))),(Fibonacci_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_Fibonacci_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)
proof end;

theorem Th21: :: NOMIN_7:21
for V, A being set
for z being Element of V
for loc being b1 -valued Function
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))),(Fibonacci_inv (A,loc,n0)))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
proof end;

theorem Th22: :: NOMIN_7:22
for V, A being set
for z being Element of V
for loc being b1 -valued Function
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))),(Fibonacci_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
proof end;

:: Partial correctness of a Fibonacci algorithm
theorem :: NOMIN_7:23
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat
for val being 6 -element FinSequence st not V is empty & 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(Fibonacci_program (A,loc,val,z)),(valid_Fibonacci_output (A,z,n0))*> is SFHT of (ND (V,A))
proof end;