scmring2.miz



    begin

    reserve I for Element of ( Segm 8),

S for non empty 1-sorted,

t for Element of S,

x for set,

k for Element of NAT ;

    reserve R for Ring,

T for InsType of ( SCM-Instr R);

    definition

      let R be Ring;

      :: SCMRING2:def1

      func SCM R -> strict AMI-Struct over ( Segm 2) means

      : Def1: the carrier of it = SCM-Memory & the ZeroF of it = NAT & the InstructionsF of it = ( SCM-Instr R) & the Object-Kind of it = SCM-OK & the ValuesF of it = ( SCM-VAL R) & the Execution of it = ( SCM-Exec R);

      existence

      proof

        take AMI-Struct (# SCM-Memory , ( In ( NAT , SCM-Memory )), ( SCM-Instr R), SCM-OK , ( SCM-VAL R), ( SCM-Exec R) #);

        thus thesis by AMI_2: 22, SUBSET_1:def 8;

      end;

      uniqueness ;

    end

    registration

      let R be Ring;

      cluster ( SCM R) -> non empty;

      coherence by Def1;

    end

     Lm1:

    now

      let R be Ring;

      

      thus ( the_Values_of ( SCM R)) = (the ValuesF of ( SCM R) * the Object-Kind of ( SCM R))

      .= (the ValuesF of ( SCM R) * SCM-OK ) by Def1

      .= (( SCM-VAL R) * SCM-OK ) by Def1;

    end;

    registration

      let R be Ring;

      cluster ( SCM R) -> with_non-empty_values;

      coherence

      proof

        ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

        hence ( the_Values_of ( SCM R)) is non-empty;

      end;

    end

    

     Lm2: for R be Ring holds (the carrier of ( SCM R) \ { NAT }) = SCM-Data-Loc

    proof

      let R be Ring;

      

       A1: not NAT in SCM-Data-Loc by AMI_2: 20;

      

      thus (the carrier of ( SCM R) \ { NAT }) = ( SCM-Memory \ { NAT }) by Def1

      .= (( { NAT } \/ SCM-Data-Loc ) \ { NAT })

      .= SCM-Data-Loc by A1, ZFMISC_1: 117;

    end;

    registration

      let R be Ring;

      cluster Int-like for Object of ( SCM R);

      existence

      proof

        the carrier of ( SCM R) = SCM-Memory by Def1;

        then

        reconsider x = the Element of SCM-Data-Loc as Object of ( SCM R);

        take x;

        thus thesis;

      end;

    end

    definition

      let R be Ring;

      mode Data-Location of R is Int-like Object of ( SCM R);

      ::$Canceled

    end

    reserve R for Ring,

r for Element of R,

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

i1 for Nat;

    theorem :: SCMRING2:1

    

     Th1: x is Data-Location of R iff x in ( Data-Locations SCM ) by Def1, AMI_2:def 16, AMI_3: 27;

    definition

      let R be Ring, s be State of ( SCM R), a be Data-Location of R;

      :: original: .

      redefine

      func s . a -> Element of R ;

      coherence

      proof

        ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

        then

        reconsider S = s as SCM-State of R by CARD_3: 107;

        a is Element of ( Data-Locations SCM ) by Th1;

        then

        reconsider a as Element of SCM-Data-Loc by AMI_3: 27;

        (S . a) in the carrier of R;

        hence thesis;

      end;

    end

    theorem :: SCMRING2:2

     [ 0 , {} , {} ] is Instruction of ( SCM R)

    proof

      ( halt ( SCM R)) = [ 0 , {} , {} ];

      hence thesis;

    end;

    theorem :: SCMRING2:3

    

     Th3: x in {1, 2, 3, 4} implies [x, {} , <*d1, d2*>] in ( SCM-Instr S)

    proof

      reconsider d1, d2 as Element of SCM-Data-Loc by Th1, AMI_3: 27;

      x in {1, 2, 3, 4} implies [x, {} , <*d1, d2*>] in ( SCM-Instr S) by SCMRINGI: 8;

      hence thesis;

    end;

    theorem :: SCMRING2:4

    

     Th4: [5, {} , <*d1, t*>] in ( SCM-Instr S)

    proof

      reconsider d1 as Element of SCM-Data-Loc by Th1, AMI_3: 27;

       [5, {} , <*d1, t*>] in ( SCM-Instr S) by SCMRINGI: 9;

      hence thesis;

    end;

    theorem :: SCMRING2:5

    

     Th5: [6, <*i1*>, {} ] in ( SCM-Instr S) by SCMRINGI: 10;

    theorem :: SCMRING2:6

    

     Th6: [7, <*i1*>, <*d1*>] in ( SCM-Instr S)

    proof

      reconsider d1 as Element of SCM-Data-Loc by Th1, AMI_3: 27;

       [7, <*i1*>, <*d1*>] in ( SCM-Instr S) by SCMRINGI: 11;

      hence thesis;

    end;

    definition

      let R be Ring, a,b be Data-Location of R;

      :: SCMRING2:def3

      func a := b -> Instruction of ( SCM R) equals [1, {} , <*a, b*>];

      coherence

      proof

        1 in {1, 2, 3, 4} by ENUMSET1:def 2;

        then [1, {} , <*a, b*>] in ( SCM-Instr R) by Th3;

        hence thesis by Def1;

      end;

      :: SCMRING2:def4

      func AddTo (a,b) -> Instruction of ( SCM R) equals [2, {} , <*a, b*>];

      coherence

      proof

        2 in {1, 2, 3, 4} by ENUMSET1:def 2;

        then [2, {} , <*a, b*>] in ( SCM-Instr R) by Th3;

        hence thesis by Def1;

      end;

      :: SCMRING2:def5

      func SubFrom (a,b) -> Instruction of ( SCM R) equals [3, {} , <*a, b*>];

      coherence

      proof

        3 in {1, 2, 3, 4} by ENUMSET1:def 2;

        then [3, {} , <*a, b*>] in ( SCM-Instr R) by Th3;

        hence thesis by Def1;

      end;

      :: SCMRING2:def6

      func MultBy (a,b) -> Instruction of ( SCM R) equals [4, {} , <*a, b*>];

      coherence

      proof

        4 in {1, 2, 3, 4} by ENUMSET1:def 2;

        then [4, {} , <*a, b*>] in ( SCM-Instr R) by Th3;

        hence thesis by Def1;

      end;

    end

    definition

      let R be Ring, a be Data-Location of R, r be Element of R;

      :: SCMRING2:def7

      func a := r -> Instruction of ( SCM R) equals [5, {} , <*a, r*>];

      coherence

      proof

         [5, {} , <*a, r*>] in ( SCM-Instr R) by Th4;

        hence thesis by Def1;

      end;

    end

    definition

      let R be Ring, l be Nat;

      :: SCMRING2:def8

      func goto (l,R) -> Instruction of ( SCM R) equals [6, <*l*>, {} ];

      coherence

      proof

         [6, <*l*>, {} ] in ( SCM-Instr R) by Th5;

        hence thesis by Def1;

      end;

    end

    definition

      let R be Ring, l be Nat, a be Data-Location of R;

      :: SCMRING2:def9

      func a =0_goto l -> Instruction of ( SCM R) equals [7, <*l*>, <*a*>];

      coherence

      proof

         [7, <*l*>, <*a*>] in ( SCM-Instr R) by Th6;

        hence thesis by Def1;

      end;

    end

    theorem :: SCMRING2:7

    

     Th7: for I be set holds I is Instruction of ( SCM R) iff 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)

    proof

      let J be set;

      

       A1: the InstructionsF of ( SCM R) = ( SCM-Instr R) by Def1;

      thus J is Instruction of ( SCM R) implies 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,R))) or (ex a, i1 st J = (a =0_goto i1)) or ex a, r st J = (a := r)

      proof

        assume J is Instruction of ( SCM R);

        then J 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 J in the set of all [5, {} , <*a, r*>] where a be Element of ( Data-Locations SCM ), r be Element of R by A1, AMI_3: 27, XBOOLE_0:def 3;

        then J 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 J in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM ) or J 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

         A2: J 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 J in the set of all [6, <*i*>, {} ] where i be Nat or J in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of ( Data-Locations SCM ) or J 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 A2, XBOOLE_0:def 3;

          suppose J in { [ 0 , {} , {} ]};

          hence thesis by TARSKI:def 1;

        end;

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

          then

          consider i be Nat such that

           A3: J = [6, <*i*>, {} ] and not contradiction;

          J = ( goto (i,R)) by A3;

          hence thesis;

        end;

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

          then

          consider i be Nat, a be Element of ( Data-Locations SCM ) such that

           A4: J = [7, <*i*>, <*a*>] and not contradiction;

          reconsider A = a as Data-Location of R by Th1, AMI_3: 27;

          J = (A =0_goto i) by A4;

          hence thesis;

        end;

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

          then

          consider a be Element of ( Data-Locations SCM ), r be Element of R such that

           A5: J = [5, {} , <*a, r*>] and not contradiction;

          reconsider A = a as Data-Location of R by Th1, AMI_3: 27;

          J = (A := r) by A5;

          hence thesis;

        end;

          suppose J 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

          consider I be Element of ( Segm 8), a,b be Element of ( Data-Locations SCM ) such that

           A6: J = [I, {} , <*a, b*>] & I in {1, 2, 3, 4};

          reconsider A = a, B = b as Data-Location of R by Th1, AMI_3: 27;

          J = (A := B) or J = ( AddTo (A,B)) or J = ( SubFrom (A,B)) or J = ( MultBy (A,B)) by A6, ENUMSET1:def 2;

          hence thesis;

        end;

      end;

      thus thesis by A1, SCMRINGI: 6;

    end;

    reserve s for State of ( SCM R);

    registration

      let R be non empty Ring;

      cluster ( SCM R) -> IC-Ins-separated;

      coherence

      proof

        

         A1: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

        ( IC ( SCM R)) = NAT by Def1;

        then ( Values ( IC ( SCM R))) = NAT by A1, SCMRING1: 2;

        hence ( SCM R) is IC-Ins-separated;

      end;

    end

    theorem :: SCMRING2:8

    ( IC ( SCM R)) = NAT by Def1;

    theorem :: SCMRING2:9

    for S be SCM-State of R st S = s holds ( IC s) = ( IC S) by Def1;

    theorem :: SCMRING2:10

    

     Th10: for I be Instruction of ( SCM R) holds for i be Element of ( SCM-Instr R) st i = I holds for S be SCM-State of R st S = s holds ( Exec (I,s)) = ( SCM-Exec-Res (i,S))

    proof

      let I be Instruction of ( SCM R), i be Element of ( SCM-Instr R) such that

       A1: i = I;

      let S be SCM-State of R;

      assume S = s;

      

      hence ( Exec (I,s)) = ((( SCM-Exec R) . i) qua Element of ( Funcs (( product (( SCM-VAL R) * SCM-OK )),( product (( SCM-VAL R) * SCM-OK )))) . S) by A1, Def1

      .= ( SCM-Exec-Res (i,S)) by SCMRING1:def 15;

    end;

    begin

    theorem :: SCMRING2:11

    

     Th11: (( Exec ((a := b),s)) . ( IC ( SCM R))) = (( IC s) + 1) & (( Exec ((a := b),s)) . a) = (s . b) & for c st c <> a holds (( Exec ((a := b),s)) . c) = (s . c)

    proof

      

       A1: a is Element of ( Data-Locations SCM ) by Th1;

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A2, CARD_3: 107;

      reconsider I = (a := b) as Element of ( SCM-Instr R) by Def1;

      set S1 = ( SCM-Chg (S,(I address_1 ),(S . (I address_2 ))));

      reconsider i = 1 as Element of ( Segm 8) by NAT_1: 44;

      

       A3: ( IC s) = ( IC S) by Def1;

      

       A4: b is Element of ( Data-Locations SCM ) by Th1;

      

       A5: ( Exec ((a := b),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, A4, AMI_3: 27, SCMRING1:def 14;

      

       A6: I = [i, {} , <*a, b*>];

      then

       A7: (I address_1 ) = a by A1, A4, AMI_3: 27, SCMRINGI: 1;

      

       A8: (I address_2 ) = b by A6, A1, A4, AMI_3: 27, SCMRINGI: 1;

      

      thus (( Exec ((a := b),s)) . ( IC ( SCM R))) = (( Exec ((a := b),s)) . NAT ) by Def1

      .= (( IC s) + 1) by A3, A5, SCMRING1: 7;

      

      thus (( Exec ((a := b),s)) . a) = (S1 . a) by A1, A5, AMI_3: 27, SCMRING1: 8

      .= (s . b) by A7, A8, SCMRING1: 11;

      let c;

      assume

       A9: c <> a;

      

       A10: c is Element of ( Data-Locations SCM ) by Th1;

      

      hence (( Exec ((a := b),s)) . c) = (S1 . c) by A5, AMI_3: 27, SCMRING1: 8

      .= (s . c) by A7, A9, A10, AMI_3: 27, SCMRING1: 12;

    end;

    theorem :: SCMRING2:12

    

     Th12: (( Exec (( AddTo (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) & (( Exec (( AddTo (a,b)),s)) . a) = ((s . a) + (s . b)) & for c st c <> a holds (( Exec (( AddTo (a,b)),s)) . c) = (s . c)

    proof

      

       A1: a is Element of ( Data-Locations SCM ) by Th1;

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A2, CARD_3: 107;

      reconsider I = ( AddTo (a,b)) as Element of ( SCM-Instr R) by Def1;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) + (S . (I address_2 )))));

      reconsider i = 2 as Element of ( Segm 8) by NAT_1: 44;

      

       A3: ( IC s) = ( IC S) by Def1;

      

       A4: b is Element of ( Data-Locations SCM ) by Th1;

      

       A5: ( Exec (( AddTo (a,b)),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, A4, AMI_3: 27, SCMRING1:def 14;

      

       A6: I = [i, {} , <*a, b*>];

      then

       A7: (I address_1 ) = a by A1, A4, AMI_3: 27, SCMRINGI: 1;

      

       A8: (I address_2 ) = b by A6, A1, A4, AMI_3: 27, SCMRINGI: 1;

      

      thus (( Exec (( AddTo (a,b)),s)) . ( IC ( SCM R))) = (( Exec (( AddTo (a,b)),s)) . NAT ) by Def1

      .= (( IC s) + 1) by A3, A5, SCMRING1: 7;

      

      thus (( Exec (( AddTo (a,b)),s)) . a) = (S1 . a) by A1, A5, AMI_3: 27, SCMRING1: 8

      .= ((s . a) + (s . b)) by A7, A8, SCMRING1: 11;

      let c;

      assume

       A9: c <> a;

      

       A10: c is Element of ( Data-Locations SCM ) by Th1;

      

      hence (( Exec (( AddTo (a,b)),s)) . c) = (S1 . c) by A5, AMI_3: 27, SCMRING1: 8

      .= (s . c) by A7, A9, A10, AMI_3: 27, SCMRING1: 12;

    end;

    theorem :: SCMRING2:13

    

     Th13: (( Exec (( SubFrom (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) & (( Exec (( SubFrom (a,b)),s)) . a) = ((s . a) - (s . b)) & for c st c <> a holds (( Exec (( SubFrom (a,b)),s)) . c) = (s . c)

    proof

      

       A1: a is Element of ( Data-Locations SCM ) by Th1;

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A2, CARD_3: 107;

      reconsider I = ( SubFrom (a,b)) as Element of ( SCM-Instr R) by Def1;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) - (S . (I address_2 )))));

      reconsider i = 3 as Element of ( Segm 8) by NAT_1: 44;

      

       A3: ( IC s) = ( IC S) by Def1;

      

       A4: b is Element of ( Data-Locations SCM ) by Th1;

      

       A5: ( Exec (( SubFrom (a,b)),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, A4, AMI_3: 27, SCMRING1:def 14;

      

       A6: I = [i, {} , <*a, b*>];

      then

       A7: (I address_1 ) = a by A1, A4, AMI_3: 27, SCMRINGI: 1;

      

       A8: (I address_2 ) = b by A6, A1, A4, AMI_3: 27, SCMRINGI: 1;

      

      thus (( Exec (( SubFrom (a,b)),s)) . ( IC ( SCM R))) = (( Exec (( SubFrom (a,b)),s)) . NAT ) by Def1

      .= (( IC s) + 1) by A3, A5, SCMRING1: 7;

      

      thus (( Exec (( SubFrom (a,b)),s)) . a) = (S1 . a) by A1, A5, AMI_3: 27, SCMRING1: 8

      .= ((s . a) - (s . b)) by A7, A8, SCMRING1: 11;

      let c;

      assume

       A9: c <> a;

      

       A10: c is Element of ( Data-Locations SCM ) by Th1;

      

      hence (( Exec (( SubFrom (a,b)),s)) . c) = (S1 . c) by A5, AMI_3: 27, SCMRING1: 8

      .= (s . c) by A7, A9, A10, AMI_3: 27, SCMRING1: 12;

    end;

    theorem :: SCMRING2:14

    

     Th14: (( Exec (( MultBy (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) & (( Exec (( MultBy (a,b)),s)) . a) = ((s . a) * (s . b)) & for c st c <> a holds (( Exec (( MultBy (a,b)),s)) . c) = (s . c)

    proof

      

       A1: a is Element of ( Data-Locations SCM ) by Th1;

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A2, CARD_3: 107;

      reconsider I = ( MultBy (a,b)) as Element of ( SCM-Instr R) by Def1;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) * (S . (I address_2 )))));

      reconsider i = 4 as Element of ( Segm 8) by NAT_1: 44;

      

       A3: ( IC s) = ( IC S) by Def1;

      

       A4: b is Element of ( Data-Locations SCM ) by Th1;

      

       A5: ( Exec (( MultBy (a,b)),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, A4, AMI_3: 27, SCMRING1:def 14;

      

       A6: I = [i, {} , <*a, b*>];

      then

       A7: (I address_1 ) = a by A1, A4, AMI_3: 27, SCMRINGI: 1;

      

       A8: (I address_2 ) = b by A6, A1, A4, AMI_3: 27, SCMRINGI: 1;

      

      thus (( Exec (( MultBy (a,b)),s)) . ( IC ( SCM R))) = (( Exec (( MultBy (a,b)),s)) . NAT ) by Def1

      .= (( IC s) + 1) by A3, A5, SCMRING1: 7;

      

      thus (( Exec (( MultBy (a,b)),s)) . a) = (S1 . a) by A1, A5, AMI_3: 27, SCMRING1: 8

      .= ((s . a) * (s . b)) by A7, A8, SCMRING1: 11;

      let c;

      assume

       A9: c <> a;

      

       A10: c is Element of ( Data-Locations SCM ) by Th1;

      

      hence (( Exec (( MultBy (a,b)),s)) . c) = (S1 . c) by A5, AMI_3: 27, SCMRING1: 8

      .= (s . c) by A7, A9, A10, AMI_3: 27, SCMRING1: 12;

    end;

    theorem :: SCMRING2:15

    (( Exec (( goto (i1,R)),s)) . ( IC ( SCM R))) = i1 & (( Exec (( goto (i1,R)),s)) . c) = (s . c)

    proof

      

       A1: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A1, CARD_3: 107;

      reconsider i = 6 as Element of ( Segm 8) by NAT_1: 44;

      reconsider I = ( goto (i1,R)) as Element of ( SCM-Instr R) by Def1;

      I = [i, <*i1*>, {} ];

      then

       A2: (I jump_address ) = i1 by SCMRINGI: 2;

      

       A3: i1 in NAT by ORDINAL1:def 12;

      

       A4: ( Exec (( goto (i1,R)),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S,(I jump_address ))) by SCMRING1:def 14, A3;

      

      thus (( Exec (( goto (i1,R)),s)) . ( IC ( SCM R))) = (( Exec (( goto (i1,R)),s)) . NAT ) by Def1

      .= i1 by A4, A2, SCMRING1: 7;

      c is Element of ( Data-Locations SCM ) by Th1;

      hence thesis by A4, AMI_3: 27, SCMRING1: 8;

    end;

    theorem :: SCMRING2:16

    

     Th16: ((s . a) = ( 0. R) implies (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = i1) & ((s . a) <> ( 0. R) implies (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = (( IC s) + 1)) & (( Exec ((a =0_goto i1),s)) . c) = (s . c)

    proof

      

       A1: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A1, CARD_3: 107;

      reconsider I = (a =0_goto i1) as Element of ( SCM-Instr R) by Def1;

      reconsider i = 7 as Element of ( Segm 8) by NAT_1: 44;

      

       A2: a is Element of ( Data-Locations SCM ) & i1 is Element of NAT by Th1, ORDINAL1:def 12;

      

       A3: ( Exec ((a =0_goto i1),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S,( IFEQ ((S . (I cond_address )),( 0. R),(I cjump_address ),(( IC S) + 1))))) by A2, AMI_3: 27, SCMRING1:def 14;

      

       A4: I = [i, <*i1*>, <*a*>];

      thus (s . a) = ( 0. R) implies (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = i1

      proof

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

        then

         A5: (S . (I cond_address )) = ( 0. R) by A4, A2, AMI_3: 27, SCMRINGI: 3;

        

        thus (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = (( Exec ((a =0_goto i1),s)) . NAT ) by Def1

        .= ( IFEQ ((S . (I cond_address )),( 0. R),(I cjump_address ),(( IC S) + 1))) by A3, SCMRING1: 7

        .= (I cjump_address ) by A5, FUNCOP_1:def 8

        .= i1 by A4, A2, AMI_3: 27, SCMRINGI: 3;

      end;

      

       A6: ( IC s) = ( IC S) by Def1;

      thus (s . a) <> ( 0. R) implies (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = (( IC s) + 1)

      proof

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

        then

         A7: (S . (I cond_address )) <> ( 0. R) by A4, A2, AMI_3: 27, SCMRINGI: 3;

        

        thus (( Exec ((a =0_goto i1),s)) . ( IC ( SCM R))) = (( Exec ((a =0_goto i1),s)) . NAT ) by Def1

        .= ( IFEQ ((S . (I cond_address )),( 0. R),(I cjump_address ),(( IC S) + 1))) by A3, SCMRING1: 7

        .= (( IC s) + 1) by A6, A7, FUNCOP_1:def 8;

      end;

      c is Element of ( Data-Locations SCM ) by Th1;

      hence thesis by A3, AMI_3: 27, SCMRING1: 8;

    end;

    theorem :: SCMRING2:17

    

     Th17: (( Exec ((a := r),s)) . ( IC ( SCM R))) = (( IC s) + 1) & (( Exec ((a := r),s)) . a) = r & for c st c <> a holds (( Exec ((a := r),s)) . c) = (s . c)

    proof

      

       A1: a is Element of ( Data-Locations SCM ) by Th1;

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider S = s as SCM-State of R by A2, CARD_3: 107;

      reconsider I = (a := r) as Element of ( SCM-Instr R) by Def1;

      set S1 = ( SCM-Chg (S,(I const_address ),(I const_value )));

      reconsider i = 5 as Element of ( Segm 8) by NAT_1: 44;

      

       A3: ( IC s) = ( IC S) by Def1;

      

       A4: I = [i, {} , <*a, r*>];

      then

       A5: (I const_address ) = a by A1, AMI_3: 27, SCMRINGI: 4;

      

       A6: (I const_value ) = r by A4, A1, AMI_3: 27, SCMRINGI: 4;

      

       A7: ( Exec ((a := r),s)) = ( SCM-Exec-Res (I,S)) by Th10

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, AMI_3: 27, SCMRING1:def 14;

      

      thus (( Exec ((a := r),s)) . ( IC ( SCM R))) = (( Exec ((a := r),s)) . NAT ) by Def1

      .= (( IC s) + 1) by A3, A7, SCMRING1: 7;

      

      thus (( Exec ((a := r),s)) . a) = (S1 . a) by A1, A7, AMI_3: 27, SCMRING1: 8

      .= r by A5, A6, SCMRING1: 11;

      let c;

      assume

       A8: c <> a;

      

       A9: c is Element of ( Data-Locations SCM ) by Th1;

      

      hence (( Exec ((a := r),s)) . c) = (S1 . c) by A7, AMI_3: 27, SCMRING1: 8

      .= (s . c) by A5, A8, A9, AMI_3: 27, SCMRING1: 12;

    end;

    begin

    theorem :: SCMRING2:18

    

     Th18: for I be Instruction of ( SCM R) st ex s st (( Exec (I,s)) . ( IC ( SCM R))) = (( IC s) + 1) holds I is non halting

    proof

      let I be Instruction of ( SCM R);

      given s such that

       A1: (( Exec (I,s)) . ( IC ( SCM R))) = (( IC s) + 1);

      

       A2: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider t = s as SCM-State of R by A2, CARD_3: 107;

      ( IC t) = (t . NAT );

      then

      reconsider w = (t . NAT ) as Element of NAT ;

      

       A3: (( Exec (I,s)) . ( IC ( SCM R))) = (w + 1) by A1, Def1;

      assume

       A4: I is halting;

      ( IC t) = ( IC s) by Def1;

      then (( Exec (I,s)) . ( IC ( SCM R))) = (t . NAT ) by A4;

      hence contradiction by A3;

    end;

    theorem :: SCMRING2:19

    

     Th19: for I be Instruction of ( SCM R) st I = [ 0 , {} , {} ] holds I is halting

    proof

      let I be Instruction of ( SCM R) such that

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

      

       A2: (I `3_3 ) = {} by A1;

      then

       A3: ( not (ex mk,ml be Element of ( Data-Locations SCM ) st I = [1, {} , <*mk, ml*>])) & not (ex mk,ml be Element of ( Data-Locations SCM ) st I = [2, {} , <*mk, ml*>]);

      

       A4: not (ex mk be Element of ( Data-Locations SCM ), r be Element of R st I = [5, {} , <*mk, r*>]) by A2;

      (I `2_3 ) = {} by A1;

      then

       A5: ( not (ex mk be Element of NAT st I = [6, <*mk*>, {} ])) & not (ex mk be Element of NAT , ml be Element of ( Data-Locations SCM ) st I = [7, <*mk*>, <*ml*>]);

      reconsider L = I as Element of ( SCM-Instr R) by A1, SCMRINGI: 6;

      let s be State of ( SCM R);

      

       A6: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider t = s as SCM-State of R by A6, CARD_3: 107;

      

       A7: ( not (ex mk,ml be Element of ( Data-Locations SCM ) st I = [3, {} , <*mk, ml*>])) & not (ex mk,ml be Element of ( Data-Locations SCM ) st I = [4, {} , <*mk, ml*>]) by A2;

      

      thus ( Exec (I,s)) = ( SCM-Exec-Res (L,t)) by Th10

      .= s by A3, A7, A5, A4, AMI_3: 27, SCMRING1:def 14;

    end;

    

     Lm3: (a := b) is non halting

    proof

      set s = the State of ( SCM R);

      (( Exec ((a := b),s)) . ( IC ( SCM R))) = (( IC s) + 1) by Th11;

      hence thesis by Th18;

    end;

    

     Lm4: ( AddTo (a,b)) is non halting

    proof

      set s = the State of ( SCM R);

      (( Exec (( AddTo (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) by Th12;

      hence thesis by Th18;

    end;

    

     Lm5: ( SubFrom (a,b)) is non halting

    proof

      set s = the State of ( SCM R);

      (( Exec (( SubFrom (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) by Th13;

      hence thesis by Th18;

    end;

    

     Lm6: ( MultBy (a,b)) is non halting

    proof

      set s = the State of ( SCM R);

      (( Exec (( MultBy (a,b)),s)) . ( IC ( SCM R))) = (( IC s) + 1) by Th14;

      hence thesis by Th18;

    end;

    

     Lm7: ( goto (i1,R)) is non halting

    proof

      reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;

      set s = the SCM-State of R;

      set t = (s +* ( NAT .--> (i1 + 1)));

      set f = ( the_Values_of ( SCM R));

      

       A1: { NAT } c= SCM-Memory by AMI_2: 22, ZFMISC_1: 31;

      

       A2: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (i1 + 1)))) by FUNCT_4:def 1

      .= ( SCM-Memory \/ ( dom ( NAT .--> (i1 + 1)))) by SCMRING1: 19

      .= ( SCM-Memory \/ { NAT })

      .= SCM-Memory by A1, XBOOLE_1: 12;

      

       A3: f = (( SCM-VAL R) * SCM-OK ) by Lm1;

       NAT in ( dom ( NAT .--> (i1 + 1))) by TARSKI:def 1;

      

      then

       A5: (t . NAT ) = (( NAT .--> (i1 + 1)) . NAT ) by FUNCT_4: 13

      .= (i5 + 1) by FUNCOP_1: 72;

      

       A6: ( dom t) = the carrier of ( SCM R) by A2, Def1

      .= ( dom f) by PARTFUN1:def 2;

      

       A7: for x be object st x in ( dom t) holds (t . x) in (f . x)

      proof

        let x be object such that

         A8: x in ( dom t);

        per cases ;

          suppose

           A9: x = NAT ;

          then (f . x) = NAT by A3, SCMRING1: 2;

          hence thesis by A5, A9, ORDINAL1:def 12;

        end;

          suppose x <> NAT ;

          then not x in ( dom ( NAT .--> (i1 + 1))) by TARSKI:def 1;

          then (t . x) = (s . x) by FUNCT_4: 11;

          hence thesis by A3, A8, A6, CARD_3: 9;

        end;

      end;

      

       A10: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      ( dom t) = the carrier of ( SCM R) by A2, Def1;

      then

      reconsider t as PartState of ( SCM R) by A7, FUNCT_1:def 14, RELAT_1:def 18;

      ( dom t) = the carrier of ( SCM R) by A2, Def1;

      then

      reconsider t as State of ( SCM R) by PARTFUN1:def 2;

      reconsider w = t as SCM-State of R by A10, CARD_3: 107;

      

       A11: i1 in NAT by ORDINAL1:def 12;

       NAT in ( dom ( NAT .--> i1)) by TARSKI:def 1;

      

      then

       A12: ((w +* ( NAT .--> i1)) . NAT ) = (( NAT .--> i1) . NAT ) by FUNCT_4: 13

      .= i1 by FUNCOP_1: 72;

      reconsider V = ( goto (i1,R)) as Element of ( SCM-Instr R) by Def1;

      assume

       A13: ( goto (i1,R)) is halting;

      

       A14: 6 is Element of ( Segm 8) by NAT_1: 44;

      (w +* ( NAT .--> i1)) = ( SCM-Chg (w,i5))

      .= ( SCM-Chg (w,(V jump_address ))) by A14, SCMRINGI: 2

      .= ( SCM-Exec-Res (V,w)) by SCMRING1:def 14, A11

      .= ( Exec (( goto (i1,R)),t)) by Th10

      .= t by A13;

      hence contradiction by A5, A12;

    end;

    

     Lm8: (a =0_goto i1) is non halting

    proof

      reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;

      set s = the SCM-State of R;

      set t = (s +* ( NAT .--> (i1 + 1)));

      set f = ( the_Values_of ( SCM R));

      reconsider V = (a =0_goto i1) as Element of ( SCM-Instr R) by Def1;

      

       A1: { NAT } c= SCM-Memory by AMI_2: 22, ZFMISC_1: 31;

      

       A2: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (i1 + 1)))) by FUNCT_4:def 1

      .= ( SCM-Memory \/ ( dom ( NAT .--> (i1 + 1)))) by SCMRING1: 19

      .= ( SCM-Memory \/ { NAT })

      .= SCM-Memory by A1, XBOOLE_1: 12;

      

       A3: f = (( SCM-VAL R) * SCM-OK ) by Lm1;

       NAT in ( dom ( NAT .--> (i1 + 1))) by TARSKI:def 1;

      

      then

       A5: (t . NAT ) = (( NAT .--> (i1 + 1)) . NAT ) by FUNCT_4: 13

      .= (i5 + 1) by FUNCOP_1: 72;

      

       A6: ( dom t) = the carrier of ( SCM R) by A2, Def1

      .= ( dom f) by PARTFUN1:def 2;

      

       A7: for x be object st x in ( dom t) holds (t . x) in (f . x)

      proof

        let x be object such that

         A8: x in ( dom t);

        per cases ;

          suppose

           A9: x = NAT ;

          then (f . x) = NAT by A3, SCMRING1: 2;

          hence thesis by A5, A9, ORDINAL1:def 12;

        end;

          suppose x <> NAT ;

          then not x in ( dom ( NAT .--> (i1 + 1))) by TARSKI:def 1;

          then (t . x) = (s . x) by FUNCT_4: 11;

          hence thesis by A3, A8, A6, CARD_3: 9;

        end;

      end;

      ( dom t) = the carrier of ( SCM R) by A2, Def1;

      then

      reconsider t as PartState of ( SCM R) by A7, FUNCT_1:def 14, RELAT_1:def 18;

      ( dom t) = the carrier of ( SCM R) by A2, Def1;

      then

      reconsider t as State of ( SCM R) by PARTFUN1:def 2;

      

       A10: ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

      reconsider w = t as SCM-State of R by A10, CARD_3: 107;

       NAT in ( dom ( NAT .--> i1)) by TARSKI:def 1;

      

      then

       A11: ((w +* ( NAT .--> i1)) . NAT ) = (( NAT .--> i1) . NAT ) by FUNCT_4: 13

      .= i1 by FUNCOP_1: 72;

      

       A12: 7 is Element of ( Segm 8) by NAT_1: 44;

      

       A13: a is Element of ( Data-Locations SCM ) by Th1;

      assume

       A14: (a =0_goto i1) is halting;

      

       A15: i1 in NAT by ORDINAL1:def 12;

      per cases ;

        suppose

         A16: (w . (V cond_address )) <> ( 0. R);

        ( IC w) = (w . NAT );

        then

        reconsider e = (w . NAT ) as Element of NAT ;

        

         A17: ( IC t) = ( IC w) by Def1;

        then

         A18: (( Exec ((a =0_goto i1),t)) . ( IC ( SCM R))) = (w . NAT ) by A14;

        a is Element of ( Data-Locations SCM ) by Th1;

        then (t . a) <> ( 0. R) by A12, A16, AMI_3: 27, SCMRINGI: 3, A15;

        then (( Exec ((a =0_goto i1),t)) . ( IC ( SCM R))) = (e + 1) by A17, Th16;

        hence contradiction by A18;

      end;

        suppose

         A19: (w . (V cond_address )) = ( 0. R);

        (w +* ( NAT .--> i1)) = ( SCM-Chg (w,i5))

        .= ( SCM-Chg (w,(V cjump_address ))) by A12, A13, AMI_3: 27, SCMRINGI: 3

        .= ( SCM-Chg (w,( IFEQ ((w . (V cond_address )),( 0. R),(V cjump_address ),(( IC w) + 1))))) by A19, FUNCOP_1:def 8

        .= ( SCM-Exec-Res (V,w)) by A13, AMI_3: 27, SCMRING1:def 14, A15

        .= ( Exec ((a =0_goto i1),t)) by Th10

        .= t by A14;

        hence contradiction by A5, A11;

      end;

    end;

    

     Lm9: (a := r) is non halting

    proof

      set s = the State of ( SCM R);

      (( Exec ((a := r),s)) . ( IC ( SCM R))) = (( IC s) + 1) by Th17;

      hence thesis by Th18;

    end;

    registration

      let R, a, b;

      cluster (a := b) -> non halting;

      coherence by Lm3;

      cluster ( AddTo (a,b)) -> non halting;

      coherence by Lm4;

      cluster ( SubFrom (a,b)) -> non halting;

      coherence by Lm5;

      cluster ( MultBy (a,b)) -> non halting;

      coherence by Lm6;

    end

    registration

      let R, i1;

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

      coherence by Lm7;

    end

    registration

      let R, a, i1;

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

      coherence by Lm8;

    end

    registration

      let R, a, r;

      cluster (a := r) -> non halting;

      coherence by Lm9;

    end

    

     Lm10: for W be Instruction of ( SCM R) st W is halting holds W = [ 0 , {} , {} ]

    proof

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

      let W be Instruction of ( SCM R) such that

       A1: W is halting;

      assume

       A2: I <> W;

      per cases by Th7;

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

        hence thesis by A2;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

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

        hence thesis by A1;

      end;

    end;

    registration

      let R;

      cluster ( SCM R) -> halting;

      coherence by Th19;

    end

    theorem :: SCMRING2:20

    for I be Instruction of ( SCM R) st I is halting holds I = ( halt ( SCM R)) by Lm10;

    theorem :: SCMRING2:21

    ( halt ( SCM R)) = [ 0 , {} , {} ];

    theorem :: SCMRING2:22

    

     Th22: ( Data-Locations ( SCM R)) = ( Data-Locations SCM )

    proof

      ( Data-Locations SCM ) misses { NAT } by AMI_2: 20, AMI_3: 27, ZFMISC_1: 50;

      then

       A1: ( Data-Locations SCM ) misses { NAT };

      

      thus ( Data-Locations ( SCM R)) = ( SCM-Memory \ {( IC ( SCM R))}) by Def1

      .= ( SCM-Memory \ { NAT }) by Def1

      .= ((( Data-Locations SCM ) \/ { NAT }) \ { NAT }) by AMI_3: 27

      .= (( Data-Locations SCM ) \ { NAT }) by XBOOLE_1: 40

      .= ( Data-Locations SCM ) by A1, XBOOLE_1: 83;

    end;

    theorem :: SCMRING2:23

    x is Data-Location of R iff x in ( Data-Locations ( SCM R))

    proof

      ( Data-Locations ( SCM R)) = ( Data-Locations SCM ) by Th22;

      hence thesis by Th1;

    end;

    theorem :: SCMRING2:24

    for R be Ring holds ( the_Values_of ( SCM R)) = (( SCM-VAL R) * SCM-OK ) by Lm1;

    theorem :: SCMRING2:25

    for R be Ring holds (the carrier of ( SCM R) \ { NAT }) = SCM-Data-Loc by Lm2;