let i, j be Nat; for N being non empty with_zero set st i <= j holds
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 P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
let N be non empty with_zero set ; ( i <= j implies 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 P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j)) )
assume A1:
i <= j
; 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 P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
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 P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
let p be NAT -defined the InstructionsF of S -valued Function; for s being State of S st p halts_at IC (Comput (p,s,i)) holds
p halts_at IC (Comput (p,s,j))
let s be State of S; ( p halts_at IC (Comput (p,s,i)) implies p halts_at IC (Comput (p,s,j)) )
assume that
A2:
IC (Comput (p,s,i)) in dom p
and
A3:
p . (IC (Comput (p,s,i))) = halt S
; COMPOS_1:def 12 p halts_at IC (Comput (p,s,j))
A4:
CurInstr (p,(Comput (p,s,i))) = halt S
by A2, A3, PARTFUN1:def 6;
hence
IC (Comput (p,s,j)) in dom p
by A2, A1, Th5; COMPOS_1:def 12 p . (IC (Comput (p,s,j))) = halt S
thus
p . (IC (Comput (p,s,j))) = halt S
by A1, A3, A4, Th5; verum