let i, j be Nat; ( i <= j implies for N being 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 NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i) )
assume
i <= j
; for N being 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 NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
then consider k being Nat such that
A1:
j = i + k
by NAT_1:10;
reconsider k = k as Nat ;
A2:
j = i + k
by A1;
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 NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let p be NAT -defined the InstructionsF of S -valued Function; for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let s be State of S; ( CurInstr (p,(Comput (p,s,i))) = halt S implies Comput (p,s,j) = Comput (p,s,i) )
assume A3:
CurInstr (p,(Comput (p,s,i))) = halt S
; Comput (p,s,j) = Comput (p,s,i)
defpred S1[ Nat] means Comput (p,s,(i + $1)) = Comput (p,s,i);
A4:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[k + 1] Comput (
p,
s,
(i + (k + 1))) =
Comput (
p,
s,
((i + k) + 1))
.=
Following (
p,
(Comput (p,s,(i + k))))
by Th3
.=
Comput (
p,
s,
i)
by A3, A5, Def3
;
hence
S1[
k + 1]
;
verum end;
A6:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A6, A4);
hence
Comput (p,s,j) = Comput (p,s,i)
by A2; verum