let k, n be Nat; :: thesis: 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
let i be Integer; :: thesis: 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
let I be Instruction of SCM; :: thesis: ( ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) implies for s being 0 -started State-consisting of <%1,n,i%>
for P being IterativeAlgorithm I -extending Instruction-Sequence of SCM holds (Comput (P,s,k)) . (dl. 1) is natural )
assume A1: ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) ; :: thesis: for s being 0 -started State-consisting of <%1,n,i%>
for P being IterativeAlgorithm I -extending Instruction-Sequence of SCM holds (Comput (P,s,k)) . (dl. 1) is natural
let s be 0 -started State-consisting of <%1,n,i%>; :: thesis: for P being IterativeAlgorithm I -extending Instruction-Sequence of SCM holds (Comput (P,s,k)) . (dl. 1) is natural
let P be IterativeAlgorithm I -extending Instruction-Sequence of SCM; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural
A2: IterativeAlgorithm I c= P by PROOFS_1:def 12;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

hence (Comput (P,s,k)) . (dl. 1) is natural by A1, A2, Th27; :: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

consider z being Nat such that
A4: ( k = 4 * z or k = (4 * z) + 1 or k = (4 * z) + 2 or k = (4 * z) + 3 ) by NUMBER02:24;

A5: now :: thesis: for s being Nat holds S₁[s]

defpred S₁[ Nat] means (Comput (P,s,(4 * $1))) . (dl. 1) is natural ;
A6: S₁[ 0 ] by Th14;
A7: for q being Nat st S₁[q] holds
S₁[q + 1]

proof

let q be Nat; :: thesis: ( S₁[q] implies S₁[q + 1] )
assume S₁[q] ; :: thesis: S₁[q + 1]

per cases ( q < n or q >= n ) ;

suppose A8: q < n ; :: thesis: S₁[q + 1]

then q + 1 <= n by NAT_1:13;
then A9: n - (q + 1) in NAT by INT_1:5;
(Comput (P,s,((4 * q) + 4))) . (dl. 1) = (n - q) - 1 by A1, A2, A8, Th29;
hence (Comput (P,s,(4 * (q + 1)))) . (dl. 1) is natural by A9; :: thesis: verum

end;

suppose q >= n ; :: thesis: S₁[q + 1]

then (Comput (P,s,(((4 * q) + 1) + 3))) . (dl. 1) is natural by A1, A2, A3, Th29;
hence (Comput (P,s,(4 * (q + 1)))) . (dl. 1) is natural ; :: thesis: verum

end;

end;

end;

thus for s being Nat holds S₁[s] from NAT_1:sch 2(A6, A7); :: thesis: verum

end;

per cases ( z < n or z >= n ) ;

suppose A10: z < n ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

then z + 1 <= n by NAT_1:13;
then A11: n - (z + 1) in NAT by INT_1:5;

per cases ( k = 4 * z or k = (4 * z) + 1 or k = (4 * z) + 2 or k = (4 * z) + 3 ) by A4;

suppose k = 4 * z ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

hence (Comput (P,s,k)) . (dl. 1) is natural by A5; :: thesis: verum

end;

suppose A12: ( k = (4 * z) + 1 or k = (4 * z) + 2 ) ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

n - z in NAT by A10, INT_1:5;
hence (Comput (P,s,k)) . (dl. 1) is natural by A1, A2, A10, A12, Th29; :: thesis: verum

end;

suppose A13: k = (4 * z) + 3 ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

(n - z) - 1 = n - (z + 1) ;
hence (Comput (P,s,k)) . (dl. 1) is natural by A1, A2, A10, A11, A13, Th29; :: thesis: verum

end;

end;

end;

suppose A14: z >= n ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

per cases ( k = 4 * z or k = ((4 * z) + 1) + 0 or k = ((4 * z) + 1) + 1 or k = ((4 * z) + 1) + 2 ) by A4;

suppose k = 4 * z ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

hence (Comput (P,s,k)) . (dl. 1) is natural by A5; :: thesis: verum

end;

suppose ( k = ((4 * z) + 1) + 0 or k = ((4 * z) + 1) + 1 or k = ((4 * z) + 1) + 2 ) ; :: thesis: (Comput (P,s,k)) . (dl. 1) is natural

hence (Comput (P,s,k)) . (dl. 1) is natural by A2, A3, A14, A1, Th29; :: thesis: verum

end;

end;

end;

end;

end;

end;