let N be non empty with_zero set ; :: thesis: 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 b_{1} -valued Function st l .--> (halt S) c= P holds

for p being b_{2} -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; :: thesis: 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 b_{1} -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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( p c= s implies for i being Nat holds Comput (P,s,i) = s )

assume A2: p c= s ; :: thesis: for i being Nat holds Comput (P,s,i) = s

A3: Start-At (l,S) c= p by MEMSTR_0:29;

defpred S_{1}[ Nat] means Comput (P,s,$1) = s;

A4: Start-At (l,S) c= s by A3, A2, XBOOLE_1:1;

_{1}[ 0 ]
;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A7, A5); :: thesis: verum

for l being Nat

for P being NAT -defined the InstructionsF of b

for p being b

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; :: thesis: 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 b

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( p c= s implies for i being Nat holds Comput (P,s,i) = s )

assume A2: p c= s ; :: thesis: for i being Nat holds Comput (P,s,i) = s

A3: Start-At (l,S) c= p by MEMSTR_0:29;

defpred S

A4: Start-At (l,S) c= s by A3, A2, XBOOLE_1:1;

A5: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A7:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A6: S_{1}[i]
; :: thesis: S_{1}[i + 1]

Comput (P,s,(i + 1)) = Following (P,s) by A6, Th3

.= Exec ((halt S),s) by A4, A1, Th9

.= s by Def3 ;

hence S_{1}[i + 1]
; :: thesis: verum

end;assume A6: S

Comput (P,s,(i + 1)) = Following (P,s) by A6, Th3

.= Exec ((halt S),s) by A4, A1, Th9

.= s by Def3 ;

hence S

thus for i being Nat holds S