let k be Nat; :: thesis: 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
let i, i1, i2 be Integer; :: thesis: 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
let I be Instruction of SCM; :: thesis: 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
let P be Instruction-Sequence of SCM; :: thesis: ( I is sequential & I is 0 -dl.constant & IterativeAlgorithm I c= P implies for s being 0 -started State-consisting of <%i,i1,i2%> holds (Comput (P,s,k)) . (dl. 0) = i )
assume that
A1: I is sequential and
A2: I is 0 -dl.constant and
A3: IterativeAlgorithm I c= P ; :: thesis: for s being 0 -started State-consisting of <%i,i1,i2%> holds (Comput (P,s,k)) . (dl. 0) = i
let s be 0 -started State-consisting of <%i,i1,i2%>; :: thesis: (Comput (P,s,k)) . (dl. 0) = i
defpred S₁[ Nat] means (Comput (P,s,$1)) . (dl. 0) = i;
A4: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
A5: S₁[ 0 ] by Th14;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
set s1 = Comput (P,s,k);
IC (Comput (P,s,k)) in {0,1,2,3,4,5} by A1, A3, A4, Th25;

per cases then ( IC (Comput (P,s,k)) = 0 or IC (Comput (P,s,k)) = 1 or IC (Comput (P,s,k)) = 3 or IC (Comput (P,s,k)) = 4 or IC (Comput (P,s,k)) = 5 or IC (Comput (P,s,k)) = 2 ) by ENUMSET1:def 4;

suppose ( IC (Comput (P,s,k)) = 0 or IC (Comput (P,s,k)) = 1 or IC (Comput (P,s,k)) = 3 or IC (Comput (P,s,k)) = 4 or IC (Comput (P,s,k)) = 5 ) ; :: thesis: S₁[k + 1]

hence (Comput (P,s,(k + 1))) . (dl. 0) = i by A3, A7, Th16, Th18, Th22, Th23, Th24; :: thesis: verum

end;

suppose A8: IC (Comput (P,s,k)) = 2 ; :: thesis: S₁[k + 1]

A9: dom (IterativeAlgorithm I) = {0,1,2,3,4,5} by Th6;
dom (IterativeAlgorithm I) c= dom P by A3, GRFUNC_1:2;
then CurInstr (P,(Comput (P,s,k))) = P . 2 by A8, A9, Lm1, PARTFUN1:def 6
.= I by A3, Th8 ;
hence (Comput (P,s,(k + 1))) . (dl. 0) = i by A7, A2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence (Comput (P,s,k)) . (dl. 0) = i ; :: thesis: verum