let k be Nat; :: thesis: 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}
let s be State of SCM; :: thesis: 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}
let I be Instruction of SCM; :: thesis: 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}
let P be Instruction-Sequence of SCM; :: thesis: ( I is sequential & IterativeAlgorithm I c= P & IC (Comput (P,s,0)) = 0 implies IC (Comput (P,s,k)) in {0,1,2,3,4,5} )
set F = IterativeAlgorithm I;
assume that
A1: I is sequential and
A2: IterativeAlgorithm I c= P and
A3: IC (Comput (P,s,0)) = 0 ; :: thesis: IC (Comput (P,s,k)) in {0,1,2,3,4,5}
defpred S₁[ Nat] means IC (Comput (P,s,$1)) in {0,1,2,3,4,5};
A4: S₁[ 0 ] by A3, ENUMSET1:def 4;
A5: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
set t = Comput (P,s,j);
set t1 = Comput (P,s,(j + 1));
assume S₁[j] ; :: thesis: S₁[j + 1]

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

suppose A6: IC (Comput (P,s,j)) = 0 ; :: thesis: S₁[j + 1]

( (Comput (P,s,j)) . (dl. 1) > 0 or (Comput (P,s,j)) . (dl. 1) <= 0 ) ;
then ( IC (Comput (P,s,(j + 1))) = 1 or IC (Comput (P,s,(j + 1))) = 2 ) by A2, A6, Th16;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

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

then IC (Comput (P,s,(j + 1))) = 1 by A2, Th18;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

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

then A8: I = P . (IC (Comput (P,s,j))) by A2, Th8;
IC (Comput (P,s,(j + 1))) = IC (Following (P,(Comput (P,s,j)))) by EXTPRO_1:3
.= (Exec (I,(Comput (P,s,j)))) . (IC ) by A8, EXTPRO_1:28
.= 2 + 1 by A7, A1, AMISTD_1:def 8 ;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

suppose IC (Comput (P,s,j)) = 3 ; :: thesis: S₁[j + 1]

then IC (Comput (P,s,(j + 1))) = 4 by A2, Th22;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

suppose A9: IC (Comput (P,s,j)) = 4 ; :: thesis: S₁[j + 1]

( (Comput (P,s,j)) . (dl. 1) = 0 or (Comput (P,s,j)) . (dl. 1) <> 0 ) ;
then ( IC (Comput (P,s,(j + 1))) = 1 or IC (Comput (P,s,(j + 1))) = 5 ) by A2, A9, Th23;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

suppose IC (Comput (P,s,j)) = 5 ; :: thesis: S₁[j + 1]

then IC (Comput (P,s,(j + 1))) = 2 by A2, Th24;
hence S₁[j + 1] by ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A4, A5);
hence IC (Comput (P,s,k)) in {0,1,2,3,4,5} ; :: thesis: verum