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 l being Nat
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds
for p being b2 -started PartState of S
for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; for l being Nat
for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being b1 -started PartState of S
for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s
let l be Nat; for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s
let P be NAT -defined the InstructionsF of S -valued Function; ( l .--> (halt S) c= P implies for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s )
assume A1:
l .--> (halt S) c= P
; for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s
let p be l -started PartState of S; for s being State of S st p c= s holds
for i being Nat holds Comput (P,s,i) = s
set h = halt S;
let s be State of S; ( p c= s implies for i being Nat holds Comput (P,s,i) = s )
assume A2:
p c= s
; for i being Nat holds Comput (P,s,i) = s
A3:
Start-At (l,S) c= p
by MEMSTR_0:29;
defpred S1[ Nat] means Comput (P,s,$1) = s;
A4:
Start-At (l,S) c= s
by A3, A2, XBOOLE_1:1;
A5:
now for i being Nat st S1[i] holds
S1[i + 1]end;
A7:
S1[ 0 ]
;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A7, A5); verum