:: by Artur Korni{\l}owicz

::

:: Received May 31, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

definition
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 );

for R1, R2 being Relation holds

( R1 is_valid_wrt R2 iff rng R1 c= dom R2 );

:: deftheorem defines are_different_wrt NOMIN_7:def 2 :

for V being set

for loc being b_{1} -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 );

for V being set

for loc being b

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 b_{2} -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

for V being set

for loc being b

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

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;

PP_composition ((PP_composition (f1,f2,f3,f4,f5)),f6) is BinominativeFunction of D ;

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

PP_composition ((PP_composition (f1,f2,f3,f4,f5)),f6) is BinominativeFunction of D ;

:: 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);

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 & <*(PP_inversion p2),f2,p3*> is SFHT of D & <*(PP_inversion p3),f3,p4*> is SFHT of D & <*(PP_inversion p4),f4,p5*> is SFHT of D & <*(PP_inversion p5),f5,p6*> is SFHT of D & <*(PP_inversion p6),f6,p7*> is SFHT of D holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p7*> is SFHT of D

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 & <*(PP_inversion p2),f2,p3*> is SFHT of D & <*(PP_inversion p3),f3,p4*> is SFHT of D & <*(PP_inversion p4),f4,p5*> is SFHT of D & <*(PP_inversion p5),f5,p6*> is SFHT of D & <*(PP_inversion p6),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 S_{1}[ 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));

ex b_{1} being FinSequence of ND (V,A) st

( len b_{1} = size & b_{1} . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = local_overlapping (V,A,(b_{1} . n),((denaming (V,A,(val . (n + 1)))) . (b_{1} . n)),(loc /. (n + 1))) ) )

for b_{1}, b_{2} being FinSequence of ND (V,A) st len b_{1} = size & b_{1} . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = local_overlapping (V,A,(b_{1} . n),((denaming (V,A,(val . (n + 1)))) . (b_{1} . n)),(loc /. (n + 1))) ) & len b_{2} = size & b_{2} . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b_{2} holds

b_{2} . (n + 1) = local_overlapping (V,A,(b_{2} . n),((denaming (V,A,(val . (n + 1)))) . (b_{2} . n)),(loc /. (n + 1))) ) holds

b_{1} = b_{2}

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

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 ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines LocalOverlapSeq NOMIN_7:def 4 :

for V, A being set

for loc being b_{1} -valued Function

for val being Function

for d1 being NonatomicND of V,A

for size being Nat st size > 0 holds

for b_{7} being FinSequence of ND (V,A) holds

( b_{7} = LocalOverlapSeq (A,loc,val,d1,size) iff ( len b_{7} = size & b_{7} . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b_{7} holds

b_{7} . (n + 1) = local_overlapping (V,A,(b_{7} . n),((denaming (V,A,(val . (n + 1)))) . (b_{7} . n)),(loc /. (n + 1))) ) ) );

for V, A being set

for loc being b

for val being Function

for d1 being NonatomicND of V,A

for size being Nat st size > 0 holds

for b

( b

b

definition

let V, A be set ;

let f be Function;

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

for n being object st n in dom f holds

f . n is NonatomicND of V,A;

:: 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 );

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;

( 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 )

end;
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 for n being Nat st 1 <= n & n <= len f holds

f . n is NonatomicND of V,A;

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

:: 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 );

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;

coherence

<*d1*> is V,A -NonatomicND-yielding

end;
let d1 be NonatomicND of V,A;

coherence

<*d1*> is V,A -NonatomicND-yielding

proof end;

registration

let V, A be set ;

ex b_{1} being FinSequence st b_{1} is V,A -NonatomicND-yielding

end;
cluster Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V,A -NonatomicND-yielding for set ;

existence ex b

proof end;

theorem :: NOMIN_7:4

for n being Nat

for V, A being set

for f being b_{2},b_{3} -NonatomicND-yielding FinSequence st n in dom f holds

f . n is NonatomicND of V,A

for V, A being set

for f being b

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;

coherence

LocalOverlapSeq (A,loc,val,d1,size) is V,A -NonatomicND-yielding

end;
let loc be V -valued Function;

let val be Function;

let d1 be NonatomicND of V,A;

let size be non zero Nat;

coherence

LocalOverlapSeq (A,loc,val,d1,size) is V,A -NonatomicND-yielding

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;

let n be Nat;

coherence

( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like )

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

coherence

( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like )

proof end;

theorem Th5: :: NOMIN_7:5

for size being non zero Nat

for V, A being set

for val being Function

for loc being b_{2} -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))

for V, A being set

for val being Function

for loc being b

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 b_{2} -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))

for V, A being set

for val being Function

for loc being b

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;

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

( 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 );

:: deftheorem defines are_correct_wrt NOMIN_7:def 7 :

for V, A being set

for loc being b_{1} -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 ) );

for V, A being set

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -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)

for V, A being set

for val being Function

for loc being b

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 b_{2} -valued Function

for d1 being NonatomicND of V,A

for val being b_{1} -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)

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for val being b

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 b_{2} -valued Function

for d1 being NonatomicND of V,A

for val being b_{1} -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)

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for val being b

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 b_{2} -valued Function

for d1 being NonatomicND of V,A

for val being b_{1} -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)

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for val being b

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 S_{1}[ 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))))) );

ex b_{1} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st

( len b_{1} = size & b_{1} . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds

b_{1} . (n + 1) = PP_composition ((b_{1} . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) )

for b_{1}, b_{2} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st len b_{1} = size & b_{1} . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds

b_{1} . (n + 1) = PP_composition ((b_{1} . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) & len b_{2} = size & b_{2} . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds

b_{2} . (n + 1) = PP_composition ((b_{2} . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) holds

b_{1} = b_{2}

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

( 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 ( 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))))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines initial_assignments_Seq NOMIN_7:def 8 :

for V, A being set

for loc being b_{1} -valued Function

for val being Function

for size being Nat st 0 < size holds

for b_{6} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) holds

( b_{6} = initial_assignments_Seq (A,loc,val,size) iff ( len b_{6} = size & b_{6} . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds

b_{6} . (n + 1) = PP_composition ((b_{6} . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) ) );

for V, A being set

for loc being b

for val being Function

for size being Nat st 0 < size holds

for b

( b

b

definition

let V, A be set ;

let loc be V -valued Function;

let val be Function;

let size be Nat;

(initial_assignments_Seq (A,loc,val,size)) . size is SCBinominativeFunction of V,A ;

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

(initial_assignments_Seq (A,loc,val,size)) . size is SCBinominativeFunction of V,A ;

:: deftheorem defines initial_assignments NOMIN_7:def 9 :

for V, A being set

for loc being b_{1} -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;

for V, A being set

for loc being b

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

::

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

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

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 ;

:: deftheorem defines Fibonacci_loop_body NOMIN_7:def 10 :

for V, A being set

for loc being b_{1} -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))));

for V, A being set

for loc being b

definition

let V, A be set ;

let loc be V -valued Function;

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

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

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

:: deftheorem defines Fibonacci_main_loop NOMIN_7:def 11 :

for V, A being set

for loc being b_{1} -valued Function holds Fibonacci_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_loop_body (A,loc)));

for V, A being set

for loc being b

definition

let V, A be set ;

let loc be V -valued Function;

let val be Function;

PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

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

PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

:: deftheorem defines Fibonacci_main_part NOMIN_7:def 12 :

for V, A being set

for loc being b_{1} -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)));

for V, A being set

for loc being b

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;

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

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

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

:: deftheorem defines Fibonacci_program NOMIN_7:def 13 :

for V, A being set

for loc being b_{1} -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)));

for V, A being set

for loc being b

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 ;

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

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

:: 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 ) );

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 S_{1}[ object ] means valid_Fibonacci_input_pred V,A,val,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b_{1} . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b_{1} . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b_{2} . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let val be Function;

let n0 be Nat;

defpred S

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 ( 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 ) ) ) );

ex b

( dom b

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b

proof end;

uniqueness for b

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b

b

proof 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 b_{5} being SCPartialNominativePredicate of V,A holds

( b_{5} = valid_Fibonacci_input (V,A,val,n0) iff ( dom b_{5} = ND (V,A) & ( for d being object st d in dom b_{5} holds

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b_{5} . d = TRUE ) & ( not valid_Fibonacci_input_pred V,A,val,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for val being Function

for n0 being Nat

for b

( b

( ( valid_Fibonacci_input_pred V,A,val,n0,d implies b

registration

let V, A be set ;

let val be Function;

let n0 be Nat;

coherence

valid_Fibonacci_input (V,A,val,n0) is total by Def15;

end;
let val be Function;

let n0 be Nat;

coherence

valid_Fibonacci_input (V,A,val,n0) is total by Def15;

definition

let V, A be set ;

let z be Element of V;

let n0 be Nat;

let d be object ;

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

ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = Fib n0 );

:: 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 ) );

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 S_{1}[ object ] means valid_Fibonacci_output_pred A,z,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_Fibonacci_output_pred A,z,n0,d implies b_{1} . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_Fibonacci_output_pred A,z,n0,d implies b_{1} . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{2} holds

( ( valid_Fibonacci_output_pred A,z,n0,d implies b_{2} . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

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

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 ( 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 ) ) ) );

ex b

( dom b

( ( valid_Fibonacci_output_pred A,z,n0,d implies b

proof end;

uniqueness for b

( ( valid_Fibonacci_output_pred A,z,n0,d implies b

( ( valid_Fibonacci_output_pred A,z,n0,d implies b

b

proof 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 b_{5} being SCPartialNominativePredicate of V,A holds

( b_{5} = valid_Fibonacci_output (A,z,n0) iff ( dom b_{5} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{5} holds

( ( valid_Fibonacci_output_pred A,z,n0,d implies b_{5} . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for z being Element of V

for n0 being Nat

for b

( b

( ( valid_Fibonacci_output_pred A,z,n0,d implies b

definition

let V, A be set ;

let loc be V -valued Function;

let n0 be Nat;

let d be object ;

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

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

:: deftheorem defines Fibonacci_inv_pred NOMIN_7:def 18 :

for V, A being set

for loc being b_{1} -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) ) ) );

for V, A being set

for loc being b

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 S_{1}[ object ] means Fibonacci_inv_pred A,loc,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( Fibonacci_inv_pred A,loc,n0,d implies b_{1} . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( Fibonacci_inv_pred A,loc,n0,d implies b_{1} . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( Fibonacci_inv_pred A,loc,n0,d implies b_{2} . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let loc be V -valued Function;

let n0 be Nat;

defpred S

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 ( 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 ) ) ) );

ex b

( dom b

( ( Fibonacci_inv_pred A,loc,n0,d implies b

proof end;

uniqueness for b

( ( Fibonacci_inv_pred A,loc,n0,d implies b

( ( Fibonacci_inv_pred A,loc,n0,d implies b

b

proof end;

:: deftheorem Def19 defines Fibonacci_inv NOMIN_7:def 19 :

for V, A being set

for loc being b_{1} -valued Function

for n0 being Nat

for b_{5} being SCPartialNominativePredicate of V,A holds

( b_{5} = Fibonacci_inv (A,loc,n0) iff ( dom b_{5} = ND (V,A) & ( for d being object st d in dom b_{5} holds

( ( Fibonacci_inv_pred A,loc,n0,d implies b_{5} . d = TRUE ) & ( not Fibonacci_inv_pred A,loc,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for loc being b

for n0 being Nat

for b

( b

( ( Fibonacci_inv_pred A,loc,n0,d implies b

registration

let V, A be set ;

let loc be V -valued Function;

let n0 be Nat;

coherence

Fibonacci_inv (A,loc,n0) is total by Def19;

end;
let loc be V -valued Function;

let n0 be Nat;

coherence

Fibonacci_inv (A,loc,n0) is total by Def19;

theorem Th16: :: NOMIN_7:16

for V, A being set

for loc being b_{1} -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))

for loc being b

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 b_{1} -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))

for loc being b

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 b_{1} -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))

for loc being b

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 b_{1} -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))

for loc being b

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 b_{1} -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)

for z being Element of V

for loc being b

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 b_{1} -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))

for z being Element of V

for loc being b

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 b_{1} -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))

for z being Element of V

for loc being b

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;

theorem :: NOMIN_7:23

for V, A being set

for z being Element of V

for loc being b_{1} -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))

for z being Element of V

for loc being b

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;