let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is proper-halt holds
for p being autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is halting iff Relocated (p,k) is halting )
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N; :: thesis: ( S is relocable1 & S is proper-halt implies for p being autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is halting iff Relocated (p,k) is halting ) )
assume ( S is relocable1 & S is proper-halt ) ; :: thesis: for p being autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is halting iff Relocated (p,k) is halting )
let p be autonomic FinPartState of S; :: thesis: for k being Element of NAT st IC in dom p holds
( p is halting iff Relocated (p,k) is halting )
let k be Element of NAT ; :: thesis: ( IC in dom p implies ( p is halting iff Relocated (p,k) is halting ) )
assume A1: IC in dom p ; :: thesis: ( p is halting iff Relocated (p,k) is halting )
RE: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;

hereby :: thesis: ( Relocated (p,k) is halting implies p is halting )

assume A3: p is halting ; :: thesis: Relocated (p,k) is halting
thus Relocated (p,k) is halting :: thesis: verum

proof

let t be State of S; :: according to EXTPRO_1:def 10 :: thesis: ( not NPP (Relocated (p,k)) c= t or for b₁ being set holds
( not ProgramPart (Relocated (p,k)) c= b₁ or b₁ halts_on t ) )
assume A4: NPP (Relocated (p,k)) c= t ; :: thesis: for b₁ being set holds
( not ProgramPart (Relocated (p,k)) c= b₁ or b₁ halts_on t )
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Relocated (p,k)) c= P or P halts_on t )
assume A5: ProgramPart (Relocated (p,k)) c= P ; :: thesis: P halts_on t
reconsider Q = P +* (ProgramPart p) as the Instructions of S -valued ManySortedSet of NAT ;
set s = t +* p;
A6: ProgramPart p c= Q by FUNCT_4:26;
p c= t +* p by FUNCT_4:26;
then B7: NPP p c= t +* p by XBOOLE_1:1;
then Q halts_on t +* p by A3, A6, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A8: CurInstr (Q,(Comput (Q,(t +* p),u))) = halt S by EXTPRO_1:30;
take u ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT by PARTFUN1:def 4;
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, RE, B7
.= halt S by COMPOS_1:93 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S ; :: thesis: verum

end;

end;

assume A9: Relocated (p,k) is halting ; :: thesis: p is halting
let t be State of S; :: according to EXTPRO_1:def 10 :: thesis: ( not NPP p c= t or for b₁ being set holds
( not ProgramPart p c= b₁ or b₁ halts_on t ) )
assume A10: NPP p c= t ; :: thesis: for b₁ being set holds
( not ProgramPart p c= b₁ or b₁ halts_on t )
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart p c= P or P halts_on t )
assume A11: ProgramPart p c= P ; :: thesis: P halts_on t
reconsider Q = P +* (Reloc ((ProgramPart p),k)) as the Instructions of S -valued ManySortedSet of NAT ;
set s = t +* (NPP (Relocated (p,k)));
A12: Reloc ((ProgramPart p),k) c= Q by FUNCT_4:26;
A13: NPP (Relocated (p,k)) c= t +* (NPP (Relocated (p,k))) by FUNCT_4:26;
then Q halts_on t +* (NPP (Relocated (p,k))) by A9, A12, RE, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A14: CurInstr (Q,(Comput (Q,(t +* (NPP (Relocated (p,k)))),u))) = halt S by EXTPRO_1:30;
take u ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT by PARTFUN1:def 4;
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:93 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S by COMPOS_1:95; :: thesis: verum