scmring3.miz



    begin

    reserve R for Ring,

r for Element of R,

a,b,d1,d2 for Data-Location of R,

il,i1,i2 for Nat,

I for Instruction of ( SCM R),

s,s1,s2 for State of ( SCM R),

T for InsType of the InstructionsF of ( SCM R),

k for Nat;

    theorem :: SCMRING3:1

    

     Th1: ( Values a) = the carrier of R

    proof

      a in ( Data-Locations SCM ) & ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by SCMRING2: 1, SCMRING2: 24;

      hence thesis by AMI_3: 27, SCMRING1: 4;

    end;

    definition

      let R be Ring;

      let la,lb be Data-Location of R;

      let a,b be Element of R;

      :: original: -->

      redefine

      func (la,lb) --> (a,b) -> FinPartState of ( SCM R) ;

      coherence

      proof

        reconsider b9 = b as Element of ( Values lb) by Th1;

        reconsider a9 = a as Element of ( Values la) by Th1;

        ((la,lb) --> (a9,b9)) is FinPartState of ( SCM R);

        hence thesis;

      end;

    end

    theorem :: SCMRING3:2

    

     Th2: a <> ( IC ( SCM R))

    proof

      a in SCM-Data-Loc by AMI_2:def 16;

      then a <> NAT by AMI_2: 20;

      hence thesis by SCMRING2: 8;

    end;

    theorem :: SCMRING3:3

    for o be Object of ( SCM R) holds o = ( IC ( 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 { NAT } by SCMRING2: 8;

       not o in { NAT } by A1;

      then o in (the carrier of ( SCM R) \ { NAT }) by XBOOLE_0:def 5;

      then o in SCM-Data-Loc by SCMRING2: 25;

      hence thesis by AMI_2:def 16;

    end;

    ::$Canceled

    theorem :: SCMRING3:5

    ( InsCode (a := b)) = 1;

    theorem :: SCMRING3:6

    ( InsCode ( AddTo (a,b))) = 2;

    theorem :: SCMRING3:7

    ( InsCode ( SubFrom (a,b))) = 3;

    theorem :: SCMRING3:8

    ( InsCode ( MultBy (a,b))) = 4;

    theorem :: SCMRING3:9

    ( InsCode (a := r)) = 5;

    theorem :: SCMRING3:10

    ( InsCode ( goto (i1,R))) = 6;

    theorem :: SCMRING3:11

    ( InsCode (a =0_goto i1)) = 7;

    theorem :: SCMRING3:12

    

     Th11: ( InsCode I) = 0 implies I = ( halt ( SCM R))

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 0 ;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:13

    

     Th12: ( InsCode I) = 1 implies ex a, b st I = (a := b)

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 1;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:14

    

     Th13: ( InsCode I) = 2 implies ex a, b st I = ( AddTo (a,b))

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 2;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:15

    

     Th14: ( InsCode I) = 3 implies ex a, b st I = ( SubFrom (a,b))

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 3;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:16

    

     Th15: ( InsCode I) = 4 implies ex a, b st I = ( MultBy (a,b))

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 4;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:17

    

     Th16: ( InsCode I) = 5 implies ex a, r st I = (a := r)

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 5;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:18

    

     Th17: ( InsCode I) = 6 implies ex i2 st I = ( goto (i2,R))

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 6;

      hence thesis by A1;

    end;

    theorem :: SCMRING3:19

    

     Th18: ( InsCode I) = 7 implies ex a, i1 st I = (a =0_goto i1)

    proof

      

       A1: 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,R))) or (ex a, i1 st I = (a =0_goto i1)) or ex a, r st I = (a := r) by SCMRING2: 7;

      assume ( InsCode I) = 7;

      hence thesis by A1;

    end;

    

     Lm1: for x,y be 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: 2, TARSKI:def 1;

    end;

    

     Lm2: T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7

    proof

      consider y be object such that

       A1: [T, y] in ( proj1 the InstructionsF of ( SCM R)) by XTUPLE_0:def 12;

      consider x be object such that

       A2: [ [T, y], x] in the InstructionsF of ( SCM R) by A1, XTUPLE_0:def 12;

       [T, y, x] in ( SCM-Instr R) by A2, SCMRING2:def 1;

      then [T, y, x] in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) \/ the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM )) or [T, y, x] in the set of all [5, {} , <*a, r*>] where a be Element of ( Data-Locations SCM ), r be Element of R by AMI_3: 27, XBOOLE_0:def 3;

      then [T, y, x] in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) or [T, y, x] in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM ) or [T, y, x] in the set of all [5, {} , <*a, r*>] where a be Element of ( Data-Locations SCM ), r be Element of R by XBOOLE_0:def 3;

      then

       A3: [T, y, x] in ( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) : I in {1, 2, 3, 4} }) or [T, y, x] in the set of all [6, <*i*>, {} ] where i be Nat or [T, y, x] in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM ) or [T, y, x] in the set of all [5, {} , <*a, r*>] where a be Element of ( Data-Locations SCM ), r be Element of R by XBOOLE_0:def 3;

      per cases by A3, XBOOLE_0:def 3;

        suppose [T, y, x] in { [ 0 , {} , {} ]};

        then [T, y, x] = [ 0 , {} , {} ] by TARSKI:def 1;

        hence thesis by XTUPLE_0: 3;

      end;

        suppose [T, y, x] in { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) : I in {1, 2, 3, 4} };

        then ex I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) st [T, y, x] = [I, {} , <*a, b*>] & I in {1, 2, 3, 4};

        then T in {1, 2, 3, 4} by XTUPLE_0: 3;

        hence thesis by ENUMSET1:def 2;

      end;

        suppose [T, y, x] in the set of all [6, <*i*>, {} ] where i be Nat;

        then ex i be Nat st [T, y, x] = [6, <*i*>, {} ];

        hence thesis by XTUPLE_0: 3;

      end;

        suppose [T, y, x] in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM );

        then ex i be Nat, a be Element of ( Data-Locations SCM ) st [T, y, x] = [7, <*i*>, <*a*>];

        hence thesis by XTUPLE_0: 3;

      end;

        suppose [T, y, x] in the set of all [5, {} , <*a, r*>] where a be Element of ( Data-Locations SCM ), r be Element of R;

        then ex a be Element of ( Data-Locations SCM ), r be Element of R st [T, y, x] = [5, {} , <*a, r*>];

        hence thesis by XTUPLE_0: 3;

      end;

    end;

    theorem :: SCMRING3:20

    T = 0 implies ( JumpParts T) = { 0 }

    proof

      assume

       A1: T = 0 ;

      hereby

        let a be object;

        assume a in ( JumpParts T);

        then

        consider I such that

         A2: a = ( JumpPart I) and

         A3: ( InsCode I) = T;

        I = ( halt ( SCM R)) by A1, A3, Th11;

        then a = {} by A2;

        hence a in { 0 } by TARSKI:def 1;

      end;

      let a be object;

      assume a in { 0 };

      then

       A4: a = 0 by TARSKI:def 1;

      ( InsCode ( halt ( SCM R))) = 0 & ( JumpPart ( halt ( SCM R))) = 0 ;

      hence thesis by A1, A4;

    end;

    theorem :: SCMRING3:21

    T = 1 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 1;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = (a := b) by A1, A3, Th12;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location of R;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a := a));

      ( InsCode (a := a)) = 1;

      hence thesis by A5, A1;

    end;

    theorem :: SCMRING3:22

    T = 2 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 2;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( AddTo (a,b)) by A1, A3, Th13;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location of R;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( AddTo (a,a)));

      ( InsCode ( AddTo (a,a))) = 2;

      hence thesis by A5, A1;

    end;

    theorem :: SCMRING3:23

    T = 3 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 3;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( SubFrom (a,b)) by A1, A3, Th14;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location of R;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( SubFrom (a,a)));

      ( InsCode ( SubFrom (a,a))) = 3;

      hence thesis by A5, A1;

    end;

    theorem :: SCMRING3:24

    T = 4 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 4;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( MultBy (a,b)) by A1, A3, Th15;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location of R;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( MultBy (a,a)));

      ( InsCode ( MultBy (a,a))) = 4;

      hence thesis by A5, A1;

    end;

    theorem :: SCMRING3:25

    T = 5 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 5;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, r such that

         A4: I = (a := r) by A1, A3, Th16;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location of R, r = the Element of R;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a := r));

      ( InsCode (a := r)) = 5;

      hence thesis by A5, A1;

    end;

    theorem :: SCMRING3:26

    

     Th25: T = 6 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Element of NAT ;

      assume

       A1: T = 6;

      hereby

        let x be object;

        ( InsCode ( goto (i1,R))) = 6;

        then

         A2: ( JumpPart ( goto (i1,R))) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart ( goto (i1,R)))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider i1 such that

         A6: I = ( goto (i1,R)) by A1, A5, Th17;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: SCMRING3:27

    

     Th26: T = 7 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Element of NAT , a = the Data-Location of R;

      assume

       A1: T = 7;

      hereby

        let x be object;

        ( InsCode (a =0_goto i1)) = 7;

        then

         A2: ( JumpPart (a =0_goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart (a =0_goto i1))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of ( SCM R) such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider a, i1 such that

         A6: I = (a =0_goto i1) by A1, A5, Th18;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: SCMRING3:28

    (( product" ( JumpParts ( InsCode ( goto (i1,R))))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode ( goto (i1,R)))))) = {1} by Th25;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode ( goto (i1,R)))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode ( goto (i1,R))))) . 1);

        then x in ( pi (( JumpParts ( InsCode ( goto (i1,R)))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode ( goto (i1,R)))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of ( SCM R) such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode ( goto (i1,R))) by A2;

        consider i2 such that

         A6: I = ( goto (i2,R)) by A5, Th17;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1:def 8;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      ( JumpPart ( goto (x,R))) = <*x*> & ( InsCode ( goto (i1,R))) = ( InsCode ( goto (x,R)));

      then

       A7: <*x*> in ( JumpParts ( InsCode ( goto (i1,R))));

      ( <*x*> . 1) = x by FINSEQ_1:def 8;

      then x in ( pi (( JumpParts ( InsCode ( goto (i1,R)))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    theorem :: SCMRING3:29

    (( product" ( JumpParts ( InsCode (a =0_goto i1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode (a =0_goto i1))))) = {1} by Th26;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode (a =0_goto i1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode (a =0_goto i1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode (a =0_goto i1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode (a =0_goto i1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of ( SCM R) such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode (a =0_goto i1)) by A2;

        consider b, i2 such that

         A6: I = (b =0_goto i2) by A5, Th18;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1: 40;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      ( JumpPart (a =0_goto x)) = <*x*> & ( InsCode (a =0_goto i1)) = ( InsCode (a =0_goto x));

      then

       A7: <*x*> in ( JumpParts ( InsCode (a =0_goto i1)));

      ( <*x*> . 1) = x by FINSEQ_1: 40;

      then x in ( pi (( JumpParts ( InsCode (a =0_goto i1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    

     Lm3: for i be Instruction of ( SCM R) holds (for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)}) implies ( JUMP i) is empty

    proof

      set p = 1, q = 2;

      let i be Instruction of ( SCM R);

      assume

       A1: for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)};

      set X = the set of all ( NIC (i,f)) where f be Nat;

      reconsider p, q as Element of NAT ;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);

      ( NIC (i,p)) = {(p + 1)} by A1;

      then {(p + 1)} in X;

      then x in {(p + 1)} by A2, SETFAM_1:def 1;

      then

       A3: x = (p + 1) by TARSKI:def 1;

      ( NIC (i,q)) = {(q + 1)} by A1;

      then {(q + 1)} in X;

      then x in {(q + 1)} by A2, SETFAM_1:def 1;

      hence contradiction by A3, TARSKI:def 1;

    end;

    registration

      let R;

      cluster ( JUMP ( halt ( SCM R))) -> empty;

      coherence ;

    end

    registration

      let R, a, b;

      cluster (a := b) -> sequential;

      coherence by SCMRING2: 11;

      cluster ( AddTo (a,b)) -> sequential;

      coherence by SCMRING2: 12;

      cluster ( SubFrom (a,b)) -> sequential;

      coherence by SCMRING2: 13;

      cluster ( MultBy (a,b)) -> sequential;

      coherence by SCMRING2: 14;

    end

    registration

      let R, a, r;

      cluster (a := r) -> sequential;

      coherence by SCMRING2: 17;

    end

    registration

      let R, a, b;

      cluster ( JUMP (a := b)) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC ((a := b),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm3;

      end;

    end

    registration

      let R, a, b;

      cluster ( JUMP ( AddTo (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( AddTo (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm3;

      end;

    end

    registration

      let R, a, b;

      cluster ( JUMP ( SubFrom (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( SubFrom (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm3;

      end;

    end

    registration

      let R, a, b;

      cluster ( JUMP ( MultBy (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( MultBy (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm3;

      end;

    end

    registration

      let R, a, r;

      cluster ( JUMP (a := r)) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC ((a := r),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm3;

      end;

    end

    theorem :: SCMRING3:30

    

     Th29: ( NIC (( goto (i1,R)),il)) = {i1}

    proof

      now

        let x be object;

        

         A1: il in NAT by ORDINAL1:def 12;

         A2:

        now

          reconsider il1 = il as Element of ( Values ( IC ( SCM R))) by MEMSTR_0:def 6, A1;

          set I = ( goto (i1,R));

          set t = the State of ( SCM R), Q = the Instruction-Sequence of ( SCM R);

          assume

           A3: x = i1;

          reconsider u = (t +* (( IC ( SCM R)),il1)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

          reconsider P = (Q +* (il,I)) as Instruction-Sequence of ( SCM R);

          

           A4: (P /. il) = (P . il) by PBOOLE: 143, A1;

          ( IC ( SCM R)) in ( dom t) by MEMSTR_0: 2;

          then

           A5: ( IC u) = il by FUNCT_7: 31;

          il in NAT by ORDINAL1:def 12;

          then il in ( dom Q) by PARTFUN1:def 2;

          then

           A6: (P . il) = I by FUNCT_7: 31;

          then ( IC ( Following (P,u))) = i1 by A5, A4, SCMRING2: 15;

          hence x in { ( IC ( Exec (( goto (i1,R)),s))) where s be Element of ( product ( the_Values_of ( SCM R))) : ( IC s) = il } by A3, A4, A5, A6;

        end;

        now

          assume x in { ( IC ( Exec (( goto (i1,R)),s))) where s be Element of ( product ( the_Values_of ( SCM R))) : ( IC s) = il };

          then ex s be Element of ( product ( the_Values_of ( SCM R))) st x = ( IC ( Exec (( goto (i1,R)),s))) & ( IC s) = il;

          hence x = i1 by SCMRING2: 15;

        end;

        hence x in {i1} iff x in { ( IC ( Exec (( goto (i1,R)),s))) where s be Element of ( product ( the_Values_of ( SCM R))) : ( IC s) = il } by A2, TARSKI:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: SCMRING3:31

    

     Th30: ( JUMP ( goto (i1,R))) = {i1}

    proof

      set X = the set of all ( NIC (( goto (i1,R)),il));

      now

        let x be object;

        hereby

          reconsider il1 = 1 as Element of NAT ;

          

           A1: ( NIC (( goto (i1,R)),il1)) in X;

          assume x in ( meet X);

          then x in ( NIC (( goto (i1,R)),il1)) by A1, SETFAM_1:def 1;

          hence x in {i1} by Th29;

        end;

        assume x in {i1};

        then

         A2: x = i1 by TARSKI:def 1;

         A3:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A4: Y = ( NIC (( goto (i1,R)),il));

          ( NIC (( goto (i1,R)),il)) = {i1} by Th29;

          hence i1 in Y by A4, TARSKI:def 1;

        end;

        ( NIC (( goto (i1,R)),i1)) in X;

        hence x in ( meet X) by A2, A3, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let R, i1;

      cluster ( JUMP ( goto (i1,R))) -> 1 -element;

      coherence

      proof

        ( JUMP ( goto (i1,R))) = {i1} by Th30;

        hence thesis;

      end;

    end

    theorem :: SCMRING3:32

    

     Th31: i1 in ( NIC ((a =0_goto i1),il)) & ( NIC ((a =0_goto i1),il)) c= {i1, (il + 1)}

    proof

      set t = the State of ( SCM R), Q = the Instruction-Sequence of ( SCM R);

      set I = (a =0_goto i1);

      reconsider a9 = a as Element of ( Data-Locations SCM ) by SCMRING2: 1;

      

       A1: il in NAT by ORDINAL1:def 12;

      reconsider il1 = il as Element of ( Values ( IC ( SCM R))) by MEMSTR_0:def 6, A1;

      ( Values a) = ((( SCM-VAL R) * SCM-OK ) . a9) by SCMRING2: 24

      .= the carrier of R by AMI_3: 27, SCMRING1: 4;

      then

      reconsider 0R = ( 0. R) as Element of ( Values a);

      reconsider u = (t +* (( IC ( SCM R)),il1)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of ( SCM R);

      reconsider v = (u +* (a .--> 0R)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

      

       A2: ( IC ( SCM R)) in ( dom t) by MEMSTR_0: 2;

      ( IC ( SCM R)) <> a by Th2;

      then not ( IC ( SCM R)) in ( dom (a .--> 0R)) by TARSKI:def 1;

      

      then

       A4: ( IC v) = ( IC u) by FUNCT_4: 11

      .= il by A2, FUNCT_7: 31;

      

       A5: (P /. il) = (P . il) by PBOOLE: 143, A1;

      il in NAT by ORDINAL1:def 12;

      then il in ( dom Q) by PARTFUN1:def 2;

      then

       A6: (P . il) = I by FUNCT_7: 31;

      a in ( dom (a .--> 0R)) by TARSKI:def 1;

      

      then (v . a) = ((a .--> 0R) . a) by FUNCT_4: 13

      .= ( 0. R) by FUNCOP_1: 72;

      then ( IC ( Following (P,v))) = i1 by A4, A6, A5, SCMRING2: 16;

      hence i1 in ( NIC ((a =0_goto i1),il)) by A4, A6, A5;

      let x be object;

      assume x in ( NIC ((a =0_goto i1),il));

      then

      consider s be Element of ( product ( the_Values_of ( SCM R))) such that

       A7: x = ( IC ( Exec ((a =0_goto i1),s))) & ( IC s) = il;

      per cases ;

        suppose (s . a) = ( 0. R);

        then x = i1 by A7, SCMRING2: 16;

        hence thesis by TARSKI:def 2;

      end;

        suppose (s . a) <> ( 0. R);

        then x = (il + 1) by A7, SCMRING2: 16;

        hence thesis by TARSKI:def 2;

      end;

    end;

    theorem :: SCMRING3:33

    for R be non trivial Ring, a be Data-Location of R, il,i1 be Element of NAT holds ( NIC ((a =0_goto i1),il)) = {i1, (il + 1)}

    proof

      let R be non trivial Ring, a be Data-Location of R, il,i1 be Element of NAT ;

      set t = the State of ( SCM R), Q = the Instruction-Sequence of ( SCM R);

      set I = (a =0_goto i1);

      reconsider a9 = a as Element of ( Data-Locations SCM ) by SCMRING2: 1;

      

       A1: ( Values a) = ((( SCM-VAL R) * SCM-OK ) . a9) by SCMRING2: 24

      .= the carrier of R by AMI_3: 27, SCMRING1: 4;

      reconsider il1 = il as Element of ( Values ( IC ( SCM R))) by MEMSTR_0:def 6;

      thus ( NIC ((a =0_goto i1),il)) c= {i1, (il + 1)} by Th31;

      reconsider u = (t +* (( IC ( SCM R)),il1)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of ( SCM R);

      let x be object;

      

       A2: ( IC ( SCM R)) <> a by Th2;

      

       A3: ( IC ( SCM R)) in ( dom t) by MEMSTR_0: 2;

      assume

       A4: x in {i1, (il + 1)};

      per cases by A4, TARSKI:def 2;

        suppose

         A5: x = i1;

        reconsider 0R = ( 0. R) as Element of ( Values a) by A1;

        reconsider v = (u +* (a .--> 0R)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

         not ( IC ( SCM R)) in ( dom (a .--> 0R)) by A2, TARSKI:def 1;

        

        then

         A7: ( IC v) = ( IC u) by FUNCT_4: 11

        .= il by A3, FUNCT_7: 31;

        

         A8: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A9: (P . il) = I by FUNCT_7: 31;

        a in ( dom (a .--> 0R)) by TARSKI:def 1;

        

        then (v . a) = ((a .--> 0R) . a) by FUNCT_4: 13

        .= ( 0. R) by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = i1 by A7, A8, A9, SCMRING2: 16;

        hence thesis by A5, A7, A8, A9;

      end;

        suppose

         A10: x = (il + 1);

        consider e be Element of R such that

         A11: e <> ( 0. R) by STRUCT_0:def 18;

        reconsider E = e as Element of ( Values a) by A1;

        reconsider v = (u +* (a .--> E)) as Element of ( product ( the_Values_of ( SCM R))) by CARD_3: 107;

         not ( IC ( SCM R)) in ( dom (a .--> E)) by A2, TARSKI:def 1;

        

        then

         A13: ( IC v) = ( IC u) by FUNCT_4: 11

        .= il by A3, FUNCT_7: 31;

        

         A14: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A15: (P . il) = I by FUNCT_7: 31;

        a in ( dom (a .--> E)) by TARSKI:def 1;

        

        then (v . a) = ((a .--> E) . a) by FUNCT_4: 13

        .= E by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = (il + 1) by A11, A13, A14, A15, SCMRING2: 16;

        hence thesis by A10, A13, A14, A15;

      end;

    end;

    theorem :: SCMRING3:34

    

     Th33: ( JUMP (a =0_goto i1)) = {i1}

    proof

      set X = the set of all ( NIC ((a =0_goto i1),il));

      now

        let x be object;

         A1:

        now

          let Y be set;

          assume Y in X;

          then ex il be Nat st Y = ( NIC ((a =0_goto i1),il));

          hence i1 in Y by Th31;

        end;

        hereby

          reconsider il1 = 1, il2 = 2 as Element of NAT ;

          assume

           A2: x in ( meet X);

          

           A3: ( NIC ((a =0_goto i1),il2)) c= {i1, (il2 + 1)} by Th31;

          ( NIC ((a =0_goto i1),il2)) in X;

          then x in ( NIC ((a =0_goto i1),il2)) by A2, SETFAM_1:def 1;

          then

           A4: x = i1 or x = (il2 + 1) by A3, TARSKI:def 2;

          

           A5: ( NIC ((a =0_goto i1),il1)) c= {i1, (il1 + 1)} by Th31;

          ( NIC ((a =0_goto i1),il1)) in X;

          then x in ( NIC ((a =0_goto i1),il1)) by A2, SETFAM_1:def 1;

          then x = i1 or x = (il1 + 1) by A5, TARSKI:def 2;

          hence x in {i1} by A4, TARSKI:def 1;

        end;

        assume x in {i1};

        then

         A6: x = i1 by TARSKI:def 1;

        ( NIC ((a =0_goto i1),i1)) in X;

        hence x in ( meet X) by A6, A1, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let R, a, i1;

      cluster ( JUMP (a =0_goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP (a =0_goto i1)) = {i1} by Th33;

        hence thesis;

      end;

    end

    theorem :: SCMRING3:35

    

     Th34: ( SUCC (il,( SCM R))) = {il, (il + 1)}

    proof

      set X = the set of all (( NIC (I,il)) \ ( JUMP I)) where I be Element of the InstructionsF of ( SCM R);

      set N = {il, (il + 1)};

      now

        let x be object;

        hereby

          assume x in ( union X);

          then

          consider Y be set such that

           A1: x in Y and

           A2: Y in X by TARSKI:def 4;

          consider i be Element of the InstructionsF of ( SCM R) such that

           A3: Y = (( NIC (i,il)) \ ( JUMP i)) by A2;

          per cases by SCMRING2: 7;

            suppose i = [ 0 , {} , {} ];

            then i = ( halt ( SCM R));

            then x in ( {il} \ ( JUMP ( halt ( SCM R)))) by A1, A3, AMISTD_1: 2;

            then x = il by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = (a := b);

            then

            consider a, b such that

             A4: i = (a := b);

            x in ( {(il + 1)} \ ( JUMP (a := b))) by A1, A3, A4, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( AddTo (a,b));

            then

            consider a, b such that

             A5: i = ( AddTo (a,b));

            x in ( {(il + 1)} \ ( JUMP ( AddTo (a,b)))) by A1, A3, A5, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( SubFrom (a,b));

            then

            consider a, b such that

             A6: i = ( SubFrom (a,b));

            x in ( {(il + 1)} \ ( JUMP ( SubFrom (a,b)))) by A1, A3, A6, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( MultBy (a,b));

            then

            consider a, b such that

             A7: i = ( MultBy (a,b));

            x in ( {(il + 1)} \ ( JUMP ( MultBy (a,b)))) by A1, A3, A7, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex i1 st i = ( goto (i1,R));

            then

            consider i1 such that

             A8: i = ( goto (i1,R));

            x in ( {i1} \ ( JUMP i)) by A1, A3, A8, Th29;

            then x in ( {i1} \ {i1}) by A8, Th30;

            hence x in N by XBOOLE_1: 37;

          end;

            suppose ex a, i1 st i = (a =0_goto i1);

            then

            consider a, i1 such that

             A9: i = (a =0_goto i1);

            

             A10: ( NIC (i,il)) c= {i1, (il + 1)} by A9, Th31;

            x in ( NIC (i,il)) by A1, A3, XBOOLE_0:def 5;

            then

             A11: x = i1 or x = (il + 1) by A10, TARSKI:def 2;

            x in (( NIC (i,il)) \ {i1}) by A1, A3, A9, Th33;

            then not x in {i1} by XBOOLE_0:def 5;

            hence x in N by A11, TARSKI:def 1, TARSKI:def 2;

          end;

            suppose ex a, r st i = (a := r);

            then

            consider a, r such that

             A12: i = (a := r);

            x in ( {(il + 1)} \ ( JUMP (a := r))) by A1, A3, A12, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

        end;

        assume

         A13: x in {il, (il + 1)};

        per cases by A13, TARSKI:def 2;

          suppose

           A14: x = il;

          set i = ( halt ( SCM R));

          (( NIC (i,il)) \ ( JUMP i)) = {il} by AMISTD_1: 2;

          then

           A15: {il} in X;

          x in {il} by A14, TARSKI:def 1;

          hence x in ( union X) by A15, TARSKI:def 4;

        end;

          suppose

           A16: x = (il + 1);

          set a = the Data-Location of R;

          set i = ( AddTo (a,a));

          (( NIC (i,il)) \ ( JUMP i)) = {(il + 1)} by AMISTD_1: 12;

          then

           A17: {(il + 1)} in X;

          x in {(il + 1)} by A16, TARSKI:def 1;

          hence x in ( union X) by A17, TARSKI:def 4;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: SCMRING3:36

    

     Th35: for k be Nat holds (k + 1) in ( SUCC (k,( SCM R))) & for j be Nat st j in ( SUCC (k,( SCM R))) holds k <= j

    proof

      let k be Nat;

      

       A1: ( SUCC (k,( SCM R))) = {k, (k + 1)} by Th34;

      hence (k + 1) in ( SUCC (k,( SCM R))) by TARSKI:def 2;

      let j be Nat;

      assume

       A2: j in ( SUCC (k,( SCM R)));

      per cases by A1, A2, TARSKI:def 2;

        suppose j = k;

        hence thesis;

      end;

        suppose j = (k + 1);

        hence thesis by NAT_1: 11;

      end;

    end;

    registration

      let R;

      cluster ( SCM R) -> standard;

      coherence

      proof

        deffunc U( Element of NAT ) = $1;

        for k be Nat holds (k + 1) in ( SUCC (k,( SCM R))) & for j be Nat st j in ( SUCC (k,( SCM R))) holds k <= j by Th35;

        hence thesis by AMISTD_1: 3;

      end;

    end

    definition

      let R be Ring, k be Nat;

      :: SCMRING3:def1

      func dl. (R,k) -> Data-Location of R equals ( dl. k);

      coherence by AMI_2:def 16, AMI_3: 27, SCMRING2: 1;

    end

    registration

      let R;

      cluster ( InsCode ( halt ( SCM R))) -> jump-only;

      coherence

      proof

        now

          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 in ( Data-Locations ( SCM R));

          I = ( halt ( SCM R)) by A1, Th11;

          hence (( Exec (I,s)) . o) = (s . o) by EXTPRO_1:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      let R;

      cluster ( halt ( SCM R)) -> jump-only;

      coherence ;

    end

    registration

      let R, i1;

      cluster ( InsCode ( goto (i1,R))) -> jump-only;

      coherence

      proof

        set S = ( SCM R);

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A1: ( InsCode I) = ( InsCode ( goto (i1,R))) and

           A2: o in ( Data-Locations ( SCM R));

          

           A3: ex i2 st I = ( goto (i2,R)) by A1, Th17;

          o in ( Data-Locations SCM ) by A2, SCMRING2: 22;

          then o is Data-Location of R by SCMRING2: 1;

          hence (( Exec (I,s)) . o) = (s . o) by A3, SCMRING2: 15;

        end;

        hence thesis;

      end;

    end

    registration

      let R, i1;

      cluster ( goto (i1,R)) -> jump-only;

      coherence ;

    end

    registration

      let R, a, i1;

      cluster ( InsCode (a =0_goto i1)) -> jump-only;

      coherence

      proof

        set S = ( SCM R);

        now

          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 in ( Data-Locations ( SCM R));

          

           A3: ex b, i2 st I = (b =0_goto i2) by A1, Th18;

          o in ( Data-Locations SCM ) by A2, SCMRING2: 22;

          then o is Data-Location of R by SCMRING2: 1;

          hence (( Exec (I,s)) . o) = (s . o) by A3, SCMRING2: 16;

        end;

        hence thesis;

      end;

    end

    registration

      let R, a, i1;

      cluster (a =0_goto i1) -> jump-only;

      coherence ;

    end

    reserve S for non trivial Ring,

p,q for Data-Location of S,

w for Element of S;

    registration

      let S, p, q;

      cluster ( InsCode (p := q)) -> non jump-only;

      coherence

      proof

        set w = the State of ( SCM S);

        consider e be Element of S such that

         A1: e <> ( 0. S) by STRUCT_0:def 18;

        reconsider e as Element of S;

        set t = (w +* ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)));

        

         A2: ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) = {( dl. (S, 0 )), ( dl. (S,1))} by FUNCT_4: 62;

        then

         A3: ( dl. (S,1)) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by TARSKI:def 2;

        

         A4: ( InsCode (p := q)) = 1

        .= ( InsCode (( dl. (S, 0 )) := ( dl. (S,1))));

        ( dl. (S, 0 )) in ( Data-Locations SCM ) by SCMRING2: 1;

        then

         A5: ( dl. (S, 0 )) in ( Data-Locations ( SCM S)) by SCMRING2: 22;

        ( dl. (S, 0 )) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by A2, TARSKI:def 2;

        

        then

         A6: (t . ( dl. (S, 0 ))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S, 0 ))) by FUNCT_4: 13

        .= ( 0. S) by AMI_3: 10, FUNCT_4: 63;

        (( Exec ((( dl. (S, 0 )) := ( dl. (S,1))),t)) . ( dl. (S, 0 ))) = (t . ( dl. (S,1))) by SCMRING2: 11

        .= (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S,1))) by A3, FUNCT_4: 13

        .= e by FUNCT_4: 63;

        hence thesis by A1, A4, A6, A5;

      end;

    end

    registration

      let S, p, q;

      cluster (p := q) -> non jump-only;

      coherence ;

    end

    registration

      let S, p, q;

      cluster ( InsCode ( AddTo (p,q))) -> non jump-only;

      coherence

      proof

        set w = the State of ( SCM S);

        consider e be Element of S such that

         A1: e <> ( 0. S) by STRUCT_0:def 18;

        reconsider e as Element of S;

        set t = (w +* ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)));

        

         A2: ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) = {( dl. (S, 0 )), ( dl. (S,1))} by FUNCT_4: 62;

        then ( dl. (S, 0 )) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by TARSKI:def 2;

        

        then

         A3: (t . ( dl. (S, 0 ))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S, 0 ))) by FUNCT_4: 13

        .= ( 0. S) by AMI_3: 10, FUNCT_4: 63;

        

         A4: ( InsCode ( AddTo (p,q))) = 2

        .= ( InsCode ( AddTo (( dl. (S, 0 )),( dl. (S,1)))));

        ( dl. (S,1)) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by A2, TARSKI:def 2;

        

        then

         A5: (t . ( dl. (S,1))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S,1))) by FUNCT_4: 13

        .= e by FUNCT_4: 63;

        ( dl. (S, 0 )) in ( Data-Locations SCM ) by SCMRING2: 1;

        then

         A6: ( dl. (S, 0 )) in ( Data-Locations ( SCM S)) by SCMRING2: 22;

        (( Exec (( AddTo (( dl. (S, 0 )),( dl. (S,1)))),t)) . ( dl. (S, 0 ))) = ((t . ( dl. (S, 0 ))) + (t . ( dl. (S,1)))) by SCMRING2: 12

        .= e by A3, A5, RLVECT_1: 4;

        hence thesis by A1, A4, A3, A6;

      end;

    end

    registration

      let S, p, q;

      cluster ( AddTo (p,q)) -> non jump-only;

      coherence ;

    end

    registration

      let S, p, q;

      cluster ( InsCode ( SubFrom (p,q))) -> non jump-only;

      coherence

      proof

        set w = the State of ( SCM S);

        consider e be Element of S such that

         A1: e <> ( 0. S) by STRUCT_0:def 18;

        reconsider e as Element of S;

         A2:

        now

          assume ( - e) = ( 0. S);

          then e = ( - ( 0. S)) by RLVECT_1: 17;

          hence contradiction by A1, RLVECT_1: 12;

        end;

        set t = (w +* ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)));

        

         A3: ( InsCode ( SubFrom (p,q))) = 3

        .= ( InsCode ( SubFrom (( dl. (S, 0 )),( dl. (S,1)))));

        

         A4: ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) = {( dl. (S, 0 )), ( dl. (S,1))} by FUNCT_4: 62;

        then ( dl. (S, 0 )) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by TARSKI:def 2;

        

        then

         A5: (t . ( dl. (S, 0 ))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S, 0 ))) by FUNCT_4: 13

        .= ( 0. S) by AMI_3: 10, FUNCT_4: 63;

        ( dl. (S,1)) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e))) by A4, TARSKI:def 2;

        

        then

         A6: (t . ( dl. (S,1))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 0. S),e)) . ( dl. (S,1))) by FUNCT_4: 13

        .= e by FUNCT_4: 63;

        ( dl. (S, 0 )) in ( Data-Locations SCM ) by SCMRING2: 1;

        then

         A7: ( dl. (S, 0 )) in ( Data-Locations ( SCM S)) by SCMRING2: 22;

        (( Exec (( SubFrom (( dl. (S, 0 )),( dl. (S,1)))),t)) . ( dl. (S, 0 ))) = ((t . ( dl. (S, 0 ))) - (t . ( dl. (S,1)))) by SCMRING2: 13

        .= ( - e) by A5, A6, RLVECT_1: 14;

        hence thesis by A3, A5, A2, A7;

      end;

    end

    registration

      let S, p, q;

      cluster ( SubFrom (p,q)) -> non jump-only;

      coherence ;

    end

    registration

      let S, p, q;

      cluster ( InsCode ( MultBy (p,q))) -> non jump-only;

      coherence

      proof

        ( IC ( SCM S)) = ( IC SCM ) by AMI_3: 1, SCMRING2: 8;

        then

         A1: ( 0. S) <> ( 1_ S) & ( dl. (S, 0 )) <> ( IC ( SCM S)) by AMI_3: 13, LMOD_6:def 1;

        set w = the State of ( SCM S);

        set t = (w +* ((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S))));

        

         A2: ( InsCode ( MultBy (p,q))) = 4

        .= ( InsCode ( MultBy (( dl. (S, 0 )),( dl. (S,1)))));

        

         A3: ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S)))) = {( dl. (S, 0 )), ( dl. (S,1))} by FUNCT_4: 62;

        then ( dl. (S, 0 )) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S)))) by TARSKI:def 2;

        

        then

         A4: (t . ( dl. (S, 0 ))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S))) . ( dl. (S, 0 ))) by FUNCT_4: 13

        .= ( 1_ S) by AMI_3: 10, FUNCT_4: 63;

        ( dl. (S,1)) in ( dom ((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S)))) by A3, TARSKI:def 2;

        

        then

         A5: (t . ( dl. (S,1))) = (((( dl. (S, 0 )),( dl. (S,1))) --> (( 1_ S),( 0. S))) . ( dl. (S,1))) by FUNCT_4: 13

        .= ( 0. S) by FUNCT_4: 63;

        ( dl. (S, 0 )) in ( Data-Locations SCM ) by SCMRING2: 1;

        then

         A6: ( dl. (S, 0 )) in ( Data-Locations ( SCM S)) by SCMRING2: 22;

        (( Exec (( MultBy (( dl. (S, 0 )),( dl. (S,1)))),t)) . ( dl. (S, 0 ))) = ((t . ( dl. (S, 0 ))) * (t . ( dl. (S,1)))) by SCMRING2: 14

        .= ( 0. S) by A5;

        hence thesis by A2, A1, A4, A6;

      end;

    end

    registration

      let S, p, q;

      cluster ( MultBy (p,q)) -> non jump-only;

      coherence ;

    end

    registration

      let S, p, w;

      cluster ( InsCode (p := w)) -> non jump-only;

      coherence

      proof

        set j = the State of ( SCM S);

        

         A1: ( InsCode (p := w)) = 5

        .= ( InsCode (( dl. (S, 0 )) := w));

        the carrier of S <> {w};

        then

        consider e be object such that

         A2: e in the carrier of S and

         A3: e <> w by ZFMISC_1: 35;

        ( Values ( dl. (S, 0 ))) = the carrier of S by Th1;

        then

        reconsider e as Element of ( Values ( dl. (S, 0 ))) by A2;

        reconsider v = (( dl. (S, 0 )) .--> e) as PartState of ( SCM S);

        set t = (j +* v);

        ( dl. (S, 0 )) in ( dom (( dl. (S, 0 )) .--> e)) by TARSKI:def 1;

        

        then

         A4: (t . ( dl. (S, 0 ))) = ((( dl. (S, 0 )) .--> e) . ( dl. (S, 0 ))) by FUNCT_4: 13

        .= e by FUNCOP_1: 72;

        ( dl. (S, 0 )) in ( Data-Locations SCM ) by SCMRING2: 1;

        then

         A5: ( dl. (S, 0 )) in ( Data-Locations ( SCM S)) by SCMRING2: 22;

        (( Exec ((( dl. (S, 0 )) := w),t)) . ( dl. (S, 0 ))) = w by SCMRING2: 17;

        hence thesis by A3, A1, A4, A5;

      end;

    end

    registration

      let S, p, w;

      cluster (p := w) -> non jump-only;

      coherence ;

    end

    registration

      let R, i1;

      cluster ( goto (i1,R)) -> non sequential;

      coherence

      proof

        ( JUMP ( goto (i1,R))) <> {} ;

        hence thesis by AMISTD_1: 13;

      end;

    end

    registration

      let R, a, i1;

      cluster (a =0_goto i1) -> non sequential;

      coherence

      proof

        ( JUMP (a =0_goto i1)) <> {} ;

        hence thesis by AMISTD_1: 13;

      end;

    end

    registration

      let R, i1;

      cluster ( goto (i1,R)) -> non ins-loc-free;

      coherence ;

    end

    registration

      let R, a, i1;

      cluster (a =0_goto i1) -> non ins-loc-free;

      coherence ;

    end

    registration

      let R;

      cluster ( SCM R) -> with_explicit_jumps;

      coherence

      proof

        let I be Instruction of ( SCM R);

        thus ( JUMP I) c= ( rng ( JumpPart I))

        proof

          let f be object such that

           A1: f in ( JUMP I);

          per cases by SCMRING2: 7;

            suppose

             A2: I = [ 0 , {} , {} ];

            ( JUMP ( halt ( SCM R))) is empty;

            hence thesis by A1, A2;

          end;

            suppose ex a, b st I = (a := b);

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( AddTo (a,b));

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( SubFrom (a,b));

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( MultBy (a,b));

            hence thesis by A1;

          end;

            suppose

             A3: ex i1 st I = ( goto (i1,R));

            consider i1 such that

             A4: I = ( goto (i1,R)) by A3;

            ( rng <*i1*>) = {i1} by FINSEQ_1: 39;

            hence f in ( rng ( JumpPart I)) by A1, A4, Th30;

          end;

            suppose

             A5: ex a, i1 st I = (a =0_goto i1);

            consider a, i1 such that

             A6: I = (a =0_goto i1) by A5;

            ( rng <*i1*>) = {i1} by FINSEQ_1: 39;

            hence thesis by A1, A6, Th33;

          end;

            suppose ex a, r st I = (a := r);

            hence thesis by A1;

          end;

        end;

        let f be object;

        assume f in ( rng ( JumpPart I));

        then

        consider k be object such that

         A7: k in ( dom ( JumpPart I)) and

         A8: f = (( JumpPart I) . k) by FUNCT_1:def 3;

        per cases by SCMRING2: 7;

          suppose I = [ 0 , {} , {} ];

          then I = ( halt ( SCM R));

          hence thesis by A7;

        end;

          suppose ex a, b st I = (a := b);

          then

          consider a, b such that

           A9: I = (a := b);

          k in ( dom {} ) by A7, A9;

          hence thesis;

        end;

          suppose ex a, b st I = ( AddTo (a,b));

          then

          consider a, b such that

           A10: I = ( AddTo (a,b));

          k in ( dom {} ) by A7, A10;

          hence thesis;

        end;

          suppose ex a, b st I = ( SubFrom (a,b));

          then

          consider a, b such that

           A11: I = ( SubFrom (a,b));

          k in ( dom {} ) by A7, A11;

          hence thesis;

        end;

          suppose ex a, b st I = ( MultBy (a,b));

          then

          consider a, b such that

           A12: I = ( MultBy (a,b));

          k in ( dom {} ) by A7, A12;

          hence thesis;

        end;

          suppose ex i1 st I = ( goto (i1,R));

          then

          consider i1 such that

           A13: I = ( goto (i1,R));

          

           A14: ( JumpPart I) = <*i1*> by A13;

          then k = 1 by A7, Lm1;

          then

           A15: f = i1 by A14, A8, FINSEQ_1:def 8;

          ( JUMP I) = {i1} by A13, Th30;

          hence thesis by A15, TARSKI:def 1;

        end;

          suppose ex a, i1 st I = (a =0_goto i1);

          then

          consider a, i1 such that

           A16: I = (a =0_goto i1);

          

           A17: ( JumpPart I) = <*i1*> by A16;

          then k = 1 by A7, Lm1;

          then

           A18: f = i1 by A17, A8, FINSEQ_1: 40;

          ( JUMP I) = {i1} by A16, Th33;

          hence thesis by A18, TARSKI:def 1;

        end;

          suppose ex a, r st I = (a := r);

          then

          consider a, r such that

           A19: I = (a := r);

          k in ( dom {} ) by A7, A19;

          hence thesis;

        end;

      end;

    end

    theorem :: SCMRING3:37

    

     Th36: ( IncAddr (( goto (i1,R)),k)) = ( goto ((i1 + k),R))

    proof

      

       A1: ( JumpPart ( IncAddr (( goto (i1,R)),k))) = (k + ( JumpPart ( goto (i1,R)))) by COMPOS_0:def 9;

      then

       A2: ( dom ( JumpPart ( IncAddr (( goto (i1,R)),k)))) = ( dom ( JumpPart ( goto (i1,R)))) by VALUED_1:def 2;

      

       A3: ( dom ( JumpPart ( goto ((i1 + k),R)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1:def 8

      .= ( dom <*i1*>) by FINSEQ_1:def 8

      .= ( dom ( JumpPart ( goto (i1,R))));

      

       A4: for x be object st x in ( dom ( JumpPart ( goto (i1,R)))) holds (( JumpPart ( IncAddr (( goto (i1,R)),k))) . x) = (( JumpPart ( goto ((i1 + k),R))) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom ( JumpPart ( goto (i1,R))));

        then x in ( dom <*i1*>);

        then

         A6: x = 1 by Lm1;

        reconsider f = (( JumpPart ( goto (i1,R))) . x) as Element of NAT by ORDINAL1:def 12;

        

         A7: (( JumpPart ( IncAddr (( goto (i1,R)),k))) . x) = (k + f) by A5, A1, A2, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A6, FINSEQ_1:def 8;

        

        hence (( JumpPart ( IncAddr (( goto (i1,R)),k))) . x) = ( <*(i1 + k)*> . x) by A6, A7, FINSEQ_1:def 8

        .= (( JumpPart ( goto ((i1 + k),R))) . x);

      end;

      

       A8: ( InsCode ( IncAddr (( goto (i1,R)),k))) = ( InsCode ( goto (i1,R))) by COMPOS_0:def 9

      .= 6

      .= ( InsCode ( goto ((i1 + k),R)));

      

       A9: ( AddressPart ( IncAddr (( goto (i1,R)),k))) = ( AddressPart ( goto (i1,R))) by COMPOS_0:def 9

      .= {}

      .= ( AddressPart ( goto ((i1 + k),R)));

      ( JumpPart ( IncAddr (( goto (i1,R)),k))) = ( JumpPart ( goto ((i1 + k),R))) by A2, A3, A4, FUNCT_1: 2;

      hence thesis by A8, A9, COMPOS_0: 1;

    end;

    theorem :: SCMRING3:38

    

     Th37: ( IncAddr ((a =0_goto i1),k)) = (a =0_goto (i1 + k))

    proof

      

       A1: ( JumpPart ( IncAddr ((a =0_goto i1),k))) = (k + ( JumpPart (a =0_goto i1))) by COMPOS_0:def 9;

      then

       A2: ( dom ( JumpPart ( IncAddr ((a =0_goto i1),k)))) = ( dom ( JumpPart (a =0_goto i1))) by VALUED_1:def 2;

      

       A3: ( dom ( JumpPart (a =0_goto (i1 + k)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*i1*>) by FINSEQ_1: 38

      .= ( dom ( JumpPart (a =0_goto i1)));

      

       A4: for x be object st x in ( dom ( JumpPart (a =0_goto i1))) holds (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (( JumpPart (a =0_goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom ( JumpPart (a =0_goto i1)));

        then x in ( dom <*i1*>);

        then

         A6: x = 1 by FINSEQ_1: 90;

        reconsider f = (( JumpPart (a =0_goto i1)) . x) as Element of NAT by ORDINAL1:def 12;

        

         A7: (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (k + f) by A5, A1, A2, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A6, FINSEQ_1: 40;

        

        hence (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A6, A7, FINSEQ_1: 40

        .= (( JumpPart (a =0_goto (i1 + k))) . x);

      end;

      

       A8: ( InsCode ( IncAddr ((a =0_goto i1),k))) = ( InsCode (a =0_goto i1)) by COMPOS_0:def 9

      .= 7

      .= ( InsCode (a =0_goto (i1 + k)));

      

       A9: ( AddressPart ( IncAddr ((a =0_goto i1),k))) = ( AddressPart (a =0_goto i1)) by COMPOS_0:def 9

      .= <*a*>

      .= ( AddressPart (a =0_goto (i1 + k)));

      ( JumpPart ( IncAddr ((a =0_goto i1),k))) = ( JumpPart (a =0_goto (i1 + k))) by A2, A3, A4, FUNCT_1: 2;

      hence thesis by A8, A9, COMPOS_0: 1;

    end;

    registration

      let R;

      cluster ( SCM R) -> IC-relocable;

      coherence

      proof

        thus ( SCM R) is IC-relocable

        proof

          let I be Instruction of ( SCM R);

          per cases by SCMRING2: 7;

            suppose I = [ 0 , {} , {} ];

            then I = ( halt ( SCM R));

            hence thesis;

          end;

            suppose ex a, b st I = (a := b);

            hence thesis;

          end;

            suppose ex a, b st I = ( AddTo (a,b));

            hence thesis;

          end;

            suppose ex a, b st I = ( SubFrom (a,b));

            hence thesis;

          end;

            suppose ex a, b st I = ( MultBy (a,b));

            hence thesis;

          end;

            suppose

             A1: ex i1 st I = ( goto (i1,R));

            let j,k be Nat, s1 be State of ( SCM R);

            set s2 = ( IncIC (s1,k));

            consider i1 such that

             A2: I = ( goto (i1,R)) by A1;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec (( goto ((j + i1),R)),s1))) + k) by A2, Th36

            .= ((j + i1) + k) by SCMRING2: 15

            .= ( IC ( Exec (( goto (((j + i1) + k),R)),s2))) by SCMRING2: 15

            .= ( IC ( Exec (( goto (((j + k) + i1),R)),s2)))

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A2, Th36;

          end;

            suppose ex a, i1 st I = (a =0_goto i1);

            then

            consider a, i1 such that

             A3: I = (a =0_goto i1);

            let j,k be Nat, s1 be State of ( SCM R);

            set s2 = ( IncIC (s1,k));

            a <> ( IC ( SCM R)) & ( dom (( IC ( SCM R)) .--> (( IC s1) + k))) = {( IC ( SCM R))} by Th2;

            then not a in ( dom (( IC ( SCM R)) .--> (( IC s1) + k))) by TARSKI:def 1;

            then

             A4: (s1 . a) = (s2 . a) by FUNCT_4: 11;

            per cases ;

              suppose

               A5: (s1 . a) = ( 0. R);

              

              thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec ((a =0_goto (j + i1)),s1))) + k) by A3, Th37

              .= ((j + i1) + k) by A5, SCMRING2: 16

              .= ( IC ( Exec ((a =0_goto ((j + i1) + k)),s2))) by A4, A5, SCMRING2: 16

              .= ( IC ( Exec ((a =0_goto ((j + k) + i1)),s2)))

              .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A3, Th37;

            end;

              suppose

               A6: (s1 . a) <> ( 0. R);

              

               A7: ( IncAddr (I,j)) = (a =0_goto (i1 + j)) by A3, Th37;

              

               A8: ( IncAddr (I,(j + k))) = (a =0_goto (i1 + (j + k))) by A3, Th37;

              ( IC ( SCM R)) in ( dom (( IC ( SCM R)) .--> (( IC s1) + k))) by TARSKI:def 1;

              

              then

               A9: ( IC s2) = ((( IC ( SCM R)) .--> (( IC s1) + k)) . ( IC ( SCM R))) by FUNCT_4: 13

              .= (( IC s1) + k) by FUNCOP_1: 72;

              

              thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ((( IC s1) + 1) + k) by A7, A6, SCMRING2: 16

              .= ((( IC s1) + 1) + k)

              .= (( IC s2) + 1) by A9

              .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A8, A6, A4, SCMRING2: 16;

            end;

          end;

            suppose ex a, r st I = (a := r);

            hence thesis;

          end;

        end;

      end;

    end

    theorem :: SCMRING3:39

    ( InsCode I) <= 7

    proof

      set T = ( InsCode I);

      T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 by Lm2;

      hence thesis;

    end;