let N be with_zero set ; :: thesis: 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 b₁ -valued finite non halt-free Function
for p being non empty b₂ -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; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b₁ -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; :: thesis: 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; :: thesis: 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; :: thesis: ( IC in dom p implies ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted ) )
assume 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 A1: 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 A2: 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 A3: Reloc (q,k) c= P ; :: thesis: 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 ; :: 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 A2, A6, Def5, A3, A4, A5
.= halt S by COMPOS_0:4 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S ; :: thesis: verum

end;

end;

assume A7: 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 A8: 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 A9: 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));
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 ; :: 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 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; :: thesis: verum