:: Relocatability
::  by Yasushi Tanaka
::
:: Received June 16, 1994
:: Copyright (c) 1994-2012 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 SUBSET_1, NUMBERS, AMI_1, AMI_3, AMISTD_2, ARYTM_3, GRAPHSP,
      CARD_1, RELAT_1, FUNCT_1, TARSKI, FUNCT_4, XBOOLE_0, FSM_1, CIRCUIT2,
      EXTPRO_1, ARYTM_1, INT_1, XXREAL_0, STRUCT_0, ORDINAL1, RELOC, FINSET_1,
      FINSEQ_1, NAT_1, AMISTD_5, COMPOS_1;
 notations TARSKI, XBOOLE_0,
      XTUPLE_0, SUBSET_1, FINSET_1, NUMBERS, XCMPLX_0, INT_1,
      ORDINAL1, NAT_1, VALUED_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, PBOOLE,
      FINSEQ_1, NAT_D, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_3,
      XXREAL_0, AMISTD_2, AMISTD_5;
 constructors DOMAIN_1, XXREAL_0, AMI_3, NAT_D, PRE_POLY, AMISTD_2,
      VALUED_1, AMI_2, AMISTD_1, AMISTD_5, PBOOLE, MEMSTR_0, RELSET_1,
      XTUPLE_0;
 registrations XBOOLE_0, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS,
      XREAL_0, INT_1, CARD_3, AMI_3, RELAT_1, FUNCT_4, GRFUNC_1, FUNCT_2,
      AMI_6, VALUED_0, AMISTD_2, COMPOS_1, EXTPRO_1, NAT_1, FINSEQ_1, AMISTD_5,
      AMI_5, PBOOLE, MEMSTR_0, COMPOS_0, XTUPLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions FUNCOP_1, COMPOS_1, EXTPRO_1, RELAT_1, TARSKI, AMI_3, AMISTD_2,
      FUNCT_1, AMISTD_5, MEMSTR_0, COMPOS_0, XTUPLE_0;
 theorems AMI_3, GRFUNC_1, NAT_1, TARSKI, FUNCT_4, FUNCT_1, AMI_5, RELAT_1,
      XBOOLE_1, PARTFUN1, VALUED_1, RECDEF_2, FINSEQ_1, COMPOS_1, EXTPRO_1,
      ORDINAL1, AMISTD_2, AMISTD_5, STRUCT_0, MEMSTR_0, AMI_2, COMPOS_0;
 schemes NAT_1;

begin  :: Relocatability

reserve j, k, m for Element of NAT;

registration
 let a,b be Data-Location;
 cluster a:=b -> ins-loc-free;
 coherence;
 cluster AddTo(a,b) -> ins-loc-free;
 coherence;
 cluster SubFrom(a,b) -> ins-loc-free;
 coherence;
 cluster MultBy(a,b) -> ins-loc-free;
 coherence;
 cluster Divide(a,b) -> ins-loc-free;
 coherence;
end;

theorem Th1:
  for k,loc being Nat
  holds IncAddr(SCM-goto loc,k) = SCM-goto (loc + k)
proof
  let k,loc be Nat;
A1: InsCode IncAddr(SCM-goto loc,k) = InsCode SCM-goto loc by COMPOS_0:def 9
     .= 6 by RECDEF_2:def 1
     .= InsCode SCM-goto (loc + k) by RECDEF_2:def 1;
A2: AddressPart IncAddr(SCM-goto loc,k) = AddressPart SCM-goto loc
           by COMPOS_0:def 9
     .= {} by RECDEF_2:def 3
     .= AddressPart SCM-goto (loc + k)by RECDEF_2:def 3;
A3: JumpPart IncAddr(SCM-goto loc,k) = k + JumpPart SCM-goto loc
                   by COMPOS_0:def 9;
  JumpPart IncAddr(SCM-goto loc,k) = JumpPart SCM-goto (loc + k)
   proof
    thus
A4:   dom JumpPart IncAddr(SCM-goto loc,k)
     = dom JumpPart SCM-goto (loc + k) by A1,COMPOS_0:def 5;
A5: JumpPart SCM-goto loc = <*loc*> by RECDEF_2:def 2;
A6: JumpPart SCM-goto(loc+k) = <*loc+k*> by RECDEF_2:def 2;
    let x be set;
    assume
A7:   x in dom JumpPart IncAddr(SCM-goto loc,k);
     dom <*loc+k*> = {1} by FINSEQ_1:2,38;
     then
A8:   x = 1 by A7,A4,A6,TARSKI:def 1;
    thus (JumpPart IncAddr(SCM-goto loc,k)).x
      = k + (JumpPart SCM-goto loc).x by A3,A7,VALUED_1:def 2
     .= loc + k by A5,A8,FINSEQ_1:40
     .= (JumpPart SCM-goto(loc + k)).x by A6,A8,FINSEQ_1:40;
   end;
 hence thesis by A1,A2,COMPOS_0:1;
end;

theorem Th2:
  for k,loc being Nat, a being Data-Location
   holds IncAddr(a=0_goto loc,k) = a=0_goto (loc + k)
proof
  let k,loc be Nat, a be Data-Location;
A1: InsCode IncAddr(a=0_goto loc,k) = InsCode(a=0_goto loc) by COMPOS_0:def 9
     .= 7 by RECDEF_2:def 1
     .= InsCode(a=0_goto(loc + k)) by RECDEF_2:def 1;
A2: AddressPart IncAddr(a=0_goto loc,k) = AddressPart(a=0_goto loc)
           by COMPOS_0:def 9
     .= <*a*> by RECDEF_2:def 3
     .= AddressPart(a=0_goto (loc + k)) by RECDEF_2:def 3;
A3: JumpPart IncAddr(a=0_goto loc,k) = k + JumpPart(a=0_goto loc)
                   by COMPOS_0:def 9;
  JumpPart IncAddr(a=0_goto loc,k) = JumpPart(a=0_goto (loc + k))
   proof
    thus
A4:   dom JumpPart IncAddr(a=0_goto loc,k)
     = dom JumpPart(a=0_goto (loc + k)) by A1,COMPOS_0:def 5;
A5: JumpPart(a=0_goto loc) = <*loc*> by RECDEF_2:def 2;
A6: JumpPart(a=0_goto (loc+k)) = <*loc+k*> by RECDEF_2:def 2;
    let x be set;
    assume
A7:   x in dom JumpPart IncAddr(a=0_goto loc,k);
     dom <*loc+k*> = {1} by FINSEQ_1:2,38;
     then
A8:   x = 1 by A7,A4,A6,TARSKI:def 1;
    thus (JumpPart IncAddr(a=0_goto loc,k)).x
      = k + (JumpPart(a=0_goto loc)).x by A3,A7,VALUED_1:def 2
     .= loc + k by A5,A8,FINSEQ_1:40
     .= (JumpPart(a=0_goto(loc + k))).x by A6,A8,FINSEQ_1:40;
   end;
 hence thesis by A1,A2,COMPOS_0:1;
end;

theorem Th3:
  for k,loc being Nat, a being Data-Location
   holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k)
proof
  let k,loc be Nat, a be Data-Location;
A1: InsCode IncAddr(a>0_goto loc,k) = InsCode(a>0_goto loc) by COMPOS_0:def 9
     .= 8 by RECDEF_2:def 1
     .= InsCode(a>0_goto(loc + k)) by RECDEF_2:def 1;
A2: AddressPart IncAddr(a>0_goto loc,k) = AddressPart(a>0_goto loc)
           by COMPOS_0:def 9
     .= <*a*> by RECDEF_2:def 3
     .= AddressPart(a>0_goto (loc + k)) by RECDEF_2:def 3;
A3: JumpPart IncAddr(a>0_goto loc,k) = k + JumpPart(a>0_goto loc)
                   by COMPOS_0:def 9;
  JumpPart IncAddr(a>0_goto loc,k) = JumpPart(a>0_goto (loc + k))
   proof
    thus
A4:   dom JumpPart IncAddr(a>0_goto loc,k)
     = dom JumpPart(a>0_goto (loc + k)) by A1,COMPOS_0:def 5;
A5: JumpPart(a>0_goto loc) = <*loc*> by RECDEF_2:def 2;
A6: JumpPart(a>0_goto (loc+k)) = <*loc+k*> by RECDEF_2:def 2;
    let x be set;
    assume
A7:   x in dom JumpPart IncAddr(a>0_goto loc,k);
     dom <*loc+k*> = {1} by FINSEQ_1:2,38;
     then
A8:   x = 1 by A7,A4,A6,TARSKI:def 1;
    thus (JumpPart IncAddr(a>0_goto loc,k)).x
      = k + (JumpPart(a>0_goto loc)).x by A3,A7,VALUED_1:def 2
     .= loc + k by A5,A8,FINSEQ_1:40
     .= (JumpPart(a>0_goto(loc + k))).x by A6,A8,FINSEQ_1:40;
   end;
 hence thesis by A1,A2,COMPOS_0:1;
end;

theorem Th4:
  for I being Instruction of SCM, k being Element of NAT st
InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I =
  4 or InsCode I = 5 holds IncAddr (I, k) = I
proof
  let I be Instruction of SCM, k be Element of NAT;
  assume that
A1: InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or
  InsCode I = 4 or InsCode I = 5;
  per cases by A1;
  suppose InsCode I = 0;
   then I = halt SCM by AMI_5:7;
  hence thesis by COMPOS_0:4;
  end;
  suppose InsCode I = 1;
   then ex da,db being Data-Location st I = da:=db by AMI_5:8;
  hence IncAddr(I,k) = I by COMPOS_0:4;
  end;
  suppose InsCode I = 2;
   then ex da,db being Data-Location st I = AddTo(da,db) by AMI_5:9;
   hence IncAddr(I,k) = I by COMPOS_0:4;
  end;
  suppose InsCode I = 3;
   then ex da,db being Data-Location st I = SubFrom(da,db) by AMI_5:10;
  hence IncAddr(I,k) = I by COMPOS_0:4;
  end;
  suppose InsCode I = 4;
   then ex da,db being Data-Location st I = MultBy(da,db) by AMI_5:11;
   hence IncAddr(I,k) = I by COMPOS_0:4;
  end;
  suppose InsCode I = 5;
   then ex da,db being Data-Location st I = Divide(da,db) by AMI_5:12;
   hence IncAddr(I,k) = I by COMPOS_0:4;
  end;
end;

theorem
  for II, I being Instruction of SCM, k being Element of NAT st (
InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I =
  4 or InsCode I = 5) & IncAddr (II, k) = I holds II = I
proof
  let II, I be Instruction of SCM, k be Element of NAT;
  assume that
A1: InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or
  InsCode I = 4 or InsCode I = 5 and
A2: IncAddr (II, k) = I;
   IncAddr(I,k) = I by A1,Th4;
  hence thesis by A2,COMPOS_0:6;
end;

registration
 cluster SCM -> relocable;
 coherence
 proof let INS be Instruction of SCM, j,k be Nat;
   reconsider k as Element of NAT by ORDINAL1:def 12;
  let s be State of SCM;
A1: IC IncIC(Exec(IncAddr(INS,j),s),k)
       = IC Exec(IncAddr(INS,j),s) + k by MEMSTR_0:53
      .= IC Exec(IncAddr(INS,j+k),IncIC(s,k)) by AMISTD_2:def 3;
  per cases by AMI_5:5,NAT_1:32;
  suppose InsCode INS = 0;
    then
A2: INS = halt SCM by AMI_5:7;
    Exec(IncAddr(INS,j+k),IncIC(s,k))
       = Exec(INS,IncIC(s,k)) by A2,COMPOS_0:4
      .= IncIC(s,k) by A2,EXTPRO_1:def 3
      .= IncIC(Exec(IncAddr(INS,j),s),k) by A2,EXTPRO_1:def 3;
   hence thesis;
  end;
  suppose InsCode INS = 1;
    then consider da,db being Data-Location such that
A3: INS = da := db by AMI_5:8;
    now
      let d be Data-Location;
      per cases;
      suppose
A4:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A3,COMPOS_0:4
          .= IncIC(s,k).db by A3,A4,AMI_3:2
          .= s.db by AMI_5:16
          .= Exec(INS, s).d by A3,A4,AMI_3:2
          .= Exec(IncAddr(INS,j), s).d by A3,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
      suppose
A5:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A3,COMPOS_0:4
          .= IncIC(s,k).d by A3,A5,AMI_3:2
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A3,A5,AMI_3:2
          .= Exec(IncAddr(INS,j), s).d by A3,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
    end;
   hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 2;
    then consider da,db being Data-Location such that
A6: INS = AddTo(da, db) by AMI_5:9;
    now let d be Data-Location;
      per cases;
      suppose
A7:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A6,COMPOS_0:4
          .= IncIC(s,k).da + IncIC(s,k).db by A7,A6,AMI_3:3
          .= s.da + IncIC(s,k).db by AMI_5:16
          .= s.da + s.db by AMI_5:16
          .= Exec(INS, s).d by A6,A7,AMI_3:3
          .= Exec(IncAddr(INS,j), s).d by A6,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
      suppose
A8:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A6,COMPOS_0:4
          .= IncIC(s,k).d by A6,A8,AMI_3:3
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A6,A8,AMI_3:3
          .= Exec(IncAddr(INS,j), s).d by A6,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
    end;
   hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 3;
    then consider da,db being Data-Location such that
A9: INS = SubFrom(da, db) by AMI_5:10;
    now let d be Data-Location;
      per cases;
      suppose
A10:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A9,COMPOS_0:4
          .= IncIC(s,k).da - IncIC(s,k).db by A10,A9,AMI_3:4
          .= s.da - IncIC(s,k).db by AMI_5:16
          .= s.da - s.db by AMI_5:16
          .= Exec(INS, s).d by A9,A10,AMI_3:4
          .= Exec(IncAddr(INS,j), s).d by A9,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
      suppose
A11:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A9,COMPOS_0:4
          .= IncIC(s,k).d by A9,A11,AMI_3:4
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A9,A11,AMI_3:4
          .= Exec(IncAddr(INS,j), s).d by A9,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
    end;
    hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 4;
    then consider da,db being Data-Location such that
A12: INS = MultBy(da, db) by AMI_5:11;
    now let d be Data-Location;
      per cases;
      suppose
A13:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A12,COMPOS_0:4
          .= IncIC(s,k).da * IncIC(s,k).db by A13,A12,AMI_3:5
          .= s.da * IncIC(s,k).db by AMI_5:16
          .= s.da * s.db by AMI_5:16
          .= Exec(INS, s).d by A12,A13,AMI_3:5
          .= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
      suppose
A14:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A12,COMPOS_0:4
          .= IncIC(s,k).d by A12,A14,AMI_3:5
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A12,A14,AMI_3:5
          .= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
      end;
    end;
    hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 5;
    then consider da,db being Data-Location such that
A15: INS = Divide(da, db) by AMI_5:12;
     now
      let d be Data-Location;
      per cases;
      suppose
A16:    da <> db;
        hereby
          per cases;
          suppose
A17:        da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A15,COMPOS_0:4
          .= IncIC(s,k).da div IncIC(s,k).db by A16,A17,A15,AMI_3:6
          .= s.da div IncIC(s,k).db by AMI_5:16
          .= s.da div s.db by AMI_5:16
          .= Exec(INS, s).d by A15,A16,A17,AMI_3:6
          .= Exec(IncAddr(INS,j), s).d by A15,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
          end;
          suppose
A18:        db = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A15,COMPOS_0:4
          .= IncIC(s,k).da mod IncIC(s,k).db by A18,A15,AMI_3:6
          .= s.da mod IncIC(s,k).db by AMI_5:16
          .= s.da mod s.db by AMI_5:16
          .= Exec(INS, s).d by A15,A18,AMI_3:6
          .= Exec(IncAddr(INS,j), s).d by A15,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
          end;
          suppose
A19:        da <> d & db <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A15,COMPOS_0:4
          .= IncIC(s,k).d by A15,A19,AMI_3:6
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A15,A19,AMI_3:6
          .= Exec(IncAddr(INS,j), s).d by A15,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
          end;
        end;
      end;
      suppose
A20:    da = db;
          per cases;
          suppose
A21:        da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A15,COMPOS_0:4
          .= IncIC(s,k).da mod IncIC(s,k).db by A20,A21,A15,AMI_3:6
          .= s.da mod IncIC(s,k).db by AMI_5:16
          .= s.da mod s.db by AMI_5:16
          .= Exec(INS, s).d by A15,A20,A21,AMI_3:6
          .= Exec(IncAddr(INS,j), s).d by A15,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
          end;
       suppose
A22:        da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A15,COMPOS_0:4
          .= IncIC(s,k).d by A15,A20,A22,AMI_3:6
          .= s.d by AMI_5:16
          .= Exec(INS, s).d by A15,A20,A22,AMI_3:6
          .= Exec(IncAddr(INS,j), s).d by A15,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
        end;
      end;
    end;
    hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 6;
    then consider loc being Element of NAT such that
A23: INS = SCM-goto loc by AMI_5:13;
A24: IncAddr(INS, j+k) = SCM-goto (loc + (j+k)) by A23,Th1;
A25: IncAddr(INS, j) = SCM-goto (loc + j) by A23,Th1;
    now let d be Data-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A24,AMI_3:7
          .= s.d by AMI_5:16
          .= Exec(IncAddr(INS,j), s).d by A25,AMI_3:7
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
    end;
    hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 7;
    then consider loc being Element of NAT, da being Data-Location such that
A26: INS = da=0_goto loc by AMI_5:14;
A27: IncAddr(INS, j+k) = da=0_goto (loc + (j+k)) by A26,Th2;
A28: IncAddr(INS, j) = da=0_goto (loc + j) by A26,Th2;
    now let d be Data-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A27,AMI_3:8
          .= s.d by AMI_5:16
          .= Exec(IncAddr(INS,j), s).d by A28,AMI_3:8
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
    end;
   hence thesis by A1,AMI_5:25;
  end;
  suppose InsCode INS = 8;
    then consider loc being Element of NAT, da being Data-Location such that
A29: INS = da>0_goto loc by AMI_5:15;
A30: IncAddr(INS, j+k) = da>0_goto (loc + (j+k)) by A29,Th3;
A31: IncAddr(INS, j) = da>0_goto (loc + j) by A29,Th3;
    now let d be Data-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A30,AMI_3:9
          .= s.d by AMI_5:16
          .= Exec(IncAddr(INS,j), s).d by A31,AMI_3:9
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by AMI_5:16;
     end;
   hence thesis by A1,AMI_5:25;
  end;
 end;
end;

begin :: Main theorems of Relocatability

Lm1: for k being Element of NAT
   for q being non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
    p being q-autonomic non empty FinPartState of SCM , s1,
s2 being State of SCM st
   p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of SCM
  st q c= P1 & Reloc(q,k) c= P2
for i being Element of 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)) &
 Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p &
 DataPart Comput(P1,s1 +* DataPart s2,i) = DataPart Comput(P2,s2,i)
proof
  let k be Element of NAT;
  let q be non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
   p be q-autonomic non empty FinPartState of SCM,
      s1,s2 be State
  of SCM such that
A2:  p c= s1 and
A3: IncIC( p,k) c= s2;
A4: IC SCM in dom  p by AMISTD_5:6;
A5:  p c= s1 by A2;
 let P1,P2 being Instruction-Sequence of SCM
  such that
A6: q c= P1 & Reloc(q,k) c= P2;
A7: Reloc(q,k) c= P2 by A6;
A8: q c= P1 by A6;
  set s3 = s1 +* DataPart s2;
  defpred Z[Element of 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)) &
  Comput(P1,s1,$1)|dom DataPart p = Comput(P2,s2,$1)|dom DataPart p &
   DataPart Comput(P1,s3,$1) = DataPart Comput(P2,s2,$1);
A9:  p c= s3 by A2,A3,MEMSTR_0:61;
A10: for i be Element of NAT st Z[i] holds Z[i+1]
  proof
    set DPp = DataPart p;
    let i be Element of NAT such that
A11: IC Comput(P1,s1,i) + k = IC Comput(P2,s2,i) and

A12: IncAddr (CurInstr(P1,Comput(P1,s1,i)), k)
 = CurInstr(P2,Comput(P2,s2,i)) and
A13: Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p and
A14: DataPart Comput(P1,s3,i) = DataPart Comput(P2,s2,i);
    set Cs2i1 = Comput(P2,s2,i+1);
    set Cs3i = Comput(P1,s3,i);
    set Cs2i = Comput(P2,s2,i);
    dom Cs2i1 = the carrier of SCM by PARTFUN1:def 2;
    then
A15: dom Cs2i1 = {IC SCM} \/ Data-Locations SCM by STRUCT_0:4;
    set Cs3i1 = Comput(P1,s3,i+1);
A16: dom DataPart Cs2i = Data-Locations SCM by MEMSTR_0:9;
A17: dom DataPart Cs3i1 = Data-Locations SCM by MEMSTR_0:9;
A18: dom DataPart Cs2i1 = Data-Locations SCM by MEMSTR_0:9;
A19: now
      let x be set;
      assume that
A20:  x in dom DataPart Cs3i1 and
A21:  Cs3i1.x = Cs2i1.x;
      thus (DataPart Cs3i1).x = Cs2i1.x by A20,A21,FUNCT_1:47
        .= (DataPart Cs2i1).x by A17,A18,A20,FUNCT_1:47;
    end;
A22: dom DataPart Cs3i = Data-Locations SCM by MEMSTR_0:9;
A23: now
      let x be set;
      assume that
A24:  x in dom DataPart Cs3i1 and
A25:  Cs3i1.x = Cs3i.x & Cs2i1.x = Cs2i.x;
      (DataPart Cs3i).x = Cs3i.x by A22,A17,A24,FUNCT_1:47;

      hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A14,A16,A17,A19,A24,A25,
FUNCT_1:47;

    end;
A26: now
      let s be State of SCM, d be Data-Location;
      d in Data-Locations SCM by AMI_2:def 16,AMI_3:27;
      hence d in dom DataPart s by MEMSTR_0:9;
    end;
A27: now
      let d be Data-Location;
A28:  d in dom DataPart Cs3i by A26;
      hence Cs3i.d = (DataPart Cs3i).d by FUNCT_1:47
        .= Cs2i.d by A14,A28,FUNCT_1:47;
    end;
    set Cs1i1 = Comput(P1,s1,i+1);
    set Cs1i = Comput(P1,s1,i);
    dom Cs1i1 = the carrier of SCM by PARTFUN1:def 2;
    then
A29: dom Cs1i1 = {IC SCM} \/ Data-Locations SCM by STRUCT_0:4;
    dom DPp = dom p /\ Data-Locations SCM by RELAT_1:61;
    then
A30: dom DPp c= {IC SCM} \/ Data-Locations SCM by XBOOLE_1:10,17;
A31: dom (Cs1i1|dom DPp) = dom Cs1i1 /\ dom DPp by RELAT_1:61
      .= dom DPp by A29,A30,XBOOLE_1:28;
A32: now
      reconsider loc = IC Cs1i1 as Element of NAT;
      assume
A33:  IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1);
      reconsider kk = loc as Element of NAT;
A34:  loc in dom q by A8,A5,AMISTD_5:def 4;
A35:  loc + k in dom Reloc(q, k) by A34,COMPOS_1:46;
A36:   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 A34,A6,GRFUNC_1:2
        .= (q).loc;
      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = Reloc(q,k).(loc+k) by A34,COMPOS_1:35
      .= P2.IC Comput(P2,s2,i+1) by A33,A35,A7,GRFUNC_1:2
      .= CurInstr(P2,Comput(P2,s2,i+1)) by A36,PARTFUN1:def 6;

    end;
    set I = CurInstr(P1, Cs1i);
A37: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
      .= Exec (CurInstr(P2, Cs2i), Cs2i);
    dom Cs2i = the carrier of SCM by PARTFUN1:def 2;
    then
A38: dom Cs2i = {IC SCM} \/ Data-Locations SCM by STRUCT_0:4;
    dom Cs1i = the carrier of SCM by PARTFUN1:def 2;
    then
A39: dom Cs1i = {IC SCM} \/ Data-Locations SCM by STRUCT_0:4;
A40: dom (Cs1i|dom DPp) = dom Cs1i /\ dom DPp by RELAT_1:61
      .= dom DPp by A39,A30,XBOOLE_1:28;
A41: Cs3i1 = Following(P1,Cs3i) by EXTPRO_1:3
      .= Exec (CurInstr(P1, Cs1i), Cs3i) by A2,A9,A6,AMISTD_5:7;
A42: dom (Cs2i1|dom DataPart p) = dom Cs2i1 /\ dom DPp by RELAT_1:61

      .= dom DPp by A15,A30,XBOOLE_1:28;
A43: now
      let x be set, d be Data-Location such that
A44:  d = x & d in dom DPp and
A45:  Cs1i1.d = Cs2i1.d;
      thus (Cs1i1|dom DPp).x = Cs2i1.d by A31,A44,A45,FUNCT_1:47
        .= (Cs2i1|dom DPp).x by A42,A44,FUNCT_1:47;
    end;

A46: dom (Cs2i|dom DataPart p) = dom Cs2i /\ dom DPp by RELAT_1:61

      .= dom DPp by A38,A30,XBOOLE_1:28;
A47: now
      let x be set, d be Data-Location such that
A48:  d = x and
A49:  d in dom DPp and
A50:  Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d;

      (Cs1i|dom DPp).d = Cs1i.d & (Cs2i|dom DPp).d = Cs2i.d by A40,A46,A49,
FUNCT_1:47;

      hence (Cs1i1|dom DPp).x = Cs2i1.d by A13,A31,A48,A49,A50,FUNCT_1:47

        .= (Cs2i1|dom DPp).x by A42,A48,A49,FUNCT_1:47;
    end;
    reconsider j = IC Cs1i as Element of NAT;
A51: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
      .= Exec (CurInstr(P1, Cs1i), Cs1i);
A52: succ (IC Cs1i +k) = (j+k+1) by NAT_1:38
      .= (j+1) + k
      .= succ j + k by NAT_1:38;
    per cases by AMI_5:5,NAT_1:32;
    suppose
      InsCode I = 0;
      then
A53:  I = halt SCM by AMI_5:7;

      thus IC Comput(P1,s1,i+1) + k = IC Cs1i + k by A51,A53,EXTPRO_1:def 3

        .= IC Comput(P2,s2,i+1)
         by A11,A37,A53,A12,EXTPRO_1:def 3;

      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1)) by A32;

A54:  Cs2i1 = Cs2i by A37,A53,A12,EXTPRO_1:def 3;
      hence Comput(P1,s1,i+1)|dom DataPart p
       = Comput(P2,s2,i+1)|dom DataPart p by A13,A51,A53,EXTPRO_1:def 3;
      thus DataPart Cs3i1 = DataPart Cs2i1 by A14,A41,A53,A54,EXTPRO_1:def 3;
    end;
    suppose
      InsCode I = 1;
      then consider da, db being Data-Location such that
A55:  I = da := db by AMI_5:8;
A56:  IncAddr(I, k) = da := db by A55,COMPOS_0:4;
A57:  Exec(I, Cs1i).IC SCM = succ IC Cs1i by A55,AMI_3:2;

      hence
      IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A11,A12,A51,A37,A52,A56,AMI_3:2;

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A11,A12,A32,A51,A37,A52,A56,A57,AMI_3:2;

A58:  Cs3i.db = Cs2i.db by A27;
      now
        DPp c= p by RELAT_1:59;
        then
A59:    dom DPp c= dom p by GRFUNC_1:2;
        let x be set;
        assume
A60:    x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A60;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
A61:      da = d;
          then Cs1i1.d = Cs1i.db & Cs2i1.d = Cs2i.db by A12,A51,A37,A55,A56,
AMI_3:2;
          hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A2,A9,A31,A43,A55,A58
,A60,A59,A61,A6,AMI_5:17;
        end;
        suppose
          da <> d;
          then Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A55,A56,
AMI_3:2;
          hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A60;
        end;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom DataPart p
          = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;
      now
        let x be set;
        assume
A62:    x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
          da = d;
          then Cs2i1.d = Cs2i.db & Cs3i1.d=Cs3i.db by A12,A37,A41,A55,A56,
AMI_3:2;
          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A27,A19,A62;
        end;
        suppose
          da <> d;

          then
          Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A55,A56,AMI_3:2;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A62;
        end;
      end;
      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2;
      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1)
          by A17,A18,GRFUNC_1:3;
    end;
    suppose
      InsCode I = 2;
      then consider da, db being Data-Location such that
A63:  I = AddTo(da, db) by AMI_5:9;
A64:  IncAddr(I, k) = AddTo(da, db) by A63,COMPOS_0:4;
A65:  Exec(I, Cs1i).IC SCM = succ IC Cs1i by A63,AMI_3:3;

      hence
      IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A11,A12,A51,A37,A52,A64,AMI_3:3;

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A11,A12,A32,A51,A37,A52,A64,A65,AMI_3:3;

A66:  Cs3i.da = Cs2i.da & Cs3i.db = Cs2i.db by A27;
      now
        DPp c= p by RELAT_1:59;
        then
A67:    dom DPp c= dom p by GRFUNC_1:2;
        let x be set such that
A68:    x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A68;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
A69:      da = d;
          then Cs1i1.d = Cs1i.da + Cs1i.db & Cs2i1.d = Cs2i.da + Cs2i.db by A12
,A51,A37,A63,A64,AMI_3:3;

          hence
          (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A2,A9,A31,A43,A63,A66,A68
,A67,A69,A6,AMI_5:18;

        end;
        suppose
          da <> d;
          then Cs1i1.d=Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A63,A64,AMI_3:3
;
          hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A68;
        end;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;
      hence Comput(P1,s1,i+1)|dom DataPart p
         = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;
      now
        let x be set;
        assume
A70:    x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
          da = d;
          then Cs2i1.d = Cs2i.da + Cs2i.db & Cs3i1.d = Cs3i.da + Cs3i.db by A12
,A37,A41,A63,A64,AMI_3:3;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A66,A70;
        end;
        suppose
          da <> d;

          then Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A63,A64,
AMI_3:3;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A70;
        end;
      end;

      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2
;

      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3
;

    end;
    suppose
      InsCode I = 3;
      then consider da, db being Data-Location such that
A71:  I = SubFrom(da, db) by AMI_5:10;
A72:  IncAddr(I, k) = SubFrom(da, db) by A71,COMPOS_0:4;
A73:  Exec(I, Cs1i).IC SCM = succ IC Cs1i by A71,AMI_3:4;

      hence
      IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A11,A12,A51,A37,A52,A72,AMI_3:4;

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A11,A12,A32,A51,A37,A52,A72,A73,AMI_3:4;

A74:  Cs3i.da = Cs2i.da & Cs3i.db = Cs2i.db by A27;
      now
        DPp c= p by RELAT_1:59;
        then
A75:    dom DPp c= dom p by GRFUNC_1:2;
        let x be set such that
A76:    x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A76;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
A77:      da = d;

          then Cs1i1.d = Cs1i.da - Cs1i.db & Cs2i1.d = Cs2i.da - Cs2i.db by A12
,A51,A37,A71,A72,AMI_3:4;

          hence
          (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A2,A9,A31,A43,A71,A74,A76
,A75,A77,A6,AMI_5:19;

        end;
        suppose
          da <> d;

          then Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A71,A72,
AMI_3:4;

          hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A76;
        end;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom (DataPart p)
       = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

      now
        let x be set;
        assume
A78:    x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
          da = d;

          then Cs2i1.d = Cs2i.da - Cs2i.db & Cs3i1.d = Cs3i.da - Cs3i.db by A12
,A37,A41,A71,A72,AMI_3:4;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A74,A78;
        end;
        suppose
          da <> d;

          then Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A71,A72,
AMI_3:4;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A78;
        end;
      end;

      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2
;

      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3
;

    end;
    suppose
      InsCode I = 4;
      then consider da, db being Data-Location such that
A79:  I = MultBy(da, db) by AMI_5:11;
A80:  IncAddr(I, k) = MultBy(da, db) by A79,COMPOS_0:4;
A81:  Exec(I, Cs1i).IC SCM = succ IC Cs1i by A79,AMI_3:5;

      hence
      IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A11,A12,A51,A37,A52,A80,AMI_3:5;

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A11,A12,A32,A51,A37,A52,A80,A81,AMI_3:5;

A82:  Cs3i.da = Cs2i.da & Cs3i.db = Cs2i.db by A27;
      now
        DPp c= p by RELAT_1:59;
        then
A83:    dom DPp c= dom p by GRFUNC_1:2;
        let x be set such that
A84:    x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A84;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
A85:      da = d;

          then Cs1i1.d = Cs1i.da * Cs1i.db & Cs2i1.d = Cs2i.da * Cs2i.db by A12
,A51,A37,A79,A80,AMI_3:5;

          hence
          (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A2,A9,A31,A43,A79,A82,A84
,A83,A85,A6,AMI_5:20;
        end;
        suppose
          da <> d;

          then Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A79,A80,
AMI_3:5;

          hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A84;
        end;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom (DataPart p)
        = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

      now
        let x be set;
        assume
A86:    x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;
        per cases;
        suppose
          da = d;

          then Cs2i1.d = Cs2i.da * Cs2i.db & Cs3i1.d = Cs3i.da * Cs3i.db by A12
,A37,A41,A79,A80,AMI_3:5;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A82,A86;
        end;
        suppose
          da <> d;

          then Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A79,A80,
AMI_3:5;

          hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A86;
        end;
      end;

      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2
;

      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3
;

    end;
    suppose
      InsCode I = 5;
      then consider da, db being Data-Location such that
A87:  I = Divide(da, db) by AMI_5:12;
A88:  IncAddr(I, k) = Divide(da, db) by A87,COMPOS_0:4;
A89:  Cs3i.da = Cs2i.da & Cs3i.db = Cs2i.db by A27;
        per cases;
        suppose
A90:      da <> db;
A91:      Exec(I, Cs1i).IC SCM = succ IC Cs1i by A87,AMI_3:6;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A11,A12,A51,A37,A52,A88,AMI_3:6;

        thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)),k)
           = CurInstr(P2,Comput(P2,s2,i+1))
            by A11,A12,A32,A51,A37,A52,A88,A91,AMI_3:6;

          now
            DPp c= p by RELAT_1:59;
            then
A92:        dom DPp c= dom p by GRFUNC_1:2;
            let x be set such that
A93:        x in dom (Cs1i1|dom DPp);
            dom DPp c= Data-Locations SCM by RELAT_1:58;
            then x in Data-Locations SCM by A31,A93;
            then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
            per cases;
            suppose
A94:          da = d;

              then
A95:          Cs1i1.d = Cs1i.da div Cs1i.db & Cs2i1.d = Cs2i.da div Cs2i
              .db by A12,A51,A37,A87,A88,A90,AMI_3:6;

              Cs3i.da div Cs3i.db = Cs1i.da div Cs1i.db by A2,A9,A31,A87,A90
,A93,A92,A94,A6,AMI_5:21;

              hence (Cs1i1|dom DPp).x = Cs2i1.d by A89,A93,A95,FUNCT_1:47

                .= (Cs2i1|dom DPp).x by A31,A42,A93,FUNCT_1:47;
            end;
            suppose
A96:          db = d;

              then Cs1i1.d = Cs1i.da mod Cs1i.db & Cs2i1.d = Cs2i.da mod Cs2i
              .db by A12,A51,A37,A87,A88,AMI_3:6;

              hence
              (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A2,A9,A31,A43,A87,A89
,A93,A92,A96,A6,AMI_5:22;

            end;
            suppose
              da <> d & db <> d;

              then Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A87,A88,
AMI_3:6;

              hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A93;
            end;
          end;

          then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

          hence Comput(P1,s1,i+1)|dom (DataPart p)
           = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

          now
            let x be set;
            assume
A97:        x in dom DataPart Cs3i1;
            then reconsider d = x as Data-Location
             by A17,AMI_2:def 16,AMI_3:27;
            per cases;
            suppose
              da = d;

              then Cs2i1.d = Cs2i.da div Cs2i.db & Cs3i1.d = Cs3i.da div Cs3i
              .db by A12,A37,A41,A87,A88,A90,AMI_3:6;

              hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A89,A97;

            end;
            suppose
              db = d;

              then Cs2i1.d = Cs2i.da mod Cs2i.db & Cs3i1.d = Cs3i.da mod Cs3i
              .db by A12,A37,A41,A87,A88,AMI_3:6;

              hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A89,A97;

            end;
            suppose
              da <> d & db <> d;

              then Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A87,A88,
AMI_3:6;

              hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A97;
            end;
          end;

          then
          DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2;

          hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,
GRFUNC_1:3;

        end;
        suppose
A98:      da = db;
A99:      Exec(I, Cs1i).IC SCM = succ IC Cs1i by A87,AMI_3:6;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A11,A12,A51,A37,A52,A88,AMI_3:6;

          thus IncAddr(CurInstr(P1,
          Comput(P1,s1,i+1)), k)
           = CurInstr(P2,Comput(P2,s2,i+1))
            by A11,A12,A32,A51,A37,A52,A88,A99,AMI_3:6;

          now
            let x be set such that
A100:        x in dom (Cs1i1|dom DPp);
            dom DPp c= Data-Locations SCM by RELAT_1:58;
            then x in Data-Locations SCM by A31,A100;
            then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;
            per cases;
            suppose
A101:          da = d;

A102:          (Cs1i|dom DPp).d = Cs1i.d & (Cs2i|dom DPp).d = Cs2i.d by A31,A40
,A46,A100,FUNCT_1:47;

A103:         (Cs1i1|dom DPp).d = Cs1i1.d & (Cs2i1|dom DPp).d = Cs2i1.d
              by A31,A42,A100,FUNCT_1:47;

              Cs2i1.d = Cs2i.da mod Cs2i.db by A12,A37,A88,A98,A101,AMI_3:6;

              hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A13,A51,A87,A98
,A101,A102,A103,AMI_3:6;

            end;
            suppose
              da <> d;

              then Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A12,A51,A37,A87,A88
,A98,AMI_3:6;

              hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A100;
            end;
          end;

          then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

          hence Comput(P1,s1,i+1)|dom (DataPart p)
           = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

          now
            let x be set;
            assume
A104:       x in dom DataPart Cs3i1;
            then reconsider d = x as Data-Location
             by A17,AMI_2:def 16,AMI_3:27;
            per cases;
            suppose
              da = d;
              then Cs2i1.d = Cs2i.da mod Cs2i.db & Cs3i1.d = Cs3i.da mod Cs3i
              .db by A12,A37,A41,A87,A88,A98,AMI_3:6;

              hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A19,A89,A104;

            end;
            suppose
              da <> d;

              then Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A12,A37,A41,A87,A88
,A98,AMI_3:6;

              hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A104;
            end;
          end;

          then
          DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2;

          hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,
GRFUNC_1:3;

        end;
    end;
    suppose
      InsCode I = 6;
      then consider loc being Element of NAT such that
A105: I = SCM-goto loc by AMI_5:13;
A106: CurInstr(P2, Cs2i) = SCM-goto (loc+k) by A12,A105,Th1;
      thus IC Comput(P1,s1,i+1) + k = loc + k by A51,A105,AMI_3:7
        .= IC Comput(P2,s2,i+1) by A37,A106,AMI_3:7;

      hence
      IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       =
       CurInstr(P2,Comput(P2,s2,i+1)) by A32;

      now
        let x be set such that
A107:   x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A107;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;

        Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A51,A37,A105,A106,AMI_3:7;

        hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A107;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom (DataPart p)
       = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

      now
        let x be set;
        assume
A108:   x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;

        Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A37,A41,A105,A106,AMI_3:7;

        hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A108;
      end;

      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2
;

      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3
;

    end;
    suppose
      InsCode I = 7;

      then consider
      loc being Element of NAT, da being Data-Location
      such that

A109: I = da=0_goto loc by AMI_5:14;
A110: now
        per cases;
        case
          Cs1i.da = 0;
          hence IC Comput(P1,s1,i+1) + k = loc + k by A51,A109,AMI_3:8;
        end;
        case
          Cs1i.da <> 0;

          hence
          IC Comput(P1,s1,i+1) + k = succ (IC Cs2i) by A11,A51,A52,A109,AMI_3:8
;

        end;
      end;
A111: CurInstr(P2, Cs2i) = da=0_goto (loc+k) by A12,A109,Th2;
A112: now
        per cases;
        case
          Cs2i.da = 0;
          hence IC Comput(P2,s2,i+1) = loc + k by A37,A111,AMI_3:8;
        end;
        case
          Cs2i.da <> 0;

          hence IC Comput(P2,s2,i+1) = succ IC Cs2i by A37,A111,AMI_3:8;

        end;
      end;
A113: Cs3i.da = Cs2i.da by A27;
A114: now
        per cases;
        suppose
          loc <> succ IC Cs1i;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A2,A9,A109,A113,A110,A112,A6,AMI_5:23;

        end;
        suppose
          loc = succ IC Cs1i;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A11,A52,A110,A112;

        end;
      end;
      hence IC Comput(P1,s1,i+1) + k = IC Comput(P2,
s2,i+1);

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A32,A114;

      now
        let x be set such that
A115:   x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A115;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;

        Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A51,A37,A109,A111,AMI_3:8;

        hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A115;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom (DataPart p)
       = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

      now
        let x be set;
        assume
A116:   x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;

        Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A37,A41,A109,A111,AMI_3:8;

        hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A116;
      end;

      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2
;

      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3
;

    end;
    suppose
      InsCode I = 8;

      then consider
      loc being Element of NAT, da being Data-Location
      such that

A117: I = da>0_goto loc by AMI_5:15;
A118: now
        per cases;
        case
          Cs1i.da > 0;
          hence IC Comput(P1,s1,i+1) + k = loc + k by A51,A117,AMI_3:9;
        end;
        case
          Cs1i.da <= 0;

          hence
          IC Comput(P1,s1,i+1) + k = succ (IC Cs2i) by A11,A51,A52,A117,AMI_3:9
;

        end;
      end;
A119: CurInstr(P2, Cs2i) = da>0_goto (loc+k) by A12,A117,Th3;
A120: now
        per cases;
        case
          Cs2i.da > 0;
          hence IC Comput(P2,s2,i+1) = loc + k by A37,A119,AMI_3:9;
        end;
        case
          Cs2i.da <= 0;

          hence IC Comput(P2,s2,i+1) = succ IC Cs2i by A37,A119,AMI_3:9;

        end;
      end;
A121: Cs3i.da = Cs2i.da by A27;
A122: now
        per cases;
        suppose
          loc <> succ IC Cs1i;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A2,A9,A117,A121,A118,A120,A6,AMI_5:24;

        end;
        suppose
          loc = succ IC Cs1i;

          hence
          IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A11,A52,A118,A120;

        end;
      end;
      hence IC Comput(P1,s1,i+1) + k = IC Comput(P2,
s2,i+1);

      thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
       = CurInstr(P2,Comput(P2,s2,i+1))
        by A32,A122;

      now
        let x be set such that
A123:   x in dom (Cs1i1|dom DPp);
        dom DPp c= Data-Locations SCM by RELAT_1:58;
        then x in Data-Locations SCM by A31,A123;
        then reconsider d = x as Data-Location by AMI_2:def 16,AMI_3:27;

        Cs1i1.d = Cs1i.d & Cs2i1.d = Cs2i.d by A51,A37,A117,A119,AMI_3:9;

        hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A31,A47,A123;
      end;
      then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A31,A42,GRFUNC_1:2;

      hence Comput(P1,s1,i+1)|dom (DataPart p)
       = Comput(P2,s2,i+1)|dom DataPart p by A31,A42,GRFUNC_1:3;

      now
        let x be set;
        assume
A124:   x in dom DataPart Cs3i1;
        then reconsider d = x as Data-Location by A17,AMI_2:def 16,AMI_3:27;

        Cs3i1.d = Cs3i.d & Cs2i1.d = Cs2i.d by A37,A41,A117,A119,AMI_3:9;

        hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A23,A124;
      end;
      then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:2;
      hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A17,A18,GRFUNC_1:3;
    end;
  end;
A125: DataPart  p c=  p by RELAT_1:59;
A126: IC SCM in dom IncIC( p,k) by MEMSTR_0:52;
  now
    thus IC Comput(P1,s1,0) + k = IC s1 + k by EXTPRO_1:2
      .= IC  p + k by A2,A4,GRFUNC_1:2
      .= IC p + k
      .= IC IncIC(p,k) by MEMSTR_0:53
      .= IC s2 by A3,A126,GRFUNC_1:2
      .= IC Comput(P2,s2,0) by EXTPRO_1:2;
    reconsider loc = IC  p as Element of NAT;
A127: IC  p = IC s1 by A2,A4,GRFUNC_1:2;
    then IC  p = IC Comput(P1,s1,0) by EXTPRO_1:2;
    then
A128: loc in dom q by A8,A5,AMISTD_5:def 4;
A129: (IC  p) + k in dom Reloc(q,k) by A128,COMPOS_1:46;
A130: IC SCM in dom IncIC( p,k) by MEMSTR_0:52;
A131: (q).IC  p = P1.IC s1 by A127,A128,A6,GRFUNC_1:2;
    dom P2 = NAT by PARTFUN1:def 2;
    then
A132:  CurInstr(P2,Comput(P2,s2,0))
      = P2.IC Comput(P2,s2,0) by PARTFUN1:def 6
     .= P2.IC s2 by EXTPRO_1:2
     .= P2.(IC IncIC(p,k)) by A3,A130,GRFUNC_1:2
      .= P2.((IC p) +k) by MEMSTR_0:53
      .= P2.((IC  p) +k)
      .= (Reloc(q, k)).((IC  p) +k) by A129,A6,GRFUNC_1:2;
A133:  dom P1 = NAT by PARTFUN1:def 2;
     CurInstr(P1,Comput(P1,s1,0))
       = CurInstr(P1,s1) by EXTPRO_1:2
      .= P1.IC s1 by A133,PARTFUN1:def 6;
    hence
    IncAddr(CurInstr(P1,Comput(P1,s1,0)), k)
     = CurInstr(P2,Comput(P2,s2,0)) by A128,A131,A132,COMPOS_1:35;
A134: dom DataPart s2 = Data-Locations SCM by MEMSTR_0:9;
A135: DataPart p c= s1 by A2,A125,XBOOLE_1:1;
A136: DataPart IncIC(p,k) = DataPart p by MEMSTR_0:51;
    DataPart p c= IncIC(p,k) by A136,MEMSTR_0:12;
    then
A137: DataPart p c= s2 by A3,XBOOLE_1:1;
    thus Comput(P1,s1,0)|dom DataPart p = s1 | dom (DataPart p)
                    by EXTPRO_1:2
      .= DataPart p by A135,GRFUNC_1:23
      .= s2 | dom (DataPart p) by A137,GRFUNC_1:23
      .= Comput(P2,s2,0)|dom DataPart p by EXTPRO_1:2;
    thus DataPart Comput(P1,s3,0) = DataPart(s1 +* DataPart s2) by EXTPRO_1:2
      .= DataPart s2 by A134,FUNCT_4:23
      .= DataPart Comput(P2,s2,0) by EXTPRO_1:2;
  end;
  then
A138: Z[0];
  thus for i being Element of NAT holds Z[i] from NAT_1:sch 1(A138,A10);
end;

theorem
  for k being Element of NAT
   for q being non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
      p being q-autonomic non empty FinPartState of SCM , s1
  , s2 being State of SCM
  st IC SCM in dom p &  p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of SCM
  st q c= P1 & Reloc(q,k) c= P2
for i being Element of NAT holds IC Comput(P1,s1,i) + k = IC
Comput(P2,s2,i) by Lm1;

registration
 cluster SCM -> relocable1 relocable2;
 coherence
  proof
   thus SCM is relocable1
   proof
   thus
    for k being Element of NAT
   for q being non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
    p being q-autonomic non empty FinPartState of SCM ,
     s1, s2 being State of SCM st p c= s1 & IncIC( p,k) c= s2
  for P1,P2 being Instruction-Sequence of SCM
   st q c= P1 & Reloc(q,k) c= P2
for i being Element of NAT
 holds IncAddr(CurInstr(P1,Comput(P1,s1,i)), k)
  = CurInstr(P2,Comput(P2,s2,i)) by Lm1;
  end;
  let k be Element of NAT;
  let q be non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
   p be q-autonomic non empty FinPartState of SCM,
      s1, s2 be State of SCM;
  assume
A1: p c= s1 & IncIC( p,k) c= s2;
  let P1,P2 be Instruction-Sequence of SCM such that
A2: q c= P1 & Reloc(q,k) c= P2;
  thus for i being Element of NAT holds
   Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p
     by A1,Lm1,A2;
  end;
end;

theorem
  for k being Element of NAT
   for q being non halt-free finite
      (the InstructionsF of SCM)-valued NAT-defined Function,
      p being q-autonomic non empty FinPartState of SCM , s1
  , s2, s3 being State of SCM st IC SCM in dom p &
   p c= s1 & IncIC(p,k) c=
  s2 & s3 = s1 +* DataPart s2 holds
  for P1,P2 being Instruction-Sequence of SCM
  st q c= P1 & Reloc(q,k) c= P2
  for i being Element of NAT holds DataPart
  Comput(P1,s3,i) = DataPart Comput(P2,s2,i) by Lm1;