:: Modifying addresses of instructions of { \bf SCM_FSA }
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 14, 1996
:: Copyright (c) 1996-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, SUBSET_1, AMI_1, AMI_3, SCMFSA_2, AMISTD_2, CARD_1,
      GRAPHSP, ARYTM_3, RELAT_1, FUNCT_1, FUNCT_4, XBOOLE_0, FSM_1, ARYTM_1,
      INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, NAT_1, COMPOS_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
      CARD_3, XXREAL_0, XCMPLX_0, NAT_1, NAT_D, VALUED_1, INT_1, INT_2,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, FUNCT_7,
      FINSEQ_1, FINSEQ_2, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1,
      AMI_3, SCMFSA_2, AMISTD_2, AMISTD_5;
 constructors DOMAIN_1, XXREAL_0, AMI_3, SCMFSA_2, NAT_D, RELSET_1, VALUED_1,
      AMISTD_2, AMISTD_5, PBOOLE, FUNCT_7, MEMSTR_0, FINSEQ_2;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, INT_1, SCMFSA_2, AMI_3,
      SCMFSA10, AMISTD_2, VALUED_0, EXTPRO_1, MEMSTR_0, FINSEQ_1, COMPOS_0,
      XTUPLE_0, NAT_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions FUNCT_1, AMISTD_5, COMPOS_0;
 equalities AMI_3, SCMFSA_2, MEMSTR_0;
 expansions COMPOS_0;
 theorems SCMFSA_2, ENUMSET1, TARSKI, SCMFSA_3, VALUED_1, AMISTD_2, SCMFSA10,
      FINSEQ_1, ORDINAL1, EXTPRO_1, MEMSTR_0, COMPOS_0;

begin :: Incrementing addresses

reserve L, j, k, l, m, n, p, q for Nat,
  A for Data-Location,
  I for Instruction of SCM;

registration
 let a,b be Int-Location;
 cluster a:=b -> ins-loc-free;
 coherence
  proof
     a := b = [1,{},<*a,b*>] by SCMFSA10:2;
   hence JumpPart(a:=b) is empty;
  end;
 cluster AddTo(a,b) -> ins-loc-free;
 coherence
  proof
    AddTo(a,b) = [2,{},<*a,b*>] by SCMFSA10:3;
   hence JumpPart AddTo(a,b) is empty;
  end;
 cluster SubFrom(a,b) -> ins-loc-free;
 coherence
  proof
    SubFrom(a,b) = [3,{},<*a,b*>] by SCMFSA10:4;
   hence JumpPart SubFrom(a,b) is empty;
  end;
 cluster MultBy(a,b) -> ins-loc-free;
 coherence
  proof
    MultBy(a,b) = [4,{},<*a,b*>] by SCMFSA10:5;
   hence JumpPart MultBy(a,b) is empty;
  end;
 cluster Divide(a,b) -> ins-loc-free;
 coherence
  proof
    Divide(a,b) = [5,{},<*a,b*>] by SCMFSA10:6;
   hence JumpPart Divide(a,b) is empty;
  end;
end;

theorem Th1:
  for k,loc being Nat
  holds IncAddr(goto loc,k) = goto (loc + k) by SCMFSA10:41;

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

theorem Th3:
  for k,loc being Nat, a being Int-Location
       holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k)
proof
  let k,loc be Nat, a be Int-Location;
A1: a>0_goto loc = [8,<* loc *>,<*a*>] by SCMFSA10:8;
A2: a>0_goto (loc + k) = [8,<* loc + k *>,<*a*>] by SCMFSA10:8;
A3: InsCode IncAddr(a>0_goto loc,k) = InsCode(a>0_goto loc) by COMPOS_0:def 9
     .= 8 by A1
     .= InsCode(a>0_goto(loc + k)) by A2;
A4: AddressPart IncAddr(a>0_goto loc,k) = AddressPart(a>0_goto loc)
           by COMPOS_0:def 9
     .= <*a*> by A1
     .= AddressPart(a>0_goto (loc + k)) by A2;
A5: 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
A6:   dom JumpPart IncAddr(a>0_goto loc,k)
     = dom JumpPart(a>0_goto (loc + k)) by A3,COMPOS_0:def 5;
A7: JumpPart(a>0_goto loc) = <*loc*> by A1;
A8: JumpPart(a>0_goto (loc+k)) = <*loc+k*> by A2;
    let x be object;
    assume
A9:   x in dom JumpPart IncAddr(a>0_goto loc,k);
     dom <*loc+k*> = {1} by FINSEQ_1:2,38;
     then
A10:   x = 1 by A9,A6,A8,TARSKI:def 1;
    thus (JumpPart IncAddr(a>0_goto loc,k)).x
      = k + (JumpPart(a>0_goto loc)).x by A5,A9,VALUED_1:def 2
     .= loc + k by A7,A10,FINSEQ_1:40
     .= (JumpPart(a>0_goto(loc + k))).x by A8,A10,FINSEQ_1:40;
   end;
 hence thesis by A3,A4,COMPOS_0:1;
end;

registration
 let a,b be Int-Location; let f be FinSeq-Location;
 cluster b:=(f,a) -> ins-loc-free;
 coherence;
 cluster (f,a):=b -> ins-loc-free;
 coherence;
end;

registration
 let a be Int-Location; let f be FinSeq-Location;
 cluster a:=len f -> ins-loc-free;
 coherence;
 cluster f:=<0,...,0>a -> ins-loc-free;
 coherence;
end;

reserve i for Instruction of SCM+FSA;

begin :: Incrementing Addresses in a finite partial state

registration
 cluster SCM+FSA -> relocable;
 coherence
 proof let INS be Instruction of SCM+FSA, j,k be Nat;
  let s be State of SCM+FSA;
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;
  InsCode INS = 0 or ... or InsCode INS = 12 by SCMFSA_2:16;
  then per cases;
  suppose InsCode INS = 0;
    then
A2: INS = halt SCM+FSA by SCMFSA_2:95;
    then
A3: IncAddr(INS,j) = halt SCM+FSA by COMPOS_0:4;
    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 A3,EXTPRO_1:def 3;
   hence thesis;
  end;
  suppose InsCode INS = 1;
    then consider da,db being Int-Location such that
A4: INS = da := db by SCMFSA_2:30;
A5: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A4,COMPOS_0:4
        .= IncIC(s,k).f by A4,SCMFSA_2:63
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A4,SCMFSA_2:63
        .= Exec(IncAddr(INS,j), s).f by A4,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now
      let d be Int-Location;
      per cases;
      suppose
A6:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A4,COMPOS_0:4
          .= IncIC(s,k).db by A4,A6,SCMFSA_2:63
          .= s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A4,A6,SCMFSA_2:63
          .= Exec(IncAddr(INS,j), s).d by A4,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
      suppose
A7:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A4,COMPOS_0:4
          .= IncIC(s,k).d by A4,A7,SCMFSA_2:63
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A4,A7,SCMFSA_2:63
          .= Exec(IncAddr(INS,j), s).d by A4,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
   hence thesis by A5,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 2;
    then consider da,db being Int-Location such that
A8: INS = AddTo(da, db) by SCMFSA_2:31;
A9: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A8,COMPOS_0:4
        .= IncIC(s,k).f by A8,SCMFSA_2:64
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A8,SCMFSA_2:64
        .= Exec(IncAddr(INS,j), s).f by A8,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
      per cases;
      suppose
A10:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A8,COMPOS_0:4
          .= IncIC(s,k).da + IncIC(s,k).db by A10,A8,SCMFSA_2:64
          .= s.da + IncIC(s,k).db by SCMFSA_3:3
          .= s.da + s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A8,A10,SCMFSA_2:64
          .= Exec(IncAddr(INS,j), s).d by A8,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
      suppose
A11:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A8,COMPOS_0:4
          .= IncIC(s,k).d by A8,A11,SCMFSA_2:64
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A8,A11,SCMFSA_2:64
          .= Exec(IncAddr(INS,j), s).d by A8,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
   hence thesis by A9,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 3;
    then consider da,db being Int-Location such that
A12: INS = SubFrom(da, db) by SCMFSA_2:32;
A13: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A12,COMPOS_0:4
        .= IncIC(s,k).f by A12,SCMFSA_2:65
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A12,SCMFSA_2:65
        .= Exec(IncAddr(INS,j), s).f by A12,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
      per cases;
      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).da - IncIC(s,k).db by A14,A12,SCMFSA_2:65
          .= s.da - IncIC(s,k).db by SCMFSA_3:3
          .= s.da - s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A12,A14,SCMFSA_2:65
          .= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
      suppose
A15:     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,A15,SCMFSA_2:65
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A12,A15,SCMFSA_2:65
          .= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
    hence thesis by A13,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 4;
    then consider da,db being Int-Location such that
A16: INS = MultBy(da, db) by SCMFSA_2:33;
A17: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A16,COMPOS_0:4
        .= IncIC(s,k).f by A16,SCMFSA_2:66
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A16,SCMFSA_2:66
        .= Exec(IncAddr(INS,j), s).f by A16,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
      per cases;
      suppose
A18:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A16,COMPOS_0:4
          .= IncIC(s,k).da * IncIC(s,k).db by A18,A16,SCMFSA_2:66
          .= s.da * IncIC(s,k).db by SCMFSA_3:3
          .= s.da * s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A16,A18,SCMFSA_2:66
          .= Exec(IncAddr(INS,j), s).d by A16,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
      suppose
A19:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A16,COMPOS_0:4
          .= IncIC(s,k).d by A16,A19,SCMFSA_2:66
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A16,A19,SCMFSA_2:66
          .= Exec(IncAddr(INS,j), s).d by A16,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
    hence thesis by A17,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 5;
    then consider da,db being Int-Location such that
A20: INS = Divide(da, db) by SCMFSA_2:34;
A21: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A20,COMPOS_0:4
        .= IncIC(s,k).f by A20,SCMFSA_2:67
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A20,SCMFSA_2:67
        .= Exec(IncAddr(INS,j), s).f by A20,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
     now
      let d be Int-Location;
      per cases;
      suppose
A22:    da <> db;
        hereby
          per cases;
          suppose
A23:        da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
          .= IncIC(s,k).da div IncIC(s,k).db by A22,A23,A20,SCMFSA_2:67
          .= s.da div IncIC(s,k).db by SCMFSA_3:3
          .= s.da div s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A20,A22,A23,SCMFSA_2:67
          .= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
          end;
          suppose
A24:        db = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
          .= IncIC(s,k).da mod IncIC(s,k).db by A24,A20,SCMFSA_2:67
          .= s.da mod IncIC(s,k).db by SCMFSA_3:3
          .= s.da mod s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A20,A24,SCMFSA_2:67
          .= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
          end;
          suppose
A25:        da <> d & db <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
          .= IncIC(s,k).d by A20,A25,SCMFSA_2:67
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A20,A25,SCMFSA_2:67
          .= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
          end;
        end;
      end;
      suppose
A26:    da = db;
          per cases;
          suppose
A27:        da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
          .= IncIC(s,k).da mod IncIC(s,k).db by A26,A27,A20,SCMFSA_2:67
          .= s.da mod IncIC(s,k).db by SCMFSA_3:3
          .= s.da mod s.db by SCMFSA_3:3
          .= Exec(INS, s).d by A20,A26,A27,SCMFSA_2:67
          .= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
          end;
       suppose
A28:        da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
          .= IncIC(s,k).d by A20,A26,A28,SCMFSA_2:67
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A20,A26,A28,SCMFSA_2:67
          .= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
        end;
      end;
    end;
    hence thesis by A21,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 6;
    then consider loc being Nat such that
A29: INS = goto loc by SCMFSA_2:35;
A30: IncAddr(INS, j+k) = goto (loc + (j+k)) by A29,Th1;
    reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A31: IncAddr(INS,jj) = goto (loc + jj) by A29,Th1;
A32: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = IncIC(s,k).f by A30,SCMFSA_2:69
        .= s.f by SCMFSA_3:4
        .= Exec(IncAddr(INS,j), s).f by A31,SCMFSA_2:69
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A30,SCMFSA_2:69
          .= s.d by SCMFSA_3:3
          .= Exec(IncAddr(INS,j), s).d by A31,SCMFSA_2:69
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
    end;
    hence thesis by A32,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 7;
    then consider loc being Nat, da being Int-Location such that
A33: INS = da=0_goto loc by SCMFSA_2:36;
A34: IncAddr(INS, j+k) = da=0_goto (loc + (j+k)) by A33,Th2;
    reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A35: IncAddr(INS,jj) = da=0_goto (loc + jj) by A33,Th2;
A36: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = IncIC(s,k).f by A34,SCMFSA_2:70
        .= s.f by SCMFSA_3:4
        .= Exec(IncAddr(INS,j), s).f by A35,SCMFSA_2:70
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A34,SCMFSA_2:70
          .= s.d by SCMFSA_3:3
          .= Exec(IncAddr(INS,j), s).d by A35,SCMFSA_2:70
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
    end;
   hence thesis by A1,A36,SCMFSA_2:104;
  end;
  suppose InsCode INS = 8;
    then consider loc being Nat, da being Int-Location such that
A37: INS = da>0_goto loc by SCMFSA_2:37;
A38: IncAddr(INS, j+k) = da>0_goto (loc + (j+k)) by A37,Th3;
    reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A39: IncAddr(INS, jj) = da>0_goto (loc + jj) by A37,Th3;
A40: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = IncIC(s,k).f by A38,SCMFSA_2:71
        .= s.f by SCMFSA_3:4
        .= Exec(IncAddr(INS,j), s).f by A39,SCMFSA_2:71
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = IncIC(s,k).d by A38,SCMFSA_2:71
          .= s.d by SCMFSA_3:3
          .= Exec(IncAddr(INS,j), s).d by A39,SCMFSA_2:71
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
     end;
   hence thesis by A40,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 9;
    then consider db,da being Int-Location, f being FinSeq-Location such that
A41: INS = da :=(f, db) by SCMFSA_2:38;
A42: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A41,COMPOS_0:4
        .= IncIC(s,k).f by A41,SCMFSA_2:72
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A41,SCMFSA_2:72
        .= Exec(IncAddr(INS,j), s).f by A41,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
      per cases;
      suppose
A43:     da = d;
      consider m being Nat such that
A44:  m = |.s.db.| and
A45:  Exec(INS, s).da = (s.f)/.m by A41,SCMFSA_2:72;
A46:  ex m1 being Nat st
        m1 = |.IncIC(s,k).db.| &
        Exec(INS,IncIC(s,k)).da = (IncIC(s,k).f)/.m1 by A41,SCMFSA_2:72;
A47:     (IncIC(s,k)).db = s.db by SCMFSA_3:3;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A41,COMPOS_0:4
          .= (s.f)/.m by A44,A46,A43,A47,SCMFSA_3:4
          .= IncIC(Exec(INS, s),k).d by A45,A43,SCMFSA_3:3
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by A41,COMPOS_0:4;
      end;
      suppose
A48:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A41,COMPOS_0:4
          .= IncIC(s,k).d by A41,A48,SCMFSA_2:72
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A41,A48,SCMFSA_2:72
          .= Exec(IncAddr(INS,j), s).d by A41,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
   hence thesis by A42,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 10;
    then consider db,da being Int-Location, f being FinSeq-Location such that
A49: INS = (f, db):=da by SCMFSA_2:39;
A50: now let g be FinSeq-Location;
      consider m being Nat such that
A51:  m = |.s.db.| and
A52:  Exec(INS, s).f = s.f+*(m,s.da) by A49,SCMFSA_2:73;
A53:  ex m1 being Nat
       st m1 = |.IncIC(s,k).db.| &
       Exec(INS,IncIC(s,k)).f = IncIC(s,k).f +*(m1,IncIC(s,k).da)
        by A49,SCMFSA_2:73;
      per cases;
      suppose
A54:    f = g;
A55:     IncIC(s,k).f = s.f & IncIC(s,k).db = s.db by SCMFSA_3:3,4;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
         =  Exec(INS, IncIC(s,k)).g by A49,COMPOS_0:4
        .= s.f+*(m,s.da) by A51,A53,A54,A55,SCMFSA_3:3
        .= IncIC(Exec(INS, s),k).g by A52,A54,SCMFSA_3:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).g by A49,COMPOS_0:4;
     end;
      suppose
A56:    f <> g;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
           = Exec(INS,IncIC(s,k)).g by A49,COMPOS_0:4
          .= IncIC(s,k).g by A49,A56,SCMFSA_2:73
          .= s.g by SCMFSA_3:4
          .= Exec(INS, s).g by A49,A56,SCMFSA_2:73
          .= Exec(IncAddr(INS,j), s).g by A49,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).g by SCMFSA_3:4;
     end;
    end;
    now let d be Int-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A49,COMPOS_0:4
          .= IncIC(s,k).d by A49,SCMFSA_2:73
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A49,SCMFSA_2:73
          .= Exec(IncAddr(INS,j), s).d by A49,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
    end;
   hence thesis by A50,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 11;
    then consider da being Int-Location, f being FinSeq-Location such that
A57: INS = da :=len f by SCMFSA_2:40;
A58: now let f be FinSeq-Location;
     thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
         = Exec(INS,IncIC(s,k)).f by A57,COMPOS_0:4
        .= IncIC(s,k).f by A57,SCMFSA_2:74
        .= s.f by SCMFSA_3:4
        .= Exec(INS, s).f by A57,SCMFSA_2:74
        .= Exec(IncAddr(INS,j), s).f by A57,COMPOS_0:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
    end;
    now let d be Int-Location;
      per cases;
      suppose
A59:     da = d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A57,COMPOS_0:4
          .= len(IncIC(s,k).f) by A59,A57,SCMFSA_2:74
          .= len(s.f) by SCMFSA_3:4
          .= Exec(INS, s).d by A57,A59,SCMFSA_2:74
          .= IncIC(Exec(INS, s),k).d by SCMFSA_3:3
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by A57,COMPOS_0:4;
      end;
      suppose
A60:     da <> d;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A57,COMPOS_0:4
          .= IncIC(s,k).d by A57,A60,SCMFSA_2:74
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A57,A60,SCMFSA_2:74
          .= Exec(IncAddr(INS,j), s).d by A57,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
      end;
    end;
   hence thesis by A58,A1,SCMFSA_2:104;
  end;
  suppose InsCode INS = 12;
    then consider da being Int-Location, f being FinSeq-Location such that
A61: INS = f:=<0,...,0>da by SCMFSA_2:41;
A62: now let g be FinSeq-Location;
A63:  (ex m being Nat
        st m = |.s.da.| & Exec(INS, s ).f = m|-> 0 ) &
       ex m being Nat st m = |.IncIC(s,k).da.|
         & Exec (INS,IncIC(s,k)).f = m |-> 0 by A61,SCMFSA_2:75;
      per cases;
      suppose
A64:    f = g;
A65:     IncIC(s,k).da = s.da by SCMFSA_3:3;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
         =  Exec(INS, IncIC(s,k)).g by A61,COMPOS_0:4
        .= IncIC(Exec(INS, s),k).g by A63,A64,A65,SCMFSA_3:4
        .= IncIC(Exec(IncAddr(INS,j),s),k).g by A61,COMPOS_0:4;
      end;
      suppose
A66:    f <> g;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
           = Exec(INS,IncIC(s,k)).g by A61,COMPOS_0:4
          .= IncIC(s,k).g by A61,A66,SCMFSA_2:75
          .= s.g by SCMFSA_3:4
          .= Exec(INS, s).g by A61,A66,SCMFSA_2:75
          .= Exec(IncAddr(INS,j), s).g by A61,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).g by SCMFSA_3:4;
     end;
    end;
    now let d be Int-Location;
       thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
           = Exec(INS,IncIC(s,k)).d by A61,COMPOS_0:4
          .= IncIC(s,k).d by A61,SCMFSA_2:75
          .= s.d by SCMFSA_3:3
          .= Exec(INS, s).d by A61,SCMFSA_2:75
          .= Exec(IncAddr(INS,j), s).d by A61,COMPOS_0:4
          .= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
    end;
   hence thesis by A62,A1,SCMFSA_2:104;
  end;
 end;
end;

theorem
 not InsCode i in {6,7,8} implies IncAddr(i,k) = i
proof
 assume not InsCode i in {6,7,8};
  then
A1: InsCode i <> 6 & InsCode i <> 7 & InsCode i <> 8 by ENUMSET1:def 1;
  InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
  then per cases by A1;
  suppose InsCode i = 0;
    then i = halt SCM+FSA by SCMFSA_2:95;
   hence thesis by COMPOS_0:4;
  end;
  suppose
    InsCode i = 1;
    then consider da,db being Int-Location such that
A2: i = da := db by SCMFSA_2:30;
   thus thesis by A2,COMPOS_0:4;
  end;
  suppose
    InsCode i = 2;
    then consider da,db being Int-Location such that
A3: i = AddTo(da, db) by SCMFSA_2:31;
    thus thesis by A3,COMPOS_0:4;
  end;
  suppose
    InsCode i = 3;
    then consider da,db being Int-Location such that
A4: i = SubFrom(da, db) by SCMFSA_2:32;
    thus thesis by A4,COMPOS_0:4;
  end;
  suppose
    InsCode i = 4;
    then consider da,db being Int-Location such that
A5: i = MultBy(da, db) by SCMFSA_2:33;
    thus thesis by A5,COMPOS_0:4;
  end;
  suppose
    InsCode i = 5;
    then consider da,db being Int-Location such that
A6: i = Divide(da, db) by SCMFSA_2:34;
    thus thesis by A6,COMPOS_0:4;
  end;
  suppose
    InsCode i = 9;
    then consider db,da being Int-Location, f being FinSeq-Location such that
A7: i = da :=(f, db) by SCMFSA_2:38;
    thus thesis by A7,COMPOS_0:4;
  end;
  suppose
    InsCode i = 10;
    then consider db,da being Int-Location, f being FinSeq-Location such that
A8: i = (f, db):=da by SCMFSA_2:39;
    thus thesis by A8,COMPOS_0:4;
  end;
  suppose
    InsCode i = 11;
    then consider da being Int-Location, f being FinSeq-Location such that
A9: i = da :=len f by SCMFSA_2:40;
    thus thesis by A9,COMPOS_0:4;
  end;
  suppose
    InsCode i = 12;
    then consider da being Int-Location, f being FinSeq-Location such that
A10: i = f:=<0,...,0>da by SCMFSA_2:41;
   thus thesis by A10,COMPOS_0:4;
  end;
 end;