scmringi.miz



    begin

    reserve i,j,k for Nat,

I for Element of ( Segm 8),

i1,i2 for Nat,

d1,d2,d3,d4 for Element of SCM-Data-Loc ,

S for non empty 1-sorted;

    registration

      cluster SCM-Instr -> non trivial;

      coherence

      proof

        set e = the Element of SCM-Data-Loc ;

        1 in {1, 2, 3, 4, 5} & 1 is Element of ( Segm 9) by ENUMSET1:def 3, NAT_1: 44;

        then [1, {} , <*e, e*>] in { [K, {} , <*b, c*>] where K be Element of ( Segm 9), b,c be Element of SCM-Data-Loc : K in {1, 2, 3, 4, 5} };

        then

         A1: [1, {} , <*e, e*>] in SCM-Instr by XBOOLE_0:def 3;

        2 in {1, 2, 3, 4, 5} & 2 is Element of ( Segm 9) by ENUMSET1:def 3, NAT_1: 44;

        then [2, {} , <*e, e*>] in { [K, {} , <*b, c*>] where K be Element of ( Segm 9), b,c be Element of SCM-Data-Loc : K in {1, 2, 3, 4, 5} };

        then

         A2: [2, {} , <*e, e*>] in SCM-Instr by XBOOLE_0:def 3;

         [1, {} , <*e, e*>] <> [2, {} , <*e, e*>] by XTUPLE_0: 3;

        hence thesis by A1, A2, SUBSET_1:def 7;

      end;

    end

    definition

      let S be non empty 1-sorted;

      :: SCMRINGI:def1

      func SCM-Instr S -> non empty set equals (((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) \/ the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S);

      coherence ;

    end

    registration

      let S be non empty 1-sorted;

      cluster ( SCM-Instr S) -> non trivial;

      coherence

      proof

        set e1 = the Element of SCM-Data-Loc ;

        

         A1: ( SCM-Instr S) = ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*d1, d2*>] : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i1*>, {} ]) \/ ( the set of all [7, <*i2*>, <*d3*>] \/ the set of all [5, {} , <*d4, r*>] where r be Element of S)) by XBOOLE_1: 4

        .= (( { [ 0 , {} , {} ]} \/ { [I, {} , <*d1, d2*>] : I in {1, 2, 3, 4} }) \/ ( the set of all [6, <*i1*>, {} ] \/ ( the set of all [7, <*i2*>, <*d3*>] \/ the set of all [5, {} , <*d4, r*>] where r be Element of S))) by XBOOLE_1: 4

        .= ({ [I, {} , <*d1, d2*>] : I in {1, 2, 3, 4} } \/ ( { [ 0 , {} , {} ]} \/ ( the set of all [6, <*i1*>, {} ] \/ ( the set of all [7, <*i2*>, <*d3*>] \/ the set of all [5, {} , <*d4, r*>] where r be Element of S)))) by XBOOLE_1: 4;

        2 in ( Segm 8) & 2 in {1, 2, 3, 4} by ENUMSET1:def 2, NAT_1: 44;

        then [2, {} , <*e1, e1*>] in { [I, {} , <*d1, d2*>] where I be Element of ( Segm 8), d1,d2 be Element of SCM-Data-Loc : I in {1, 2, 3, 4} };

        then

         A2: [2, {} , <*e1, e1*>] in ( SCM-Instr S) by A1, XBOOLE_0:def 3;

        

         A3: [1, {} , <*e1, e1*>] <> [2, {} , <*e1, e1*>] by XTUPLE_0: 3;

        1 in ( Segm 8) & 1 in {1, 2, 3, 4} by ENUMSET1:def 2, NAT_1: 44;

        then [1, {} , <*e1, e1*>] in { [I, {} , <*d1, d2*>] where d1,d2 be Element of SCM-Data-Loc : I in {1, 2, 3, 4} };

        then [1, {} , <*e1, e1*>] in ( SCM-Instr S) by A1, XBOOLE_0:def 3;

        hence thesis by A2, A3, SUBSET_1:def 7;

      end;

    end

    reserve G for non empty 1-sorted;

    definition

      let S be non empty 1-sorted, x be Element of ( SCM-Instr S);

      given mk,ml be Element of SCM-Data-Loc , I such that

       A1: x = [I, {} , <*mk, ml*>];

      :: SCMRINGI:def2

      func x address_1 -> Element of SCM-Data-Loc means

      : Def2: ex f be FinSequence of SCM-Data-Loc st f = (x `3_3 ) & it = (f /. 1);

      existence

      proof

        take mk, <*mk, ml*>;

        thus thesis by A1, FINSEQ_4: 17;

      end;

      uniqueness ;

      :: SCMRINGI:def3

      func x address_2 -> Element of SCM-Data-Loc means

      : Def3: ex f be FinSequence of SCM-Data-Loc st f = (x `3_3 ) & it = (f /. 2);

      existence

      proof

        take ml, <*mk, ml*>;

        thus thesis by A1, FINSEQ_4: 17;

      end;

      uniqueness ;

    end

    theorem :: SCMRINGI:1

    for x be Element of ( SCM-Instr S), mk,ml be Element of SCM-Data-Loc st x = [I, {} , <*mk, ml*>] holds (x address_1 ) = mk & (x address_2 ) = ml

    proof

      let x be Element of ( SCM-Instr S), mk,ml be Element of SCM-Data-Loc ;

      assume

       A1: x = [I, {} , <*mk, ml*>];

      then

      consider f be FinSequence of SCM-Data-Loc such that

       A2: f = (x `3_3 ) and

       A3: (x address_1 ) = (f /. 1) by Def2;

      f = <*mk, ml*> by A1, A2;

      hence (x address_1 ) = mk by A3, FINSEQ_4: 17;

      consider f be FinSequence of SCM-Data-Loc such that

       A4: f = (x `3_3 ) and

       A5: (x address_2 ) = (f /. 2) by A1, Def3;

      f = <*mk, ml*> by A1, A4;

      hence thesis by A5, FINSEQ_4: 17;

    end;

    definition

      let R be non empty 1-sorted, x be Element of ( SCM-Instr R);

      given mk be Element of NAT , I such that

       A1: x = [I, <*mk*>, {} ];

      :: SCMRINGI:def4

      func x jump_address -> Element of NAT means

      : Def4: ex f be FinSequence of NAT st f = (x `2_3 ) & it = (f /. 1);

      existence

      proof

        take mk, <*mk*>;

        thus thesis by A1, FINSEQ_4: 16;

      end;

      uniqueness ;

    end

    theorem :: SCMRINGI:2

    for x be Element of ( SCM-Instr S), mk be Nat st x = [I, <*mk*>, {} ] holds (x jump_address ) = mk

    proof

      let x be Element of ( SCM-Instr S), mk be Nat;

      assume

       A1: x = [I, <*mk*>, {} ];

      reconsider mk as Element of NAT by ORDINAL1:def 12;

      x = [I, <*mk*>, {} ] by A1;

      then

      consider f be FinSequence of NAT such that

       A2: f = (x `2_3 ) and

       A3: (x jump_address ) = (f /. 1) by Def4;

      f = <*mk*> by A1, A2;

      hence thesis by A3, FINSEQ_4: 16;

    end;

    definition

      let S be non empty 1-sorted, x be Element of ( SCM-Instr S);

      given mk be Element of NAT , ml be Element of SCM-Data-Loc , I such that

       A1: x = [I, <*mk*>, <*ml*>];

      :: SCMRINGI:def5

      func x cjump_address -> Element of NAT means

      : Def5: ex mk be Element of NAT st <*mk*> = (x `2_3 ) & it = ( <*mk*> /. 1);

      existence

      proof

        take mk, mk;

        thus thesis by A1, FINSEQ_4: 16;

      end;

      uniqueness ;

      :: SCMRINGI:def6

      func x cond_address -> Element of SCM-Data-Loc means

      : Def6: ex ml be Element of SCM-Data-Loc st <*ml*> = (x `3_3 ) & it = ( <*ml*> /. 1);

      existence

      proof

        take ml, ml;

        thus thesis by A1, FINSEQ_4: 16;

      end;

      uniqueness ;

    end

    theorem :: SCMRINGI:3

    for x be Element of ( SCM-Instr S), mk be Element of NAT , ml be Element of SCM-Data-Loc st x = [I, <*mk*>, <*ml*>] holds (x cjump_address ) = mk & (x cond_address ) = ml

    proof

      let x be Element of ( SCM-Instr S), mk be Element of NAT , ml be Element of SCM-Data-Loc ;

      assume

       A1: x = [I, <*mk*>, <*ml*>];

      then

      consider mk9 be Element of NAT such that

       A2: <*mk9*> = (x `2_3 ) and

       A3: (x cjump_address ) = ( <*mk9*> /. 1) by Def5;

       <*mk9*> = <*mk*> by A1, A2;

      hence (x cjump_address ) = mk by A3, FINSEQ_4: 16;

      consider ml9 be Element of SCM-Data-Loc such that

       A4: <*ml9*> = (x `3_3 ) and

       A5: (x cond_address ) = ( <*ml9*> /. 1) by A1, Def6;

       <*ml9*> = <*ml*> by A1, A4;

      hence thesis by A5, FINSEQ_4: 16;

    end;

    definition

      let S be non empty 1-sorted, d be Element of SCM-Data-Loc , s be Element of S;

      :: original: <*

      redefine

      func <*d,s*> -> FinSequence of ( SCM-Data-Loc \/ the carrier of S) ;

      coherence

      proof

        let y be object;

        

         A1: ( dom <*d, s*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        assume y in ( rng <*d, s*>);

        then

        consider x be object such that

         A2: x in ( dom <*d, s*>) and

         A3: ( <*d, s*> . x) = y by FUNCT_1:def 3;

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

          suppose x = 1;

          then y = d by A3, FINSEQ_1: 44;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x = 2;

          then y = s by A3, FINSEQ_1: 44;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

    end

    definition

      let S be non empty 1-sorted, x be Element of ( SCM-Instr S);

      given mk be Element of SCM-Data-Loc , r be Element of S, I such that

       A1: x = [I, {} , <*mk, r*>];

      :: SCMRINGI:def7

      func x const_address -> Element of SCM-Data-Loc means

      : Def7: ex f be FinSequence of ( SCM-Data-Loc \/ the carrier of S) st f = (x `3_3 ) & it = (f /. 1);

      existence

      proof

        take mk, <*mk, r*>;

        mk is Element of ( SCM-Data-Loc \/ the carrier of S) & r is Element of ( SCM-Data-Loc \/ the carrier of S) by XBOOLE_0:def 3;

        hence thesis by A1, FINSEQ_4: 17;

      end;

      uniqueness ;

      :: SCMRINGI:def8

      func x const_value -> Element of S means

      : Def8: ex f be FinSequence of ( SCM-Data-Loc \/ the carrier of S) st f = (x `3_3 ) & it = (f /. 2);

      existence

      proof

        take r, <*mk, r*>;

        mk is Element of ( SCM-Data-Loc \/ the carrier of S) & r is Element of ( SCM-Data-Loc \/ the carrier of S) by XBOOLE_0:def 3;

        hence thesis by A1, FINSEQ_4: 17;

      end;

      uniqueness ;

    end

    theorem :: SCMRINGI:4

    for x be Element of ( SCM-Instr S), mk be Element of SCM-Data-Loc , r be Element of S st x = [I, {} , <*mk, r*>] holds (x const_address ) = mk & (x const_value ) = r

    proof

      let x be Element of ( SCM-Instr S), mk be Element of SCM-Data-Loc , r be Element of S;

      

       A1: mk is Element of ( SCM-Data-Loc \/ the carrier of S) & r is Element of ( SCM-Data-Loc \/ the carrier of S) by XBOOLE_0:def 3;

      assume

       A2: x = [I, {} , <*mk, r*>];

      then

      consider f be FinSequence of ( SCM-Data-Loc \/ the carrier of S) such that

       A3: f = (x `3_3 ) and

       A4: (x const_address ) = (f /. 1) by Def7;

      f = <*mk, r*> by A2, A3;

      hence (x const_address ) = mk by A4, A1, FINSEQ_4: 17;

      consider f be FinSequence of ( SCM-Data-Loc \/ the carrier of S) such that

       A5: f = (x `3_3 ) and

       A6: (x const_value ) = (f /. 2) by A2, Def8;

      f = <*mk, r*> by A2, A5;

      hence thesis by A1, A6, FINSEQ_4: 17;

    end;

    theorem :: SCMRINGI:5

    

     Th5: for S be non empty 1-sorted holds ( SCM-Instr S) c= [: NAT , ( NAT * ), ( proj2 ( SCM-Instr S)):]

    proof

      let S be non empty 1-sorted;

      set X = ( proj2 ( SCM-Instr S));

      let u be object;

      assume

       A1: u in ( SCM-Instr S);

      

       A2: {} in ( NAT * ) by FINSEQ_1: 49;

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A3: u in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc );

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: u in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat);

          per cases by A4, XBOOLE_0:def 3;

            suppose

             A5: u in ( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} });

            per cases by A5, XBOOLE_0:def 3;

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

              then

               A6: u = [ 0 , {} , {} ] by TARSKI:def 1;

              then 0 in NAT & {} in ( proj2 ( SCM-Instr S)) by A1, XTUPLE_0:def 13;

              hence u in [: NAT , ( NAT * ), X:] by A6, A2, MCART_1: 69;

            end;

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

              then

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

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

              I in NAT & <*a, b*> in ( proj2 ( SCM-Instr S)) by A7, A1, XTUPLE_0:def 13;

              hence u in [: NAT , ( NAT * ), X:] by A7, A2, MCART_1: 69;

            end;

          end;

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

            then

            consider i be Nat such that

             A8: u = [6, <*i*>, {} ];

            i in NAT by ORDINAL1:def 12;

            then

             A9: <*i*> in ( NAT * ) by FUNCT_7: 18;

            6 in NAT & {} in ( proj2 ( SCM-Instr S)) by A8, A1, XTUPLE_0:def 13;

            hence u in [: NAT , ( NAT * ), X:] by A8, A9, MCART_1: 69;

          end;

        end;

          suppose u in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc ;

          then

          consider i be Nat, a be Element of SCM-Data-Loc such that

           A10: u = [7, <*i*>, <*a*>];

          i in NAT by ORDINAL1:def 12;

          then

           A11: <*i*> in ( NAT * ) by FUNCT_7: 18;

          7 in NAT & <*a*> in ( proj2 ( SCM-Instr S)) by A10, A1, XTUPLE_0:def 13;

          hence u in [: NAT , ( NAT * ), X:] by A10, A11, MCART_1: 69;

        end;

      end;

        suppose u in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S;

        then

        consider a be Element of SCM-Data-Loc , r be Element of S such that

         A12: u = [5, {} , <*a, r*>];

        5 in NAT & <*a, r*> in ( proj2 ( SCM-Instr S)) by A12, A1, XTUPLE_0:def 13;

        hence u in [: NAT , ( NAT * ), X:] by A12, A2, MCART_1: 69;

      end;

    end;

    registration

      let S be non empty 1-sorted;

      cluster ( proj2 ( SCM-Instr S)) -> FinSequence-membered;

      coherence

      proof

        let f be object;

        assume f in ( proj2 ( SCM-Instr S));

        then

        consider y be object such that

         A1: [y, f] in ( SCM-Instr S) by XTUPLE_0:def 13;

        set u = [y, f];

        per cases by A1, XBOOLE_0:def 3;

          suppose

           A2: u in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc );

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A3: u in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat);

            per cases by A3, XBOOLE_0:def 3;

              suppose

               A4: u in ( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} });

              per cases by A4, XBOOLE_0:def 3;

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

                then u = [ 0 , {} , {} ] by TARSKI:def 1;

                then f = {} by XTUPLE_0: 1;

                hence f is FinSequence;

              end;

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

                then

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

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

                f = <*a, b*> by A5, XTUPLE_0: 1;

                hence f is FinSequence;

              end;

            end;

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

              then

              consider i be Nat such that

               A6: u = [6, <*i*>, {} ];

              f = {} by A6, XTUPLE_0: 1;

              hence f is FinSequence;

            end;

          end;

            suppose u in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc ;

            then

            consider i be Nat, a be Element of SCM-Data-Loc such that

             A7: u = [7, <*i*>, <*a*>];

            f = <*a*> by A7, XTUPLE_0: 1;

            hence f is FinSequence;

          end;

        end;

          suppose u in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S;

          then

          consider a be Element of SCM-Data-Loc , r be Element of S such that

           A8: u = [5, {} , <*a, r*>];

          f = <*a, r*> by A8, XTUPLE_0: 1;

          hence f is FinSequence;

        end;

      end;

    end

    theorem :: SCMRINGI:6

    

     Th6: [ 0 , {} , {} ] in ( SCM-Instr S)

    proof

       [ 0 , {} , {} ] in { [ 0 , {} , {} ]} by TARSKI:def 1;

      then [ 0 , {} , {} ] in ( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) by XBOOLE_0:def 3;

      then [ 0 , {} , {} ] in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) by XBOOLE_0:def 3;

      then [ 0 , {} , {} ] in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: SCMRINGI:7

    

     Th7: for S be non empty 1-sorted holds for x be Element of ( SCM-Instr S) holds x in { [ 0 , {} , {} ]} & ( InsCode x) = 0 or x in { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} } & (( InsCode x) = 1 or ( InsCode x) = 2 or ( InsCode x) = 3 or ( InsCode x) = 4) or x in the set of all [6, <*i*>, {} ] where i be Nat & ( InsCode x) = 6 or x in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc & ( InsCode x) = 7 or x in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S & ( InsCode x) = 5

    proof

      let S be non empty 1-sorted;

      let x be Element of ( SCM-Instr S);

      x in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) or x in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S by XBOOLE_0:def 3;

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

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

      per cases by XBOOLE_0:def 3;

        case x in { [ 0 , {} , {} ]};

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

        hence thesis;

      end;

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

        then

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

         A1: x = [I, {} , <*a, b*>] and

         A2: I in {1, 2, 3, 4};

        ( InsCode x) = I by A1;

        hence thesis by A2, ENUMSET1:def 2;

      end;

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

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

        hence thesis;

      end;

        case x in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc ;

        then ex i be Nat, a be Element of SCM-Data-Loc st x = [7, <*i*>, <*a*>];

        hence thesis;

      end;

        case x in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S;

        then ex a be Element of SCM-Data-Loc , r be Element of S st x = [5, {} , <*a, r*>];

        hence thesis;

      end;

    end;

    begin

    reserve I for Element of ( Segm 8),

S for non empty 1-sorted,

t for Element of S,

x for set,

k for Nat;

    registration

      cluster strict trivial for Ring;

      existence

      proof

        take the strict1 -element doubleLoopStr;

        thus thesis;

      end;

    end

    registration

      let R be Ring;

      cluster ( SCM-Instr R) -> standard-ins;

      coherence

      proof

        consider X be non empty set such that

         A1: ( proj2 ( SCM-Instr R)) c= (X * ) by FINSEQ_1: 85;

        take X;

        

         A2: ( SCM-Instr R) c= [: NAT , ( NAT * ), ( proj2 ( SCM-Instr R)):] by Th5;

         [: NAT , ( NAT * ), ( proj2 ( SCM-Instr R)):] c= [: NAT , ( NAT * ), (X * ):] by A1, MCART_1: 73;

        hence ( SCM-Instr R) c= [: NAT , ( NAT * ), (X * ):] by A2;

      end;

    end

    

     Lm1: for R be Ring holds for i be Element of ( SCM-Instr R) holds ( InsCode i) <= 7

    proof

      let R be Ring;

      let i be Element of ( SCM-Instr R);

      ( InsCode i) = 0 or ... or ( InsCode i) = 7 by Th7;

      hence thesis;

    end;

    

     Lm2: for S be non empty 1-sorted holds for i be Element of ( SCM-Instr S) st ( InsCode i) = 1 or ... or ( InsCode i) = 4 holds ( JumpPart i) = {}

    proof

      let S be non empty 1-sorted;

      let i be Element of ( SCM-Instr S);

      assume ( InsCode i) = 1 or ... or ( InsCode i) = 4;

      then i in { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} } by Th7;

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

      hence thesis;

    end;

    

     Lm3: for S be non empty 1-sorted holds for i be Element of ( SCM-Instr S) st ( InsCode i) = 5 holds ( JumpPart i) = {}

    proof

      let S be non empty 1-sorted;

      let i be Element of ( SCM-Instr S);

      assume ( InsCode i) = 5;

      then i in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of S by Th7;

      then ex a be Element of SCM-Data-Loc , r be Element of S st i = [5, {} , <*a, r*>];

      hence thesis;

    end;

    

     Lm4: for R be Ring holds for I be Element of ( SCM-Instr R) st ( InsCode I) = 6 holds ( dom ( JumpPart I)) = ( Seg 1)

    proof

      let R be Ring;

      let I be Element of ( SCM-Instr R);

      assume ( InsCode I) = 6;

      then I in the set of all [6, <*i*>, {} ] where i be Nat by Th7;

      then

      consider i be Nat such that

       A1: I = [6, <*i*>, {} ];

      ( JumpPart I) = <*i*> by A1;

      hence thesis by FINSEQ_1: 38;

    end;

    

     Lm5: for R be Ring holds for I be Element of ( SCM-Instr R) st ( InsCode I) = 7 holds ( dom ( JumpPart I)) = ( Seg 1)

    proof

      let R be Ring;

      let I be Element of ( SCM-Instr R);

      assume ( InsCode I) = 7;

      then I in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc by Th7;

      then

      consider i be Nat, a be Element of SCM-Data-Loc such that

       A1: I = [7, <*i*>, <*a*>];

      ( JumpPart I) = <*i*> by A1;

      hence thesis by FINSEQ_1: 38;

    end;

    registration

      let R be Ring;

      cluster ( SCM-Instr R) -> homogeneous;

      coherence

      proof

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

         A1: ( InsCode i) = ( InsCode j);

        ( InsCode i) <= 7 by Lm1;

        then ( InsCode i) = 0 or ... or ( InsCode i) = 7 by NAT_1: 60;

        per cases ;

          suppose ( InsCode i) = 0 ;

          then i in { [ 0 , {} , {} ]} & j in { [ 0 , {} , {} ]} by A1, Th7;

          then i = [ 0 , {} , {} ] & j = [ 0 , {} , {} ] by TARSKI:def 1;

          hence thesis;

        end;

          suppose ( InsCode i) = 1 or ... or ( InsCode i) = 4;

          then ( JumpPart i) = {} & ( JumpPart j) = {} by A1, Lm2;

          hence thesis;

        end;

          suppose ( InsCode i) = 5;

          then ( JumpPart i) = {} & ( JumpPart j) = {} by A1, Lm3;

          hence thesis;

        end;

          suppose ( InsCode i) = 6;

          then ( dom ( JumpPart i)) = ( Seg 1) & ( dom ( JumpPart j)) = ( Seg 1) by A1, Lm4;

          hence thesis;

        end;

          suppose ( InsCode i) = 7;

          then ( dom ( JumpPart i)) = ( Seg 1) & ( dom ( JumpPart j)) = ( Seg 1) by A1, Lm5;

          hence thesis;

        end;

      end;

    end

    reserve R for Ring,

T for InsType of ( SCM-Instr R);

    registration

      let R be Ring;

      cluster ( SCM-Instr R) -> J/A-independent;

      coherence

      proof

        let T be InsType of ( SCM-Instr R), f1,f2 be natural-valued Function such that

         A1: f1 in ( JumpParts T) and

         A2: ( dom f1) = ( dom f2);

        let p be object such that

         A3: [T, f1, p] in ( SCM-Instr R);

        reconsider II = [T, f1, p] as Element of ( SCM-Instr R) by A3;

        

         A4: ( InsCode II) = T;

        ( InsCode II) <= 7 by Lm1;

        then ( InsCode II) = 0 or ... or ( InsCode II) = 7 by NAT_1: 60;

        per cases ;

          suppose T = 0 ;

          then II in { [ 0 , {} , {} ]} by A4, Th7;

          then II = [ 0 , {} , {} ] by TARSKI:def 1;

          then ( JumpPart II) = {} ;

          then

           A5: ( JumpParts T) = { 0 } by A4, COMPOS_0: 11;

          f1 = 0 by A5, A1, TARSKI:def 1;

          then f1 = f2 by A2;

          hence [T, f2, p] in ( SCM-Instr R) by A3;

        end;

          suppose T = 1 or ... or T = 4;

          then II in { [I, {} , <*a, b*>] where I be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} } by A4, Th7;

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

          then ( JumpPart II) = {} ;

          then

           A6: ( JumpParts T) = { 0 } by A4, COMPOS_0: 11;

          f1 = 0 by A6, A1, TARSKI:def 1;

          then f1 = f2 by A2;

          hence [T, f2, p] in ( SCM-Instr R) by A3;

        end;

          suppose T = 5;

          then II in the set of all [5, {} , <*a, r*>] where a be Element of SCM-Data-Loc , r be Element of R by A4, Th7;

          then ex a be Element of SCM-Data-Loc , r be Element of R st II = [5, {} , <*a, r*>];

          then ( JumpPart II) = {} ;

          then

           A7: ( JumpParts T) = { 0 } by A4, COMPOS_0: 11;

          f1 = 0 by A7, A1, TARSKI:def 1;

          then f1 = f2 by A2;

          hence [T, f2, p] in ( SCM-Instr R) by A3;

        end;

          suppose

           A8: T = 6;

          reconsider J = [T, f1, p] as Element of ( SCM-Instr R) by A3;

          ( InsCode J) = 6 by A8;

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

          then

          consider i1 be Nat such that

           A9: J = [6, <*i1*>, {} ];

          

           A10: p = {} by A9, XTUPLE_0: 3;

          f1 = <*i1*> by A9, XTUPLE_0: 3;

          then

           A11: ( dom f2) = {1} by A2, FINSEQ_1: 2, FINSEQ_1: 38;

          reconsider l = (f2 . 1) as Element of NAT by ORDINAL1:def 12;

          set I = [T, f2, {} ];

          

           A12: I = [6, <*l*>, {} ] by A8, A11, FINSEQ_1: 2, FINSEQ_1:def 8;

           [6, <*l*>, {} ] in the set of all [6, <*n*>, {} ] where n be Nat;

          then [6, <*l*>, {} ] in (( { [ 0 , {} , {} ]} \/ { [H, {} , <*a, b*>] where H be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : H in {1, 2, 3, 4} }) \/ the set of all [6, <*n*>, {} ] where n be Nat) by XBOOLE_0:def 3;

          then [6, <*l*>, {} ] in ((( { [ 0 , {} , {} ]} \/ { [H, {} , <*a, b*>] where H be Element of ( Segm 8), a,b be Element of SCM-Data-Loc : H in {1, 2, 3, 4} }) \/ the set of all [6, <*n*>, {} ] where n be Nat) \/ the set of all [7, <*n*>, <*a*>] where n be Nat, a be Element of SCM-Data-Loc ) by XBOOLE_0:def 3;

          then [6, <*l*>, {} ] in ( SCM-Instr R) by XBOOLE_0:def 3;

          then

          reconsider I as Element of ( SCM-Instr R) by A12;

          f2 = ( JumpPart I);

          hence [T, f2, p] in ( SCM-Instr R) by A10;

        end;

          suppose

           A13: T = 7;

          reconsider J = [T, f1, p] as Element of ( SCM-Instr R) by A3;

          ( InsCode J) = T;

          then J in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc by A13, Th7;

          then

          consider i1 be Nat, a be Element of SCM-Data-Loc such that

           A14: J = [7, <*i1*>, <*a*>];

          

           A15: p = <*a*> by A14, XTUPLE_0: 3;

          f1 = <*i1*> by A14, XTUPLE_0: 3;

          then

           A16: ( dom f2) = {1} by A2, FINSEQ_1: 2, FINSEQ_1: 38;

          reconsider l = (f2 . 1) as Element of NAT by ORDINAL1:def 12;

          set I = [T, f2, p];

          

           A17: I = [T, <*l*>, <*a*>] by A15, A16, FINSEQ_1: 2, FINSEQ_1:def 8;

           [( InsCode I), <*l*>, <*a*>] in the set of all [7, <*n*>, <*c*>] where n be Nat, c be Element of SCM-Data-Loc by A13;

          then [( InsCode I), <*l*>, <*a*>] in ((( { [ 0 , {} , {} ]} \/ { [H, {} , <*a7, b7*>] where H be Element of ( Segm 8), a7,b7 be Element of SCM-Data-Loc : H in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) \/ the set of all [7, <*i*>, <*a7*>] where i be Nat, a7 be Element of SCM-Data-Loc ) by XBOOLE_0:def 3;

          then [( InsCode I), <*l*>, <*a*>] in (((( { [ 0 , {} , {} ]} \/ { [H, {} , <*a7, b7*>] where H be Element of ( Segm 8), a7,b7 be Element of SCM-Data-Loc : H in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) \/ the set of all [7, <*i*>, <*a7*>] where i be Nat, a7 be Element of SCM-Data-Loc ) \/ the set of all [5, {} , <*a7, r7*>] where a7 be Element of SCM-Data-Loc , r7 be Element of R) by XBOOLE_0:def 3;

          then [( InsCode I), <*l*>, <*a*>] in ( SCM-Instr R);

          then

          reconsider I as Element of ( SCM-Instr R) by A17;

          ( InsCode I) = T;

          then I in the set of all [7, <*i2*>, <*b*>] where i2 be Nat, b be Element of SCM-Data-Loc by A13, Th7;

          then

          consider i2 be Nat, b be Element of SCM-Data-Loc such that

           A18: I = [7, <*i2*>, <*b*>];

          7 = ( InsCode I) by A18

          .= T;

          then

           A19: I = [T, <*i2*>, <*b*>] by A18;

          thus [T, f2, p] in ( SCM-Instr R) by A19;

        end;

      end;

    end

    reserve R for Ring,

r for Element of R,

a,b,c,d1,d2 for Element of SCM-Data-Loc ;

    reserve i1 for Nat;

    theorem :: SCMRINGI:8

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

    proof

      reconsider D1 = d1, D2 = d2 as Element of SCM-Data-Loc ;

      assume

       A1: x in {1, 2, 3, 4};

      then x = 1 or x = 2 or x = 3 or x = 4 by ENUMSET1:def 2;

      then

      reconsider x as Element of ( Segm 8) by NAT_1: 44;

       [x, {} , <*D1, D2*>] in { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} } by A1;

      then [x, {} , <*D1, D2*>] in ( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) by XBOOLE_0:def 3;

      then [x, {} , <*D1, D2*>] in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) by XBOOLE_0:def 3;

      then [x, {} , <*D1, D2*>] in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: SCMRINGI:9

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

    proof

      reconsider D1 = d1 as Element of SCM-Data-Loc ;

       [5, {} , <*D1, t*>] in the set of all [5, {} , <*i, a*>] where i be Element of SCM-Data-Loc , a be Element of S;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: SCMRINGI:10

     [6, <*i1*>, {} ] in ( SCM-Instr S)

    proof

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

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

      then [6, <*I1*>, {} ] in (( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : I in {1, 2, 3, 4} }) \/ the set of all [6, <*i*>, {} ] where i be Nat) by XBOOLE_0:def 3;

      then [6, <*I1*>, {} ] in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: SCMRINGI:11

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

    proof

      reconsider D1 = d1 as Element of SCM-Data-Loc ;

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

       [7, <*I1*>, <*D1*>] in the set of all [7, <*i*>, <*a*>] where i be Nat, a be Element of SCM-Data-Loc ;

      then [7, <*I1*>, <*D1*>] in ((( { [ 0 , {} , {} ]} \/ { [I, {} , <*a, b*>] where a,b be Element of SCM-Data-Loc : 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 SCM-Data-Loc ) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    registration

      let S;

      cluster ( SCM-Instr S) -> with_halt;

      coherence by Th6;

    end