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_{1} -valued finite non halt-free Function

for p being non empty b_{2} -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_{1} -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 )

let t be State of S; :: according to EXTPRO_1:def 11 :: thesis: ( not p c= t or for b_{1} being set holds

( not q c= b_{1} or b_{1} halts_on t ) )

assume A8: p c= t ; :: thesis: for b_{1} being set holds

( not q c= b_{1} or b_{1} 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

for q being NAT -defined the InstructionsF of b

for p being non empty b

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

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 A7:
IncIC (p,k) is Reloc (q,k) -halted
; :: thesis: 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

end;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_{1} being set holds

( not Reloc (q,k) c= b_{1} or b_{1} halts_on t ) )

assume A2: IncIC (p,k) c= t ; :: thesis: for b_{1} being set holds

( not Reloc (q,k) c= b_{1} or b_{1} 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;( not Reloc (q,k) c= b

assume A2: IncIC (p,k) c= t ; :: thesis: for b

( not Reloc (q,k) c= b

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

let t be State of S; :: according to EXTPRO_1:def 11 :: thesis: ( not p c= t or for b

( not q c= b

assume A8: p c= t ; :: thesis: for b

( not q c= b

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