let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is proper-halt holds
for q being NAT -defined the Instructions of b₁ -valued finite non halt-free Function
for p being non empty b₂ -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let S be standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized relocable1 AMI-Struct of N; :: thesis: ( S is relocable1 & S is proper-halt implies for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted ) )
assume ( S is relocable1 & S is proper-halt ) ; :: thesis: for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of S
for k being Element of 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 Instructions of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of S
for k being Element of 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; :: thesis: for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let k be Element of NAT ; :: thesis: ( IC in dom p implies ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted ) )
assume A1: IC in dom p ; :: thesis: ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )

hereby :: thesis: ( IncIC (p,k) is Reloc (q,k) -halted implies p is q -halted )

assume A3: p is q -halted ; :: thesis: IncIC (p,k) is Reloc (q,k) -halted
thus IncIC (p,k) is Reloc (q,k) -halted :: thesis: verum

proof

let t be State of S; :: according to EXTPRO_1:def 11 :: thesis: ( not IncIC (p,k) c= t or for b₁ being set holds
( not Reloc (q,k) c= b₁ or b₁ halts_on t ) )
assume A4: IncIC (p,k) c= t ; :: thesis: for b₁ being set holds
( not Reloc (q,k) c= b₁ or b₁ halts_on t )
let P be Instruction-Sequence of S; :: thesis: ( not Reloc (q,k) c= P or P halts_on t )
assume A5: Reloc (q,k) c= P ; :: thesis: P halts_on t
reconsider Q = P +* q as Instruction-Sequence of S ;
set s = t +* p;
A6: q c= Q by FUNCT_4:25;
C7: p c= t +* p by FUNCT_4:25;
then p c= t +* p ;
then Q halts_on t +* p by A3, A6, EXTPRO_1:def 11;
then consider u being Element of NAT such that
A8: CurInstr (Q,(Comput (Q,(t +* p),u))) = halt S by EXTPRO_1:29;
take u ; :: according to EXTPRO_1:def 8 :: thesis: ( 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 ; :: thesis: CurInstr (P,(Comput (P,t,u))) = halt S
CurInstr (P,(Comput (P,t,u))) = IncAddr ((halt S),k) by A1, A4, A8, Def5, A5, A6, C7
.= halt S by COMPOS_1:11 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S ; :: thesis: verum

end;

end;

assume A9: IncIC (p,k) is Reloc (q,k) -halted ; :: thesis: p is q -halted
let t be State of S; :: according to EXTPRO_1:def 11 :: thesis: ( not p c= t or for b₁ being set holds
( not q c= b₁ or b₁ halts_on t ) )
assume A10: p c= t ; :: thesis: for b₁ being set holds
( not q c= b₁ or b₁ halts_on t )
let P be Instruction-Sequence of S; :: thesis: ( not q c= P or P halts_on t )
assume A11: q c= P ; :: thesis: P halts_on t
reconsider Q = P +* (Reloc (q,k)) as Instruction-Sequence of S ;
set s = t +* (IncIC (p,k));
A12: Reloc (q,k) c= Q by FUNCT_4:25;
A13: IncIC (p,k) c= t +* (IncIC (p,k)) by FUNCT_4:25;
then Q halts_on t +* (IncIC (p,k)) by A9, A12, EXTPRO_1:def 11;
then consider u being Element of NAT such that
A14: CurInstr (Q,(Comput (Q,(t +* (IncIC (p,k))),u))) = halt S by EXTPRO_1:29;
take u ; :: according to EXTPRO_1:def 8 :: thesis: ( 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 ; :: thesis: CurInstr (P,(Comput (P,t,u))) = halt S
IncAddr ((CurInstr (P,(Comput (P,t,u)))),k) = halt S by A1, A10, A14, Def5, A13, A11, A12
.= IncAddr ((halt S),k) by COMPOS_1:11 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S by COMPOS_1:13; :: thesis: verum