The Mizar article:

The Properties of Instructions of SCM over Ring

by
Artur Kornilowicz

Received April 14, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: SCMRING3
[ MML identifier index ]


environ

 vocabulary AMI_3, SCMFSA7B, FUNCSDOM, AMI_1, ORDINAL2, ARYTM, INT_1, FINSET_1,
      INT_3, AMI_2, GR_CY_1, TARSKI, BOOLE, FUNCT_1, FUNCOP_1, CAT_1, FUNCT_7,
      RELAT_1, AMI_5, MCART_1, FINSEQ_1, AMISTD_2, AMISTD_1, FUNCT_4, SETFAM_1,
      REALSET1, RLVECT_1, SGRAPH1, GOBOARD5, ARYTM_1, VECTSP_1, FRECHET,
      UNIALG_1, CARD_5, CARD_3, RELOC;
 notation TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, MCART_1, SETFAM_1, RELAT_1,
      FUNCT_1, FUNCT_2, STRUCT_0, FUNCSDOM, REALSET1, ORDINAL1, ORDINAL2,
      NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RLVECT_1, CQC_LANG, FINSEQ_1, FUNCT_4,
      GR_CY_1, CARD_3, FUNCT_7, VECTSP_1, GROUP_1, AMI_1, AMI_2, AMI_3, AMI_5,
      SCMRING1, SCMRING2, INT_3, AMISTD_1, AMISTD_2;
 constructors AMI_5, AMISTD_2, DOMAIN_1, NAT_1, SCMRING2, FUNCT_7, PRALG_2,
      INT_3, GCD_1, ALGSTR_2, MEMBERED;
 clusters AMI_1, RELSET_1, SCMRING1, SCMRING2, STRUCT_0, TEX_2, AMISTD_2,
      RELAT_1, FUNCT_1, CQC_LANG, FINSEQ_1, INT_1, INT_3, WAYBEL12, XBOOLE_0,
      REVROT_1, AMI_3, NAT_1, VECTSP_1, FRAENKEL, MEMBERED;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FUNCT_1, GROUP_1, FUNCT_2, FUNCT_7, SCMRING1, SCMRING2,
      AMISTD_1, AMISTD_2, XBOOLE_0;
 theorems TARSKI, NAT_1, AMI_1, SCMRING2, AMI_3, FUNCT_4, AMI_5, FUNCT_1,
      FUNCT_2, RELSET_1, ZFMISC_1, CQC_LANG, SCMRING1, SETFAM_1, AMI_2,
      AMISTD_1, MCART_1, INT_1, INT_3, FINSET_1, ANPROJ_1, RLVECT_1, VECTSP_1,
      LMOD_6, FINSEQ_1, FINSEQ_3, CQC_THE1, GR_CY_1, AMISTD_2, FUNCT_7, CARD_3,
      SCMFSA6A, ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_1, YELLOW_8;
 schemes FUNCT_2;

begin

reserve R for good Ring,
        r for Element of R,
        a, b, d1, d2 for Data-Location of R,
        il, i1, i2 for Instruction-Location of SCM R,
        I for Instruction of SCM R,
        s, s1, s2 for State of SCM R,
        T for InsType of SCM R,
        k for natural number;

definition
 cluster INT -> infinite;
coherence by FINSET_1:13,INT_1:14;
end;

definition
 cluster INT.Ring -> infinite good;
coherence
  proof
    thus the carrier of INT.Ring is infinite by INT_3:def 3;
    thus the carrier of INT.Ring <> SCM-Instr-Loc by AMI_2:6,INT_3:def 3;
    assume the carrier of INT.Ring = SCM-Instr INT.Ring;
    then 1 in SCM-Instr INT.Ring by INT_1:12,INT_3:def 3;
    then ex a, b being set st a in Segm 8 &
     b in (union {the carrier of INT.Ring} \/ NAT)* & 1 = [a,b]
      by ZFMISC_1:def 2;
    hence thesis by AMI_1:2;
  end;
end;

definition
 cluster strict infinite 1-sorted;
existence
  proof
    take A = 1-sorted(#INT#);
    thus A is strict & the carrier of A is infinite;
  end;
end;

definition
 cluster strict infinite good Ring;
existence
  proof
    take INT.Ring;
    thus thesis;
  end;
end;

theorem Th1:
 ObjectKind a = the carrier of R
  proof
A1: a in SCM-Data-Loc by SCMRING2:1;
A2: the Object-Kind of SCM R = SCM-OK R by SCMRING2:def 1;
    thus ObjectKind a = (the Object-Kind of SCM R).a by AMI_1:def 6
        .= the carrier of R by A1,A2,SCMRING1:5;
  end;

definition
 let R be good Ring;
 let la, lb be Data-Location of R;
 let a, b be Element of R;
 redefine func (la,lb) --> (a,b) -> FinPartState of SCM R;
coherence
  proof
    reconsider a' = a as Element of ObjectKind la by Th1;
    reconsider b' = b as Element of ObjectKind lb by Th1;
      (la,lb) --> (a',b') is FinPartState of SCM R;
    hence thesis;
  end;
end;

theorem Th2:
 not a in the Instruction-Locations of SCM R
  proof
      a in (the carrier of SCM R) \ (SCM-Instr-Loc \/
 {0}) by SCMRING2:def 2;
    then not a in SCM-Instr-Loc \/ {0} by XBOOLE_0:def 4;
    then not a in SCM-Instr-Loc by XBOOLE_0:def 2;
    hence thesis by SCMRING2:def 1;
  end;

theorem Th3:
 a <> IC SCM R
  proof
      a in (the carrier of SCM R) \ (SCM-Instr-Loc \/
 {0}) by SCMRING2:def 2;
    then not a in SCM-Instr-Loc \/ {0} by XBOOLE_0:def 4;
    then not a in {0} by XBOOLE_0:def 2;
    then a <> 0 by TARSKI:def 1;
    hence thesis by SCMRING2:9;
  end;

theorem Th4:
 SCM-Data-Loc <> the Instruction-Locations of SCM R
  proof
    assume
A1:   not thesis;
A2: the Instruction-Locations of SCM R = SCM-Instr-Loc by SCMRING2:def 1;
    consider a being Element of SCM-Instr-Loc;
      a in SCM-Instr-Loc;
    hence thesis by A1,A2,AMI_2:12;
  end;

theorem Th5:
 for o being Object of SCM R holds
  o = IC SCM R or o in the Instruction-Locations of SCM R or
  o is Data-Location of R
  proof
     let o be Object of SCM R;
     assume o <> IC SCM R;
     then not o in {IC SCM R} by TARSKI:def 1;
then A1:  not o in {0} by SCMRING2:9;
     assume not o in the Instruction-Locations of SCM R;
     then not o in SCM-Instr-Loc by SCMRING2:def 1;
     then not o in SCM-Instr-Loc \/ {0} by A1,XBOOLE_0:def 2;
     hence o in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0}) by XBOOLE_0:def
4;
  end;

theorem Th6:
 i1 <> i2 implies Next i1 <> Next i2
  proof
    assume
A1:   i1 <> i2 & Next i1 = Next i2;
    consider m1 being Element of SCM-Instr-Loc such that
A2:   m1 = i1 & Next i1 = Next m1 by SCMRING2:def 10;
    consider m2 being Element of SCM-Instr-Loc such that
A3:   m2 = i2 & Next i2 = Next m2 by SCMRING2:def 10;
    Next m1 = m1+2 & Next m2 = m2+2 by AMI_2:def 15;
    hence contradiction by A1,A2,A3,XCMPLX_1:2;
  end;

theorem Th7:
 s1,s2 equal_outside the Instruction-Locations of SCM R implies s1.a = s2.a
  proof
    set IL = the Instruction-Locations of SCM R;
    assume
A1:   s1,s2 equal_outside IL;
A2: dom s1 = the carrier of SCM R by AMI_3:36;
A3: dom s2 = the carrier of SCM R by AMI_3:36;
A4: not a in IL by Th2;
    then a in dom s1 \ IL by A2,XBOOLE_0:def 4;
then A5: a in dom s1 /\ (dom s1 \ IL) by A2,XBOOLE_0:def 3;
      a in dom s2 \ IL by A3,A4,XBOOLE_0:def 4;
then A6: a in dom s2 /\ (dom s2 \ IL) by A3,XBOOLE_0:def 3;
    thus s1.a = (s1|(dom s1 \ IL)).a by A5,FUNCT_1:71
             .= (s2|(dom s2 \ IL)).a by A1,FUNCT_7:def 2
             .= s2.a by A6,FUNCT_1:71;
  end;

theorem Th8:
 InsCode halt SCM R = 0
  proof
    thus InsCode halt SCM R = (halt SCM R)`1 by AMI_5:def 1
       .= [ 0, {}]`1 by SCMRING2:30
       .= 0 by MCART_1:def 1;
  end;

theorem Th9:
 InsCode (a:=b) = 1
  proof
    thus InsCode (a:=b) = (a:=b)`1 by AMI_5:def 1
       .= [ 1, <*a,b*>]`1 by SCMRING2:def 3
       .= 1 by MCART_1:def 1;
  end;

theorem Th10:
 InsCode AddTo(a,b) = 2
  proof
    thus InsCode AddTo(a,b) = AddTo(a,b)`1 by AMI_5:def 1
       .= [ 2, <*a,b*>]`1 by SCMRING2:def 4
       .= 2 by MCART_1:def 1;
  end;

theorem Th11:
 InsCode SubFrom(a,b) = 3
  proof
    thus InsCode SubFrom(a,b) = SubFrom(a,b)`1 by AMI_5:def 1
       .= [ 3, <*a,b*>]`1 by SCMRING2:def 5
       .= 3 by MCART_1:def 1;
  end;

theorem Th12:
 InsCode MultBy(a,b) = 4
  proof
    thus InsCode MultBy(a,b) = MultBy(a,b)`1 by AMI_5:def 1
       .= [ 4, <*a,b*>]`1 by SCMRING2:def 6
       .= 4 by MCART_1:def 1;
  end;

theorem Th13:
 InsCode (a:=r) = 5
  proof
    thus InsCode (a:=r) = (a:=r)`1 by AMI_5:def 1
       .= [ 5, <*a,r*>]`1 by SCMRING2:def 7
       .= 5 by MCART_1:def 1;
  end;

theorem Th14:
 InsCode goto i1 = 6
  proof
    thus InsCode goto i1 = (goto i1)`1 by AMI_5:def 1
       .= [ 6, <*i1*>]`1 by SCMRING2:def 8
       .= 6 by MCART_1:def 1;
  end;

theorem Th15:
 InsCode (a=0_goto i1) = 7
  proof
    thus InsCode (a=0_goto i1) = (a=0_goto i1)`1 by AMI_5:def 1
       .= [ 7, <*i1,a*>]`1 by SCMRING2:def 9
       .= 7 by MCART_1:def 1;
  end;

theorem Th16:
 InsCode I = 0 implies I = halt SCM R
  proof
    assume
A1:   InsCode I = 0;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,Th9,Th10,Th11,Th12,Th13,Th14,Th15,SCMRING2:30;
  end;

theorem Th17:
 InsCode I = 1 implies ex a, b st I = a:=b
  proof
    assume
A1:   InsCode I = 1;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th10,Th11,Th12,Th13,Th14,Th15;
  end;

theorem Th18:
 InsCode I = 2 implies ex a, b st I = AddTo(a,b)
  proof
    assume
A1:   InsCode I = 2;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th11,Th12,Th13,Th14,Th15;
  end;

theorem Th19:
 InsCode I = 3 implies ex a, b st I = SubFrom(a,b)
  proof
    assume
A1:   InsCode I = 3;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th10,Th12,Th13,Th14,Th15;
  end;

theorem Th20:
 InsCode I = 4 implies ex a, b st I = MultBy(a,b)
  proof
    assume
A1:   InsCode I = 4;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th10,Th11,Th13,Th14,Th15;
  end;

theorem Th21:
 InsCode I = 5 implies ex a, r st I = a:=r
  proof
    assume
A1:   InsCode I = 5;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th10,Th11,Th12,Th14,Th15;
  end;

theorem Th22:
 InsCode I = 6 implies ex i2 st I = goto i2
  proof
    assume
A1:   InsCode I = 6;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th10,Th11,Th12,Th13,Th15;
  end;

theorem Th23:
 InsCode I = 7 implies ex a, i1 st I = a=0_goto i1
  proof
    assume
A1:   InsCode I = 7;
A2: [0,{}] = halt SCM R by SCMRING2:30;
      I = [0,{}] or
    (ex a,b st I = a:=b) or
    (ex a,b st I = AddTo(a,b)) or
    (ex a,b st I = SubFrom(a,b)) or
    (ex a,b st I = MultBy(a,b)) or
    (ex i1 st I = goto i1) or
    (ex a,i1 st I = a=0_goto i1) or
    ex a,r st I = a:=r by SCMRING2:8;
    hence thesis by A1,A2,Th8,Th9,Th10,Th11,Th12,Th13,Th14;
  end;

Lm1:
 for x, y being set st x in dom <*y*> holds x = 1
  proof
    let x, y be set;
    assume x in dom <*y*>;
    then x in Seg 1 by FINSEQ_1:def 8;
    hence thesis by FINSEQ_1:4,TARSKI:def 1;
  end;

Lm2:
 for x, y, z being set st x in dom <*y,z*> holds x = 1 or x = 2
  proof
    let x, y, z be set;
    assume x in dom <*y,z*>;
    then x in Seg 2 by FINSEQ_3:29;
    hence thesis by FINSEQ_1:4,TARSKI:def 2;
  end;

Lm3:
 T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7
  proof
A1: the Instruction-Codes of SCM R = Segm 8 by SCMRING2:def 1;
    then T in Segm 8;
    then reconsider t = T as Nat;
      t = 0 or t < 7+1 by A1,GR_CY_1:10;
    then t = 0 or t <= 7 by NAT_1:38;
    hence thesis by CQC_THE1:8;
  end;

theorem Th24:
 AddressPart halt SCM R = {}
  proof
    thus AddressPart halt SCM R = (halt SCM R)`2 by AMISTD_2:def 3
       .= [ 0, {}]`2 by SCMRING2:30
       .= {} by MCART_1:def 2;
  end;

theorem Th25:
 AddressPart (a:=b) = <*a,b*>
  proof
    thus AddressPart (a:=b) = (a:=b)`2 by AMISTD_2:def 3
       .= [ 1, <*a,b*>]`2 by SCMRING2:def 3
       .= <*a,b*> by MCART_1:def 2;
  end;

theorem Th26:
 AddressPart AddTo(a,b) = <*a,b*>
  proof
    thus AddressPart AddTo(a,b) = AddTo(a,b)`2 by AMISTD_2:def 3
       .= [ 2, <*a,b*>]`2 by SCMRING2:def 4
       .= <*a,b*> by MCART_1:def 2;
  end;

theorem Th27:
 AddressPart SubFrom(a,b) = <*a,b*>
  proof
    thus AddressPart SubFrom(a,b) = SubFrom(a,b)`2 by AMISTD_2:def 3
       .= [ 3, <*a,b*>]`2 by SCMRING2:def 5
       .= <*a,b*> by MCART_1:def 2;
  end;

theorem Th28:
 AddressPart MultBy(a,b) = <*a,b*>
  proof
    thus AddressPart MultBy(a,b) = MultBy(a,b)`2 by AMISTD_2:def 3
       .= [ 4, <*a,b*>]`2 by SCMRING2:def 6
       .= <*a,b*> by MCART_1:def 2;
  end;

theorem Th29:
 AddressPart (a:=r) = <*a,r*>
  proof
    thus AddressPart (a:=r) = (a:=r)`2 by AMISTD_2:def 3
       .= [ 5, <*a,r*>]`2 by SCMRING2:def 7
       .= <*a,r*> by MCART_1:def 2;
  end;

theorem Th30:
 AddressPart goto i1 = <*i1*>
  proof
    thus AddressPart goto i1 = (goto i1)`2 by AMISTD_2:def 3
       .= [ 6, <*i1*>]`2 by SCMRING2:def 8
       .= <*i1*> by MCART_1:def 2;
  end;

theorem Th31:
 AddressPart (a=0_goto i1) = <*i1,a*>
  proof
    thus AddressPart (a=0_goto i1) = (a=0_goto i1)`2 by AMISTD_2:def 3
       .= [ 7, <*i1,a*>]`2 by SCMRING2:def 9
       .= <*i1,a*> by MCART_1:def 2;
  end;

theorem Th32:
 T = 0 implies AddressParts T = {0}
  proof
    assume
A1:   T = 0;
A2: AddressParts T =
      { AddressPart I where I is Instruction of SCM R: InsCode I = T }
        by AMISTD_2:def 5;
    hereby
      let a be set;
      assume a in AddressParts T;
      then consider I such that
A3:     a = AddressPart I and
A4:     InsCode I = T by A2;
        I = halt SCM R by A1,A4,Th16;
      then a = {} by A3,Th24;
      hence a in {0} by TARSKI:def 1;
    end;
    let a be set;
    assume a in {0};
then A5: a = 0 by TARSKI:def 1;
      InsCode halt SCM R = 0 & AddressPart halt SCM R = 0
      by Th8,Th24;
    hence thesis by A1,A2,A5;
  end;

definition let R, T;
 cluster AddressParts T -> non empty;
coherence
  proof
A1: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, b, i1, r;
A2: T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7
      by Lm3;
      InsCode halt SCM R = 0 & InsCode (a:=b) = 1 & InsCode AddTo(a,b) = 2 &
     InsCode SubFrom(a,b) = 3 & InsCode MultBy(a,b) = 4 & InsCode (a:=r) = 5 &
      InsCode goto i1 = 6 & InsCode (a =0_goto i1) = 7
       by Th8,Th9,Th10,Th11,Th12,Th13,Th14,Th15;
    then AddressPart halt SCM R in AddressParts T or
     AddressPart (a:=b) in AddressParts T or
      AddressPart AddTo(a,b) in AddressParts T or
       AddressPart SubFrom(a,b) in AddressParts T or
        AddressPart MultBy(a,b) in AddressParts T or
         AddressPart (a:=r) in AddressParts T or
          AddressPart goto i1 in AddressParts T or
           AddressPart (a =0_goto i1) in AddressParts T by A1,A2;
    hence thesis;
  end;
end;

theorem Th33:
 T = 1 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 1;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, b;
A3: AddressPart (a:=b) = <*a,b*> by Th25;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode (a:=b) = 1 by Th9;
      then AddressPart (a:=b) in AddressParts T by A1,A2;
      then x in dom AddressPart (a:=b) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider d1, d2 such that
A8:     I = d1:=d2 by A1,A7,Th17;
        f = <*d1,d2*> by A6,A8,Th25;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th34:
 T = 2 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 2;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, b;
A3: AddressPart AddTo(a,b) = <*a,b*> by Th26;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode AddTo(a,b) = 2 by Th10;
      then AddressPart AddTo(a,b) in AddressParts T by A1,A2;
      then x in dom AddressPart AddTo(a,b) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider d1, d2 such that
A8:     I = AddTo(d1,d2) by A1,A7,Th18;
        f = <*d1,d2*> by A6,A8,Th26;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th35:
 T = 3 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 3;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, b;
A3: AddressPart SubFrom(a,b) = <*a,b*> by Th27;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode SubFrom(a,b) = 3 by Th11;
      then AddressPart SubFrom(a,b) in AddressParts T by A1,A2;
      then x in dom AddressPart SubFrom(a,b) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider d1, d2 such that
A8:     I = SubFrom(d1,d2) by A1,A7,Th19;
        f = <*d1,d2*> by A6,A8,Th27;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th36:
 T = 4 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 4;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, b;
A3: AddressPart MultBy(a,b) = <*a,b*> by Th28;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode MultBy(a,b) = 4 by Th12;
      then AddressPart MultBy(a,b) in AddressParts T by A1,A2;
      then x in dom AddressPart MultBy(a,b) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider d1, d2 such that
A8:     I = MultBy(d1,d2) by A1,A7,Th20;
        f = <*d1,d2*> by A6,A8,Th28;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th37:
 T = 5 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 5;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider a, r;
A3: AddressPart (a:=r) = <*a,r*> by Th29;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode (a:=r) = 5 by Th13;
      then AddressPart (a:=r) in AddressParts T by A1,A2;
      then x in dom AddressPart (a:=r) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider a, r such that
A8:     I = a:=r by A1,A7,Th21;
        f = <*a,r*> by A6,A8,Th29;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th38:
 T = 6 implies dom PA AddressParts T = {1}
  proof
    assume
A1:   T = 6;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider i1;
A3: AddressPart goto i1 = <*i1*> by Th30;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode goto i1 = 6 by Th14;
      then AddressPart goto i1 in AddressParts T by A1,A2;
      then x in dom AddressPart goto i1 by A4,AMISTD_2:def 1;
      hence x in {1} by A3,FINSEQ_1:4,def 8;
    end;
    let x be set;
    assume
A5:   x in {1};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider i1 such that
A8:     I = goto i1 by A1,A7,Th22;
        f = <*i1*> by A6,A8,Th30;
      hence x in dom f by A5,FINSEQ_1:4,def 8;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th39:
 T = 7 implies dom PA AddressParts T = {1,2}
  proof
    assume
A1:   T = 7;
A2: AddressParts T = {AddressPart I where
      I is Instruction of SCM R: InsCode I = T} by AMISTD_2:def 5;
    consider i1, a;
A3: AddressPart (a =0_goto i1) = <*i1,a*> by Th31;
    hereby
      let x be set;
      assume
A4:     x in dom PA AddressParts T;
        InsCode (a =0_goto i1) = 7 by Th15;
      then AddressPart (a =0_goto i1) in AddressParts T by A1,A2;
      then x in dom AddressPart (a =0_goto i1) by A4,AMISTD_2:def 1;
      hence x in {1,2} by A3,FINSEQ_1:4,FINSEQ_3:29;
    end;
    let x be set;
    assume
A5:   x in {1,2};
      for f being Function st f in AddressParts T holds x in dom f
    proof
      let f be Function;
      assume f in AddressParts T;
      then consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = T by A2;
      consider a, i1 such that
A8:     I = a =0_goto i1 by A1,A7,Th23;
        f = <*i1,a*> by A6,A8,Th31;
      hence x in dom f by A5,FINSEQ_1:4,FINSEQ_3:29;
    end;
    hence thesis by AMISTD_2:def 1;
  end;

theorem Th40:
 (PA AddressParts InsCode (a:=b)).1 = SCM-Data-Loc
  proof
A1: InsCode (a:=b) = 1 by Th9;
    then dom PA AddressParts InsCode (a:=b) = {1,2} by Th33;
then A2: 1 in dom PA AddressParts InsCode (a:=b) by TARSKI:def 2;
A3: AddressParts InsCode (a:=b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a:=b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode (a:=b)).1;
      then x in pi(AddressParts InsCode (a:=b),1) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode (a:=b) and
A5:     f.1 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode (a:=b) by A3,A4;
        InsCode I = 1 by A7,Th9;
      then consider d1, d2 such that
A8:     I = d1:=d2 by Th17;
        x = <*d1,d2*>.1 by A5,A6,A8,Th25
       .= d1 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode (x:=d1) = 1 by Th9;
    then AddressPart (x:=d1) in AddressParts InsCode (a:=b) by A1,A3;
then A9: (AddressPart (x:=d1)).1 in pi
(AddressParts InsCode (a:=b),1) by CARD_3:def 6
;
      (AddressPart (x:=d1)).1 = <*x,d1*>.1 by Th25
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th41:
 (PA AddressParts InsCode (a:=b)).2 = SCM-Data-Loc
  proof
A1: InsCode (a:=b) = 1 by Th9;
    then dom PA AddressParts InsCode (a:=b) = {1,2} by Th33;
then A2: 2 in dom PA AddressParts InsCode (a:=b) by TARSKI:def 2;
A3: AddressParts InsCode (a:=b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a:=b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode (a:=b)).2;
      then x in pi(AddressParts InsCode (a:=b),2) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode (a:=b) and
A5:     f.2 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode (a:=b) by A3,A4;
        InsCode I = 1 by A7,Th9;
      then consider d1, d2 such that
A8:     I = d1:=d2 by Th17;
        x = <*d1,d2*>.2 by A5,A6,A8,Th25
       .= d2 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode (d1:=x) = 1 by Th9;
    then AddressPart (d1:=x) in AddressParts InsCode (a:=b) by A1,A3;
then A9: (AddressPart (d1:=x)).2 in pi
(AddressParts InsCode (a:=b),2) by CARD_3:def 6
;
      (AddressPart (d1:=x)).2 = <*d1,x*>.2 by Th25
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th42:
 (PA AddressParts InsCode AddTo(a,b)).1 = SCM-Data-Loc
  proof
A1: InsCode AddTo(a,b) = 2 by Th10;
    then dom PA AddressParts InsCode AddTo(a,b) = {1,2} by Th34;
then A2: 1 in dom PA AddressParts InsCode AddTo(a,b) by TARSKI:def 2;
A3: AddressParts InsCode AddTo(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode AddTo(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode AddTo(a,b)).1;
      then x in pi(AddressParts InsCode AddTo(a,b),1) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode AddTo(a,b) and
A5:     f.1 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode AddTo(a,b) by A3,A4;
        InsCode I = 2 by A7,Th10;
      then consider d1, d2 such that
A8:     I = AddTo(d1,d2) by Th18;
        x = <*d1,d2*>.1 by A5,A6,A8,Th26
       .= d1 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode AddTo(x,d1) = 2 by Th10;
    then AddressPart AddTo(x,d1) in AddressParts InsCode AddTo(a,b) by A1,A3;
then A9: (AddressPart AddTo(x,d1)).1 in pi(AddressParts InsCode AddTo(a,b),1)
      by CARD_3:def 6;
      (AddressPart AddTo(x,d1)).1 = <*x,d1*>.1 by Th26
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th43:
 (PA AddressParts InsCode AddTo(a,b)).2 = SCM-Data-Loc
  proof
A1: InsCode AddTo(a,b) = 2 by Th10;
    then dom PA AddressParts InsCode AddTo(a,b) = {1,2} by Th34;
then A2: 2 in dom PA AddressParts InsCode AddTo(a,b) by TARSKI:def 2;
A3: AddressParts InsCode AddTo(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode AddTo(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode AddTo(a,b)).2;
      then x in pi(AddressParts InsCode AddTo(a,b),2) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode AddTo(a,b) and
A5:     f.2 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode AddTo(a,b) by A3,A4;
        InsCode I = 2 by A7,Th10;
      then consider d1, d2 such that
A8:     I = AddTo(d1,d2) by Th18;
        x = <*d1,d2*>.2 by A5,A6,A8,Th26
       .= d2 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode AddTo(d1,x) = 2 by Th10;
    then AddressPart AddTo(d1,x) in AddressParts InsCode AddTo(a,b) by A1,A3;
then A9: (AddressPart AddTo(d1,x)).2 in pi(AddressParts InsCode AddTo(a,b),2)
       by CARD_3:def 6;
      (AddressPart AddTo(d1,x)).2 = <*d1,x*>.2 by Th26
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th44:
 (PA AddressParts InsCode SubFrom(a,b)).1 = SCM-Data-Loc
  proof
A1: InsCode SubFrom(a,b) = 3 by Th11;
    then dom PA AddressParts InsCode SubFrom(a,b) = {1,2} by Th35;
then A2: 1 in dom PA AddressParts InsCode SubFrom(a,b) by TARSKI:def 2;
A3: AddressParts InsCode SubFrom(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode SubFrom(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode SubFrom(a,b)).1;
      then x in pi(AddressParts InsCode SubFrom(a,b),1) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode SubFrom(a,b) and
A5:     f.1 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode SubFrom(a,b) by A3,A4;
        InsCode I = 3 by A7,Th11;
      then consider d1, d2 such that
A8:     I = SubFrom(d1,d2) by Th19;
        x = <*d1,d2*>.1 by A5,A6,A8,Th27
       .= d1 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode SubFrom(x,d1) = 3 by Th11;
    then AddressPart SubFrom(x,d1) in AddressParts InsCode SubFrom(a,b) by A1,
A3;
      then A9: (AddressPart SubFrom(x,d1)).1 in pi(AddressParts InsCode SubFrom
(a,b),1)
      by CARD_3:def 6;
      (AddressPart SubFrom(x,d1)).1 = <*x,d1*>.1 by Th27
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th45:
 (PA AddressParts InsCode SubFrom(a,b)).2 = SCM-Data-Loc
  proof
A1: InsCode SubFrom(a,b) = 3 by Th11;
    then dom PA AddressParts InsCode SubFrom(a,b) = {1,2} by Th35;
then A2: 2 in dom PA AddressParts InsCode SubFrom(a,b) by TARSKI:def 2;
A3: AddressParts InsCode SubFrom(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode SubFrom(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode SubFrom(a,b)).2;
      then x in pi(AddressParts InsCode SubFrom(a,b),2) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode SubFrom(a,b) and
A5:     f.2 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode SubFrom(a,b) by A3,A4;
        InsCode I = 3 by A7,Th11;
      then consider d1, d2 such that
A8:     I = SubFrom(d1,d2) by Th19;
        x = <*d1,d2*>.2 by A5,A6,A8,Th27
       .= d2 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode SubFrom(d1,x) = 3 by Th11;
    then AddressPart SubFrom(d1,x) in AddressParts InsCode SubFrom(a,b) by A1,
A3;
      then A9: (AddressPart SubFrom(d1,x)).2 in pi(AddressParts InsCode SubFrom
(a,b),2)
       by CARD_3:def 6;
      (AddressPart SubFrom(d1,x)).2 = <*d1,x*>.2 by Th27
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th46:
 (PA AddressParts InsCode MultBy(a,b)).1 = SCM-Data-Loc
  proof
A1: InsCode MultBy(a,b) = 4 by Th12;
    then dom PA AddressParts InsCode MultBy(a,b) = {1,2} by Th36;
then A2: 1 in dom PA AddressParts InsCode MultBy(a,b) by TARSKI:def 2;
A3: AddressParts InsCode MultBy(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode MultBy(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode MultBy(a,b)).1;
      then x in pi(AddressParts InsCode MultBy(a,b),1) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode MultBy(a,b) and
A5:     f.1 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode MultBy(a,b) by A3,A4;
        InsCode I = 4 by A7,Th12;
      then consider d1, d2 such that
A8:     I = MultBy(d1,d2) by Th20;
        x = <*d1,d2*>.1 by A5,A6,A8,Th28
       .= d1 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode MultBy(x,d1) = 4 by Th12;
    then AddressPart MultBy(x,d1) in AddressParts InsCode MultBy(a,b) by A1,A3
;
      then A9: (AddressPart MultBy(x,d1)).1 in pi(AddressParts InsCode MultBy(a
,b),1)
      by CARD_3:def 6;
      (AddressPart MultBy(x,d1)).1 = <*x,d1*>.1 by Th28
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th47:
 (PA AddressParts InsCode MultBy(a,b)).2 = SCM-Data-Loc
  proof
A1: InsCode MultBy(a,b) = 4 by Th12;
    then dom PA AddressParts InsCode MultBy(a,b) = {1,2} by Th36;
then A2: 2 in dom PA AddressParts InsCode MultBy(a,b) by TARSKI:def 2;
A3: AddressParts InsCode MultBy(a,b) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode MultBy(a,b)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode MultBy(a,b)).2;
      then x in pi(AddressParts InsCode MultBy(a,b),2) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode MultBy(a,b) and
A5:     f.2 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode MultBy(a,b) by A3,A4;
        InsCode I = 4 by A7,Th12;
      then consider d1, d2 such that
A8:     I = MultBy(d1,d2) by Th20;
        x = <*d1,d2*>.2 by A5,A6,A8,Th28
       .= d2 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider d1;
      InsCode MultBy(d1,x) = 4 by Th12;
    then AddressPart MultBy(d1,x) in AddressParts InsCode MultBy(a,b) by A1,A3
;
      then A9: (AddressPart MultBy(d1,x)).2 in pi(AddressParts InsCode MultBy(a
,b),2)
       by CARD_3:def 6;
      (AddressPart MultBy(d1,x)).2 = <*d1,x*>.2 by Th28
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th48:
 (PA AddressParts InsCode (a:=r)).1 = SCM-Data-Loc
  proof
A1: InsCode (a:=r) = 5 by Th13;
    then dom PA AddressParts InsCode (a:=r) = {1,2} by Th37;
then A2: 1 in dom PA AddressParts InsCode (a:=r) by TARSKI:def 2;
A3: AddressParts InsCode (a:=r) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a:=r)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode (a:=r)).1;
      then x in pi(AddressParts InsCode (a:=r),1) by A2,AMISTD_2:def 1;
      then consider f being Function such that
A4:     f in AddressParts InsCode (a:=r) and
A5:     f.1 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode (a:=r) by A3,A4;
        InsCode I = 5 by A7,Th13;
      then consider d1 being Data-Location of R,
               r2 being Element of R such that
A8:     I = d1:=r2 by Th21;
        x = <*d1,r2*>.1 by A5,A6,A8,Th29
       .= d1 by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider r1 being Element of R;
      InsCode (x:=r1) = 5 by Th13;
    then AddressPart (x:=r1) in AddressParts InsCode (a:=r) by A1,A3;
then A9: (AddressPart (x:=r1)).1 in pi(AddressParts InsCode (a:=r),1)
      by CARD_3:def 6;
      (AddressPart (x:=r1)).1 = <*x,r1*>.1 by Th29
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

theorem Th49:
 (PA AddressParts InsCode (a:=r)).2 = the carrier of R
  proof
A1: InsCode (a:=r) = 5 by Th13;
    then dom PA AddressParts InsCode (a:=r) = {1,2} by Th37;
then A2: 2 in dom PA AddressParts InsCode (a:=r) by TARSKI:def 2;
A3: AddressParts InsCode (a:=r) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a:=r)}
        by AMISTD_2:def 5;
    thus (PA AddressParts InsCode (a:=r)).2 c= the carrier of R
    proof
      let k be set;
      assume k in (PA AddressParts InsCode (a:=r)).2;
      then k in pi(AddressParts InsCode (a:=r),2) by A2,AMISTD_2:def 1;
      then consider g being Function such that
A4:     g in AddressParts InsCode (a:=r) and
A5:     g.2 = k by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     g = AddressPart I and
A7:     InsCode I = InsCode (a:=r) by A3,A4;
        InsCode I = 5 by A7,Th13;
      then consider d1 being Data-Location of R,
               r1 being Element of R such that
A8:     I = d1:=r1 by Th21;
        k = <*d1,r1*>.2 by A5,A6,A8,Th29
        .= r1 by FINSEQ_1:61;
      hence k in the carrier of R;
    end;
    let k be set;
    assume k in the carrier of R;
    then reconsider r1 = k as Element of R;
    consider b;
    set J = b:=r1;
A9: AddressPart J = <*b,r1*> by Th29;
      InsCode J = 5 by Th13;
    then AddressPart J in AddressParts InsCode (a:=r) by A1,A3;
then A10: (AddressPart J).2 in pi(AddressParts InsCode (a:=r),2) by CARD_3:def
6;
      r1 = <*b,r1*>.2 by FINSEQ_1:61;
    hence k in (PA AddressParts InsCode (a:=r)).2 by A2,A9,A10,AMISTD_2:def 1;
  end;

theorem Th50:
 (PA AddressParts InsCode goto i1).1 = the Instruction-Locations of SCM R
  proof
      InsCode goto i1 = 6 by Th14;
    then dom PA AddressParts InsCode goto i1 = {1} by Th38;
then A1: 1 in dom PA AddressParts InsCode goto i1 by TARSKI:def 1;
A2: AddressParts InsCode goto i1 = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode goto i1}
        by AMISTD_2:def 5;
A3: InsCode goto i1 = 6 by Th14;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode goto i1).1;
      then x in pi(AddressParts InsCode goto i1,1) by A1,AMISTD_2:8;
      then consider g being Function such that
A4:     g in AddressParts InsCode goto i1 and
A5:     x = g.1 by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     g = AddressPart I and
A7:     InsCode I = InsCode goto i1 by A2,A4;
      consider i2 such that
A8:     I = goto i2 by A3,A7,Th22;
A9:   goto i2 = [ 6, <*i2*>] by SCMRING2:def 8;
        g = I`2 by A6,AMISTD_2:def 3
       .= <*i2*> by A8,A9,MCART_1:def 2;
      then x = i2 by A5,FINSEQ_1:def 8;
      hence x in the Instruction-Locations of SCM R;
    end;
    let x be set;
    assume x in the Instruction-Locations of SCM R;
    then reconsider x as Instruction-Location of SCM R;
A10: goto x = [ 6, <*x*>] by SCMRING2:def 8;
A11: AddressPart goto x = (goto x)`2 by AMISTD_2:def 3
      .= <*x*> by A10,MCART_1:def 2;
      InsCode goto i1 = InsCode goto x by A3,Th14;
then A12: <*x*> in AddressParts InsCode goto i1 by A2,A11;
      <*x*>.1 = x by FINSEQ_1:def 8;
    then x in pi(AddressParts InsCode goto i1,1) by A12,CARD_3:def 6;
    hence thesis by A1,AMISTD_2:8;
  end;

theorem Th51:
 (PA AddressParts InsCode (a =0_goto i1)).1 =
   the Instruction-Locations of SCM R
  proof
      InsCode (a =0_goto i1) = 7 by Th15;
    then dom PA AddressParts InsCode (a =0_goto i1) = {1,2} by Th39;
then A1: 1 in dom PA AddressParts InsCode (a =0_goto i1) by TARSKI:def 2;
A2: AddressParts InsCode (a =0_goto i1) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a =0_goto i1)}
        by AMISTD_2:def 5;
A3: InsCode (a =0_goto i1) = 7 by Th15;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode (a =0_goto i1)).1;
      then x in pi(AddressParts InsCode (a =0_goto i1),1) by A1,AMISTD_2:8;
      then consider g being Function such that
A4:     g in AddressParts InsCode (a =0_goto i1) and
A5:     x = g.1 by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     g = AddressPart I and
A7:     InsCode I = InsCode (a =0_goto i1) by A2,A4;
      consider b, i2 such that
A8:     I = b =0_goto i2 by A3,A7,Th23;
A9:   b =0_goto i2 = [ 7, <*i2,b*>] by SCMRING2:def 9;
        g = I`2 by A6,AMISTD_2:def 3
       .= <*i2,b*> by A8,A9,MCART_1:def 2;
      then x = i2 by A5,FINSEQ_1:61;
      hence x in the Instruction-Locations of SCM R;
    end;
    let x be set;
    assume x in the Instruction-Locations of SCM R;
    then reconsider x as Instruction-Location of SCM R;
A10: a =0_goto x = [ 7, <*x,a*>] by SCMRING2:def 9;
A11: AddressPart (a =0_goto x) = (a =0_goto x)`2 by AMISTD_2:def 3
      .= <*x,a*> by A10,MCART_1:def 2;
      InsCode (a =0_goto i1) = InsCode (a =0_goto x) by A3,Th15;
then A12: <*x,a*> in AddressParts InsCode (a =0_goto i1) by A2,A11;
      <*x,a*>.1 = x by FINSEQ_1:61;
    then x in pi(AddressParts InsCode (a =0_goto i1),1) by A12,CARD_3:def 6;
    hence thesis by A1,AMISTD_2:8;
  end;

theorem Th52:
 (PA AddressParts InsCode (a =0_goto i1)).2 = SCM-Data-Loc
  proof
A1: InsCode (a =0_goto i1) = 7 by Th15;
    then dom PA AddressParts InsCode (a =0_goto i1) = {1,2} by Th39;
then A2: 2 in dom PA AddressParts InsCode (a =0_goto i1) by TARSKI:def 2;
A3: AddressParts InsCode (a =0_goto i1) = {AddressPart I where
      I is Instruction of SCM R: InsCode I = InsCode (a =0_goto i1)}
        by AMISTD_2:def 5;
    hereby
      let x be set;
      assume x in (PA AddressParts InsCode (a =0_goto i1)).2;
      then x in pi(AddressParts InsCode (a =0_goto i1),2) by A2,AMISTD_2:def 1
;
      then consider f being Function such that
A4:     f in AddressParts InsCode (a =0_goto i1) and
A5:     f.2 = x by CARD_3:def 6;
      consider I being Instruction of SCM R such that
A6:     f = AddressPart I and
A7:     InsCode I = InsCode (a =0_goto i1) by A3,A4;
        InsCode I = 7 by A7,Th15;
      then consider b, i2 such that
A8:     I = b =0_goto i2 by Th23;
        x = <*i2,b*>.2 by A5,A6,A8,Th31
       .= b by FINSEQ_1:61;
      hence x in SCM-Data-Loc by SCMRING2:1;
    end;
    let x be set;
    assume x in SCM-Data-Loc;
    then reconsider x as Data-Location of R by SCMRING2:1;
    consider i2;
      InsCode (x =0_goto i2) = 7 by Th15;
    then AddressPart (x =0_goto i2) in AddressParts InsCode (a =0_goto i1) by
A1,A3;
      then A9: (AddressPart (x =0_goto i2)).2 in pi(AddressParts InsCode (a
=0_goto i1),2)
       by CARD_3:def 6;
      (AddressPart (x =0_goto i2)).2 = <*i2,x*>.2 by Th31
      .= x by FINSEQ_1:61;
    hence thesis by A2,A9,AMISTD_2:def 1;
  end;

Lm4:
 for N being with_non-empty_elements set,
     S being realistic IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     t, u being State of S,
     il being Instruction-Location of S,
     e being Element of ObjectKind IC S,
     I being Element of ObjectKind il
  st e = il & u = t+*((IC S, il)-->(e, I))
  holds
    u.il = I &
    IC u = il &
    IC Following u = Exec(u.IC u, u).IC S
  proof
    let N be with_non-empty_elements set,
        S be realistic IC-Ins-separated definite
          (non empty non void AMI-Struct over N),
        t, u be State of S,
        il be Instruction-Location of S,
        e be Element of ObjectKind IC S,
        I be Element of ObjectKind il such that
A1:  e = il and
A2:  u = t+*((IC S, il)-->(e, I));
     A3: dom ((IC S, il)-->(e, I)) = {IC S, il} by FUNCT_4:65;
     then A4: IC S in dom ((IC S, il)-->(e, I)) by TARSKI:def 2;
     A5: IC S <> il by AMI_1:48;
       il in dom ((IC S, il)-->(e, I)) by A3,TARSKI:def 2;
         hence
        u.il = ((IC S, il)-->(e, I)).il by A2,FUNCT_4:14
             .= I by A5,FUNCT_4:66;
         thus
        IC u = u.IC S by AMI_1:def 15
             .= ((IC S, il)-->(e, I)).IC S by A2,A4,FUNCT_4:14
             .= il by A1,A5,FUNCT_4:66;
         thus
           IC Following u = IC Exec(CurInstr u,u) by AMI_1:def 18
           .= IC Exec(u.IC u, u) by AMI_1:def 17
           .= Exec(u.IC u, u).IC S by AMI_1:def 15;
  end;

Lm5:
for l being Instruction-Location of SCM R,
    i being Instruction of SCM R holds
  (for s being State of SCM R st IC s = l & s.l = i
   holds Exec(i,s).IC SCM R = Next IC s)
  implies
  NIC(i, l) = {Next l}
  proof
    let l be Instruction-Location of SCM R,
        i be Instruction of SCM R;
    assume
A1:   for s being State of SCM R st IC s = l & s.l = i
        holds Exec(i, s).IC SCM R = Next IC s;
    set X = {IC Following s where s is State of SCM R: IC s = l & s.l = i};
A2: NIC(i,l) = X by AMISTD_1:def 5;
    hereby
      let x be set;
      assume x in NIC(i,l);
      then consider s being State of SCM R such that
A3:     x = IC Following s & IC s = l & s.l = i by A2;
      x = (Following s).IC SCM R by A3,AMI_1:def 15
       .= Exec(CurInstr s,s).IC SCM R by AMI_1:def 18
       .= Exec(s.IC s,s).IC SCM R by AMI_1:def 17
       .= Next l by A1,A3;
      hence x in {Next l} by TARSKI:def 1;
    end;
    let x be set;
    assume x in {Next l};
    then
A4: x = Next l by TARSKI:def 1;
    consider t being State of SCM R;
    reconsider il1 = l as Element of ObjectKind IC SCM R by AMI_1:def 11;
    reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
    set u = t+*((IC SCM R, l)-->(il1, I));
A5: IC u = l by Lm4;
A6: u.l = i by Lm4;
    IC Following u = Exec(u.IC u, u).IC SCM R by Lm4
    .= Next l by A1,A5,A6;
    hence thesis by A2,A4,A5,A6;
  end;

Lm6:
  for i being Instruction of SCM R holds
  (for l being Instruction-Location of SCM R holds NIC(i,l)={Next l})
  implies JUMP i is empty
  proof
    let i be Instruction of SCM R;
    assume
A1:   for l being Instruction-Location of SCM R holds NIC(i,l)={Next l};
    the Instruction-Locations of SCM R = SCM-Instr-Loc by SCMRING2:def 1;
    then consider p, q being Element of the Instruction-Locations of SCM R
     such that
A2:   p <> q by YELLOW_8:def 1;
    set X = { NIC(i,f) where f is Instruction-Location of SCM R:
        not contradiction };
    assume not thesis;
    then meet X is non empty by AMISTD_1:def 6;
    then consider x being set such that
A3:   x in meet X by XBOOLE_0:def 1;
    NIC(i,p) = {Next p} & NIC(i,q) = {Next q} by A1;
    then {Next p} in X & {Next q} in X;
    then x in {Next p} & x in {Next q} by A3,SETFAM_1:def 1;
    then x = Next p & x = Next q by TARSKI:def 1;
    hence contradiction by A2,Th6;
  end;

theorem Th53:
 NIC(halt SCM R, il) = {il}
proof
    now let x be set;
  A1: now assume
     A2: x = il;
       consider t being State of SCM R;
        reconsider il1 = il as Element of ObjectKind IC SCM R by AMI_1:def 11;
        reconsider I = halt SCM R as Element of ObjectKind il by AMI_1:def 14;
        set u = t+*((IC SCM R, il)-->(il1, I));
     A3: dom ((IC SCM R, il)-->(il1, I)) = {IC SCM R, il} by FUNCT_4:65;
     then A4: IC SCM R in dom ((IC SCM R, il)-->(il1, I)) by TARSKI:def 2;
     A5: IC SCM R <> il by AMI_1:48;
       il in dom ((IC SCM R, il)-->(il1, I)) by A3,TARSKI:def 2;
     then A6: u.il = ((IC SCM R, il)-->(il1, I)).il by FUNCT_4:14
             .= halt SCM R by A5,FUNCT_4:66;
     A7: IC u = u.IC SCM R by AMI_1:def 15
             .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A4,FUNCT_4:14
             .= il by A5,FUNCT_4:66;
           IC Following u = IC Exec(CurInstr u,u) by AMI_1:def 18
           .= IC Exec(u.IC u, u) by AMI_1:def 17
           .= Exec(u.IC u, u).IC SCM R by AMI_1:def 15
           .= u.IC SCM R by A6,A7,AMI_1:def 8
           .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A4,FUNCT_4:14
           .= il by A5,FUNCT_4:66;
      hence x in {IC Following s : IC s = il & s.il=halt SCM R} by A2,A6,A7;
     end;
       now assume
           x in {IC Following s : IC s = il & s.il=halt SCM R};
         then consider s being State of SCM R such that
     A8: x = IC Following s & IC s = il & s.il = halt SCM R;
      thus x = IC Exec(CurInstr s,s) by A8,AMI_1:def 18
           .= IC Exec(s.IC s, s) by AMI_1:def 17
           .= Exec(halt SCM R, s).IC SCM R by A8,AMI_1:def 15
           .= s.IC SCM R by AMI_1:def 8
           .= il by A8,AMI_1:def 15;
     end;
    hence x in {il} iff x in {IC Following s : IC s = il & s.il=halt SCM R}
       by A1,TARSKI:def 1;
  end;
  then {il} = { IC Following s : IC s = il & s.il = halt SCM R } by TARSKI:2;
 hence thesis by AMISTD_1:def 5;
end;

definition let R;
 cluster JUMP halt SCM R -> empty;
coherence
proof
 set X = { NIC(halt SCM R, il) : not contradiction };
 assume not thesis;
   then meet X is non empty by AMISTD_1:def 6;
   then consider x being set such that
A1:   x in meet X by XBOOLE_0:def 1;
   reconsider i1 = il.1, i2 = il.2 as Instruction-Location of SCM R
    by AMI_3:def 1,SCMRING2:def 1;
     NIC(halt SCM R, i1) in X & NIC(halt SCM R, i2) in X;
   then {i1} in X & {i2} in X by Th53;
   then x in {i1} & x in {i2} by A1,SETFAM_1:def 1;
   then x = i1 & x = i2 by TARSKI:def 1;
 hence contradiction by AMI_3:53;
end;
end;

theorem Th54:
 NIC(a := b, il) = {Next il}
proof
  set i = a:=b;
  for s being State of SCM R st IC s = il & s.il = i
   holds Exec(i,s).IC SCM R = Next IC s by SCMRING2:13;
  hence thesis by Lm5;
end;

definition let R, a, b;
 cluster JUMP (a := b) -> empty;
coherence
proof
  for l being Instruction-Location of SCM R holds NIC(a:=b,l)={Next l} by Th54;
  hence thesis by Lm6;
end;
end;

theorem Th55:
 NIC(AddTo(a,b), il) = {Next il}
proof
  set i = AddTo(a,b);
  for s being State of SCM R st IC s = il & s.il = i
   holds Exec(i,s).IC SCM R = Next IC s by SCMRING2:14;
  hence thesis by Lm5;
end;

definition let R, a, b;
 cluster JUMP AddTo(a, b) -> empty;
coherence
proof
  for l being Instruction-Location of SCM R holds NIC(AddTo(a,b),l)={Next l}
   by Th55;
  hence thesis by Lm6;
end;
end;

theorem Th56:
 NIC(SubFrom(a,b), il) = {Next il}
proof
  set i = SubFrom(a,b);
  for s being State of SCM R st IC s = il & s.il = i
   holds Exec(i,s).IC SCM R = Next IC s by SCMRING2:15;
  hence thesis by Lm5;
end;

definition let R, a, b;
 cluster JUMP SubFrom(a, b) -> empty;
coherence
proof
  for l being Instruction-Location of SCM R holds NIC(SubFrom(a,b),l)={Next l}
   by Th56;
  hence thesis by Lm6;
end;
end;

theorem Th57:
 NIC(MultBy(a,b), il) = {Next il}
proof
  set i = MultBy(a,b);
  for s being State of SCM R st IC s = il & s.il = i
   holds Exec(i,s).IC SCM R = Next IC s by SCMRING2:16;
  hence thesis by Lm5;
end;

definition let R, a, b;
 cluster JUMP MultBy(a,b) -> empty;
coherence
proof
  for l being Instruction-Location of SCM R holds NIC(MultBy(a,b),l)={Next l}
   by Th57;
  hence thesis by Lm6;
end;
end;

theorem Th58:
 NIC(a := r, il) = {Next il}
proof
  set i = a:=r;
  for s being State of SCM R st IC s = il & s.il = i
   holds Exec(i,s).IC SCM R = Next IC s by SCMRING2:19;
  hence thesis by Lm5;
end;

definition let R, a, r;
 cluster JUMP (a := r) -> empty;
coherence
proof
  for l being Instruction-Location of SCM R holds NIC(a:=r,l)={Next l}
   by Th58;
  hence thesis by Lm6;
end;
end;

theorem Th59:
 NIC(goto i1, il) = {i1}
proof
    now let x be set;
  A1: now assume
     A2: x = i1;
         consider t being State of SCM R;
         reconsider il1 = il as Element of ObjectKind IC SCM R by AMI_1:def 11;
         reconsider I = goto i1 as Element of ObjectKind il by AMI_1:def 14;
         set u = t+*((IC SCM R, il)-->(il1, I));
     A3: dom ((IC SCM R, il)-->(il1, I)) = {IC SCM R, il} by FUNCT_4:65;
     then A4: IC SCM R in dom ((IC SCM R, il)-->(il1, I)) by TARSKI:def 2;
     A5: IC SCM R <> il by AMI_1:48;
     A6: IC u = u.IC SCM R by AMI_1:def 15
             .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A4,FUNCT_4:14
             .= il by A5,FUNCT_4:66;
       il in dom ((IC SCM R, il)-->(il1, I)) by A3,TARSKI:def 2;
     then A7: u.il = ((IC SCM R, il)-->(il1, I)).il by FUNCT_4:14
             .= goto i1 by A5,FUNCT_4:66;
           IC Following u = IC Exec(CurInstr u,u) by AMI_1:def 18
           .= IC Exec(u.IC u, u) by AMI_1:def 17
           .= Exec(u.IC u, u).IC SCM R by AMI_1:def 15
           .= i1 by A6,A7,SCMRING2:17;
      hence x in {IC Following s : IC s = il & s.il=goto i1} by A2,A6,A7;
     end;
       now assume
           x in {IC Following s : IC s = il & s.il=goto i1};
         then consider s being State of SCM R such that
     A8: x = IC Following s & IC s = il & s.il = goto i1;
      thus x = IC Exec(CurInstr s,s) by A8,AMI_1:def 18
           .= IC Exec(s.IC s, s) by AMI_1:def 17
           .= Exec(s.IC s, s).IC SCM R by AMI_1:def 15
           .= i1 by A8,SCMRING2:17;
     end;
    hence x in {i1} iff x in {IC Following s : IC s = il & s.il=goto i1}
       by A1,TARSKI:def 1;
  end;
  then {i1} = { IC Following s : IC s = il & s.il = goto i1 } by TARSKI:2;
 hence thesis by AMISTD_1:def 5;
end;

theorem Th60:
 JUMP goto i1 = {i1}
proof
set X = { NIC(goto i1, il) : not contradiction };
A1: JUMP (goto i1) = meet X by AMISTD_1:def 6;
   now
  let x be set;
  hereby assume
  A2: x in meet X;
      reconsider il1 = il.1 as Instruction-Location of SCM R
       by AMI_3:def 1,SCMRING2:def 1;
        NIC(goto i1, il1) in X;
     then x in NIC(goto i1, il1) by A2,SETFAM_1:def 1;
     hence x in {i1} by Th59;
  end;
  assume x in {i1};
  then A3: x = i1 by TARSKI:def 1;
A4:   NIC(goto i1, i1) in X;
        now let Y be set; assume Y in X;
         then consider il being Instruction-Location of SCM R such that
      A5: Y = NIC(goto i1, il);
         NIC(goto i1, il) = {i1} by Th59;
       hence i1 in Y by A5,TARSKI:def 1;
      end;
  hence x in meet X by A3,A4,SETFAM_1:def 1;
 end;
 hence JUMP goto i1 = {i1} by A1,TARSKI:2;
end;

definition let R, i1;
 cluster JUMP goto i1 -> non empty trivial;
coherence
  proof
      JUMP goto i1 = {i1} by Th60;
    hence thesis;
  end;
end;

theorem Th61:
 i1 in NIC(a=0_goto i1, il) & NIC(a=0_goto i1, il) c= {i1, Next il}
proof
   set F = {IC Following s : IC s = il & s.il= a=0_goto i1};
   consider t being State of SCM R;
   reconsider il1 = il as Element of ObjectKind IC SCM R by AMI_1:def 11;
   reconsider I = a=0_goto i1 as Element of ObjectKind il by AMI_1:def 14;
   set u = t+*((IC SCM R, il)-->(il1, I));
   reconsider a' = a as Element of SCM-Data-Loc by SCMRING2:1;
     ObjectKind a = (the Object-Kind of SCM R).a by AMI_1:def 6
      .= (SCM-OK R).a' by SCMRING2:def 1
      .= the carrier of R by SCMRING1:5;
   then reconsider 0R = 0.R as Element of ObjectKind a;
   set v = u+*(a .--> 0R);
   A1: dom ((IC SCM R, il)-->(il1, I)) = {IC SCM R, il} by FUNCT_4:65;
   A2: dom (a .--> 0R) = {a} by CQC_LANG:5;
   A3: IC SCM R in dom ((IC SCM R, il)-->(il1, I)) by A1,TARSKI:def 2;
   A4: IC SCM R <> il by AMI_1:48;
         IC SCM R <> a by Th3;
   then A5: not IC SCM R in dom (a .--> 0R) by A2,TARSKI:def 1;
   A6: IC v = v.IC SCM R by AMI_1:def 15
           .= u.IC SCM R by A5,FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A3,FUNCT_4:14
           .= il by A4,FUNCT_4:66;
   A7: il in dom ((IC SCM R, il)-->(il1, I)) by A1,TARSKI:def 2;
         a <> il by Th2;
       then not il in dom (a .--> 0R) by A2,TARSKI:def 1;
   then A8: v.il = u.il by FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).il by A7,FUNCT_4:14
             .= I by A4,FUNCT_4:66;
         a in dom (a .--> 0R) by A2,TARSKI:def 1;
   then A9: v.a = (a .--> 0R).a by FUNCT_4:14
          .= 0.R by CQC_LANG:6;
         IC Following v = IC Exec(CurInstr v, v) by AMI_1:def 18
           .= IC Exec(v.IC v, v) by AMI_1:def 17
           .= Exec(v.IC v, v).IC SCM R by AMI_1:def 15
           .= i1 by A6,A8,A9,SCMRING2:18;
   then i1 in F by A6,A8;
 hence i1 in NIC(a=0_goto i1, il) by AMISTD_1:def 5;
 let x be set; assume
      x in NIC(a=0_goto i1, il);
    then x in F by AMISTD_1:def 5;
    then consider s being State of SCM R such that
A10: x = IC Following s & IC s = il & s.il = a=0_goto i1;
A11: x = IC Exec(CurInstr s,s) by A10,AMI_1:def 18
     .= IC Exec(s.IC s, s) by AMI_1:def 17
     .= Exec(a=0_goto i1, s).IC SCM R by A10,AMI_1:def 15;
  per cases;
  suppose s.a = 0.R;
    then x = i1 by A11,SCMRING2:18;
   hence x in {i1, Next il} by TARSKI:def 2;
  suppose s.a <> 0.R;
    then x = Next il by A10,A11,SCMRING2:18;
   hence x in {i1, Next il} by TARSKI:def 2;
end;

theorem
  for R being non trivial good Ring,
      a being Data-Location of R,
      il, i1 being Instruction-Location of SCM R
  holds NIC(a=0_goto i1, il) = {i1, Next il}
proof
  let R be non trivial good Ring,
      a be Data-Location of R,
      il, i1 be Instruction-Location of SCM R;
   thus NIC(a=0_goto i1, il) c= {i1, Next il} by Th61;
   let x be set;
   assume
A1:  x in {i1, Next il};
   consider t being State of SCM R;
   reconsider il1 = il as Element of ObjectKind IC SCM R by AMI_1:def 11;
   reconsider I = a=0_goto i1 as Element of ObjectKind il by AMI_1:def 14;
   set u = t+*((IC SCM R, il)-->(il1, I));
   reconsider a' = a as Element of SCM-Data-Loc by SCMRING2:1;
A2:ObjectKind a = (the Object-Kind of SCM R).a by AMI_1:def 6
      .= (SCM-OK R).a' by SCMRING2:def 1
      .= the carrier of R by SCMRING1:5;
   A3: IC SCM R <> il by AMI_1:48;
A4:   a <> il by Th2;
A5:   IC SCM R <> a by Th3;
   set F = {IC Following s where s is State of SCM R:
    IC s = il & s.il= a=0_goto i1};
   per cases by A1,TARSKI:def 2;
   suppose
A6:  x = i1;
   reconsider 0R = 0.R as Element of ObjectKind a by A2;
   set v = u+*(a .--> 0R);
   A7: dom ((IC SCM R, il)-->(il1, I)) = {IC SCM R, il} by FUNCT_4:65;
   A8: dom (a .--> 0R) = {a} by CQC_LANG:5;
   A9: IC SCM R in dom ((IC SCM R, il)-->(il1, I)) by A7,TARSKI:def 2;
   A10: not IC SCM R in dom (a .--> 0R) by A5,A8,TARSKI:def 1;
   A11: IC v = v.IC SCM R by AMI_1:def 15
           .= u.IC SCM R by A10,FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A9,FUNCT_4:14
           .= il by A3,FUNCT_4:66;
   A12: il in dom ((IC SCM R, il)-->(il1, I)) by A7,TARSKI:def 2;
    not il in dom (a .--> 0R) by A4,A8,TARSKI:def 1;
   then A13: v.il = u.il by FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).il by A12,FUNCT_4:14
             .= I by A3,FUNCT_4:66;
         a in dom (a .--> 0R) by A8,TARSKI:def 1;
   then A14: v.a = (a .--> 0R).a by FUNCT_4:14
          .= 0.R by CQC_LANG:6;
         IC Following v = IC Exec(CurInstr v, v) by AMI_1:def 18
           .= IC Exec(v.IC v, v) by AMI_1:def 17
           .= Exec(v.IC v, v).IC SCM R by AMI_1:def 15
           .= i1 by A11,A13,A14,SCMRING2:18;
   then i1 in F by A11,A13;
   hence thesis by A6,AMISTD_1:def 5;
   suppose
A15:  x = Next il;
   consider e being Element of R such that
A16:   e <> 0.R by ANPROJ_1:def 8;
   reconsider E = e as Element of ObjectKind a by A2;
   set v = u+*(a .--> E);
   A17: dom ((IC SCM R, il)-->(il1, I)) = {IC SCM R, il} by FUNCT_4:65;
   A18: dom (a .--> E) = {a} by CQC_LANG:5;
   A19: IC SCM R in dom ((IC SCM R, il)-->(il1, I)) by A17,TARSKI:def 2;
   A20: not IC SCM R in dom (a .--> E) by A5,A18,TARSKI:def 1;
   A21: IC v = v.IC SCM R by AMI_1:def 15
           .= u.IC SCM R by A20,FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).IC SCM R by A19,FUNCT_4:14
           .= il by A3,FUNCT_4:66;
   A22: il in dom ((IC SCM R, il)-->(il1, I)) by A17,TARSKI:def 2;
    not il in dom (a .--> E) by A4,A18,TARSKI:def 1;
   then A23: v.il = u.il by FUNCT_4:12
           .= ((IC SCM R, il)-->(il1, I)).il by A22,FUNCT_4:14
             .= I by A3,FUNCT_4:66;
         a in dom (a .--> E) by A18,TARSKI:def 1;
   then A24: v.a = (a .--> E).a by FUNCT_4:14
          .= E by CQC_LANG:6;
         IC Following v = IC Exec(CurInstr v, v) by AMI_1:def 18
           .= IC Exec(v.IC v, v) by AMI_1:def 17
           .= Exec(v.IC v, v).IC SCM R by AMI_1:def 15
           .= Next il by A16,A21,A23,A24,SCMRING2:18;
   then Next il in F by A21,A23;
   hence thesis by A15,AMISTD_1:def 5;
end;

theorem Th63:
 JUMP (a=0_goto i1) = {i1}
proof
set X = { NIC(a=0_goto i1, il) : not contradiction };
A1: JUMP (a=0_goto i1) = meet X by AMISTD_1:def 6;
   now
  let x be set;
  hereby assume
  A2: x in meet X;
      reconsider il1 = il.1, il2 = il.2 as Instruction-Location of SCM R
       by AMI_3:def 1,SCMRING2:def 1;
        NIC(a=0_goto i1, il1) in X & NIC(a=0_goto i1, il2) in X;
  then A3: x in NIC(a=0_goto i1, il1) & x in NIC(a=0_goto i1, il2)
       by A2,SETFAM_1:def 1;
        NIC(a=0_goto i1, il1) c= {i1, Next il1} &
      NIC(a=0_goto i1, il2) c= {i1, Next il2} by Th61;
  then A4: (x = i1 or x = Next il1) & (x = i1 or x = Next il2) by A3,TARSKI:def
2;
        il1 <> il2 by AMI_3:53;
   hence x in {i1} by A4,Th6,TARSKI:def 1;
  end;
  assume x in {i1};
  then A5: x = i1 by TARSKI:def 1;
A6:   NIC(a=0_goto i1, i1) in X;
        now let Y be set; assume Y in X;
         then ex il being Instruction-Location of SCM R st
          Y = NIC(a=0_goto i1, il);
        hence i1 in Y by Th61;
      end;
  hence x in meet X by A5,A6,SETFAM_1:def 1;
 end;
 hence JUMP (a=0_goto i1) = {i1} by A1,TARSKI:2;
end;

definition let R, a, i1;
 cluster JUMP (a =0_goto i1) -> non empty trivial;
coherence
  proof
      JUMP (a =0_goto i1) = {i1} by Th63;
    hence thesis;
  end;
end;

theorem Th64:
 SUCC il = {il, Next il}
proof
   set X = { NIC(I, il) \ JUMP I where
    I is Element of the Instructions of SCM R: not contradiction };
   set N = {il, Next il};
    now let x be set;
   hereby assume x in union X; then consider Y being set such that
   A1: x in Y & Y in X by TARSKI:def 4;
       consider i being Element of the Instructions of SCM R such that
   A2: Y = NIC(i, il) \ JUMP i by A1;
    per cases by SCMRING2:8;
    suppose i = [0,{}]; then i = halt SCM R by SCMRING2:30;
      then x in {il} \ JUMP halt SCM R by A1,A2,Th53;
      then x = il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
    suppose ex a,b st i = a:=b; then consider a, b such that
    A4: i = a:=b;
        x in {Next il} \ JUMP (a:=b) by A1,A2,A4,Th54;
      then x = Next il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
    suppose ex a,b st i = AddTo(a,b); then consider a, b such that
    A5: i = AddTo(a,b);
        x in {Next il} \ JUMP AddTo(a,b) by A1,A2,A5,Th55;
      then x = Next il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
    suppose ex a,b st i = SubFrom(a,b); then consider a, b such that
    A6: i = SubFrom(a,b);
        x in {Next il} \ JUMP SubFrom(a,b) by A1,A2,A6,Th56;
      then x = Next il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
    suppose ex a,b st i = MultBy(a,b); then consider a, b such that
    A7: i = MultBy(a,b);
        x in {Next il} \ JUMP MultBy(a,b) by A1,A2,A7,Th57;
      then x = Next il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
    suppose ex i1 st i = goto i1; then consider i1 such that
    A8: i = goto i1;
        x in {i1} \ JUMP i by A1,A2,A8,Th59;
      then x in {i1} \ {i1} by A8,Th60;
     hence x in N by XBOOLE_1:37;
    suppose ex a,i1 st i = a=0_goto i1; then consider a, i1 such that
    A9:  i = a=0_goto i1;
          x in NIC(i, il) \ {i1} by A1,A2,A9,Th63;
    then A10: x in NIC(i, il) & not x in {i1} by XBOOLE_0:def 4;
          NIC(i, il) c= {i1, Next il} by A9,Th61;
        then x = i1 or x = Next il by A10,TARSKI:def 2;
     hence x in N by A10,TARSKI:def 1,def 2;
    suppose ex a,r st i = a:=r; then consider a, r such that
    A11: i = a := r;
        x in {Next il} \ JUMP (a:=r) by A1,A2,A11,Th58;
      then x = Next il by TARSKI:def 1;
     hence x in N by TARSKI:def 2;
   end;
   assume A12: x in {il, Next il};
   per cases by A12,TARSKI:def 2;
   suppose A13: x = il;
     set i = halt SCM R;
       NIC(i, il) \ JUMP i = {il} by Th53;
     then x in {il} & {il} in X by A13,TARSKI:def 1;
    hence x in union X by TARSKI:def 4;
   suppose A14: x = Next il;
    consider a, b being Data-Location of R;
    set i = AddTo(a,b);
      NIC(i, il) \ JUMP i = {Next il} by Th55;
     then x in {Next il} & {Next il} in X by A14,TARSKI:def 1;
    hence x in union X by TARSKI:def 4;
  end;
  then union X = {il, Next il} by TARSKI:2;
 hence SUCC il = {il, Next il} by AMISTD_1:def 7;
end;

theorem Th65:
 for f being Function of NAT, the Instruction-Locations of SCM R
   st for k being Nat holds f.k = il.k holds
  f is bijective &
  for k being Nat holds f.(k+1) in SUCC (f.k) &
   for j being Nat st f.j in SUCC (f.k) holds k <= j
  proof
    let f be Function of NAT, the Instruction-Locations of SCM R such that
A1:   for k being Nat holds f.k = il.k;
A2: the Instruction-Locations of SCM
    = the Instruction-Locations of SCM R by AMI_3:def 1,SCMRING2:def 1;
   thus
A3:   f is bijective
   proof
    thus f is one-to-one
    proof let x1, x2 be set such that
  A4: x1 in dom f & x2 in dom f and
  A5: f.x1 = f.x2;
      reconsider k1 = x1, k2 = x2 as Nat by A4,FUNCT_2:def 1;
        f.k1 = il.k1 & f.k2 = il.k2 by A1;
      hence x1 = x2 by A5,AMI_3:53;
    end;
    thus f is onto
    proof
     thus rng f c= the Instruction-Locations of SCM R by RELSET_1:12;
     thus the Instruction-Locations of SCM R c= rng f proof
     let x be set; assume x in the Instruction-Locations of SCM R;
      then consider i being Nat such that
    A6: x = il.i by A2,AMI_5:19;
          dom f = NAT by FUNCT_2:def 1;
        then il.i = f.i & i in dom f by A1;
    hence x in rng f by A6,FUNCT_1:def 5;
   end;
  end;
  end;
 let k be Nat;
   A7: SUCC (f.k) = {f.k, Next (f.k)} by Th64;
   A8: f.(k+1) = il.(k+1) & f.k = il.k by A1;
       consider m being Element of SCM-Instr-Loc such that
   A9:   m = f.k & Next m = Next (f.k) by SCMRING2:def 10;
       consider p being Element of SCM-Instr-Loc such that
   A10:   p = il.k & Next il.k = Next p by AMI_3:def 11;
   A11: f.(k+1) = il.(k+1) by A1
              .= Next il.k by AMI_3:54;
    hence f.(k+1) in SUCC (f.k) by A7,A8,A9,A10,TARSKI:def 2;
    let j be Nat;
    assume
 A12:  f.j in SUCC (f.k);
   A13: f is one-to-one by A3,FUNCT_2:def 4;
   A14: dom f = NAT by FUNCT_2:def 1;
     per cases by A7,A12,TARSKI:def 2;
     suppose f.j = f.k;
      hence k <= j by A13,A14,FUNCT_1:def 8;
     suppose f.j = Next (f.k);
         then j = k+1 by A8,A9,A10,A11,A13,A14,FUNCT_1:def 8;
      hence k <= j by NAT_1:29;
   end;

definition let R;
 cluster SCM R -> standard;
coherence
  proof deffunc U(Nat) = il.$1;
    consider f being Function of NAT, the Instruction-Locations of SCM
       such that
A1:   for k being Nat holds f.k = U(k) from LambdaD;
      the Instruction-Locations of SCM
     = the Instruction-Locations of SCM R by AMI_3:def 1,SCMRING2:def 1;
    then reconsider f as Function of NAT, the Instruction-Locations of SCM R;
      for k being Nat holds f.k = il.k by A1;
    then f is bijective &
     for k being Nat holds f.(k+1) in SUCC (f.k) &
      for j being Nat st f.j in SUCC (f.k) holds k <= j by Th65;
    hence SCM R is standard by AMISTD_1:19;
  end;
end;

theorem Th66:
 il.(SCM R,k) = il.k
  proof deffunc U(Nat) = il.$1;
    consider f being Function of NAT, the Instruction-Locations of SCM
      such that
A1:   for k being Nat holds f.k = U(k) from LambdaD;
      the Instruction-Locations of SCM
     = the Instruction-Locations of SCM R by AMI_3:def 1,SCMRING2:def 1;
    then reconsider f as Function of NAT, the Instruction-Locations of SCM R;
A2:  for k being Nat holds f.k = il.k by A1;
then A3:  f is bijective by Th65;
A4:  for k being Nat holds f.(k+1) in SUCC (f.k) &
      for j being Nat st f.j in SUCC (f.k) holds k <= j by A2,Th65;
    reconsider k as Nat by ORDINAL2:def 21;
      ex f being Function of NAT, the Instruction-Locations of SCM R st
     f is bijective &
     (for m, n being Nat holds m <= n iff f.m <= f.n) &
     il.k = f.k
    proof
      take f;
      thus f is bijective by A2,Th65;
      thus for m, n being Nat holds m <= n iff f.m <= f.n by A3,A4,AMISTD_1:18
;
      thus thesis by A1;
    end;
    hence thesis by AMISTD_1:def 12;
  end;

theorem Th67:
 Next il.(SCM R,k) = il.(SCM R,k+1)
  proof
A1: ex mj being Element of SCM-Instr-Loc st mj = il.(SCM R,k) &
     Next il.(SCM R,k) = Next mj by SCMRING2:def 10;
      ex mj1 being Element of SCM-Instr-Loc st mj1 = il.k &
     Next il.k = Next mj1 by AMI_3:def 11;
    hence Next il.(SCM R,k) = Next il.k by A1,Th66
      .= il.(k+1) by AMI_3:54
      .= il.(SCM R,k+1) by Th66;
  end;

theorem Th68:
 Next il = NextLoc il
  proof
      Next il = il.(SCM R,locnum il + 1)
    proof
        Next il.(SCM R,locnum il) = il.(SCM R,locnum il+1) by Th67;
      hence thesis by AMISTD_1:def 13;
    end;
    hence thesis by AMISTD_1:34;
  end;

definition let R be good Ring, k be Nat;
 func dl.(R,k) -> Data-Location of R equals :Def1:
  dl.k;
coherence
  proof
      dl.k in SCM-Data-Loc by AMI_3:def 2;
    hence thesis by SCMRING2:1;
  end;
end;

definition let R;
 cluster InsCode halt SCM R -> jump-only;
coherence
  proof
    let s be State of SCM R, o be Object of SCM R, I be Instruction of SCM R;
    assume that
A1:   InsCode I = InsCode halt SCM R and
        o <> IC SCM R;
      InsCode halt SCM R = 0 by Th8;
    then I = halt SCM R by A1,Th16;
    hence Exec(I, s).o = s.o by AMI_1:def 8;
  end;
end;

definition let R;
 cluster halt SCM R -> jump-only;
coherence
  proof
    thus InsCode halt SCM R is jump-only;
  end;
end;

definition let R, i1;
 cluster InsCode goto i1 -> jump-only;
coherence
  proof
    set S = SCM R;
    let s be State of S, o be Object of S, I be Instruction of S;
    assume that
A1:    InsCode I = InsCode goto i1 and
A2:    o <> IC S;
      InsCode goto i1 = 6 by Th14;
    then consider i2 such that
A3:    I = goto i2 by A1,Th22;
    per cases by A2,Th5;
    suppose o in the Instruction-Locations of S;
    hence Exec(I, s).o = s.o by AMI_1:def 13;
    suppose o is Data-Location of R;
    hence Exec(I, s).o = s.o by A3,SCMRING2:17;
  end;
end;

definition let R, i1;
 cluster goto i1 -> jump-only;
coherence
  proof
    thus InsCode goto i1 is jump-only;
  end;
end;

definition let R, a, i1;
 cluster InsCode (a =0_goto i1) -> jump-only;
coherence
  proof
    set S = SCM R;
    let s be State of S, o be Object of S, I be Instruction of S;
    assume that
A1:    InsCode I = InsCode (a =0_goto i1) and
A2:    o <> IC S;
      InsCode (a =0_goto i1) = 7 by Th15;
    then consider b, i2 such that
A3:    I = (b =0_goto i2) by A1,Th23;
    per cases by A2,Th5;
    suppose o in the Instruction-Locations of S;
    hence Exec(I, s).o = s.o by AMI_1:def 13;
    suppose o is Data-Location of R;
    hence Exec(I, s).o = s.o by A3,SCMRING2:18;
  end;
end;

definition let R, a, i1;
 cluster a =0_goto i1 -> jump-only;
coherence
  proof
    thus InsCode (a =0_goto i1) is jump-only;
  end;
end;

reserve S for non trivial good Ring,
        p, q for Data-Location of S,
        w for Element of S;

definition let S, p, q;
 cluster InsCode (p:=q) -> non jump-only;
coherence
proof
   consider e being Element of S such that
A1:   e <> 0.S by ANPROJ_1:def 8;
   reconsider e as Element of S;
   consider w being State of SCM S;
   set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A2: InsCode (p:=q) = 1 by Th9
    .= InsCode (dl.(S,0):=dl.(S,1)) by Th9;
A3: IC SCM S = IC SCM by AMI_3:4,SCMRING2:9;
A4: dl.(S,0) = dl.0 by Def1;
then A5: dl.(S,0) <> IC SCM S by A3,AMI_3:57;
     dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:65
;
then A6: dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) &
   dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
     dl.(S,1) = dl.1 by Def1;
then A7: dl.(S,0) <> dl.(S,1) by A4,AMI_3:52;
A8: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by A6,FUNCT_4:14
             .= 0.S by A7,FUNCT_4:66;
     Exec((dl.(S,0):=dl.(S,1)), t).dl.(S,0)
    = t.dl.(S,1) by SCMRING2:13
   .= (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by A6,FUNCT_4:14
   .= e by A7,FUNCT_4:66;
  hence thesis by A1,A2,A5,A8,AMISTD_1:def 3;
end;
end;

definition let S, p, q;
 cluster p:=q -> non jump-only;
coherence
  proof
    thus InsCode (p:=q) is not jump-only;
  end;
end;

definition let S, p, q;
 cluster InsCode AddTo(p,q) -> non jump-only;
coherence
proof
   consider e being Element of S such that
A1:   e <> 0.S by ANPROJ_1:def 8;
   reconsider e as Element of S;
   consider w being State of SCM S;
   set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A2: InsCode AddTo(p,q) = 2 by Th10
    .= InsCode AddTo(dl.(S,0), dl.(S,1)) by Th10;
A3: IC SCM S = IC SCM by AMI_3:4,SCMRING2:9;
A4: dl.(S,0) = dl.0 by Def1;
then A5: dl.(S,0) <> IC SCM S by A3,AMI_3:57;
     dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:65
;
then A6: dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) &
   dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
     dl.(S,1) = dl.1 by Def1;
then A7: dl.(S,0) <> dl.(S,1) by A4,AMI_3:52;
A8: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by A6,FUNCT_4:14
             .= 0.S by A7,FUNCT_4:66;
A9: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by A6,FUNCT_4:14
             .= e by A7,FUNCT_4:66;
     Exec(AddTo(dl.(S,0), dl.(S,1)), t).dl.(S,0)
    = t.dl.(S,0) + t.dl.(S,1) by SCMRING2:14
   .= e by A8,A9,RLVECT_1:10;
  hence thesis by A1,A2,A5,A8,AMISTD_1:def 3;
end;
end;

definition let S, p, q;
 cluster AddTo(p, q) -> non jump-only;
coherence
  proof
    thus InsCode AddTo(p, q) is not jump-only;
  end;
end;

definition let S, p, q;
 cluster InsCode SubFrom(p,q) -> non jump-only;
coherence
proof
   consider e being Element of S such that
A1:   e <> 0.S by ANPROJ_1:def 8;
   reconsider e as Element of S;
   consider w being State of SCM S;
   set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A2: InsCode SubFrom(p,q) = 3 by Th11
    .= InsCode SubFrom(dl.(S,0), dl.(S,1)) by Th11;
A3: IC SCM S = IC SCM by AMI_3:4,SCMRING2:9;
A4: dl.(S,0) = dl.0 by Def1;
then A5: dl.(S,0) <> IC SCM S by A3,AMI_3:57;
     dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:65
;
then A6: dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) &
   dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
     dl.(S,1) = dl.1 by Def1;
then A7: dl.(S,0) <> dl.(S,1) by A4,AMI_3:52;
A8: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by A6,FUNCT_4:14
             .= 0.S by A7,FUNCT_4:66;
A9: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by A6,FUNCT_4:14
             .= e by A7,FUNCT_4:66;
A10: Exec(SubFrom(dl.(S,0), dl.(S,1)), t).dl.(S,0)
    = t.dl.(S,0) - t.dl.(S,1) by SCMRING2:15
   .= -e by A8,A9,RLVECT_1:27;
    now
    assume -e = 0.S;
    then e = -0.S by RLVECT_1:30;
    hence contradiction by A1,RLVECT_1:25;
  end;
  hence thesis by A2,A5,A8,A10,AMISTD_1:def 3;
end;
end;

definition let S, p, q;
 cluster SubFrom(p, q) -> non jump-only;
coherence
  proof
    thus InsCode SubFrom(p, q) is not jump-only;
  end;
end;

definition let S, p, q;
 cluster InsCode MultBy(p,q) -> non jump-only;
coherence
proof
A1: 0.S <> 1_ S by LMOD_6:def 2;
   consider w being State of SCM S;
   set t = w+*((dl.(S,0), dl.(S,1))-->(1_ S,0.S));
A2: InsCode MultBy(p,q) = 4 by Th12
    .= InsCode MultBy(dl.(S,0), dl.(S,1)) by Th12;
A3: IC SCM S = IC SCM by AMI_3:4,SCMRING2:9;
A4:  dl.(S,0) = dl.0 by Def1;
then A5:  dl.(S,0) <> IC SCM S by A3,AMI_3:57;
      dom ((dl.(S,0), dl.(S,1))-->(1_ S,0.S)) = {dl.(S,0), dl.(S,1)} by FUNCT_4
:65;
     then A6: dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(1_ S,0.S)) &
   dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(1_ S,0.S)) by TARSKI:def 2;
     dl.(S,1) = dl.1 by Def1;
then A7: dl.(S,0) <> dl.(S,1) by A4,AMI_3:52;
A8: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(1_ S,0.S).dl.(S,0) by A6,FUNCT_4:14
             .= 1_ S by A7,FUNCT_4:66;
A9: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(1_ S,0.S).dl.(S,1) by A6,FUNCT_4:14
             .= 0.S by A7,FUNCT_4:66;
     Exec(MultBy(dl.(S,0), dl.(S,1)), t).dl.(S,0)
    = t.dl.(S,0) * t.dl.(S,1) by SCMRING2:16
   .= 0.S by A9,VECTSP_1:36;
  hence thesis by A1,A2,A5,A8,AMISTD_1:def 3;
end;
end;

definition let S, p, q;
 cluster MultBy(p, q) -> non jump-only;
coherence
  proof
    thus InsCode MultBy(p, q) is not jump-only;
  end;
end;

definition let S, p, w;
 cluster InsCode (p:=w) -> non jump-only;
coherence
  proof
      the carrier of S <> {w};
    then consider e being set such that
A1:   e in the carrier of S and
A2:   e <> w by ZFMISC_1:41;
    reconsider e as Element of S by A1;
    consider j being State of SCM S;
      ObjectKind dl.(S,0) = the carrier of S by Th1;
    then reconsider v = dl.(S,0) .--> e as FinPartState of SCM S by AMI_1:59;
    set t = j+*v;
A3: InsCode (p:=w) = 5 by Th13
      .= InsCode (dl.(S,0):=w) by Th13;
A4: IC SCM S = IC SCM by AMI_3:4,SCMRING2:9;
      dl.(S,0) = dl.0 by Def1;
then A5: dl.(S,0) <> IC SCM S by A4,AMI_3:57;
      dom (dl.(S,0).-->e) = {dl.(S,0)} by CQC_LANG:5;
then dl.(S,0) in dom (dl.(S,0).-->e) by TARSKI:def 1;
then A6: t.dl.(S,0) = (dl.(S,0) .--> e).dl.(S,0) by FUNCT_4:14
              .= e by CQC_LANG:6;
      Exec((dl.(S,0):=w), t).dl.(S,0) = w by SCMRING2:19;
    hence thesis by A2,A3,A5,A6,AMISTD_1:def 3;
  end;
end;

definition let S, p, w;
 cluster p:=w -> non jump-only;
coherence
  proof
    thus InsCode (p:=w) is not jump-only;
  end;
end;

definition let R, a, b;
 cluster a:=b -> sequential;
coherence
  proof
    let s be State of SCM R;
      Next IC s = NextLoc IC s by Th68;
    hence thesis by SCMRING2:13;
  end;
end;

definition let R, a, b;
 cluster AddTo(a,b) -> sequential;
coherence
  proof
    let s be State of SCM R;
      Next IC s = NextLoc IC s by Th68;
    hence thesis by SCMRING2:14;
  end;
end;

definition let R, a, b;
 cluster SubFrom(a,b) -> sequential;
coherence
  proof
    let s be State of SCM R;
      Next IC s = NextLoc IC s by Th68;
    hence thesis by SCMRING2:15;
  end;
end;

definition let R, a, b;
 cluster MultBy(a,b) -> sequential;
coherence
  proof
    let s be State of SCM R;
      Next IC s = NextLoc IC s by Th68;
    hence thesis by SCMRING2:16;
  end;
end;

definition let R, a, r;
 cluster a:=r -> sequential;
coherence
  proof
    let s be State of SCM R;
      Next IC s = NextLoc IC s by Th68;
    hence thesis by SCMRING2:19;
  end;
end;

definition let R, i1;
 cluster goto i1 -> non sequential;
coherence
  proof
      JUMP goto i1 <> {};
    hence thesis by AMISTD_1:43;
  end;
end;

definition let R, a, i1;
 cluster a =0_goto i1 -> non sequential;
coherence
  proof
      JUMP (a =0_goto i1) <> {};
    hence thesis by AMISTD_1:43;
  end;
end;

definition let R, i1;
 cluster goto i1 -> non ins-loc-free;
coherence
  proof
    take 1;
      dom AddressPart goto i1 = dom <*i1*> by Th30
      .= {1} by FINSEQ_1:4,def 8;
    hence 1 in dom AddressPart goto i1 by TARSKI:def 1;
    thus thesis by Th50;
  end;
end;

definition let R, a, i1;
 cluster a =0_goto i1 -> non ins-loc-free;
coherence
  proof
    take 1;
      dom AddressPart (a =0_goto i1) = dom <*i1,a*> by Th31
      .= {1,2} by FINSEQ_1:4,FINSEQ_3:29;
    hence 1 in dom AddressPart (a =0_goto i1) by TARSKI:def 2;
    thus thesis by Th51;
  end;
end;

definition let R;
 cluster SCM R -> homogeneous with_explicit_jumps without_implicit_jumps;
coherence
  proof
    thus SCM R is homogeneous
    proof
      let I, J be Instruction of SCM R such that
A1:     InsCode I = InsCode J;
A2:   J = [0,{}] or
      (ex a,b st J = a:=b) or
      (ex a,b st J = AddTo(a,b)) or
      (ex a,b st J = SubFrom(a,b)) or
      (ex a,b st J = MultBy(a,b)) or
      (ex i1 st J = goto i1) or
      (ex a,i1 st J = a=0_goto i1) or
      ex a,r st J = a:=r by SCMRING2:8;
      per cases by SCMRING2:8;
      suppose
A3:     I = [0,{}];
      then I = halt SCM R by SCMRING2:30;
      then InsCode I = 0 by Th8;
      hence thesis by A1,A2,A3,Th9,Th10,Th11,Th12,Th13,Th14,Th15;
      suppose ex a,b st I = a:=b;
      then consider a, b such that
A4:     I = a:=b;
A5:   InsCode I = 1 by A4,Th9;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A5,Th8;
        suppose ex a,b st J = a:=b;
        then consider d1, d2 such that
A6:       J = d1:=d2;
        thus dom AddressPart I = dom <*a,b*> by A4,Th25
          .= Seg 2 by FINSEQ_3:29
          .= dom <*d1,d2*> by FINSEQ_3:29
          .= dom AddressPart J by A6,Th25;
        suppose (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,i1 st J = a=0_goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A5,Th10,Th11,Th12,Th13,Th14,Th15;
      end;
      hence thesis;
      suppose ex a,b st I = AddTo(a,b);
      then consider a, b such that
A7:     I = AddTo(a,b);
A8:   InsCode I = 2 by A7,Th10;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A8,Th8;
        suppose ex a,b st J = AddTo(a,b);
        then consider d1, d2 such that
A9:       J = AddTo(d1,d2);
        thus dom AddressPart I = dom <*a,b*> by A7,Th26
          .= Seg 2 by FINSEQ_3:29
          .= dom <*d1,d2*> by FINSEQ_3:29
          .= dom AddressPart J by A9,Th26;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,i1 st J = a=0_goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A8,Th9,Th11,Th12,Th13,Th14,Th15;
      end;
      hence thesis;
      suppose ex a,b st I = SubFrom(a,b);
      then consider a, b such that
A10:     I = SubFrom(a,b);
A11:   InsCode I = 3 by A10,Th11;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A11,Th8;
        suppose ex a,b st J = SubFrom(a,b);
        then consider d1, d2 such that
A12:       J = SubFrom(d1,d2);
        thus dom AddressPart I = dom <*a,b*> by A10,Th27
          .= Seg 2 by FINSEQ_3:29
          .= dom <*d1,d2*> by FINSEQ_3:29
          .= dom AddressPart J by A12,Th27;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,i1 st J = a=0_goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A11,Th9,Th10,Th12,Th13,Th14,Th15;
      end;
      hence thesis;
      suppose ex a,b st I = MultBy(a,b);
      then consider a, b such that
A13:     I = MultBy(a,b);
A14:   InsCode I = 4 by A13,Th12;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A14,Th8;
        suppose ex a,b st J = MultBy(a,b);
        then consider d1, d2 such that
A15:       J = MultBy(d1,d2);
        thus dom AddressPart I = dom <*a,b*> by A13,Th28
          .= Seg 2 by FINSEQ_3:29
          .= dom <*d1,d2*> by FINSEQ_3:29
          .= dom AddressPart J by A15,Th28;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,i1 st J = a=0_goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A14,Th9,Th10,Th11,Th13,Th14,Th15;
      end;
      hence thesis;
      suppose ex i1 st I = goto i1;
      then consider i1 such that
A16:     I = goto i1;
A17:   InsCode I = 6 by A16,Th14;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A17,Th8;
        suppose ex i2 st J = goto i2;
        then consider i2 such that
A18:       J = goto i2;
        thus dom AddressPart I = dom <*i1*> by A16,Th30
          .= Seg 1 by FINSEQ_1:def 8
          .= dom <*i2*> by FINSEQ_1:def 8
          .= dom AddressPart J by A18,Th30;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex a,i1 st J = a=0_goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A17,Th9,Th10,Th11,Th12,Th13,Th15;
      end;
      hence thesis;
      suppose ex a,i1 st I = a=0_goto i1;
      then consider a, i1 such that
A19:     I = a=0_goto i1;
A20:   InsCode I = 7 by A19,Th15;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A20,Th8;
        suppose ex d1,i2 st J = d1 =0_goto i2;
        then consider d1, i2 such that
A21:       J = d1 =0_goto i2;
        thus dom AddressPart I = dom <*i1,a*> by A19,Th31
          .= Seg 2 by FINSEQ_3:29
          .= dom <*i2,d1*> by FINSEQ_3:29
          .= dom AddressPart J by A21,Th31;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,r st J = a:=r);
        hence dom AddressPart I = dom AddressPart J
          by A1,A20,Th9,Th10,Th11,Th12,Th13,Th14;
      end;
      hence thesis;
      suppose ex a,r st I = a:=r;
      then consider a, r such that
A22:     I = a:=r;
A23:   InsCode I = 5 by A22,Th13;
        now per cases by SCMRING2:8;
        suppose J = [0,{}];
        then J = halt SCM R by SCMRING2:30;
        hence dom AddressPart I = dom AddressPart J by A1,A23,Th8;
        suppose ex a,r st J = a:=r;
        then consider b being Data-Location of R,
                 r1 being Element of R such that
A24:       J = b:=r1;
        thus dom AddressPart I = dom <*a,r*> by A22,Th29
          .= Seg 2 by FINSEQ_3:29
          .= dom <*b,r1*> by FINSEQ_3:29
          .= dom AddressPart J by A24,Th29;
        suppose (ex a,b st J = a:=b) or
                (ex a,b st J = AddTo(a,b)) or
                (ex a,b st J = SubFrom(a,b)) or
                (ex a,b st J = MultBy(a,b)) or
                (ex i1 st J = goto i1) or
                (ex a,i1 st J = a =0_goto i1);
        hence dom AddressPart I = dom AddressPart J
          by A1,A23,Th9,Th10,Th11,Th12,Th14,Th15;
      end;
      hence thesis;
    end;

    thus SCM R is with_explicit_jumps
    proof
      let I be Instruction of SCM R;
      let f be set such that
A25:     f in JUMP I;
      per cases by SCMRING2:8;
      suppose
A26:     I = [0,{}];
        JUMP halt SCM R is empty;
      hence thesis by A25,A26,SCMRING2:30;
      suppose ex a,b st I = a:=b;
      then consider a, b such that
A27:     I = a:=b;
        JUMP (a:=b) is empty;
      hence thesis by A25,A27;
      suppose ex a,b st I = AddTo(a,b);
      then consider a, b such that
A28:     I = AddTo(a,b);
        JUMP AddTo(a,b) is empty;
      hence thesis by A25,A28;
      suppose ex a,b st I = SubFrom(a,b);
      then consider a, b such that
A29:     I = SubFrom(a,b);
        JUMP SubFrom(a,b) is empty;
      hence thesis by A25,A29;
      suppose ex a,b st I = MultBy(a,b);
      then consider a, b such that
A30:     I = MultBy(a,b);
        JUMP MultBy(a,b) is empty;
      hence thesis by A25,A30;
      suppose ex i1 st I = goto i1;
      then consider i1 such that
A31:     I = goto i1;
        JUMP goto i1 = {i1} by Th60;
then A32:   f = i1 by A25,A31,TARSKI:def 1;
      take 1;
A33:   AddressPart goto i1 = <*i1*> by Th30;
        dom <*i1*> = Seg 1 by FINSEQ_1:def 8;
      hence 1 in dom AddressPart I by A31,A33,FINSEQ_1:4,TARSKI:def 1;
      thus f = (AddressPart I).1 &
       (PA AddressParts InsCode I).1 = the Instruction-Locations of SCM R
        by A31,A32,A33,Th50,FINSEQ_1:def 8;
      suppose ex a,i1 st I = a=0_goto i1;
      then consider a, i1 such that
A34:     I = a=0_goto i1;
        JUMP (a=0_goto i1) = {i1} by Th63;
then A35:   f = i1 by A25,A34,TARSKI:def 1;
      take 1;
A36:   AddressPart (a=0_goto i1) = <*i1,a*> by Th31;
        dom <*i1,a*> = Seg 2 by FINSEQ_3:29;
      hence 1 in dom AddressPart I by A34,A36,FINSEQ_1:4,TARSKI:def 2;
      thus f = (AddressPart I).1 &
       (PA AddressParts InsCode I).1 = the Instruction-Locations of SCM R
        by A34,A35,A36,Th51,FINSEQ_1:61;
      suppose ex a,r st I = a:=r;
      then consider a, r such that
A37:     I = a:=r;
        JUMP (a:=r) is empty;
      hence thesis by A25,A37;
    end;

    let I be Instruction of SCM R;
    let f be set;
    given k being set such that
A38:   k in dom AddressPart I and
A39:   f = (AddressPart I).k and
A40:   (PA AddressParts InsCode I).k = the Instruction-Locations of SCM R;
A41: SCM-Data-Loc <> the Instruction-Locations of SCM R by Th4;
    per cases by SCMRING2:8;
    suppose I = [0,{}];
    then I = halt SCM R by SCMRING2:30;
    then dom AddressPart I = dom {} by Th24;
    hence thesis by A38;
    suppose ex a,b st I = a:=b;
    then consider a, b such that
A42:   I = a:=b;
      k in dom <*a,b*> by A38,A42,Th25;
    then k = 1 or k = 2 by Lm2;
    hence thesis by A40,A41,A42,Th40,Th41;
    suppose ex a,b st I = AddTo(a,b);
    then consider a, b such that
A43:   I = AddTo(a,b);
      k in dom <*a,b*> by A38,A43,Th26;
    then k = 1 or k = 2 by Lm2;
    hence thesis by A40,A41,A43,Th42,Th43;
    suppose ex a,b st I = SubFrom(a,b);
    then consider a, b such that
A44:   I = SubFrom(a,b);
      k in dom <*a,b*> by A38,A44,Th27;
    then k = 1 or k = 2 by Lm2;
    hence thesis by A40,A41,A44,Th44,Th45;
    suppose ex a,b st I = MultBy(a,b);
    then consider a, b such that
A45:   I = MultBy(a,b);
      k in dom <*a,b*> by A38,A45,Th28;
    then k = 1 or k = 2 by Lm2;
    hence thesis by A40,A41,A45,Th46,Th47;
    suppose ex i1 st I = goto i1;
    then consider i1 such that
A46:   I = goto i1;
A47: AddressPart I = <*i1*> by A46,Th30;
    then k = 1 by A38,Lm1;
then A48: f = i1 by A39,A47,FINSEQ_1:def 8;
      JUMP I = {i1} by A46,Th60;
    hence thesis by A48,TARSKI:def 1;
    suppose ex a,i1 st I = a=0_goto i1;
    then consider a, i1 such that
A49:   I = a=0_goto i1;
A50: AddressPart I = <*i1,a*> by A49,Th31;
    then k = 1 or k = 2 by A38,Lm2;
then A51: f = i1 by A39,A40,A41,A49,A50,Th52,FINSEQ_1:61;
      JUMP I = {i1} by A49,Th63;
    hence thesis by A51,TARSKI:def 1;
    suppose ex a,r st I = a:=r;
    then consider a, r such that
A52:   I = a:=r;
      k in dom <*a,r*> by A38,A52,Th29;
then A53: k = 1 or k = 2 by Lm2;
      (PA AddressParts InsCode I).2 = the carrier of R by A52,Th49;
    then (PA AddressParts InsCode I).2 <> SCM-Instr-Loc by SCMRING1:def 2;
    hence thesis by A40,A41,A52,A53,Th48,SCMRING2:def 1;
  end;
end;

definition let R;
 cluster SCM R -> regular;
coherence
  proof
    let T be InsType of SCM R;
A1: AddressParts T =
      { AddressPart I where I is Instruction of SCM R: InsCode I = T }
        by AMISTD_2:def 5;
    per cases by Lm3;
    suppose
A2:   T = 0;
    reconsider f = {} as Function;
    take f;
    thus thesis by A2,Th32,CARD_3:19;

    suppose
A3:   T = 1;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A4:   x = f and
A5:   dom f = dom PA AddressParts T and
A6:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A7: dom PA AddressParts T = {1,2} by A3,Th33;
then A8: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A6;
    then f.1 in pi(AddressParts T,1) by A8,AMISTD_2:def 1;
    then consider g being Function such that
A9:   g in AddressParts T and
A10:   g.1 = f.1 by CARD_3:def 6;
A11: 2 in dom PA AddressParts T by A7,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A6;
    then f.2 in pi(AddressParts T,2) by A11,AMISTD_2:def 1;
    then consider h being Function such that
A12:   h in AddressParts T and
A13:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A14:   g = AddressPart I and
A15:   InsCode I = T by A1,A9;
    consider d1, b such that
A16:   I = d1:=b by A3,A15,Th17;
A17: g = <*d1,b*> by A14,A16,Th25;
    consider J being Instruction of SCM R such that
A18:   h = AddressPart J and
A19:   InsCode J = T by A1,A12;
    consider a, d2 such that
A20:   J = a:=d2 by A3,A19,Th17;
A21: h = <*a,d2*> by A18,A20,Th25;
A22: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*d1,d2*>.k = f.k
    proof
      let k be set;
      assume
A23:     k in {1,2};
      per cases by A23,TARSKI:def 2;
      suppose
A24:     k = 1;
        <*d1,d2*>.1 = d1 by FINSEQ_1:61
        .= f.1 by A10,A17,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A24;
      suppose
A25:     k = 2;
        <*d1,d2*>.2 = d2 by FINSEQ_1:61
        .= f.2 by A13,A21,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A25;
    end;
then A26: <*d1,d2*> = f by A5,A7,A22,FUNCT_1:9;
      InsCode (d1:=d2) = 1 & AddressPart (d1:=d2) = <*d1,d2*> by Th9,Th25;
    hence thesis by A1,A3,A4,A26;

    suppose
A27:   T = 2;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A28:   x = f and
A29:   dom f = dom PA AddressParts T and
A30:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A31: dom PA AddressParts T = {1,2} by A27,Th34;
then A32: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A30;
    then f.1 in pi(AddressParts T,1) by A32,AMISTD_2:def 1;
    then consider g being Function such that
A33:   g in AddressParts T and
A34:   g.1 = f.1 by CARD_3:def 6;
A35: 2 in dom PA AddressParts T by A31,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A30;
    then f.2 in pi(AddressParts T,2) by A35,AMISTD_2:def 1;
    then consider h being Function such that
A36:   h in AddressParts T and
A37:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A38:   g = AddressPart I and
A39:   InsCode I = T by A1,A33;
    consider d1, b such that
A40:   I = AddTo(d1,b) by A27,A39,Th18;
A41: g = <*d1,b*> by A38,A40,Th26;
    consider J being Instruction of SCM R such that
A42:   h = AddressPart J and
A43:   InsCode J = T by A1,A36;
    consider a, d2 such that
A44:   J = AddTo(a,d2) by A27,A43,Th18;
A45: h = <*a,d2*> by A42,A44,Th26;
A46: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*d1,d2*>.k = f.k
    proof
      let k be set;
      assume
A47:     k in {1,2};
      per cases by A47,TARSKI:def 2;
      suppose
A48:     k = 1;
        <*d1,d2*>.1 = d1 by FINSEQ_1:61
        .= f.1 by A34,A41,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A48;
      suppose
A49:     k = 2;
        <*d1,d2*>.2 = d2 by FINSEQ_1:61
        .= f.2 by A37,A45,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A49;
    end;
then A50: <*d1,d2*> = f by A29,A31,A46,FUNCT_1:9;
      InsCode AddTo(d1,d2) = 2 & AddressPart AddTo(d1,d2) = <*d1,d2*>
      by Th10,Th26;
    hence thesis by A1,A27,A28,A50;

    suppose
A51:   T = 3;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A52:   x = f and
A53:   dom f = dom PA AddressParts T and
A54:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A55: dom PA AddressParts T = {1,2} by A51,Th35;
then A56: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A54;
    then f.1 in pi(AddressParts T,1) by A56,AMISTD_2:def 1;
    then consider g being Function such that
A57:   g in AddressParts T and
A58:   g.1 = f.1 by CARD_3:def 6;
A59: 2 in dom PA AddressParts T by A55,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A54;
    then f.2 in pi(AddressParts T,2) by A59,AMISTD_2:def 1;
    then consider h being Function such that
A60:   h in AddressParts T and
A61:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A62:   g = AddressPart I and
A63:   InsCode I = T by A1,A57;
    consider d1, b such that
A64:   I = SubFrom(d1,b) by A51,A63,Th19;
A65: g = <*d1,b*> by A62,A64,Th27;
    consider J being Instruction of SCM R such that
A66:   h = AddressPart J and
A67:   InsCode J = T by A1,A60;
    consider a, d2 such that
A68:   J = SubFrom(a,d2) by A51,A67,Th19;
A69: h = <*a,d2*> by A66,A68,Th27;
A70: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*d1,d2*>.k = f.k
    proof
      let k be set;
      assume
A71:     k in {1,2};
      per cases by A71,TARSKI:def 2;
      suppose
A72:     k = 1;
        <*d1,d2*>.1 = d1 by FINSEQ_1:61
        .= f.1 by A58,A65,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A72;
      suppose
A73:     k = 2;
        <*d1,d2*>.2 = d2 by FINSEQ_1:61
        .= f.2 by A61,A69,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A73;
    end;
then A74: <*d1,d2*> = f by A53,A55,A70,FUNCT_1:9;
      InsCode SubFrom(d1,d2) = 3 & AddressPart SubFrom(d1,d2) = <*d1,d2*>
      by Th11,Th27;
    hence thesis by A1,A51,A52,A74;

    suppose
A75:   T = 4;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A76:   x = f and
A77:   dom f = dom PA AddressParts T and
A78:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A79: dom PA AddressParts T = {1,2} by A75,Th36;
then A80: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A78;
    then f.1 in pi(AddressParts T,1) by A80,AMISTD_2:def 1;
    then consider g being Function such that
A81:   g in AddressParts T and
A82:   g.1 = f.1 by CARD_3:def 6;
A83: 2 in dom PA AddressParts T by A79,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A78;
    then f.2 in pi(AddressParts T,2) by A83,AMISTD_2:def 1;
    then consider h being Function such that
A84:   h in AddressParts T and
A85:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A86:   g = AddressPart I and
A87:   InsCode I = T by A1,A81;
    consider d1, b such that
A88:   I = MultBy(d1,b) by A75,A87,Th20;
A89: g = <*d1,b*> by A86,A88,Th28;
    consider J being Instruction of SCM R such that
A90:   h = AddressPart J and
A91:   InsCode J = T by A1,A84;
    consider a, d2 such that
A92:   J = MultBy(a,d2) by A75,A91,Th20;
A93: h = <*a,d2*> by A90,A92,Th28;
A94: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*d1,d2*>.k = f.k
    proof
      let k be set;
      assume
A95:     k in {1,2};
      per cases by A95,TARSKI:def 2;
      suppose
A96:     k = 1;
        <*d1,d2*>.1 = d1 by FINSEQ_1:61
        .= f.1 by A82,A89,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A96;
      suppose
A97:     k = 2;
        <*d1,d2*>.2 = d2 by FINSEQ_1:61
        .= f.2 by A85,A93,FINSEQ_1:61;
      hence <*d1,d2*>.k = f.k by A97;
    end;
then A98: <*d1,d2*> = f by A77,A79,A94,FUNCT_1:9;
      InsCode MultBy(d1,d2) = 4 & AddressPart MultBy(d1,d2) = <*d1,d2*>
      by Th12,Th28;
    hence thesis by A1,A75,A76,A98;

    suppose
A99:   T = 5;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A100:   x = f and
A101:   dom f = dom PA AddressParts T and
A102:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A103: dom PA AddressParts T = {1,2} by A99,Th37;
then A104: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A102;
    then f.1 in pi(AddressParts T,1) by A104,AMISTD_2:def 1;
    then consider g being Function such that
A105:   g in AddressParts T and
A106:   g.1 = f.1 by CARD_3:def 6;
A107: 2 in dom PA AddressParts T by A103,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A102;
    then f.2 in pi(AddressParts T,2) by A107,AMISTD_2:def 1;
    then consider h being Function such that
A108:   h in AddressParts T and
A109:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A110:   g = AddressPart I and
A111:   InsCode I = T by A1,A105;
    consider d1, r such that
A112:   I = d1:=r by A99,A111,Th21;
A113: g = <*d1,r*> by A110,A112,Th29;
    consider J being Instruction of SCM R such that
A114:   h = AddressPart J and
A115:   InsCode J = T by A1,A108;
    consider a being Data-Location of R,
             r2 being Element of R such that
A116:   J = a:=r2 by A99,A115,Th21;
A117: h = <*a,r2*> by A114,A116,Th29;
A118: dom <*d1,r2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*d1,r2*>.k = f.k
    proof
      let k be set;
      assume
A119:     k in {1,2};
      per cases by A119,TARSKI:def 2;
      suppose
A120:     k = 1;
        <*d1,r2*>.1 = d1 by FINSEQ_1:61
        .= f.1 by A106,A113,FINSEQ_1:61;
      hence <*d1,r2*>.k = f.k by A120;
      suppose
A121:     k = 2;
        <*d1,r2*>.2 = r2 by FINSEQ_1:61
        .= f.2 by A109,A117,FINSEQ_1:61;
      hence <*d1,r2*>.k = f.k by A121;
    end;
then A122: <*d1,r2*> = f by A101,A103,A118,FUNCT_1:9;
      InsCode (d1:=r2) = 5 & AddressPart (d1:=r2) = <*d1,r2*> by Th13,Th29;
    hence thesis by A1,A99,A100,A122;

    suppose
A123:   T = 6;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A124:   x = f and
A125:   dom f = dom PA AddressParts T and
A126:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A127: dom PA AddressParts T = {1} by A123,Th38;
then A128: 1 in dom PA AddressParts T by TARSKI:def 1;
    then f.1 in (PA AddressParts T).1 by A126;
    then f.1 in pi(AddressParts T,1) by A128,AMISTD_2:def 1;
    then consider g being Function such that
A129:   g in AddressParts T and
A130:   g.1 = f.1 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A131:   g = AddressPart I and
A132:   InsCode I = T by A1,A129;
    consider i1 such that
A133:   I = goto i1 by A123,A132,Th22;
A134: dom <*i1*> = {1} by FINSEQ_1:4,def 8;
      for k being set st k in {1} holds <*i1*>.k = f.k
    proof
      let k be set;
      assume k in {1};
then k = 1 by TARSKI:def 1;
      hence <*i1*>.k = f.k by A130,A131,A133,Th30;
    end;
then A135: <*i1*> = f by A125,A127,A134,FUNCT_1:9;
      InsCode goto i1 = 6 & AddressPart goto i1 = <*i1*> by Th14,Th30;
    hence thesis by A1,A123,A124,A135;

    suppose
A136:   T = 7;
    take PA AddressParts T;
    thus AddressParts T c= product PA AddressParts T by AMISTD_2:9;
    let x be set;
    assume x in product PA AddressParts T;
    then consider f being Function such that
A137:   x = f and
A138:   dom f = dom PA AddressParts T and
A139:   for k being set st k in dom PA AddressParts T holds
        f.k in (PA AddressParts T).k by CARD_3:def 5;
A140: dom PA AddressParts T = {1,2} by A136,Th39;
then A141: 1 in dom PA AddressParts T by TARSKI:def 2;
    then f.1 in (PA AddressParts T).1 by A139;
    then f.1 in pi(AddressParts T,1) by A141,AMISTD_2:def 1;
    then consider g being Function such that
A142:   g in AddressParts T and
A143:   g.1 = f.1 by CARD_3:def 6;
A144: 2 in dom PA AddressParts T by A140,TARSKI:def 2;
    then f.2 in (PA AddressParts T).2 by A139;
    then f.2 in pi(AddressParts T,2) by A144,AMISTD_2:def 1;
    then consider h being Function such that
A145:   h in AddressParts T and
A146:   h.2 = f.2 by CARD_3:def 6;
    consider I being Instruction of SCM R such that
A147:   g = AddressPart I and
A148:   InsCode I = T by A1,A142;
    consider d1, i1 such that
A149:   I = d1 =0_goto i1 by A136,A148,Th23;
A150: g = <*i1,d1*> by A147,A149,Th31;
    consider J being Instruction of SCM R such that
A151:   h = AddressPart J and
A152:   InsCode J = T by A1,A145;
    consider d2, i2 such that
A153:   J = d2 =0_goto i2 by A136,A152,Th23;
A154: h = <*i2,d2*> by A151,A153,Th31;
A155: dom <*i1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
      for k being set st k in {1,2} holds <*i1,d2*>.k = f.k
    proof
      let k be set;
      assume
A156:     k in {1,2};
      per cases by A156,TARSKI:def 2;
      suppose
A157:     k = 1;
        <*i1,d2*>.1 = i1 by FINSEQ_1:61
        .= f.1 by A143,A150,FINSEQ_1:61;
      hence <*i1,d2*>.k = f.k by A157;
      suppose
A158:     k = 2;
        <*i1,d2*>.2 = d2 by FINSEQ_1:61
        .= f.2 by A146,A154,FINSEQ_1:61;
      hence <*i1,d2*>.k = f.k by A158;
    end;
then A159: <*i1,d2*> = f by A138,A140,A155,FUNCT_1:9;
      InsCode (d2 =0_goto i1) = 7 & AddressPart (d2 =0_goto i1) = <*i1,d2*>
      by Th15,Th31;
    hence thesis by A1,A136,A137,A159;
  end;
end;

theorem Th69:
 IncAddr(goto i1,k) = goto il.(SCM R, locnum i1 + k)
  proof
A1: InsCode IncAddr(goto i1,k) = InsCode goto i1 by AMISTD_2:def 14
      .= 6 by Th14
      .= InsCode goto il.(SCM R, locnum i1 + k) by Th14;
A2: dom AddressPart IncAddr(goto i1,k) = dom AddressPart goto i1
        by AMISTD_2:def 14;
A3: dom AddressPart goto il.(SCM R, locnum i1 + k)
      = dom <*il.(SCM R, locnum i1 + k)*> by Th30
     .= Seg 1 by FINSEQ_1:def 8
     .= dom <*i1*> by FINSEQ_1:def 8
     .= dom AddressPart goto i1 by Th30;
      for x being set st x in dom AddressPart goto i1 holds
      (AddressPart IncAddr(goto i1,k)).x =
      (AddressPart goto il.(SCM R, locnum i1 + k)).x
    proof
      let x be set;
      assume
A4:     x in dom AddressPart goto i1;
      then x in dom <*i1*> by Th30;
then A5:   x = 1 by Lm1;
      then (PA AddressParts InsCode goto i1).x =
        the Instruction-Locations of SCM R by Th50;
      then consider f being Instruction-Location of SCM R such that
A6:     f = (AddressPart goto i1).x and
A7:     (AddressPart IncAddr(goto i1,k)).x = il.(SCM R,k + locnum f)
          by A4,AMISTD_2:def 14;
        f = <*i1*>.x by A6,Th30
       .= i1 by A5,FINSEQ_1:def 8;
      hence (AddressPart IncAddr(goto i1,k)).x
        = <*il.(SCM R, locnum i1 + k)*>.x by A5,A7,FINSEQ_1:def 8
       .= (AddressPart goto il.(SCM R, locnum i1 + k)).x by Th30;
    end;
    then AddressPart IncAddr(goto i1,k) =
      AddressPart goto il.(SCM R, locnum i1 + k) by A2,A3,FUNCT_1:9;
    hence IncAddr(goto i1,k) = goto il.(SCM R, locnum i1 + k)
      by A1,AMISTD_2:16;
  end;

theorem Th70:
 IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM R, locnum i1 + k)
  proof
A1: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by AMISTD_2:def 14
      .= 7 by Th15
      .= InsCode (a=0_goto il.(SCM R, locnum i1 + k)) by Th15;
A2: dom AddressPart IncAddr(a=0_goto i1,k) = dom AddressPart (a=0_goto i1)
        by AMISTD_2:def 14;
A3: dom AddressPart (a=0_goto il.(SCM R, locnum i1 + k))
      = dom <*il.(SCM R, locnum i1 + k), a*> by Th31
     .= Seg 2 by FINSEQ_3:29
     .= dom <*i1,a*> by FINSEQ_3:29
     .= dom AddressPart (a=0_goto i1) by Th31;
      for x being set st x in dom AddressPart (a=0_goto i1) holds
      (AddressPart IncAddr(a=0_goto i1,k)).x =
      (AddressPart (a=0_goto il.(SCM R, locnum i1 + k))).x
    proof
      let x be set;
      assume
A4:     x in dom AddressPart (a=0_goto i1);
then A5:   x in dom <*i1,a*> by Th31;
      per cases by A5,Lm2;
      suppose
A6:     x = 1;
      then (PA AddressParts InsCode (a=0_goto i1)).x =
        the Instruction-Locations of SCM R by Th51;
      then consider f being Instruction-Location of SCM R such that
A7:     f = (AddressPart (a=0_goto i1)).x and
A8:     (AddressPart IncAddr(a=0_goto i1,k)).x = il.(SCM R,k + locnum f)
          by A4,AMISTD_2:def 14;
        f = <*i1,a*>.x by A7,Th31
       .= i1 by A6,FINSEQ_1:61;
      hence (AddressPart IncAddr(a=0_goto i1,k)).x
        = <*il.(SCM R, locnum i1 + k),a*>.x by A6,A8,FINSEQ_1:61
       .= (AddressPart (a=0_goto il.(SCM R, locnum i1 + k))).x by Th31;
      suppose
A9:     x = 2;
        SCM-Data-Loc <> the Instruction-Locations of SCM R by Th4;
      then (PA AddressParts InsCode (a=0_goto i1)).x <>
        the Instruction-Locations of SCM R by A9,Th52;
      hence (AddressPart IncAddr(a=0_goto i1,k)).x
        = (AddressPart (a=0_goto i1)).x by A4,AMISTD_2:def 14
       .= <*i1,a*>.x by Th31
       .= a by A9,FINSEQ_1:61
       .= <*il.(SCM R, locnum i1 + k),a*>.x by A9,FINSEQ_1:61
       .= (AddressPart (a=0_goto il.(SCM R, locnum i1 + k))).x by Th31;
    end;
    then AddressPart IncAddr(a=0_goto i1,k) =
      AddressPart (a=0_goto il.(SCM R, locnum i1 + k)) by A2,A3,FUNCT_1:9;
    hence IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM R, locnum i1 + k)
      by A1,AMISTD_2:16;
  end;

definition let R;
 cluster SCM R -> IC-good Exec-preserving;
coherence
  proof
    thus SCM R is IC-good
    proof
      let I be Instruction of SCM R;
      per cases by SCMRING2:8;
      suppose I = [0,{}];
      then I = halt SCM R by SCMRING2:30;
      hence thesis;
      suppose ex a,b st I = a:=b;
      then consider a, b such that
A1:     I = a:=b;
      thus thesis by A1;
      suppose ex a,b st I = AddTo(a,b);
      then consider a, b such that
A2:     I = AddTo(a,b);
      thus thesis by A2;
      suppose ex a,b st I = SubFrom(a,b);
      then consider a, b such that
A3:     I = SubFrom(a,b);
      thus thesis by A3;
      suppose ex a,b st I = MultBy(a,b);
      then consider a, b such that
A4:     I = MultBy(a,b);
      thus thesis by A4;
      suppose ex i1 st I = goto i1;
      then consider i1 such that
A5:     I = goto i1;
      let k be natural number,
          s1, s2 be State of SCM R such that
          s2 = s1 +* (IC SCM R .--> (IC s1 + k));
A6:   IC Exec(I,s1) = Exec(I,s1).IC SCM R by AMI_1:def 15
        .= i1 by A5,SCMRING2:17;
      thus IC Exec(I,s1) + k
         = il.(SCM R, locnum IC Exec(I,s1) + k) by AMISTD_1:def 14
        .= Exec(goto il.(SCM R, locnum i1 + k),s2).IC SCM R by A6,SCMRING2:17
        .= IC Exec(goto il.(SCM R, locnum i1 + k),s2) by AMI_1:def 15
        .= IC Exec(IncAddr(I,k), s2) by A5,Th69;
      suppose ex a,i1 st I = a=0_goto i1;
      then consider a, i1 such that
A7:     I = a=0_goto i1;
      let k be natural number,
          s1, s2 be State of SCM R such that
A8:     s2 = s1 +* (IC SCM R .--> (IC s1 + k));
A9:   a <> IC SCM R by Th3;
        dom (IC SCM R .--> (IC s1 + k)) = {IC SCM R} by CQC_LANG:5;
      then not a in dom (IC SCM R .--> (IC s1 + k)) by A9,TARSKI:def 1;
then A10:   s1.a = s2.a by A8,FUNCT_4:12;
        now per cases;
        suppose
A11:       s1.a = 0.R;
A12:     IC Exec(I,s1) = Exec(I,s1).IC SCM R by AMI_1:def 15
          .= i1 by A7,A11,SCMRING2:18;
        thus IC Exec(I,s1) + k
           = il.(SCM R, locnum IC Exec(I,s1) + k) by AMISTD_1:def 14
          .= Exec(a=0_goto il.(SCM R, locnum i1 + k),s2).IC SCM R
             by A10,A11,A12,SCMRING2:18
          .= IC Exec(a=0_goto il.(SCM R, locnum i1 + k),s2) by AMI_1:def 15
          .= IC Exec(IncAddr(I,k), s2) by A7,Th70;
        suppose
A13:       s1.a <> 0.R;
          dom (IC SCM R .--> (IC s1 + k)) = {IC SCM R} by CQC_LANG:5;
then A14:     IC SCM R in dom (IC SCM R .--> (IC s1 + k)) by TARSKI:def 1;
A15:     IC s2 = s2.IC SCM R by AMI_1:def 15
             .= (IC SCM R .--> (IC s1 + k)).IC SCM R by A8,A14,FUNCT_4:14
             .= IC s1 + k by CQC_LANG:6
             .= il.(SCM R,locnum IC s1 + k) by AMISTD_1:def 14;
A16:     IC Exec(I, s2) = Exec(I, s2).IC SCM R by AMI_1:def 15
          .= Next IC s2 by A7,A10,A13,SCMRING2:18
          .= NextLoc IC s2 by Th68
          .= il.(SCM R,locnum IC s1 + k) + 1 by A15,AMISTD_1:def 15
          .= il.(SCM R,locnum il.(SCM R,locnum IC s1 + k) + 1)
             by AMISTD_1:def 14
          .= il.(SCM R,locnum IC s1 + k + 1) by AMISTD_1:def 13
          .= il.(SCM R,locnum IC s1 + 1 + k) by XCMPLX_1:1;
A17:     IC Exec(I,s1) = Exec(I,s1).IC SCM R by AMI_1:def 15
          .= Next IC s1 by A7,A13,SCMRING2:18
          .= NextLoc IC s1 by Th68
          .= il.(SCM R,locnum IC s1 + 1) by AMISTD_1:34;
        thus IC Exec(I,s1) + k = il.(SCM R,locnum IC Exec(I,s1) + k)
             by AMISTD_1:def 14
          .= IC Exec(I,s2) by A16,A17,AMISTD_1:def 13
          .= Exec(I,s2).IC SCM R by AMI_1:def 15
          .= Next IC s2 by A7,A10,A13,SCMRING2:18
          .= Exec(a=0_goto il.(SCM R, locnum i1 + k),s2).IC SCM R
             by A10,A13,SCMRING2:18
          .= IC Exec(a=0_goto il.(SCM R, locnum i1 + k),s2) by AMI_1:def 15
          .= IC Exec(IncAddr(I,k), s2) by A7,Th70;
      end;
      hence thesis;
      suppose ex a,r st I = a:=r;
      then consider a, r such that
A18:     I = a:=r;
      thus thesis by A18;
    end;

    let I be Instruction of SCM R;
    let s1, s2 be State of SCM R such that
A19:   s1, s2 equal_outside the Instruction-Locations of SCM R;
A20: dom Exec(I,s1) = dom the Object-Kind of SCM R by CARD_3:18;
then A21: dom Exec(I,s1) = dom Exec(I,s2) by CARD_3:18;
A22: dom the Object-Kind of SCM R = the carrier of SCM R by FUNCT_2:def 1;
A23: dom Exec(I,s1) \ the Instruction-Locations of SCM R c= dom Exec(I,s1)
      by XBOOLE_1:36;
A24: IC s1 = IC s2 by A19,SCMFSA6A:29;
    per cases by SCMRING2:8;
    suppose I = [0,{}];
    then I = halt SCM R by SCMRING2:30;
    hence thesis by A19,AMISTD_2:def 19;
    suppose ex a,b st I = a:=b;
    then consider a, b such that
A25:   I = a:=b;
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A26:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A27:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A28:   x in dom Exec(I,s1) by A26,XBOOLE_0:def 4;
      per cases by A20,A22,A27,A28,Th5;
      suppose
A29:     x = IC SCM R;
      hence Exec(I,s1).x = Next IC s1 by A25,SCMRING2:13
         .= Exec(I,s2).x by A24,A25,A29,SCMRING2:13;
      suppose
A30:     x = a;
      hence Exec(I,s1).x = s1.b by A25,SCMRING2:13
        .= s2.b by A19,Th7
        .= Exec(I,s2).x by A25,A30,SCMRING2:13;
      suppose that
A31:     x is Data-Location of R and
A32:     x <> a;
      thus Exec(I,s1).x = s1.x by A25,A31,A32,SCMRING2:13
        .= s2.x by A19,A31,Th7
        .= Exec(I,s2).x by A25,A31,A32,SCMRING2:13;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex a,b st I = AddTo(a,b);
    then consider a, b such that
A33:   I = AddTo(a,b);
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A34:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A35:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A36:   x in dom Exec(I,s1) by A34,XBOOLE_0:def 4;
      per cases by A20,A22,A35,A36,Th5;
      suppose
A37:     x = IC SCM R;
      hence Exec(I,s1).x = Next IC s1 by A33,SCMRING2:14
         .= Exec(I,s2).x by A24,A33,A37,SCMRING2:14;
      suppose
A38:     x = a;
      hence Exec(I,s1).x = s1.a + s1.b by A33,SCMRING2:14
        .= s1.a + s2.b by A19,Th7
        .= s2.a + s2.b by A19,Th7
        .= Exec(I,s2).x by A33,A38,SCMRING2:14;
      suppose that
A39:     x is Data-Location of R and
A40:     x <> a;
      thus Exec(I,s1).x = s1.x by A33,A39,A40,SCMRING2:14
        .= s2.x by A19,A39,Th7
        .= Exec(I,s2).x by A33,A39,A40,SCMRING2:14;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex a,b st I = SubFrom(a,b);
    then consider a, b such that
A41:   I = SubFrom(a,b);
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A42:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A43:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A44:   x in dom Exec(I,s1) by A42,XBOOLE_0:def 4;
      per cases by A20,A22,A43,A44,Th5;
      suppose
A45:     x = IC SCM R;
      hence Exec(I,s1).x = Next IC s1 by A41,SCMRING2:15
         .= Exec(I,s2).x by A24,A41,A45,SCMRING2:15;
      suppose
A46:     x = a;
      hence Exec(I,s1).x = s1.a - s1.b by A41,SCMRING2:15
        .= s1.a - s2.b by A19,Th7
        .= s2.a - s2.b by A19,Th7
        .= Exec(I,s2).x by A41,A46,SCMRING2:15;
      suppose that
A47:     x is Data-Location of R and
A48:     x <> a;
      thus Exec(I,s1).x = s1.x by A41,A47,A48,SCMRING2:15
        .= s2.x by A19,A47,Th7
        .= Exec(I,s2).x by A41,A47,A48,SCMRING2:15;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex a,b st I = MultBy(a,b);
    then consider a, b such that
A49:   I = MultBy(a,b);
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A50:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A51:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A52:   x in dom Exec(I,s1) by A50,XBOOLE_0:def 4;
      per cases by A20,A22,A51,A52,Th5;
      suppose
A53:     x = IC SCM R;
      hence Exec(I,s1).x = Next IC s1 by A49,SCMRING2:16
         .= Exec(I,s2).x by A24,A49,A53,SCMRING2:16;
      suppose
A54:     x = a;
      hence Exec(I,s1).x = s1.a * s1.b by A49,SCMRING2:16
        .= s1.a * s2.b by A19,Th7
        .= s2.a * s2.b by A19,Th7
        .= Exec(I,s2).x by A49,A54,SCMRING2:16;
      suppose that
A55:     x is Data-Location of R and
A56:     x <> a;
      thus Exec(I,s1).x = s1.x by A49,A55,A56,SCMRING2:16
        .= s2.x by A19,A55,Th7
        .= Exec(I,s2).x by A49,A55,A56,SCMRING2:16;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex i1 st I = goto i1;
    then consider i1 such that
A57:   I = goto i1;
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A58:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A59:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A60:   x in dom Exec(I,s1) by A58,XBOOLE_0:def 4;
      per cases by A20,A22,A59,A60,Th5;
      suppose
A61:     x = IC SCM R;
      hence Exec(I,s1).x = i1 by A57,SCMRING2:17
         .= Exec(I,s2).x by A57,A61,SCMRING2:17;
      suppose
A62:     x is Data-Location of R;
      hence Exec(I,s1).x = s1.x by A57,SCMRING2:17
        .= s2.x by A19,A62,Th7
        .= Exec(I,s2).x by A57,A62,SCMRING2:17;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex a,i1 st I = a=0_goto i1;
    then consider a, i1 such that
A63:   I = a=0_goto i1;
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A64:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A65:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A66:   x in dom Exec(I,s1) by A64,XBOOLE_0:def 4;
A67:   s1.a = s2.a by A19,Th7;
      per cases by A20,A22,A65,A66,Th5;
      suppose that
A68:     x = IC SCM R and
A69:     s1.a = 0.R;
      thus Exec(I,s1).x = i1 by A63,A68,A69,SCMRING2:18
        .= Exec(I,s2).x by A63,A67,A68,A69,SCMRING2:18;
      suppose that
A70:     x = IC SCM R and
A71:     s1.a <> 0.R;
      thus Exec(I,s1).x = Next IC s1 by A63,A70,A71,SCMRING2:18
        .= Exec(I,s2).x by A24,A63,A67,A70,A71,SCMRING2:18;
      suppose
A72:     x is Data-Location of R;
      hence Exec(I,s1).x = s1.x by A63,SCMRING2:18
        .= s2.x by A19,A72,Th7
        .= Exec(I,s2).x by A63,A72,SCMRING2:18;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
    suppose ex a,r st I = a:=r;
    then consider a, r such that
A73:   I = a:=r;
      for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM
R
      holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A74:     x in dom Exec(I,s1) \ the Instruction-Locations of SCM R;
then A75:   not x in the Instruction-Locations of SCM R by XBOOLE_0:def 4;
A76:   x in dom Exec(I,s1) by A74,XBOOLE_0:def 4;
      per cases by A20,A22,A75,A76,Th5;
      suppose
A77:     x = IC SCM R;
      hence Exec(I,s1).x = Next IC s1 by A73,SCMRING2:19
         .= Exec(I,s2).x by A24,A73,A77,SCMRING2:19;
      suppose
A78:     x = a;
      hence Exec(I,s1).x = r by A73,SCMRING2:19
        .= Exec(I,s2).x by A73,A78,SCMRING2:19;
      suppose that
A79:     x is Data-Location of R and
A80:     x <> a;
      thus Exec(I,s1).x = s1.x by A73,A79,A80,SCMRING2:19
        .= s2.x by A19,A79,Th7
        .= Exec(I,s2).x by A73,A79,A80,SCMRING2:19;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM R) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM R)
        by A21,A23,SCMFSA6A:9;
  end;
end;


Back to top