let N be non empty with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Nat holds Comput (P,s,n) = s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Nat holds Comput (P,s,n) = s
let P be Instruction-Sequence of S; for s being State of S st s = Following (P,s) holds
for n being Nat holds Comput (P,s,n) = s
let s be State of S; ( s = Following (P,s) implies for n being Nat holds Comput (P,s,n) = s )
defpred S1[ Nat] means Comput (P,s,$1) = s;
assume
s = Following (P,s)
; for n being Nat holds Comput (P,s,n) = s
then A1:
for n being Nat st S1[n] holds
S1[n + 1]
by Th3;
A2:
S1[ 0 ]
;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A1); verum