:: Relocable Instructions
::  by Andrzej Trybulec
::
:: Received November 20, 2010
:: Copyright (c) 2010-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ARYTM_1, ARYTM_3, CARD_1, AMI_1, XBOOLE_0, RELAT_1,
      TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1, FUNCT_1, STRUCT_0,
      VALUED_1, FSM_1, FUNCT_4, TURING_1, CIRCUIT2, AMISTD_2, PARTFUN1,
      EXTPRO_1, NAT_1, RELOC, AMISTD_5, COMPOS_1, MSUALG_1, FINSET_1, QUANTAL1,
      MEMSTR_0, SCMFSA6B;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, FINSET_1, CARD_1,
      NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D,
      FUNCT_7, VALUED_0, VALUED_1, AFINSQ_1, MEASURE6, STRUCT_0, MEMSTR_0,
      COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2;
 constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY,
      AFINSQ_1, ORDINAL4, VALUED_1, AMISTD_2, PBOOLE, RELSET_1, FUNCT_7,
      FUNCT_4, MEMSTR_0, MEASURE6, XTUPLE_0;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1,
      AMISTD_1, FUNCT_4, RELSET_1, GRFUNC_1, ORDINAL1, VALUED_1, COMPOS_1,
      EXTPRO_1, AMISTD_2, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions EXTPRO_1, AMISTD_1, AMISTD_2;
 equalities COMPOS_1, EXTPRO_1, FUNCOP_1, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0;
 expansions EXTPRO_1, AMISTD_1;
 theorems AMISTD_1, FUNCOP_1, FUNCT_1, FUNCT_4, GRFUNC_1, RELAT_1, TARSKI,
      ZFMISC_1, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, VALUED_1, COMPOS_1,
      EXTPRO_1, NAT_D, AMISTD_2, MEMSTR_0, COMPOS_0;
 schemes NAT_1;

begin  :: Relocable instructions

theorem
  for N be with_zero set
  for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
  for I be Instruction of S st I is jump-only
  for k be Nat holds IncAddr(I,k) is jump-only
  by COMPOS_0:def 9;

registration
  let N be with_zero set,
  S be with_explicit_jumps IC-Ins-separated halting
  non empty with_non-empty_values AMI-Struct over N,
  I be IC-relocable Instruction of S, k be Nat;
 cluster IncAddr(I,k) -> IC-relocable;
 coherence
  proof
   let j,i being Nat, s being State of S;
   thus IC Exec(IncAddr(IncAddr(I,k),j),s) + i
    = IC Exec(IncAddr(I,k+j),s) + i by COMPOS_0:7
   .= IC Exec(IncAddr(I,k+j+i),IncIC(s,i)) by AMISTD_2:def 3
   .= IC Exec(IncAddr(I,k+(j+i)),IncIC(s,i))
   .= IC Exec(IncAddr(IncAddr(I,k),j+i),IncIC(s,i)) by COMPOS_0:7;
  end;
end;

definition
  let N be with_zero set,
  S be halting
    IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  I be Instruction of S;
  attr I is relocable means
:Def1:  for j,k being Nat, s being State of S holds
    Exec(IncAddr(I,j+k),IncIC(s,k)) =  IncIC(Exec(IncAddr(I,j),s),k);
end;

registration
  let N be with_zero set,
  S be halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
 cluster relocable -> IC-relocable for Instruction of S;
 coherence
  proof let I be Instruction of S such that
A1:  I is relocable;
   let j,k be Nat, s be State of S;
    reconsider kk=k as Nat;
   thus IC Exec(IncAddr(I,j),s) + k
     = IC  IncIC(Exec(IncAddr(I,j),s),kk) by MEMSTR_0:53
    .= IC Exec(IncAddr(I,j+k),IncIC(s,k)) by A1;
  end;
end;

definition
  let N be with_zero set,
  S be halting
   IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
  attr S is relocable means
:Def2: for I being Instruction of S holds I is relocable;
end;

theorem Th2:
 for N being with_zero set,
  I being Instruction of STC N, s be State of STC N,
  k being Nat
 holds Exec(I,IncIC(s,k)) = IncIC(Exec(I,s),k)
proof
 let N being with_zero set,
  I being Instruction of STC N, s be State of STC N,
  k being Nat;
 per cases by AMISTD_1:6;
 suppose
A1: InsCode I = 1;
  hence Exec(I,IncIC(s,k)) = IncIC(IncIC(s,k),1) by AMISTD_1:20
     .= IncIC(s,1+k) by MEMSTR_0:57
     .= IncIC(IncIC(s,1),k) by MEMSTR_0:57
     .= IncIC(Exec(I,s),k) by A1,AMISTD_1:20;
 end;
 suppose InsCode I = 0;
   then
A2:  I is halting by AMISTD_1:4;
  hence Exec(I,IncIC(s,k)) = IncIC(s,k)
     .= IncIC(Exec(I,s),k) by A2;
 end;
end;

definition
 let N be with_zero set;
 let S be halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N;
 attr S is IC-recognized means

 for q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function
 for p being q-autonomic
  FinPartState of S st  p is non empty
   holds IC S in dom p;
end;

theorem Th3:
 for N being with_zero set
 for S being halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N
 holds S is IC-recognized iff
  for q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic
  FinPartState of S st DataPart p <> {}
   holds IC S in dom p
proof
 let N be with_zero set;
 let S be halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N;
 thus S is IC-recognized implies
  for q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic FinPartState of S st DataPart p <> {}
   holds IC S in dom p
 proof assume
A1: S is IC-recognized;
  let q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic FinPartState of S;
  assume DataPart p <> {};
   then  p is non empty;
  hence thesis by A1;
 end;
 assume
A2: for q be non halt-free finite
    (the InstructionsF of S)-valued NAT-defined Function
 for p being q-autonomic FinPartState of S st DataPart p <> {}
   holds IC S in dom p;
  let q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic FinPartState of S;
A3: dom  p c= {IC S} \/ dom DataPart p by MEMSTR_0:32;
  assume
A4:  p is non empty;
  per cases;
  suppose
A5: IC S in dom  p;
   thus IC S in dom p by A5;
  end;
  suppose not IC S in dom  p;
   then {IC S} misses dom  p by ZFMISC_1:50;
   then dom DataPart p is non empty by A4,A3,XBOOLE_1:3,73;
   then DataPart p is non empty;
  hence IC S in dom p by A2;
  end;
end;

registration
 let N be with_zero set;
 cluster Data-Locations STC N -> empty;
 coherence
  proof
    the carrier of STC N = {0} by AMISTD_1:def 7
        .= {IC STC N} by AMISTD_1:def 7;
   hence thesis by XBOOLE_1:37;
  end;
end;

registration
 let N be with_zero set;
 let p be PartState of STC N;
 cluster DataPart p -> empty;
 coherence;
end;

registration
 let N be with_zero set;
 cluster STC N -> IC-recognized relocable;
 coherence
  proof
  for q be non halt-free finite
   (the InstructionsF of STC N)-valued NAT-defined Function
    for p being q-autonomic
     FinPartState of STC N st DataPart p <> {}
     holds IC STC N in dom p;
   hence STC N is IC-recognized by Th3;
   let I be Instruction of STC N;
   let j,k be Nat, s be State of STC N;
   thus  Exec(IncAddr(I,j+k),IncIC(s,k))
        =  Exec(I,IncIC(s,k)) by COMPOS_0:4
       .=  IncIC(Exec(I,s),k) by Th2
       .=  IncIC(Exec(IncAddr(I,j),s),k) by COMPOS_0:4;
  end;
end;

registration
  let N be with_zero set;
  cluster relocable IC-recognized
   for standard halting
   IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
 existence
  proof
   take STC N;
   thus thesis;
  end;
end;

registration
  let N be with_zero set;
  let S be relocable halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
 cluster -> relocable for Instruction of S;
 coherence by Def2;
end;

reserve k for Nat;

theorem Th4:
  for N be with_zero set
  for S be relocable halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N
  for INS being Instruction of S, s being State of S
   holds  Exec(IncAddr(INS,k),IncIC(s,k)) =  IncIC(Exec(INS,s),k)
 proof
  let N be with_zero set;
  let S be relocable halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  let INS be Instruction of S, s be State of S;
  thus  Exec(IncAddr(INS,k),IncIC(s,k))
          =  Exec(IncAddr(INS,(0 qua Nat)+k),IncIC(s,k))
         .=  IncIC(Exec(IncAddr(INS,0),s),k) by Def1
         .=  IncIC(Exec(INS,s),k) by COMPOS_0:3;
 end;

theorem Th5:
  for N be with_zero set
  for S be relocable halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N
  for INS being Instruction of S, s being State of S,
      j, k being Nat st IC s = j+k
 holds  Exec(INS, DecIC(s,k)) =  DecIC(Exec(IncAddr(INS, k), s),k)
proof
  let N be with_zero set;
  let S be relocable halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  let INS be Instruction of S, s be State of S,
      j,k be Nat such that
A1: IC s = j+k;
  set s1 = s +* Start-At(j,S);
A2: IncIC(s1,k) = s +* Start-At(IC s,S) by A1,MEMSTR_0:58
     .= s by MEMSTR_0:31;
 thus  Exec(INS, DecIC(s,k))
    =  Exec(INS,s1) by A1,NAT_D:34
   .= (Exec(INS,s1) +* Start-At(IC Exec(INS,s1),S)) by MEMSTR_0:31
   .= (IncIC(Exec(INS,s1),k) +*
       Start-At(IC Exec(INS,s1),S)) by FUNCT_4:114
   .= DecIC( IncIC(Exec(INS,s1),k),k) by MEMSTR_0:59
   .=  DecIC(Exec(IncAddr(INS, k), s),k) by A2,Th4;
end;

registration let N be with_zero set;
 cluster relocable IC-recognized
  for halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
 existence
  proof
   take STC N;
   thus thesis;
  end;
end;

reserve N for with_zero set,
   S for IC-recognized
    halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;

theorem Th6:
  for q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic non empty FinPartState of S
   holds IC S in dom p
proof
  let q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic non empty FinPartState of S;
A1:  dom p meets {IC S} \/ Data-Locations S by MEMSTR_0:41;
  per cases by A1,XBOOLE_1:70;
  suppose dom p meets {IC S};
    hence thesis by ZFMISC_1:50;
  end;
  suppose dom p meets Data-Locations S;
    then dom p /\ Data-Locations S <> {} by XBOOLE_0:def 7;
    then DataPart p <> {} by RELAT_1:38,61;
    hence thesis by Th3;
  end;
end;

definition let N;
 let S be halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N;
 attr S is CurIns-recognized means
:Def4:
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
 for p being q-autonomic non empty FinPartState of S
  for s being State of S st  p c= s
 for P being Instruction-Sequence of S
       st q c= P
  for i being Nat holds IC Comput(P,s,i) in dom q;
end;

registration let N;
 cluster STC N -> CurIns-recognized;
 coherence
proof
  let q be non halt-free finite
   (the InstructionsF of STC N)-valued NAT-defined Function;
  let p be q-autonomic non empty FinPartState of STC N,
      s be State of STC N such that
A1:  p c= s;
  let P be Instruction-Sequence of STC N such that
A2: q c= P;
  let i be Nat;
  set Csi = Comput(P,s,i);
  set loc = IC Csi;
  set loc1 = loc+1;
  assume
A3:  not IC Comput(P,s,i) in dom q;
  the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
  then
  reconsider I = [1,0,0] as Instruction of STC N by TARSKI:def 2;
  set p1 = q +* (loc .--> I);
  set p2 = q +* (loc .--> halt STC N);
  reconsider P1 = P +* (loc .--> I)
   as Instruction-Sequence of STC N;
  reconsider P2 = P +* (loc .--> halt STC N)
   as Instruction-Sequence of STC N;
A5: loc in dom (loc .--> halt STC N) by TARSKI:def 1;
A7: loc in dom (loc .--> I) by TARSKI:def 1;
A8: dom q misses dom (loc .--> halt STC N) by A3,ZFMISC_1:50;
A9: dom q misses dom (loc .--> I) by A3,ZFMISC_1:50;
A10: p1 c= P1 by A2,FUNCT_4:123;
A11: p2 c= P2 by A2,FUNCT_4:123;
  set Cs2i = Comput(P2,s,i), Cs1i = Comput(P1,s,i);
  p is not q-autonomic
  proof
    (loc .--> halt STC N).loc = halt STC N by FUNCOP_1:72;
    then
A12:  P2.loc = halt STC N by A5,FUNCT_4:13;
    (loc .--> I).loc = I by FUNCOP_1:72;
    then
A13:  P1.loc = I by A7,FUNCT_4:13;
    take P1, P2;
    q c= p1 by A9,FUNCT_4:32;
    hence
A14:  q c= P1 by A10,XBOOLE_1:1;
    q c= p2 by A8,FUNCT_4:32;
    hence
A15: q c= P2 by A11,XBOOLE_1:1;
    take s, s;
    thus  p c= s by A1;
A16: (Cs1i|dom  p) = (Csi|dom  p) by A14,A2,A1,EXTPRO_1:def 10;
    thus  p c= s by A1;
A17: (Cs1i|dom  p) = (Cs2i|dom  p) by A14,A15,A1,EXTPRO_1:def 10;
    take k = i+1;
    set Cs1k = Comput(P1,s,k);
A18: Cs1k = Following(P1,Cs1i) by EXTPRO_1:3
      .= Exec (CurInstr(P1,Cs1i), Cs1i);
   InsCode I = 1;
   then
A19:  IC Exec(I,Cs1i) = IC Cs1i + 1 by AMISTD_1:9;
A20: IC Csi = IC(Csi|dom  p) by Th6,FUNCT_1:49;
    then IC Cs1i = loc by A16,Th6,FUNCT_1:49;
    then
A21: IC Cs1k = loc1 by A19,A18,A13,PBOOLE:143;
    set Cs2k = Comput(P2,s,k);
A22: Cs2k = Following(P2,Cs2i) by EXTPRO_1:3
      .= Exec (CurInstr(P2,Cs2i), Cs2i);
A23:  P2/.IC Cs2i = P2.IC Cs2i by PBOOLE:143;
    IC Cs2i = loc by A16,A20,A17,Th6,FUNCT_1:49;
    then
A24: IC Cs2k = loc by A22,A12,A23,EXTPRO_1:def 3;
    IC(Cs1k|dom  p) = IC Cs1k & IC(Cs2k|dom  p) = IC Cs2k
     by Th6,FUNCT_1:49;
    hence thesis by A21,A24;
  end;
  hence contradiction;
end;
end;

registration let N be with_zero set;
 cluster relocable IC-recognized CurIns-recognized
  for halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
 existence
  proof
   take STC N;
   thus thesis;
  end;
end;

reserve
   S for IC-recognized CurIns-recognized
    halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;


theorem
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
 for p being q-autonomic non empty FinPartState of S,
     s1,s2 being State of S st  p c= s1 &  p c= s2
 for P1,P2 being Instruction-Sequence of S
    st q c= P1 & q c= P2
 for i being Nat
 holds IC Comput(P1,s1,i) = IC Comput(P2,s2,i) &
   CurInstr(P1,Comput(P1,s1,i)) = CurInstr(P2,Comput(P2,s2,i))
proof
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic non empty FinPartState of S,
      s1, s2 be State of S such that
A1:  p c= s1 and
A2:  p c= s2;
 let P1,P2 be Instruction-Sequence of S such that
A3: q c= P1 and
A4: q c= P2;
A5: dom q c= dom P1 by A3,RELAT_1:11;
A6: dom q c= dom P2 by A4,RELAT_1:11;
  let i be Nat;
  set Cs2i = Comput(P2,s2,i);
  set Cs1i = Comput(P1,s1,i);
A7: IC Cs1i in dom q by A3,Def4,A1;
A8: IC Cs2i in dom q by A4,Def4,A2;
  thus
A9: IC Cs1i = IC Cs2i
  proof
    assume
A10: IC Comput(P1,s1,i) <> IC Comput(P2,s2,i);
    (Cs1i|dom  p).IC S = Cs1i.IC S & (Cs2i|dom  p).IC S = Cs2i.IC S
    by Th6,FUNCT_1:49;
    hence contradiction by A10,A3,A4,A1,A2,EXTPRO_1:def 10;
  end;
  thus CurInstr(P1,Comput(P1,s1,i))
   = P1.IC Cs1i by A7,A5,PARTFUN1:def 6
  .= q.IC Cs1i by A7,A3,GRFUNC_1:2
  .= P2.IC Cs2i by A8,A4,A9,GRFUNC_1:2
  .= CurInstr(P2,Comput(P2,s2,i)) by A8,A6,PARTFUN1:def 6;
end;

reserve S for relocable IC-recognized CurIns-recognized
     halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;

theorem
  for k being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
   for p being q-autonomic FinPartState of S
  st IC S in dom p
 for s being State of S st  p c= s
 for P being Instruction-Sequence of S
   st q c= P
  for i being Nat
   holds  Comput(P +* Reloc(q,k),s +* IncIC( p,k),i) =
     IncIC(Comput(P,s,i),k)
proof
  let k be Nat;
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
 let p be q-autonomic FinPartState of S such that
A1: IC S in dom p;
  let s be State of S such that
A2:  p c= s;
  let P be Instruction-Sequence of S;
  assume
A3: q c= P;
  defpred P[Nat] means
    Comput(P+*Reloc(q,k),s+*IncIC( p,k),$1) =
     IncIC(Comput(P,s,$1),k);
A4: for i being Nat st P[i] holds P[i+1]
  proof
    let i be Nat such that
A5:  Comput(P+*Reloc(q,k),s+*IncIC( p,k),i)
     =  IncIC(Comput(P,s,i),k);
    reconsider kk = IC Comput(P,s,i) as Nat;
A6: IC S in dom Start-At (IC Comput(P,s,i) +k,S) by TARSKI:def 1;
A7: IC (IncIC(Comput(P,s,i),k))
     = IC Start-At (IC Comput(P,s,i) +k,S) by A6,FUNCT_4:13
    .= IC Comput(P,s,i) + k by FUNCOP_1:72;
    p is not empty by A1;
    then
A8: IC Comput(P,s,i) in dom q by A3,Def4,A2;
    then
A9: IC Comput(P,s,i) in dom IncAddr(q,k) by COMPOS_1:def 21;
A10: q/.kk = q.IC Comput(P,s,i) by A8,PARTFUN1:def 6
      .= P.IC Comput(P,s,i) by A8,A3,GRFUNC_1:2;
    reconsider kk = IC Comput(P,s,i) as Nat;
A11:  (IC Comput(P,s,i) +k)
     in dom Reloc(q,k) by A8,COMPOS_1:46;
A12: CurInstr(P+*Reloc(q,k),
         Comput(P+*Reloc(q,k),s+*IncIC( p,k),i))
   = (P+*Reloc(q,k)).
         IC Comput(P+*Reloc(q,k),s+*IncIC( p,k),i)
             by PBOOLE:143
      .= Reloc(q,k).(IC Comput(P,s,i) +k) by A5,A7,A11,FUNCT_4:13
      .= IncAddr(q,k).kk by A9,VALUED_1:def 12
      .= IncAddr((q)/.kk,k) by A8,COMPOS_1:def 21
      .= IncAddr (CurInstr(P,Comput(P,s,i)),k) by A10,PBOOLE:143;
    thus  Comput(P+*Reloc(q,k),
       s+*IncIC( p,k),i+1)
     =  Following(P+*Reloc(q,k),
         Comput(P+*Reloc(q,k),s+*IncIC( p,k),i))
              by EXTPRO_1:3
    .=  IncIC(Following(P,Comput(P,s,i)),k) by A5,A12,Th4
    .=  IncIC(Comput(P,s,i+1),k) by EXTPRO_1:3;
  end;
A13: IC p = IC s by A2,A1,GRFUNC_1:2;
A14:  DataPart p c=  p by MEMSTR_0:12;
  Comput(P+*Reloc(q,k),s+*IncIC( p,k),0)
    = s +* (DataPart p +* Start-At ((IC p) +k,S)) by A1,MEMSTR_0:56
   .= s +* DataPart p +* Start-At ((IC p) +k,S) by FUNCT_4:14
    .= IncIC(Comput(P,s,0),k) by A13,A14,A2,FUNCT_4:98,XBOOLE_1:1;
  then
A15: P[0];
  thus for i being Nat holds P[i] from NAT_1:sch 2(A15,A4);
end;

theorem Th9:
  for k being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic FinPartState of S st IC S in dom p
  for s being State of S st IncIC(p,k) c= s holds
  for P being Instruction-Sequence of S
   st Reloc(q,k) c= P
  for i being Nat holds  Comput(P,s,i) =
     IncIC(Comput(P+*q,s+* p,i),k)
proof
  let k be Nat;
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic FinPartState of S such that
A1: IC S in dom p;
  let s be State of S such that
A2: IncIC(p,k) c= s;
  let P be Instruction-Sequence of S such that
A3: Reloc(q,k) c= P;
  defpred Z[Nat] means  Comput(P,s,$1) =
    IncIC(Comput(P+*q,s+* p,$1),k);
A4: for i being Nat st Z[i] holds Z[i+1]
  proof
    let i be Nat such that
A5:  Comput(P,s,i) =
      IncIC(Comput(P+*q,s+* p,i),k);
    reconsider kk = IC Comput(P+*q,s+* p,i) as Nat;
A6: IC S in dom (Start-At (IC Comput(P+*q,s+* p,i) +k,S)) by TARSKI:def 1;
A7:  p c= s+* p by FUNCT_4:25;
A8: q c= P+*q by FUNCT_4:25;
    p is not empty by A1;
    then
A9: IC Comput(P+*q,s+* p,i) in dom q by Def4,A7,A8;
    then
A10: IC Comput(P+*q,s+* p,i) in dom IncAddr(q,k) by COMPOS_1:def 21;
A11: (IC Comput(P+*q,s+* p,i) +k) in dom Reloc(q,k)
              by A9,COMPOS_1:46;
    reconsider kk = (IC Comput(P+*q,s+* p,i)) as Nat;
A12:  IC Comput(P,s,i)
       = IC(Start-At (IC Comput(P+*q,s+* p,i) +k,S)) by A5,A6,FUNCT_4:13
      .= IC Comput(P+*q,s+* p,i) + k by FUNCOP_1:72;
A13: q c= P+*q by FUNCT_4:25;
A14: (q)/.kk = (q).kk by A9,PARTFUN1:def 6;
A15:  dom(P+*q) = NAT by PARTFUN1:def 2;
    dom P = NAT by PARTFUN1:def 2;
    then
A16: CurInstr(P,Comput(P,s,i))
     = P.IC Comput(P,s,i) by PARTFUN1:def 6
    .= Reloc(q,k).IC Comput(P,s,i) by A3,A11,A12,GRFUNC_1:2
      .= IncAddr(q,k).kk by A10,A12,VALUED_1:def 12
      .= IncAddr((q)/.kk,k) by A9,COMPOS_1:def 21
      .= IncAddr(
          (P+*q).IC Comput(P+*q,s+* p,i)
          ,k) by A9,A14,A13,GRFUNC_1:2
      .= IncAddr(
          CurInstr(P+*q,Comput(P+*q,s+* p,i))
          ,k) by A15,PARTFUN1:def 6;
    thus  Comput(P,s,i+1)
       =  Following(P,Comput(P,s,i)) by EXTPRO_1:3
      .=  IncIC(Following(P+*q,
         Comput(P+*q,s+* p,i)),k) by A5,A16,Th4
      .=  IncIC(Comput(P+*q,s+* p,i+1),k) by EXTPRO_1:3;
  end;
  set IP = Start-At (IC p,S);
A17: dom Start-At(IC p,S) = {IC S};
A18: Start-At (IC p + k,S) c= IncIC(p,k) by MEMSTR_0:55;
A19: IC Comput(P+*q,s+* p,0) = IC p by A1,FUNCT_4:13;
  set DP = DataPart p;
  DataPart IncIC(p,k) c= IncIC(p,k) by RELAT_1:59;
  then DataPart IncIC(p,k) c= s by A2,XBOOLE_1:1;
  then
A20: DataPart p c= s by MEMSTR_0:51;
  set PR = Reloc(q,k);
  set IS = Start-At (IC Comput(P+*q,s+* p,0) +k,S);
A21: dom Start-At (IC Comput(P+*q,s+* p,0) +k,S) = {IC S};
  Comput(P,s,0)
     = s +* IS by A19,A2,A18,FUNCT_4:98,XBOOLE_1:1
    .= s +* DP +* IS by A20,FUNCT_4:98
    .= s+* DP +* IP +* IS by A21,A17,FUNCT_4:74
    .= s +*(DP +* IP) +* IS by FUNCT_4:14
    .= IncIC(Comput(P+*q,s+* p,0),k) by A1,MEMSTR_0:26;
  then
A22: Z[0];
  thus for i being Nat holds Z[i] from NAT_1:sch 2 (A22,A4 );
end;

reserve m,j for Nat;

theorem Th10:
  for k being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being non empty FinPartState of S st IC
  S in dom p
   for s being State of S st  p c= s &
     IncIC(p,k) is Reloc(q,k)-autonomic
   for P being Instruction-Sequence of S
    st q c= P
   for i being Nat holds  Comput(P,s,i)
   =  DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k)
proof
  let k be Nat;
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be non empty FinPartState of S;
  assume
A1:  IC S in dom p;
  then
A2: Start-At (IC p,S) c=  p by FUNCOP_1:84;
  let s be State of S such that
A3:  p c= s and
A4: IncIC(p,k) is Reloc(q,k)-autonomic;
  let P be Instruction-Sequence of S such that
A5: q c= P;
  defpred Z[Nat] means  Comput(P,s,$1) =
    DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),$1),k);
A6: for i being Nat st Z[i] holds Z[i+1]
  proof
    reconsider pp = q as preProgram of S;
    let i be Nat such that
A7:  Comput(P,s,i) =
       DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k);
    reconsider kk = IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) as Nat;
    reconsider jk = IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) as Nat;
A8: IncIC(p,k) c= s+*IncIC(p,k) by FUNCT_4:25;
A9: Reloc(q,k) c= P+*Reloc(q,k) by FUNCT_4:25;

A10: IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) in dom
          Reloc(q,k) by A4,Def4,A8,A9;
    then
A11: jk in { j+k where j is Nat : j in dom q } by COMPOS_1:33;
A12: IC S in dom (Start-At (IC Comput(P+*Reloc(q,k),s+*
        IncIC(p,k),i) -'k,S))
    by TARSKI:def 1;
    consider j being Nat such that
A13: jk = j+k and
A14: j in dom q by A11;
A15:  dom(P+*Reloc(q,k)) = NAT by PARTFUN1:def 2;
A16: Reloc(q,k) c= P+*Reloc(q,k) by FUNCT_4:25;
A17:  Reloc(q,k) = IncAddr(Shift(q,k),k) by COMPOS_1:34;
    dom Shift(pp, k) = { m+k where m is Nat : m in dom pp} by VALUED_1:def 12;
    then
A18: (j+k) in dom Shift(q, k) by A14;
    then
A19: IncAddr(Shift(q, k)/.kk,k)
    = Reloc(q,
    k). IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) by A13,A17,COMPOS_1:def 21
      .= (P+*Reloc(q,k)).
         IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i)
           by A10,A16,GRFUNC_1:2
      .= CurInstr(P+*Reloc(q,k),
         Comput(P+*Reloc(q,k),s+*IncIC(p,k),i))
           by A15,PARTFUN1:def 6;
A20: j+k -' k = j by NAT_D:34;
A21:  dom P = NAT by PARTFUN1:def 2;
A22: IC ( DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k)
      )
      = (Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) -'k,S)).IC S
       by A12,FUNCT_4:13
      .= IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) -' k by FUNCOP_1:72;
    CurInstr(P,Comput(P,s,i))
     = P.IC Comput(P,s,i)
        by A21,PARTFUN1:def 6
    .= (q).IC Comput(P,s,i)
        by A7,A13,A14,A20,A5,A22,GRFUNC_1:2
    .= Shift(q, k).
        (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i))
         by A13,A14,A20,A7,A22,VALUED_1:def 12
    .= Shift(q, k)/.kk by A13,A18,PARTFUN1:def 6;
    then
A23: Comput(P+*Reloc(q,k),s+*IncIC(p,k),i+1)
 = Following(P+*Reloc(q,k),
 Comput(P+*Reloc(q,k),s+*IncIC(p,k),i)) &
  Exec(CurInstr(P,Comput(P,s,i)),
 DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k))
 =  DecIC(Following(P+*Reloc(q,k),
 Comput(P+*Reloc(q,k),s +*IncIC(p,k),i)),k)
  by A13,A19,Th5,EXTPRO_1:3;
    thus  Comput(P,s,i+1)
     =  Following(P,Comput(P,s,i)) by EXTPRO_1:3
    .=  DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i+1),k)
    by A7,A23;
  end;
A24: IC S in dom IncIC(p,k) by MEMSTR_0:52;
A25: IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0) = IC IncIC(p,k)
             by A24,FUNCT_4:13;
A26: DataPart p c=  p by RELAT_1:59;
  set DP = DataPart p;
  set IP = Start-At((IC p)+k,S);
  set PP = q;
  set IS = Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0) -'k,S);
A27: dom Start-At((IC p)+k,S) = {IC S};
  set PR = Reloc(q,k);
  set SD = s|(dom Reloc(q,k));
A28: {IC S} misses dom DataPart p by MEMSTR_0:4;
A29: dom Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0
) -'k,S) = {IC S};
A30: dom IP misses dom DP by A28;
A31: IP +* DP = DP +* IP by A30,FUNCT_4:35
      .= IncIC(p,k) by A1,MEMSTR_0:56;
   Comput(P,s,0)
     = s +* Start-At(IC p,S) by A3,A2,FUNCT_4:98,XBOOLE_1:1
    .= s +* Start-At (IC p + k -'k,S) by NAT_D:34
    .= s +* IS by A25,MEMSTR_0:53
    .= s +* DP +* IS by A26,A3,FUNCT_4:98,XBOOLE_1:1
    .= s +* DP +* IP +* IS by A29,A27,FUNCT_4:74
    .= s +*(DP +* IP) +* IS by FUNCT_4:14
    .= DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),0),k)
              by A31,A27,A28,FUNCT_4:35;
  then
A32: Z[0];
  thus for i being Nat holds Z[i] from NAT_1:sch 2 (A32, A6);
end;

theorem Th11:
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being non empty FinPartState of S st IC S in dom p
  for k being Nat holds
   p is q-autonomic iff IncIC(p,k) is Reloc(q,k)-autonomic
proof
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be non empty FinPartState of S such that
A1: IC S in dom p;
  let k be Nat;
  hereby
    assume
A2: p is q-autonomic;
    thus IncIC(p,k) is Reloc(q,k)-autonomic
    proof
     let P,Q be Instruction-Sequence of S such that
A3:   Reloc(q,k) c= P and
A4:   Reloc(q,k) c= Q;
      let s1,s2 be State of S such that
A5:    IncIC(p,k) c= s1 and
A6:    IncIC(p,k) c= s2;
      let i be Nat;
A7:   dom (Start-At ((IC Comput(Q+*q,s2+* p,i))+k,S)) = {IC S};
A8:   dom(DataPart p) misses
       dom (Start-At (IC Comput(Q+*q,s2+* p,i) +k,S))
      by MEMSTR_0:4;
A9:  dom (Start-At ((IC Comput(P+*q,s1+* p,i))+k,S)) = {IC S};
A10:  dom(DataPart p) misses
       dom (Start-At (IC Comput(P+*q,s1+* p,i) +k,S))
      by MEMSTR_0:4;
A11:   q c= P+*q & q c= Q+*q
              by FUNCT_4:25;
       p c= s1 +*  p &  p c= s2 +*  p by FUNCT_4:25;
    then
A12:  Comput(P+*q,s1+* p,i)|dom  p
    = Comput(Q+*q,s2+* p,i) |dom  p
     by A2,A11;
A13:  DataPart p c=  p by MEMSTR_0:12;
A14:  Comput(P,s1,i)|dom (DataPart p)
        = IncIC(Comput(P+*q,s1+* p,i),k) | dom DataPart p by A1,A2,A5,Th9,A3
       .= ( Comput(P+*q,s1+* p,i)) | dom (DataPart p)
         by A10,FUNCT_4:72
        .= ( Comput(Q+*q,s2+* p,i)) | dom (DataPart p)
         by A12,A13,RELAT_1:11,153
        .= ( IncIC(Comput(Q+*q,s2+* p,i),k))|dom DataPart p by A8,FUNCT_4:72
        .= Comput(Q,s2,i)|dom DataPart p by A1,A2,A6,Th9,A4;
A15:  {IC S} c= dom  p by A1,ZFMISC_1:31;
A16:  Start-At (IC Comput(P+*q,s1+* p,i),S)
      = Comput(P+*q,s1+* p,i)|{IC S} by MEMSTR_0:18
        .= Comput(Q+*q,s2+* p,i)|{IC S}
        by A12,A15,RELAT_1:153
        .= Start-At (IC Comput(Q+*q,s2+* p,i),S) by MEMSTR_0:18;
A18:  Comput(P,s1,i)|dom (Start-At((IC p)+k,S))
        = IncIC(Comput(P+*q,s1+* p,i),k)|
              dom (Start-At((IC p)+k,S)) by A1,A2,A5,Th9,A3
       .= Start-At (IC Comput(P+*q,s1+* p,i) +k,S)
         by A9
        .= Start-At (IC Comput(Q+*q,s2+* p,i) +k,S)
              by A16,MEMSTR_0:21
        .= ( IncIC(Comput(Q+*q,s2+* p,i),k))|
                dom (Start-At((IC p)+k,S)) by A7
        .= Comput(Q,s2,i)|dom (Start-At((IC p)+k,S)) by A1,A2,A6,Th9,A4;
A20:  dom  p = {IC S} \/ dom DataPart p by A1,MEMSTR_0:24;
A21: Comput(P,s1,i)|dom  p
       = Comput(P,s1,i)|{IC S}
          \/ Comput(P,s1,i)|dom DataPart p by A20,RELAT_1:78
       .= Comput(Q,s2,i)|dom  p
       by A20,A14,A18,RELAT_1:78;
A22:  dom IncIC( p,k)
     = dom  p \/ dom Start-At((IC p)+k,S) by FUNCT_4:def 1;
A23: Comput(P,s1,i)|dom IncIC( p,k)
     = Comput(P,s1,i)|dom  p
        \/ Comput(P,s1,i)|dom Start-At((IC p)+k,S) by A22,RELAT_1:78
    .= Comput(Q,s2,i)|dom IncIC( p,k)
         by A22,A18,A21,RELAT_1:78;
     thus Comput(P,s1,i)|dom  IncIC(p,k)
       = Comput(Q,s2,i)|dom  IncIC(p,k) by A23;

    end;
  end;
  assume
A24: IncIC(p,k) is Reloc(q,k)-autonomic;
A25: DataPart p c= IncIC(p,k) by MEMSTR_0:62;
    let P,Q be Instruction-Sequence of S such that
A26: q c= P and
A27: q c= Q;
A28: Reloc(q,k) c= P +* Reloc(q,k) &
    Reloc(q,k) c= Q +* Reloc(q,k)
         by FUNCT_4:25;
    let s1,s2 be State of S such that
A29:  p c= s1 and
A30:  p c= s2;
    let i be Nat;
     IncIC(p,k) c= s1 +*  IncIC(p,k) &
     IncIC(p,k) c= s2 +*  IncIC(p,k) by FUNCT_4:25;
    then
A31: Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)|dom  IncIC(p,k)
     = Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)|dom  IncIC(p,k)
           by A24,A28;
A32: dom (Start-At ((IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)) -'k,S))
       = {IC S};
A33: dom(DataPart p) misses
 dom(Start-At (IC Comput(Q+*Reloc(q,k),s2+*IncIC(p,k),i) -'k,S))
         by MEMSTR_0:4;
A34: dom (Start-At ((IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)) -'k,S))
      = {IC S};
A35: dom(DataPart p) misses
     dom(Start-At (IC Comput(P+*Reloc(q,k),s1+*IncIC(p,k),i) -'k,S))
           by MEMSTR_0:4;
A36: Comput(P,s1,i)|dom (DataPart p)
    = ( DecIC(Comput(P+*Reloc(q,k),s1+*IncIC(p,k)
    ,i),k)) | dom(DataPart p) by A1,A24,A29,Th10,A26
      .= ( Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)) | dom
(DataPart p) by A35,FUNCT_4:72
      .= ( Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)) | dom
(DataPart p) by A31,A25,RELAT_1:11,153
      .= DecIC(Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i),k)
     | dom(DataPart p) by A33,FUNCT_4:72
      .= Comput(Q,s2,i)|dom (DataPart p) by A1,A24,A30,Th10,A27;
    IC S in dom  IncIC(p,k) by MEMSTR_0:52;
    then
A37: {IC S} c= dom IncIC(p,k) by ZFMISC_1:31;
A38: Start-At (IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i),
S) = Comput(P+*Reloc(q,k),s1+*
    IncIC(p,k),i)|{IC S} by MEMSTR_0:18
      .= Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)|{IC S}
        by A31,A37,RELAT_1:153
      .= Start-At (IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k)
,i),S) by MEMSTR_0:18;
A40: Comput(P,s1,i)|dom (Start-At(IC p,S))
     = ( DecIC(Comput(P+*Reloc(q,k),s1+*IncIC(p,k),i),k))
         |dom (Start-At(IC p,S)) by A1,A24,A29,Th10,A26
      .= Start-At (IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k)
,i) -'k,S) by A34
      .= Start-At (IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i) -'k,S)
       by A38,MEMSTR_0:22
      .= DecIC(Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i),k)
     |dom (Start-At(IC p,S))
     by A32
      .= Comput(Q,s2,i)|dom Start-At(IC p,S) by A1,A24,A30,Th10,A27;
    thus Comput(P,s1,i)|dom  p
     = Comput(P,s1,i)|dom(Start-At(IC p,S) +*
          DataPart p ) by A1,MEMSTR_0:19
      .= Comput(P,s1,i)|(dom (Start-At(IC p,S)) \/ dom (DataPart p))
          by FUNCT_4:def 1
      .= Comput(Q,s2,i)|dom (Start-At(IC p,S)) \/
            Comput(Q,s2,i)|dom (DataPart p) by A36,A40,RELAT_1:78
      .= Comput(Q,s2,i)|(dom (Start-At(IC p,S)) \/ dom DataPart p)
           by RELAT_1:78
      .= Comput(Q,s2,i)|dom (Start-At(IC p,S) +* DataPart p) by FUNCT_4:def 1
      .= Comput(Q,s2,i)|dom  p by A1,MEMSTR_0:19;
end;

definition let N,S;
 attr S is relocable1 means
:Def5: for k being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic non empty FinPartState of S,
      s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2
  for P1,P2 being Instruction-Sequence of S
   st q c= P1 & Reloc(q,k) c= P2
  for i being Nat
   holds IncAddr(CurInstr(P1,Comput(P1,s1,i)),k)
       = CurInstr(P2,Comput(P2,s2,i));
 attr S is relocable2 means
:Def6: for k being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
   for p being q-autonomic non empty FinPartState of S,
      s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2
  for P1,P2 being Instruction-Sequence of S
   st q c= P1 & Reloc(q,k) c= P2
  for i being Nat holds
   Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p;
end;

Lm1: for k being Nat
 for q be non halt-free finite
  (the InstructionsF of STC N)-valued NAT-defined Function
  for p being non empty q-autonomic FinPartState of STC N , s1,
    s2 being State of STC N st p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of STC N
 st q c= P1 & Reloc(q,k) c= P2
for i being Nat holds
 IC Comput(P1,s1,i) + k = IC Comput(P2,s2,i) &
IncAddr(CurInstr(P1,Comput(P1,s1,i)), k)
 = CurInstr(P2,Comput(P2,s2,i))
proof
  let k be Nat;
 let q be non halt-free finite
  (the InstructionsF of STC N)-valued NAT-defined Function;
  let p be non empty q-autonomic FinPartState of STC N,
      s1,s2 be State of STC N such that
A1:  p c= s1 and
A2: IncIC( p,k) c= s2;
A3: IC STC N in dom p by Th6;
  let P1,P2 being Instruction-Sequence of STC N
  such that
A4: q c= P1 & Reloc(q,k) c= P2;
  set s3 = s1 +* DataPart s2;
  defpred Z[Nat] means
   IC Comput(P1,s1,$1) + k = IC Comput(P2,s2,$1) &
 IncAddr(CurInstr(P1,Comput(P1,s1,$1)), k)
 = CurInstr(P2,Comput(P2,s2,$1));
A5: for i be Nat st Z[i] holds Z[i+1]
  proof
    set DPp = DataPart p;
    let i be Nat such that
A6: IC Comput(P1,s1,i) + k = IC Comput(P2,s2,i) and
A7: IncAddr (CurInstr(P1,Comput(P1,s1,i)), k)
    = CurInstr(P2,Comput(P2,s2,i));
    set Cs2i1 = Comput(P2,s2,i+1);
    set Cs3i = Comput(P1,s3,i);
    set Cs2i = Comput(P2,s2,i);
    set Cs3i1 = Comput(P1,s3,i+1);
    set Cs1i1 = Comput(P1,s1,i+1);
    set Cs1i = Comput(P1,s1,i);
A8: now
      reconsider loc = IC Cs1i1 as Nat;
      assume
A9:  IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1);
      reconsider kk = loc as Nat;
A10:  loc in dom q by Def4,A4,A1;
A11:  loc + k in dom Reloc(q, k) by A10,COMPOS_1:46;
A12: dom P2 = NAT by PARTFUN1:def 2;
      dom P1 = NAT by PARTFUN1:def 2;
      then CurInstr(P1, Cs1i1) = P1.loc by PARTFUN1:def 6
        .= (q).loc by A10,A4,GRFUNC_1:2;

      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = Reloc(q,k).(loc+k) by A10,COMPOS_1:35
      .= P2.IC Comput(P2,s2,i+1) by A9,A11,A4,GRFUNC_1:2
      .= CurInstr(P2,Comput(P2,s2,i+1)) by A12,PARTFUN1:def 6;
    end;
    set I = CurInstr(P1, Cs1i);
A13: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
      .= Exec (CurInstr(P2, Cs2i), Cs2i);
    reconsider j = IC Cs1i as Nat;
A14: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
      .= Exec (CurInstr(P1, Cs1i), Cs1i);
A15:  the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
    per cases by A15,TARSKI:def 2;
    suppose
      I = [0,0,0];
      then
A16:  I = halt STC N;
      thus IC Comput(P1,s1,i+1) + k = IC Cs1i + k
       by A14,A16,EXTPRO_1:def 3
        .= IC Comput(P2,s2,i+1) by A6,A13,A16,A7,EXTPRO_1:def 3;
      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1)) by A8;
    end;
    suppose
      I = [1,0,0];
      then
A17:    InsCode I = 1;
      then
A18:   Exec(I,Cs2i) = IncIC(Cs2i,1) by AMISTD_1:20;
      thus IC Comput(P1,s1,i+1) + k = IC Cs1i + 1 + k
         by A14,A17,AMISTD_1:9
        .= IC Exec(I,Cs2i) by A18,A6,MEMSTR_0:53
        .= IC Comput(P2,s2,i+1) by A13,A7,COMPOS_0:4;
      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1)) by A8;
    end;
  end;
A19: IC STC N in dom IncIC( p,k) by MEMSTR_0:52;
  now
    thus IC Comput(P1,s1,0) + k
       = IC  p + k by A1,A3,GRFUNC_1:2
      .= IC IncIC(p,k) by MEMSTR_0:53
      .= IC Comput(P2,s2,0) by A2,A19,GRFUNC_1:2;
    reconsider loc = IC  p as Nat;
A20: IC  p = IC s1 by A1,A3,GRFUNC_1:2;
    IC  p = IC Comput(P1,s1,0) by A1,A3,GRFUNC_1:2;
    then
A21: loc in dom q by Def4,A4,A1;
A22: (IC  p) + k in dom Reloc(q,k) by A21,COMPOS_1:46;
A23: IC STC N in dom IncIC( p,k) by MEMSTR_0:52;
A24: (q).IC  p = P1.IC s1 by A20,A21,A4,GRFUNC_1:2;
    dom P2 = NAT by PARTFUN1:def 2;
    then
A25:  CurInstr(P2,Comput(P2,s2,0))
      = P2.IC Comput(P2,s2,0) by PARTFUN1:def 6
     .= P2.IC IncIC( p,k) by A2,A23,GRFUNC_1:2
      .= P2.((IC p) +k) by MEMSTR_0:53
      .= (Reloc(q, k)).((IC  p) +k) by A22,A4,GRFUNC_1:2;
A26:  dom P1 = NAT by PARTFUN1:def 2;
     CurInstr(P1,Comput(P1,s1,0)) = P1.IC s1 by A26,PARTFUN1:def 6;
    hence
    IncAddr(CurInstr(P1,Comput(P1,s1,0)), k)
     = CurInstr(P2,Comput(P2,s2,0)) by A25,A21,A24,COMPOS_1:35;
  end;
  then
A27: Z[0];
  thus for i being Nat holds Z[i] from NAT_1:sch 2(A27,A5);
end;

registration let N;
 cluster STC N -> relocable1 relocable2;
 coherence
  by Lm1;
end;

registration let N be with_zero set;
 cluster relocable1 relocable2
   for relocable IC-recognized CurIns-recognized
     halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
 existence
  proof
   take STC N;
   thus thesis;
  end;
end;

reserve S for relocable1 relocable2
  relocable IC-recognized CurIns-recognized halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;

theorem Th12:
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic non empty FinPartState of S,
      k being Nat st IC S in dom p
   holds p is q-halted iff IncIC(p,k) is Reloc(q,k)-halted
proof
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic non empty FinPartState of S,
      k be Nat;
  assume
 IC S in dom p;
  hereby
    assume
A1: p is q-halted;
    thus IncIC(p,k) is Reloc(q,k)-halted
    proof
      let t be State of S;
      assume
A2:    IncIC(p,k) c= t;
      let P be Instruction-Sequence of S such that
A3:   Reloc(q,k) c= P;
      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 s by A1,A4;
      then consider u being Nat such that
A6:   CurInstr(Q,Comput(Q,s,u)) = halt S;
      take u;
     dom P = NAT by PARTFUN1:def 2;
    hence IC Comput(P,t,u) in dom P;
      CurInstr(P,Comput(P,t,u))
       = IncAddr(halt S, k) by A2,A6,Def5,A3,A4,A5
        .= halt S by COMPOS_0:4;
      hence thesis;
    end;
  end;
  assume
A7: IncIC(p,k) is Reloc(q,k)-halted;
  let t be State of S;
  assume
A8:  p c= t;
  let P be Instruction-Sequence of S such that
A9: q c= P;
  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 s by A7,A10;
  then consider u being Nat such that
A12: CurInstr(Q,Comput(Q,s,u)) = halt S;
  take u;
   dom P = NAT by PARTFUN1:def 2;
  hence IC Comput(P,t,u) in dom P;
  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;
end;

theorem Th13:
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being q-halted q-autonomic non empty FinPartState of S
   st IC S in dom p
  for k being Nat holds DataPart(Result(q, p)) =
   DataPart Result(Reloc(q,k),IncIC( p,k))
proof
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-halted q-autonomic non empty FinPartState of S
  such that
A1: IC S in dom p;
  let k be Nat;
  consider s being State of S such that
A2: p c= s by PBOOLE:141;
  consider P being
   Instruction-Sequence of S
   such that
A3: q c= P by PBOOLE:145;
A4: IncIC(p,k) is Reloc(q,k)-halted Reloc(q,k)-autonomic by A1,Th12,Th11;
A5: IncIC( p,k) is Autonomy of Reloc(q,k)
       by A4,EXTPRO_1:def 12;
  P halts_on s by A2,A3,EXTPRO_1:def 11;
  then consider j1 being Nat such that
A6: Result(P,s) = Comput(P,s,j1) and
A7: CurInstr(P, Result(P,s)) = halt S by EXTPRO_1:def 9;
  consider t being State of S such that
A8: IncIC( p,k) c= t by PBOOLE:141;
  consider Q being
   Instruction-Sequence of S
   such that
A9: Reloc(q,k) c= Q by PBOOLE:145;
  Q.(IC Comput(Q,t,j1)) = CurInstr(Q,Comput(Q,t,j1)) by PBOOLE:143
    .= IncAddr(CurInstr(P,Comput(P,s,j1)), k)
     by Def5,A3,A9,A2,A8
    .= halt S by A6,A7,COMPOS_0:4;
  then
A10: Result(Q,t) = Comput(Q,t,j1) by EXTPRO_1:7;
A11: Comput(Q,t,j1) | dom DataPart p
        = Comput(P,s,j1) | dom DataPart p
         by Def6,A9,A3,A8,A2;
A12: DataPart p = DataPart IncIC( p,k) by MEMSTR_0:51;
A13:  p is Autonomy of q by EXTPRO_1:def 12;
  thus DataPart(Result(q, p))
     = DataPart((Result(P,s)) | dom  p) by A2,A3,A13,EXTPRO_1:def 13
    .= (Result(P,s)) | (dom  p /\ Data-Locations S) by RELAT_1:71
    .= (Result(P,s)) | dom DataPart p by MEMSTR_0:14
    .= (Result(Q,t))|(dom IncIC( p,k) /\ Data-Locations S)
          by A6,A10,A11,A12,MEMSTR_0:14
    .= ((Result(Q,t)) | dom IncIC( p,k))|Data-Locations S
           by RELAT_1:71
    .= DataPart Result(Reloc(q,k),IncIC( p,k))
       by A5,A9,A8,EXTPRO_1:def 13;
end;

registration let N,S;
  let q be non halt-free finite
   (the InstructionsF of S)-valued NAT-defined Function;
  let p be q-autonomic q-halted non empty FinPartState of S,
    k be Nat;
  cluster IncIC(p,k) -> Reloc(q,k)-halted;
  coherence
   proof
     IC S in dom p by Th6;
    hence thesis by Th12;
   end;
end;

theorem
  for F being data-only PartFunc of FinPartSt S, FinPartSt S,
      l being Nat
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function,
      p being q-autonomic q-halted non empty FinPartState of S
        st IC S in dom p
  for k being Nat holds q,  p computes F
    iff Reloc(q,k), IncIC( p,k) computes F
proof
  let F be data-only PartFunc of FinPartSt S ,FinPartSt S,
      l be Nat;
  let q be non halt-free finite
    (the InstructionsF of S)-valued NAT-defined Function,
      p be q-autonomic q-halted non empty FinPartState of S
  such that
A1: IC S in dom p;
  let k be Nat;
  hereby
    assume
A2: q,  p computes F;
    thus Reloc(q,k), IncIC( p,k) computes F
    proof
      let x be set;
      assume
A3:   x in dom F;
      then consider d1 being FinPartState of S such that
A4:   x = d1 and
A5:    p +* d1 is Autonomy of q and
A6:   F.d1 c= Result(q, p +* d1) by A2;
      dom F c= FinPartSt S by RELAT_1:def 18;
      then reconsider d = x as FinPartState of S by A3,MEMSTR_0:76;
      reconsider d as data-only FinPartState of S by A3,MEMSTR_0:def 17;
      dom(p +* d) = dom p \/ dom d by FUNCT_4:def 1;
      then
A7:   IC S in dom(p +* d) by A1,XBOOLE_0:def 3;
A8:  p+*d is q-autonomic by A4,A5,EXTPRO_1:def 12;
    then
A9:   IncIC((p +* d) ,k) is Reloc(q,k)-autonomic by A7,Th11;
A10:    p+*d is q-halted by A4,A5,EXTPRO_1:def 12;
  reconsider pd = p +* d
   as q-halted q-autonomic non empty FinPartState of S
         by A4,A5,EXTPRO_1:def 12;
A11:   DataPart(Result(q, pd))
     = DataPart Result(Reloc(q,k),IncIC((p+*d),k)) by A7,Th13
    .= DataPart Result(Reloc(q,k),IncIC(p,k) +* d)
            by MEMSTR_0:54;
      reconsider Fs1 = F.d1 as FinPartState of S by A6;
      take d;
      thus x=d;
   IncIC(p,k) +* d = IncIC(p+*d ,k) by MEMSTR_0:54;
      hence IncIC( p,k) +* d is Autonomy of Reloc(q,k)
            by A8,A10,A9,EXTPRO_1:def 12;
A12:  Fs1 is data-only by A3,A4,MEMSTR_0:def 17;
      F.d1 c= DataPart Result(Reloc(q,k),IncIC(p,k) +* d)
         by A6,A12,A4,A11,MEMSTR_0:5;
      hence F.d c= Result(Reloc(q,k),IncIC( p,k) +* d)
      by A4,A12,MEMSTR_0:5;
    end;
  end;
  assume
A13: Reloc(q,k), IncIC( p,k) computes F;
  let x be set;
  assume
A14: x in dom F;
  then consider d1 being FinPartState of S such that
A15: x = d1 and
A16: IncIC(p,k) +* d1 is Autonomy of Reloc(q,k) and
A17: F.d1 c= Result(Reloc(q,k),IncIC(p,k) +* d1)
          by A13;
  dom F c= FinPartSt S by RELAT_1:def 18;
  then reconsider d = x as FinPartState of S by A14,MEMSTR_0:76;
  reconsider d as data-only FinPartState of S by A14,MEMSTR_0:def 17;
A18: dom(p +* d) = dom p \/ dom d by FUNCT_4:def 1;
  then
A19: IC S in dom(p +* d) by A1,XBOOLE_0:def 3;
A20: IncIC(p,k) +* d = IncIC((p +* d),k) by MEMSTR_0:54;
 IncIC(p+*d,k) is Reloc(q,k)-autonomic
  by A15,A16,A20,EXTPRO_1:def 12;
  then
A21: p +* d is q-autonomic by A19,Th11;
A22:  IncIC(p+*d,k) is Reloc(q,k)-halted
 by A15,A16,A20,EXTPRO_1:def 12;
A23: p +* d is q-halted by A19,Th12,A21,A22;
  reconsider pd = p +* d
   as q-halted q-autonomic non empty FinPartState of S
    by A19,Th12,A21,A22;
A24: IC S in dom pd by A18,A1,XBOOLE_0:def 3;
A25: DataPart Result(Reloc(q,k),IncIC(p,k) +* d1)
   = DataPart Result(Reloc(q,k),IncIC(p +* d,k)) by A15,MEMSTR_0:54
  .= DataPart(Result(q, p+*d)) by Th13,A24;
  take d;
  thus x=d;
  thus  p +* d is Autonomy of q by A21,A23,EXTPRO_1:def 12;
  reconsider Fs1 = F.d1 as FinPartState of S by A17;
A26: Fs1 is data-only by A14,A15,MEMSTR_0:def 17;
  then F.d1 c= DataPart Result(q, p +* d)
   by A25,A17,MEMSTR_0:5;
  hence thesis by A15,A26,MEMSTR_0:5;
end;

reserve S for IC-recognized CurIns-recognized halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;

theorem
 for q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function
  for p being q-autonomic
   FinPartState of S st IC S in dom p holds IC p in dom q
proof
 let q be non halt-free finite
  (the InstructionsF of S)-valued NAT-defined Function;
 let p be q-autonomic FinPartState of S;
 assume
A1: IC S in dom p;
  then
A2: p is non empty;
  consider s being State of S such that
A3: p c= s by PBOOLE:141;
  set P = (the Instruction-Sequence of S) +* q;
A4: q c= P by FUNCT_4:25;
   IC Comput(P,s,0) in dom q by A4,Def4,A2,A3;
 hence  IC p in dom q by A3,A1,GRFUNC_1:2;
end;

definition
  let N be with_zero set;
  let S be halting IC-Ins-separated non empty with_non-empty_values
         AMI-Struct over N;
  let k be Nat;
  let F be NAT-defined (the InstructionsF of S)-valued Function;
  attr F is k-halting means
 for s being k-started State of S
  for P being Instruction-Sequence of S st F c= P
   holds P halts_on s;
end;

registration
  let N be with_zero set;
  let S be halting IC-Ins-separated non empty with_non-empty_values
         AMI-Struct over N;
 cluster parahalting -> 0-halting for
        NAT-defined (the InstructionsF of S)-valued Function;
 coherence;
 cluster 0-halting -> parahalting for
         NAT-defined (the InstructionsF of S)-valued Function;
 coherence;
end;