let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of S
for k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N; for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of S
for k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of S
for k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let p be non empty q -autonomic FinPartState of S; for k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let k be Nat; ( IC in dom p implies ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted ) )
assume
IC in dom p
; ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
hereby ( IncIC (p,k) is Reloc (q,k) -halted implies p is q -halted )
assume A1:
p is
q -halted
;
IncIC (p,k) is Reloc (q,k) -halted thus
IncIC (
p,
k) is
Reloc (
q,
k)
-halted
verumproof
let t be
State of
S;
EXTPRO_1:def 11 ( not IncIC (p,k) c= t or for b1 being set holds
( not Reloc (q,k) c= b1 or b1 halts_on t ) )
assume A2:
IncIC (
p,
k)
c= t
;
for b1 being set holds
( not Reloc (q,k) c= b1 or b1 halts_on t )
let P be
Instruction-Sequence of
S;
( not Reloc (q,k) c= P or P halts_on t )
assume A3:
Reloc (
q,
k)
c= P
;
P halts_on t
reconsider Q =
P +* q as
Instruction-Sequence of
S ;
set s =
t +* p;
A4:
q c= Q
by FUNCT_4:25;
A5:
p c= t +* p
by FUNCT_4:25;
then
Q halts_on t +* p
by A1, A4;
then consider u being
Nat such that A6:
CurInstr (
Q,
(Comput (Q,(t +* p),u)))
= halt S
;
take
u
;
EXTPRO_1:def 8 ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT
by PARTFUN1:def 2;
hence
IC (Comput (P,t,u)) in dom P
;
CurInstr (P,(Comput (P,t,u))) = halt S
CurInstr (
P,
(Comput (P,t,u))) =
IncAddr (
(halt S),
k)
by A2, A6, Def5, A3, A4, A5
.=
halt S
by COMPOS_0:4
;
hence
CurInstr (
P,
(Comput (P,t,u)))
= halt S
;
verum
end;
end;
assume A7:
IncIC (p,k) is Reloc (q,k) -halted
; p is q -halted
let t be State of S; EXTPRO_1:def 11 ( not p c= t or for b1 being set holds
( not q c= b1 or b1 halts_on t ) )
assume A8:
p c= t
; for b1 being set holds
( not q c= b1 or b1 halts_on t )
let P be Instruction-Sequence of S; ( not q c= P or P halts_on t )
assume A9:
q c= P
; P halts_on t
reconsider Q = P +* (Reloc (q,k)) as Instruction-Sequence of S ;
set s = t +* (IncIC (p,k));
A10:
Reloc (q,k) c= Q
by FUNCT_4:25;
A11:
IncIC (p,k) c= t +* (IncIC (p,k))
by FUNCT_4:25;
then
Q halts_on t +* (IncIC (p,k))
by A7, A10;
then consider u being Nat such that
A12:
CurInstr (Q,(Comput (Q,(t +* (IncIC (p,k))),u))) = halt S
;
take
u
; EXTPRO_1:def 8 ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT
by PARTFUN1:def 2;
hence
IC (Comput (P,t,u)) in dom P
; CurInstr (P,(Comput (P,t,u))) = halt S
IncAddr ((CurInstr (P,(Comput (P,t,u)))),k) =
halt S
by A8, A12, Def5, A11, A9, A10
.=
IncAddr ((halt S),k)
by COMPOS_0:4
;
hence
CurInstr (P,(Comput (P,t,u))) = halt S
by COMPOS_0:6; verum