:: Formal Verification of a Generic Iterative Algorithm
:: by Artur Korni{\l}owicz
::
:: Received July 20, 2026
:: Copyright (c) 2026 Association of Mizar Users

Lm1: 2 in {0,1,2,3,4,5}
by ENUMSET1:def 4;

Lm2: 0 in {0}
by TARSKI:def 1;

registration

let a, b, c, x, y, z be object ;

cluster (a,b,c) --> (x,y,z) -> finite ;

coherence
(a,b,c) --> (x,y,z) is finite ;

end;

theorem Th1: :: AMI_8:1

for x1, x2, x3, x4 being object holds dom <%x1,x2,x3,x4%> = {0,1,2,3}

proof end;

theorem :: AMI_8:2

for x1, x2, x3, x4 being object holds len <%x1,x2,x3,x4%> = 4 by Th1, CARD_1:52;

theorem Th3: :: AMI_8:3

for f, g being Function
for w, x, y, z being object st dom f = dom g & f . w = g . w & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {w,x,y,z} = g | {w,x,y,z}

proof end;

definition

let x1, x2, x3, x4, x5 be object ;

func <%x1,x2,x3,x4,x5%> -> set equals :: AMI_8:def 1
<%x1,x2,x3,x4%> ^ <%x5%>;

coherence
<%x1,x2,x3,x4%> ^ <%x5%> is set ;

end;

:: deftheorem defines <% AMI_8:def 1 :
for x1, x2, x3, x4, x5 being object holds <%x1,x2,x3,x4,x5%> = <%x1,x2,x3,x4%> ^ <%x5%>;

registration

let x1, x2, x3, x4, x5 be object ;

cluster <%x1,x2,x3,x4,x5%> -> Relation-like Function-like ;

coherence
( <%x1,x2,x3,x4,x5%> is Function-like & <%x1,x2,x3,x4,x5%> is Relation-like ) ;

end;

registration

let x1, x2, x3, x4, x5 be object ;

cluster <%x1,x2,x3,x4,x5%> -> Sequence-like finite ;

coherence
( <%x1,x2,x3,x4,x5%> is finite & <%x1,x2,x3,x4,x5%> is Sequence-like ) ;

end;

theorem Th4: :: AMI_8:4

for x1, x2, x3, x4, x5 being object holds dom <%x1,x2,x3,x4,x5%> = {0,1,2,3,4}

proof end;

theorem :: AMI_8:5

for x1, x2, x3, x4, x5 being object holds len <%x1,x2,x3,x4,x5%> = 5 by Th4, CARD_1:53;

registration

let x1, x2, x3, x4, x5 be object ;
A1: dom <%x1,x2,x3,x4%> = {0,1,2,3} by Th1;

reduce <%x1,x2,x3,x4,x5%> . 0 to x1;

reducibility
<%x1,x2,x3,x4,x5%> . 0 = x1

proof end;

reduce <%x1,x2,x3,x4,x5%> . 1 to x2;

reducibility
<%x1,x2,x3,x4,x5%> . 1 = x2

proof end;

reduce <%x1,x2,x3,x4,x5%> . 2 to x3;

reducibility
<%x1,x2,x3,x4,x5%> . 2 = x3

proof end;

reduce <%x1,x2,x3,x4,x5%> . 3 to x4;

reducibility
<%x1,x2,x3,x4,x5%> . 3 = x4

proof end;

reduce <%x1,x2,x3,x4,x5%> . 4 to x5;

reducibility
<%x1,x2,x3,x4,x5%> . 4 = x5

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6 be object ;

func <%x1,x2,x3,x4,x5,x6%> -> set equals :: AMI_8:def 2
<%x1,x2,x3,x4,x5%> ^ <%x6%>;

coherence
<%x1,x2,x3,x4,x5%> ^ <%x6%> is set ;

end;

:: deftheorem defines <% AMI_8:def 2 :
for x1, x2, x3, x4, x5, x6 being object holds <%x1,x2,x3,x4,x5,x6%> = <%x1,x2,x3,x4,x5%> ^ <%x6%>;

registration

let x1, x2, x3, x4, x5, x6 be object ;

cluster <%x1,x2,x3,x4,x5,x6%> -> Relation-like Function-like ;

coherence
( <%x1,x2,x3,x4,x5,x6%> is Function-like & <%x1,x2,x3,x4,x5,x6%> is Relation-like ) ;

end;

registration

let x1, x2, x3, x4, x5, x6 be object ;

cluster <%x1,x2,x3,x4,x5,x6%> -> Sequence-like finite ;

coherence
( <%x1,x2,x3,x4,x5,x6%> is finite & <%x1,x2,x3,x4,x5,x6%> is Sequence-like ) ;

end;

theorem Th6: :: AMI_8:6

for x1, x2, x3, x4, x5, x6 being object holds dom <%x1,x2,x3,x4,x5,x6%> = {0,1,2,3,4,5}

proof end;

theorem :: AMI_8:7

for x1, x2, x3, x4, x5, x6 being object holds len <%x1,x2,x3,x4,x5,x6%> = 6 by Th6, CARD_1:54;

registration

let x1, x2, x3, x4, x5, x6 be object ;
A1: dom <%x1,x2,x3,x4,x5%> = {0,1,2,3,4} by Th4;

reduce <%x1,x2,x3,x4,x5,x6%> . 0 to x1;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 0 = x1

proof end;

reduce <%x1,x2,x3,x4,x5,x6%> . 1 to x2;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 1 = x2

proof end;

reduce <%x1,x2,x3,x4,x5,x6%> . 2 to x3;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 2 = x3

proof end;

reduce <%x1,x2,x3,x4,x5,x6%> . 3 to x4;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 3 = x4

proof end;

reduce <%x1,x2,x3,x4,x5,x6%> . 4 to x5;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 4 = x5

proof end;

reduce <%x1,x2,x3,x4,x5,x6%> . 5 to x6;

reducibility
<%x1,x2,x3,x4,x5,x6%> . 5 = x6

proof end;

end;

theorem Th8: :: AMI_8:8

for x1, x2, x3, x4, x5, x6 being object
for f being Function st <%x1,x2,x3,x4,x5,x6%> c= f holds
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 )

proof end;

set a = dl. 0;

set b = dl. 1;

set c = dl. 2;

theorem :: AMI_8:9

for i being Integer
for d being Data-Location holds i in (the_Values_of SCM) . d

proof end;

registration

let la be Data-Location;
let a be Integer;

cluster la .--> a -> the_Values_of SCM -compatible ;

coherence
la .--> a is the_Values_of SCM -compatible ;

end;

registration

let la, lb be Data-Location;
let a, b be Integer;

cluster (la,lb) --> (a,b) -> the_Values_of SCM -compatible ;

coherence
(la,lb) --> (a,b) is the_Values_of SCM -compatible ;

end;

registration

let la, lb, lc be Data-Location;
let a, b, c be Integer;

cluster (la,lb,lc) --> (a,b,c) -> the_Values_of SCM -compatible ;

coherence
(la,lb,lc) --> (a,b,c) is the_Values_of SCM -compatible ;

end;

registration

let d be Data-Location;
let i be Integer;

cluster d .--> i -> data-only for PartState of SCM;

coherence
for b₁ being PartState of SCM st b₁ = d .--> i holds
b₁ is data-only by ZFMISC_1:11, AMI_5:2;

end;

registration

let p, q be data-only FinPartState of SCM;

cluster p +* q -> data-only ;

coherence
p +* q is data-only

proof end;

end;

registration

let la, lb be Data-Location;
let a, b be Integer;

cluster (la,lb) --> (a,b) -> data-only for FinPartState of SCM;

coherence
for b₁ being FinPartState of SCM st b₁ = (la,lb) --> (a,b) holds
b₁ is data-only ;

end;

registration

let la, lb, lc be Data-Location;
let a, b, c be Integer;

cluster (la,lb,lc) --> (a,b,c) -> data-only for FinPartState of SCM;

coherence
for b₁ being FinPartState of SCM st b₁ = (la,lb,lc) --> (a,b,c) holds
b₁ is data-only ;

end;

definition

let n be Nat;
let I be Instruction of SCM;

attr I is n -dl.constant means :: AMI_8:def 3
for P being Instruction-Sequence of SCM
for s being State of SCM
for k being Nat st CurInstr (P,(Comput (P,s,k))) = I holds
(Comput (P,s,(k + 1))) . (dl. n) = (Comput (P,s,k)) . (dl. n);

end;

:: deftheorem defines -dl.constant AMI_8:def 3 :
for n being Nat
for I being Instruction of SCM holds
( I is n -dl.constant iff for P being Instruction-Sequence of SCM
for s being State of SCM
for k being Nat st CurInstr (P,(Comput (P,s,k))) = I holds
(Comput (P,s,(k + 1))) . (dl. n) = (Comput (P,s,k)) . (dl. n) );

theorem Th10: :: AMI_8:10

for j, m, n being Nat st m <> j holds
AddTo ((dl. m),(dl. n)) is j -dl.constant

proof end;

theorem Th11: :: AMI_8:11

for j, m, n being Nat st m <> j holds
SubFrom ((dl. m),(dl. n)) is j -dl.constant

proof end;

theorem Th12: :: AMI_8:12

for j, m, n being Nat st m <> j holds
MultBy ((dl. m),(dl. n)) is j -dl.constant

proof end;

registration

let m be Nat;
let n be non zero Nat;

cluster AddTo ((dl. (m + n)),(dl. m)) -> m -dl.constant ;

coherence
AddTo ((dl. (m + n)),(dl. m)) is m -dl.constant

proof end;

cluster SubFrom ((dl. (m + n)),(dl. m)) -> m -dl.constant ;

coherence
SubFrom ((dl. (m + n)),(dl. m)) is m -dl.constant

proof end;

cluster MultBy ((dl. (m + n)),(dl. m)) -> m -dl.constant ;

coherence
MultBy ((dl. (m + n)),(dl. m)) is m -dl.constant

proof end;

end;

registration

cluster AddTo ((dl. 2),(dl. 1)) -> 0 -dl.constant ;

coherence
AddTo ((dl. 2),(dl. 1)) is 0 -dl.constant by Th10;

cluster SubFrom ((dl. 2),(dl. 1)) -> 0 -dl.constant ;

coherence
SubFrom ((dl. 2),(dl. 1)) is 0 -dl.constant by Th11;

cluster MultBy ((dl. 2),(dl. 1)) -> 0 -dl.constant ;

coherence
MultBy ((dl. 2),(dl. 1)) is 0 -dl.constant by Th12;

end;

registration

let n be Nat;

cluster sequential n -dl.constant for Element of the InstructionsF of SCM;

existence
ex b₁ being Instruction of SCM st
( b₁ is sequential & b₁ is n -dl.constant )

proof end;

end;

theorem Th13: :: AMI_8:13

for n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM
for I being sequential Instruction of SCM st CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P holds
IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1

proof end;

theorem Th14: :: AMI_8:14

for n being Nat
for i1, i2, i3 being Integer
for s being b₁ -started State-consisting of <%i1,i2,i3%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 )

proof end;

registration

let X be XFinSequence of the InstructionsF of SCM;

cluster non empty Relation-like omega -defined the InstructionsF of SCM -valued Function-like total X -extending for set ;

existence
ex b₁ being Instruction-Sequence of SCM st b₁ is X -extending

proof end;

end;

set SA = Start-At (0,SCM);

theorem Th15: :: AMI_8:15

for i1, i2, i3 being Integer
for s being State of SCM st Initialize (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= s holds
s is State-consisting of <%i1,i2,i3%>

proof end;

:: dl.0 - a, dl.1 - b, dl.2 - c
:: a := 1 - for step
:: b - input
:: c - output
:: 0) if b > 0 then goto 2
:: 1) halt
:: 2) I (e.g., c := c+b or c := c*b)
:: 3) b := b-a
:: 4) if b = 0 then goto 1
:: 5) goto 2

definition

let OPER be Instruction of SCM;

func IterativeAlgorithm OPER -> XFinSequence of the InstructionsF of SCM equals :: AMI_8:def 4
<%((dl. 1) >0_goto 2),(halt SCM),OPER,(SubFrom ((dl. 1),(dl. 0))),((dl. 1) =0_goto 1),(SCM-goto 2)%>;

coherence
<%((dl. 1) >0_goto 2),(halt SCM),OPER,(SubFrom ((dl. 1),(dl. 0))),((dl. 1) =0_goto 1),(SCM-goto 2)%> is XFinSequence of the InstructionsF of SCM ;

end;

:: deftheorem defines IterativeAlgorithm AMI_8:def 4 :
for OPER being Instruction of SCM holds IterativeAlgorithm OPER = <%((dl. 1) >0_goto 2),(halt SCM),OPER,(SubFrom ((dl. 1),(dl. 0))),((dl. 1) =0_goto 1),(SCM-goto 2)%>;

theorem Th16: :: AMI_8:16

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 2 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th17: :: AMI_8:17

for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
P halts_at 1

proof end;

theorem Th18: :: AMI_8:18

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k, j being Nat st IC (Comput (P,s,k)) = 1 holds
Comput (P,s,(k + j)) = Comput (P,s,k)

proof end;

theorem Th19: :: AMI_8:19

for m, n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm (AddTo ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) + ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th20: :: AMI_8:20

for m, n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm (SubFrom ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) - ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th21: :: AMI_8:21

for m, n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. m),(dl. n))) c= P holds
for k being Nat st IC (Comput (P,s,k)) = 2 holds
( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. m) = ((Comput (P,s,k)) . (dl. m)) * ((Comput (P,s,k)) . (dl. n)) & ( for j being Nat st j <> m holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th22: :: AMI_8:22

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 3 holds
( IC (Comput (P,s,(k + 1))) = 4 & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 1)) - ((Comput (P,s,k)) . (dl. 0)) & ( for j being Nat st j <> 1 holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th23: :: AMI_8:23

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 4 holds
( ( (Comput (P,s,k)) . (dl. 1) = 0 implies IC (Comput (P,s,(k + 1))) = 1 ) & ( (Comput (P,s,k)) . (dl. 1) <> 0 implies IC (Comput (P,s,(k + 1))) = 5 ) & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

theorem Th24: :: AMI_8:24

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 5 holds
( IC (Comput (P,s,(k + 1))) = 2 & ( for j being Nat holds (Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )

proof end;

registration

let I be Instruction of SCM;

cluster IterativeAlgorithm I -> ;

coherence
IterativeAlgorithm I is the InstructionsF of SCM -valued ;

end;

registration

let I be Instruction of SCM;

cluster IterativeAlgorithm I -> non halt-free ;

coherence
not IterativeAlgorithm I is halt-free

proof end;

end;

theorem Th25: :: AMI_8:25

for k being Nat
for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st I is sequential & IterativeAlgorithm I c= P & IC (Comput (P,s,0)) = 0 holds
IC (Comput (P,s,k)) in {0,1,2,3,4,5}

proof end;

theorem Th26: :: AMI_8:26

for k being Nat
for i, i1, i2 being Integer
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st I is sequential & I is 0 -dl.constant & IterativeAlgorithm I c= P holds
for s being 0 -started State-consisting of <%i,i1,i2%> holds (Comput (P,s,k)) . (dl. 0) = i

proof end;

theorem Th27: :: AMI_8:27

for i1, i2 being Integer
for I being Instruction of SCM st I is sequential & I is 0 -dl.constant holds
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for s being 0 -started State-consisting of <%i1,0,i2%> holds
( IC (Comput (P,s,0)) = 0 & ( for k being Nat st k >= 1 holds
IC (Comput (P,s,k)) = 1 ) & ( for k being Nat holds
( (Comput (P,s,k)) . (dl. 0) = i1 & (Comput (P,s,k)) . (dl. 1) = 0 & (Comput (P,s,k)) . (dl. 2) = i2 ) ) & LifeSpan (P,s) = 1 )

proof end;

theorem :: AMI_8:28

for I being Instruction of SCM
for A being Integer
for N being Nat
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P & I is sequential & I is 0 -dl.constant holds
for s being 0 -started State-consisting of <%1,N,A%> st (Comput (P,s,2)) . (dl. 1) = (Comput (P,s,1)) . (dl. 1) & ( for k being Nat holds (Comput (P,s,((4 * k) + 6))) . (dl. 1) = (Comput (P,s,((4 * k) + 5))) . (dl. 1) ) holds
( P halts_on s & IC (Comput (P,s,0)) = 0 & (Comput (P,s,1)) . (dl. 2) = A & ( for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 ) & ( for k being Nat st k < N holds
( IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 ) ) & ( N <> 0 implies ( LifeSpan (P,s) = 4 * N & ( for k, j being Nat st k >= N holds
( IC (Comput (P,s,((4 * k) + j))) = 1 & (Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) ) ) ) )

proof end;

theorem Th29: :: AMI_8:29

for I being Instruction of SCM
for A being Integer
for N being Nat
for P being Instruction-Sequence of SCM st ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) & IterativeAlgorithm I c= P holds
for s being 0 -started State-consisting of <%1,N,A%> holds
( P halts_on s & (Comput (P,s,1)) . (dl. 2) = A & ( for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 ) & ( for k being Nat st k < N holds
( IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 ) ) & ( N <> 0 implies ( LifeSpan (P,s) = 4 * N & ( for k, j being Nat st k >= N holds
( IC (Comput (P,s,((4 * k) + j))) = 1 & (Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) ) ) ) )

proof end;

now :: thesis: for A being Integer
for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,0,A%> holds verum

let A be Integer; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,0,A%> holds verum
set N = 0 ;
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P implies for s being 0 -started State-consisting of <%1,0,A%> holds verum )
assume A1: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P ; :: thesis: for s being 0 -started State-consisting of <%1,0,A%> holds verum
let s be 0 -started State-consisting of <%1,0,A%>; :: thesis: verum
IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
IC (Comput (P,s,1)) = 1 by A1, Th27;
IC (Comput (P,s,2)) = 1 by A1, Th27;
IC (Comput (P,s,3)) = 1 by A1, Th27;
IC (Comput (P,s,4)) = 1 by A1, Th27;
IC (Comput (P,s,5)) = 1 by A1, Th27;
for x being Nat holds (Comput (P,s,x)) . (dl. 0) = 1 by A1, Th26;
(Comput (P,s,0)) . (dl. 1) = 0 by Th14;
(Comput (P,s,1)) . (dl. 1) = 0 by A1, Th27;
(Comput (P,s,2)) . (dl. 1) = 0 by A1, Th27;
(Comput (P,s,3)) . (dl. 1) = 0 by A1, Th27;
(Comput (P,s,4)) . (dl. 1) = 0 by A1, Th27;
(Comput (P,s,5)) . (dl. 1) = 0 by A1, Th27;
(Comput (P,s,100)) . (dl. 1) = 0 by A1, Th27;

end;

now :: thesis: for A being Integer
for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,1,A%> holds verum

let A be Integer; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,1,A%> holds verum
set N = 1;
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P implies for s being 0 -started State-consisting of <%1,1,A%> holds verum )
assume A1: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P ; :: thesis: for s being 0 -started State-consisting of <%1,1,A%> holds verum
let s be 0 -started State-consisting of <%1,1,A%>; :: thesis: verum
IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
IC (Comput (P,s,((4 * 0) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 0) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 0) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 1))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 2))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 3))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 7))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 5) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 5) + 1))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 6) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 1))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 2))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 3))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 4))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 5))) = 1 by A1, Th29;
for x being Nat holds (Comput (P,s,x)) . (dl. 0) = 1 by A1, Th26;
(Comput (P,s,0)) . (dl. 1) = 1 by Th14;
(Comput (P,s,((4 * 0) + 1))) . (dl. 1) = 1 - 0 by A1, Th29;
(Comput (P,s,((4 * 0) + 2))) . (dl. 1) = 1 - 0 by A1, Th29;
(Comput (P,s,((4 * 0) + 3))) . (dl. 1) = (1 - 0) - 1 by A1, Th29;
(Comput (P,s,((4 * 0) + 4))) . (dl. 1) = (1 - 0) - 1 by A1, Th29;
(Comput (P,s,(((4 * 1) + 1) + 0))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 1) + 1) + 1))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 1) + 1) + 2))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 1) + 1) + 3))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 2) + 1) + 0))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 2) + 1) + 1))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 2) + 1) + 2))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 2) + 1) + 3))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 5) + 1) + 0))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 5) + 1) + 1))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 3))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 4))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 5))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 6))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 7))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 8))) . (dl. 1) = 0 by A1, Th29;

end;

now :: thesis: for A being Integer
for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,5,A%> holds verum

let A be Integer; :: thesis: for P being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P holds
for s being 0 -started State-consisting of <%1,5,A%> holds verum
set N = 5;
let P be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P implies for s being 0 -started State-consisting of <%1,5,A%> holds verum )
assume A1: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P ; :: thesis: for s being 0 -started State-consisting of <%1,5,A%> holds verum
let s be 0 -started State-consisting of <%1,5,A%>; :: thesis: verum
IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
IC (Comput (P,s,((4 * 0) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 0) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 0) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,(4 * 1))) = 5 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 1) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,(4 * 2))) = 5 by A1, Th29;
IC (Comput (P,s,((4 * 2) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 2) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 2) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,(4 * 3))) = 5 by A1, Th29;
IC (Comput (P,s,((4 * 3) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 3) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 3) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,(4 * 4))) = 5 by A1, Th29;
IC (Comput (P,s,((4 * 4) + 1))) = 2 by A1, Th29;
IC (Comput (P,s,((4 * 4) + 2))) = 3 by A1, Th29;
IC (Comput (P,s,((4 * 4) + 3))) = 4 by A1, Th29;
IC (Comput (P,s,((4 * 5) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 5) + 1))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 6) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 0))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 1))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 2))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 3))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 4))) = 1 by A1, Th29;
IC (Comput (P,s,((4 * 22) + 5))) = 1 by A1, Th29;
for x being Nat holds (Comput (P,s,x)) . (dl. 0) = 1 by A1, Th26;
(Comput (P,s,0)) . (dl. 1) = 5 by Th14;
(Comput (P,s,((4 * 0) + 1))) . (dl. 1) = 5 - 0 by A1, Th29;
(Comput (P,s,((4 * 0) + 2))) . (dl. 1) = 5 - 0 by A1, Th29;
(Comput (P,s,((4 * 0) + 3))) . (dl. 1) = (5 - 0) - 1 by A1, Th29;
(Comput (P,s,((4 * 0) + 4))) . (dl. 1) = (5 - 0) - 1 by A1, Th29;
(Comput (P,s,((4 * 1) + 1))) . (dl. 1) = 5 - 1 by A1, Th29;
(Comput (P,s,((4 * 1) + 2))) . (dl. 1) = 5 - 1 by A1, Th29;
(Comput (P,s,((4 * 1) + 3))) . (dl. 1) = (5 - 1) - 1 by A1, Th29;
(Comput (P,s,((4 * 1) + 4))) . (dl. 1) = (5 - 1) - 1 by A1, Th29;
(Comput (P,s,((4 * 2) + 1))) . (dl. 1) = 5 - 2 by A1, Th29;
(Comput (P,s,((4 * 2) + 2))) . (dl. 1) = 5 - 2 by A1, Th29;
(Comput (P,s,((4 * 2) + 3))) . (dl. 1) = (5 - 2) - 1 by A1, Th29;
(Comput (P,s,((4 * 2) + 4))) . (dl. 1) = (5 - 2) - 1 by A1, Th29;
(Comput (P,s,((4 * 3) + 1))) . (dl. 1) = 5 - 3 by A1, Th29;
(Comput (P,s,((4 * 3) + 2))) . (dl. 1) = 5 - 3 by A1, Th29;
(Comput (P,s,((4 * 3) + 3))) . (dl. 1) = (5 - 3) - 1 by A1, Th29;
(Comput (P,s,((4 * 3) + 4))) . (dl. 1) = (5 - 3) - 1 by A1, Th29;
(Comput (P,s,((4 * 4) + 1))) . (dl. 1) = 5 - 4 by A1, Th29;
(Comput (P,s,((4 * 4) + 2))) . (dl. 1) = 5 - 4 by A1, Th29;
(Comput (P,s,((4 * 4) + 3))) . (dl. 1) = (5 - 4) - 1 by A1, Th29;
(Comput (P,s,((4 * 4) + 4))) . (dl. 1) = (5 - 4) - 1 by A1, Th29;
(Comput (P,s,(((4 * 5) + 1) + 0))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 5) + 1) + 1))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 3))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 4))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 5))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 6))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 7))) . (dl. 1) = 0 by A1, Th29;
(Comput (P,s,(((4 * 21) + 1) + 8))) . (dl. 1) = 0 by A1, Th29;

end;

:::$T-

registration

let i1, i2 be Integer;
let k, n be Nat;
let s be 0 -started State-consisting of <%n,i1,i2%>;
let I be sequential 0 -dl.constant Instruction of SCM;
let P be IterativeAlgorithm I -extending Instruction-Sequence of SCM;

cluster (Comput (P,s,k)) . (dl. 0) -> natural ;

coherence
(Comput (P,s,k)) . (dl. 0) is natural by Th26, PROOFS_1:def 12;

end;

theorem Th30: :: AMI_8:30

for k, n being Nat
for i being Integer
for I being Instruction of SCM st ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) holds
for s being 0 -started State-consisting of <%1,n,i%>
for P being IterativeAlgorithm b₄ -extending Instruction-Sequence of SCM holds (Comput (P,s,k)) . (dl. 1) is natural

proof end;

registration

let i be Integer;
let k, n be Nat;
let s be 0 -started State-consisting of <%1,n,i%>;
let P be IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM;

cluster (Comput (P,s,k)) . (dl. 1) -> natural ;

coherence
(Comput (P,s,k)) . (dl. 1) is natural by Th30;

end;

registration

let i be Integer;
let k, n be Nat;
let s be 0 -started State-consisting of <%1,n,i%>;
let P be IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM;

cluster (Comput (P,s,k)) . (dl. 1) -> natural ;

coherence
(Comput (P,s,k)) . (dl. 1) is natural by Th30;

end;

scheme :: AMI_8:sch 1
AddOfOneSch{ F₁() -> Integer, F₂() -> Nat, F₃( object ) -> Integer } :

for P being IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,F₂(),F₁()%> holds
( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() + (F₃(F₂()) - F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() + (F₃(F₂()) - F₃((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )

provided

A1: F₃(0) = F₁() and
A2: for n being Nat holds F₃((n + 1)) = (n + 1) + F₃(n)

proof end;

scheme :: AMI_8:sch 2
MultOfOneSch{ F₁() -> Integer, F₂() -> Nat, F₃( object ) -> Integer } :

for P being IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,F₂(),F₁()%> holds
( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )

provided

A1: F₃(0) = F₁() and
A2: F₁() <> 0 and
A3: for n being Nat holds F₃((n + 1)) = (n + 1) * F₃(n)

proof end;

deffunc H₁( Nat) -> set = Triangle $1;

theorem Th31: :: AMI_8:31

for n being Nat
for P being IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,0%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Triangle n) - (Triangle ((Comput (P,s,((4 * k) + 1))) . (dl. 1))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Triangle n) - (Triangle (((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1)) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = Triangle n ) & (Result (P,s)) . (dl. 2) = Triangle n )

proof end;

deffunc H₂( Nat) -> Element of omega = $1 ! ;

theorem Th32: :: AMI_8:32

for n being Nat
for P being IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,1%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (n !) / (((Comput (P,s,((4 * k) + 1))) . (dl. 1)) !) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (n !) / ((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) !) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )

proof end;

scheme :: AMI_8:sch 3
PartFuncFinPartStEx{ F₁() -> Integer, F₂() -> Integer, F₃( object ) -> Integer } :

ex f being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st
for p, q being FinPartState of SCM holds
( [p,q] in f iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (F₁(),n,F₂()) & q = (dl. 2) .--> F₃(n) ) )

proof end;

scheme :: AMI_8:sch 4
PartFuncFinPartStUn{ F₁() -> Integer, F₂() -> Integer, F₃( object ) -> Integer } :

for f1, f2 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds
( [p,q] in f1 iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (F₁(),n,F₂()) & q = (dl. 2) .--> F₃(n) ) ) ) & ( for p, q being FinPartState of SCM holds
( [p,q] in f2 iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (F₁(),n,F₂()) & q = (dl. 2) .--> F₃(n) ) ) ) holds
f1 = f2

proof end;

definition

func powerSCMFunction -> PartFunc of (FinPartSt SCM),(FinPartSt SCM) means :Def5: :: AMI_8:def 5
for p, q being FinPartState of SCM holds
( [p,q] in it iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) & q = (dl. 2) .--> (n !) ) );

existence
ex b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st
for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) & q = (dl. 2) .--> (n !) ) ) from AMI_8:sch 3();
uniqueness
for b₁, b₂ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) & q = (dl. 2) .--> (n !) ) ) ) & ( for p, q being FinPartState of SCM holds
( [p,q] in b₂ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) & q = (dl. 2) .--> (n !) ) ) ) holds
b₁ = b₂ from AMI_8:sch 4();

end;

:: deftheorem Def5 defines powerSCMFunction AMI_8:def 5 :
for b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b₁ = powerSCMFunction iff for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) & q = (dl. 2) .--> (n !) ) ) );

set pf = powerSCMFunction ;

theorem Th33: :: AMI_8:33

for p being object holds
( p in dom powerSCMFunction iff ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) )

proof end;

set q = IterativeAlgorithm (MultBy ((dl. 2),(dl. 1)));

theorem Th34: :: AMI_8:34

for n being Nat holds powerSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)) = (dl. 2) .--> (n !)

proof end;

scheme :: AMI_8:sch 5
AutonomicSch{ F₁() -> PartFunc of (FinPartSt SCM),(FinPartSt SCM), F₂() -> Instruction of SCM, F₃( object ) -> Nat } :

for x being FinPartState of SCM st x in dom F₁() holds
Initialize x is IterativeAlgorithm F₂() -autonomic

provided

A1: ( F₂() = AddTo ((dl. 2),(dl. 1)) or F₂() = SubFrom ((dl. 2),(dl. 1)) or F₂() = MultBy ((dl. 2),(dl. 1)) ) and
A2: for x being object st x in dom F₁() holds
ex n being Nat st x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,F₃(n)) and
A3: for P, Q being Instruction-Sequence of SCM st IterativeAlgorithm F₂() c= P & IterativeAlgorithm F₂() c= Q holds
for x being FinPartState of SCM st x in dom F₁() holds
for s1, s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2 holds
for k being Nat holds (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2)

proof end;

scheme :: AMI_8:sch 6
HaltedSch{ F₁() -> PartFunc of (FinPartSt SCM),(FinPartSt SCM), F₂() -> Instruction of SCM, F₃( object ) -> Nat } :

for x being FinPartState of SCM st x in dom F₁() holds
Initialize x is IterativeAlgorithm F₂() -halted

provided

A1: ( F₂() = AddTo ((dl. 2),(dl. 1)) or F₂() = SubFrom ((dl. 2),(dl. 1)) or F₂() = MultBy ((dl. 2),(dl. 1)) ) and
A2: for x being object st x in dom F₁() holds
ex n being Nat st x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,F₃(n))

proof end;

scheme :: AMI_8:sch 7
AutonomySch{ F₁() -> PartFunc of (FinPartSt SCM),(FinPartSt SCM), F₂() -> Instruction of SCM, F₃( object ) -> Nat } :

for x being FinPartState of SCM st x in dom F₁() holds
Initialize x is Autonomy of IterativeAlgorithm F₂()

provided

A1: ( F₂() = AddTo ((dl. 2),(dl. 1)) or F₂() = SubFrom ((dl. 2),(dl. 1)) or F₂() = MultBy ((dl. 2),(dl. 1)) ) and
A2: for x being object st x in dom F₁() holds
ex n being Nat st x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,F₃(n)) and
A3: for P, Q being Instruction-Sequence of SCM st IterativeAlgorithm F₂() c= P & IterativeAlgorithm F₂() c= Q holds
for x being FinPartState of SCM st x in dom F₁() holds
for s1, s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2 holds
for k being Nat holds (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2)

proof end;

theorem Th35: :: AMI_8:35

for x being FinPartState of SCM st x in dom powerSCMFunction holds
Initialize x is Autonomy of IterativeAlgorithm (MultBy ((dl. 2),(dl. 1)))

proof end;

theorem :: AMI_8:36

IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))), Start-At (0,SCM) computes powerSCMFunction

proof end;

definition

func sumSCMFunction -> PartFunc of (FinPartSt SCM),(FinPartSt SCM) means :Def6: :: AMI_8:def 6
for p, q being FinPartState of SCM holds
( [p,q] in it iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) );

existence
ex b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st
for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) ) from AMI_8:sch 3();
uniqueness
for b₁, b₂ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) ) ) & ( for p, q being FinPartState of SCM holds
( [p,q] in b₂ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) ) ) holds
b₁ = b₂ from AMI_8:sch 4();

end;

:: deftheorem Def6 defines sumSCMFunction AMI_8:def 6 :
for b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b₁ = sumSCMFunction iff for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) ) );

set pf = sumSCMFunction ;

theorem Th37: :: AMI_8:37

for p being object holds
( p in dom sumSCMFunction iff ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) )

proof end;

set q = IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)));

theorem Th38: :: AMI_8:38

for n being Nat holds sumSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0)) = (dl. 2) .--> (Triangle n)

proof end;

theorem Th39: :: AMI_8:39

for x being FinPartState of SCM st x in dom sumSCMFunction holds
Initialize x is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))

proof end;

theorem :: AMI_8:40

IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))), Start-At (0,SCM) computes sumSCMFunction

proof end;