compos_0.miz



    begin

    reserve x,A for set,

i,j,k,m,n,l,l1,l2 for Nat;

    reserve D for non empty set,

z for Nat;

    definition

      let S be set;

      :: COMPOS_0:def1

      attr S is standard-ins means

      : Def1: ex X be non empty set st S c= [: NAT , ( NAT * ), (X * ):];

    end

    registration

      cluster { [ 0 , {} , {} ]} -> standard-ins;

      coherence

      proof

        take { {} };

        

         A1: { {} } c= ( { {} } * ) by FINSEQ_1: 49, ZFMISC_1: 31;

        

         A2: { {} } c= ( NAT * ) by FINSEQ_1: 49, ZFMISC_1: 31;

         { [ 0 , {} , {} ]} = [: { 0 }, { {} }, { {} }:] by MCART_1: 35;

        hence { [ 0 , {} , {} ]} c= [: NAT , ( NAT * ), ( { {} } * ):] by A1, A2, MCART_1: 73;

      end;

      cluster { [1, {} , {} ]} -> standard-ins;

      coherence

      proof

        take { {} };

        

         A3: { {} } c= ( { {} } * ) by FINSEQ_1: 49, ZFMISC_1: 31;

        

         A4: { {} } c= ( NAT * ) by FINSEQ_1: 49, ZFMISC_1: 31;

         { [1, {} , {} ]} = [: {1}, { {} }, { {} }:] by MCART_1: 35;

        hence { [1, {} , {} ]} c= [: NAT , ( NAT * ), ( { {} } * ):] by A3, A4, MCART_1: 73;

      end;

    end

    notation

      let x be object;

      synonym InsCode x for x `1_3 ;

      synonym JumpPart x for x `2_3 ;

      synonym AddressPart x for x `3_3 ;

    end

    definition

      let x be object;

      :: original: InsCode

      redefine

      func InsCode x -> set ;

      coherence by TARSKI: 1;

      :: original: JumpPart

      redefine

      func JumpPart x -> set ;

      coherence by TARSKI: 1;

      :: original: AddressPart

      redefine

      func AddressPart x -> set ;

      coherence by TARSKI: 1;

    end

    registration

      cluster non empty standard-ins for set;

      existence

      proof

        take { [ 0 , {} , {} ]};

        thus thesis;

      end;

    end

    registration

      let S be non empty standard-ins set;

      let I be Element of S;

      cluster ( AddressPart I) -> Function-like Relation-like;

      coherence

      proof

        consider X be non empty set such that

         A1: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I in S;

        then ( AddressPart I) in (X * ) by A1, RECDEF_2: 2;

        hence thesis;

      end;

      cluster ( JumpPart I) -> Function-like Relation-like;

      coherence

      proof

        consider X be non empty set such that

         A2: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I in S;

        then ( JumpPart I) in ( NAT * ) by A2, RECDEF_2: 2;

        hence thesis;

      end;

    end

    registration

      let S be non empty standard-ins set;

      let I be Element of S;

      cluster ( AddressPart I) -> FinSequence-like;

      coherence

      proof

        consider X be non empty set such that

         A1: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I in S;

        then ( AddressPart I) in (X * ) by A1, RECDEF_2: 2;

        hence thesis;

      end;

      cluster ( JumpPart I) -> FinSequence-like;

      coherence

      proof

        consider X be non empty set such that

         A2: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I in S;

        then ( JumpPart I) in ( NAT * ) by A2, RECDEF_2: 2;

        hence thesis;

      end;

    end

    registration

      let S be non empty standard-ins set;

      let x be Element of S;

      cluster ( InsCode x) -> natural;

      coherence

      proof

        consider X be non empty set such that

         A1: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        x in S;

        then (x `1_3 ) in NAT by A1, RECDEF_2: 2;

        hence thesis;

      end;

    end

    registration

      cluster standard-ins -> Relation-like for set;

      coherence ;

    end

    definition

      let S be standard-ins set;

      :: COMPOS_0:def2

      func InsCodes S -> set equals ( proj1_3 S);

      correctness ;

    end

    registration

      let S be non empty standard-ins set;

      cluster ( InsCodes S) -> non empty;

      coherence

      proof

        ex X be non empty set st S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        then

        reconsider II = ( dom S) as Relation;

        assume ( InsCodes S) is empty;

        then II = {} ;

        hence contradiction;

      end;

    end

    definition

      let S be non empty standard-ins set;

      mode InsType of S is Element of ( InsCodes S);

    end

    definition

      let S be non empty standard-ins set;

      let I be Element of S;

      :: original: InsCode

      redefine

      func InsCode I -> InsType of S ;

      coherence

      proof

        consider X be non empty set such that

         A1: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I = [(I `1_3 ), (I `2_3 ), (I `3_3 )] by A1, RECDEF_2: 3;

        then [(I `1_3 ), (I `2_3 )] in ( proj1 S) by XTUPLE_0:def 12;

        hence thesis by XTUPLE_0:def 12;

      end;

    end

    definition

      let S be non empty standard-ins set;

      let T be InsType of S;

      :: COMPOS_0:def3

      func JumpParts T -> set equals { ( JumpPart I) where I be Element of S : ( InsCode I) = T };

      coherence ;

      :: COMPOS_0:def4

      func AddressParts T -> set equals { ( AddressPart I) where I be Element of S : ( InsCode I) = T };

      coherence ;

    end

    registration

      let S be non empty standard-ins set;

      let T be InsType of S;

      cluster ( AddressParts T) -> functional;

      coherence

      proof

        let f be object;

        assume f in ( AddressParts T);

        then ex I be Element of S st f = ( AddressPart I) & ( InsCode I) = T;

        hence thesis;

      end;

      cluster ( JumpParts T) -> non empty functional;

      coherence

      proof

        consider y be object such that

         A1: [T, y] in ( proj1 S) by XTUPLE_0:def 12;

        consider x be object such that

         A2: [ [T, y], x] in S by A1, XTUPLE_0:def 12;

        reconsider I = [T, y, x] as Element of S by A2;

        ( InsCode I) = T;

        then ( JumpPart I) in ( JumpParts T);

        hence ( JumpParts T) is non empty;

        let f be object;

        assume f in ( JumpParts T);

        then ex I be Element of S st f = ( JumpPart I) & ( InsCode I) = T;

        hence thesis;

      end;

    end

    definition

      let S be non empty standard-ins set;

      :: COMPOS_0:def5

      attr S is homogeneous means

      : Def5: for I,J be Element of S st ( InsCode I) = ( InsCode J) holds ( dom ( JumpPart I)) = ( dom ( JumpPart J));

      ::$Canceled

      :: COMPOS_0:def7

      attr S is J/A-independent means

      : Def6: for T be InsType of S, f1,f2 be natural-valued Function st f1 in ( JumpParts T) & ( dom f1) = ( dom f2) holds for p be object st [T, f1, p] in S holds [T, f2, p] in S;

    end

    

     Lm1: for T be InsType of { [ 0 , {} , {} ]} holds ( JumpParts T) = { 0 }

    proof

      let T be InsType of { [ 0 , {} , {} ]};

      set A = { ( JumpPart I) where I be Element of { [ 0 , {} , {} ]} : ( InsCode I) = T };

       { 0 } = A

      proof

        hereby

          let a be object;

          assume a in { 0 };

          then

           A1: a = 0 by TARSKI:def 1;

          

           A2: ( InsCodes { [ 0 , {} , {} ]}) = { 0 } by MCART_1: 92;

          

           A3: T = 0 by A2, TARSKI:def 1;

          reconsider I = [ 0 , 0 , 0 ] as Element of { [ 0 , {} , {} ]} by TARSKI:def 1;

          

           A4: ( JumpPart I) = 0 ;

          ( InsCode I) = 0 ;

          hence a in A by A1, A3, A4;

        end;

        let a be object;

        assume a in A;

        then

        consider I be Element of { [ 0 , {} , {} ]} such that

         A5: a = ( JumpPart I) & ( InsCode I) = T;

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

        then a = 0 by A5;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      cluster { [ 0 , {} , {} ]} -> J/A-independent homogeneous;

      coherence

      proof

        thus { [ 0 , {} , {} ]} is J/A-independent

        proof

          let T be InsType of { [ 0 , {} , {} ]}, f1,f2 be natural-valued Function such that

           A1: f1 in ( JumpParts T) and

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

          let p be object;

          

           A3: f1 in { 0 } by A1, Lm1;

          f1 = 0 & f2 = 0 by A3, A2, CARD_3: 10;

          hence thesis;

        end;

        let I,J be Element of { [ 0 , {} , {} ]} such that ( InsCode I) = ( InsCode J);

        I = [ 0 , {} , {} ] & J = [ 0 , {} , {} ] by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      cluster J/A-independent homogeneous for non empty standard-ins set;

      existence

      proof

        take S = { [ 0 , {} , {} ]};

        thus thesis;

      end;

    end

    registration

      let S be homogeneous non empty standard-ins set;

      let T be InsType of S;

      cluster ( JumpParts T) -> with_common_domain;

      coherence

      proof

        let f,g be Function;

        assume that

         A1: f in ( JumpParts T) and

         A2: g in ( JumpParts T);

        

         A3: ex I be Element of S st f = ( JumpPart I) & ( InsCode I) = T by A1;

        ex J be Element of S st g = ( JumpPart J) & ( InsCode J) = T by A2;

        hence thesis by A3, Def5;

      end;

    end

    registration

      let S be non empty standard-ins set;

      let I be Element of S;

      cluster ( JumpPart I) -> NAT -valued;

      coherence

      proof

        let f be Function such that

         A1: f = ( JumpPart I);

        consider X be non empty set such that

         A2: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

        I in S;

        then ( JumpPart I) in ( NAT * ) by A2, RECDEF_2: 2;

        hence thesis by A1, FINSEQ_1:def 11;

      end;

    end

    

     Lm2: for S be homogeneous non empty standard-ins set holds for I be Element of S, x st x in ( dom ( JumpPart I)) holds (( product" ( JumpParts ( InsCode I))) . x) c= NAT

    proof

      let S be homogeneous non empty standard-ins set;

      let I be Element of S, x be set such that

       A1: x in ( dom ( JumpPart I));

      ( JumpPart I) in ( JumpParts ( InsCode I));

      then ( dom ( product" ( JumpParts ( InsCode I)))) = ( dom ( JumpPart I)) by CARD_3: 100;

      then

       A2: (( product" ( JumpParts ( InsCode I))) . x) = the set of all (f . x) where f be Element of ( JumpParts ( InsCode I)) by A1, CARD_3: 74;

      let e be object;

      assume e in (( product" ( JumpParts ( InsCode I))) . x);

      then

      consider f be Element of ( JumpParts ( InsCode I)) such that

       A3: e = (f . x) by A2;

      f in ( JumpParts ( InsCode I));

      then ex J be Element of S st f = ( JumpPart J) & ( InsCode J) = ( InsCode I);

      hence e in NAT by A3, ORDINAL1:def 12;

    end;

    

     Lm3: for S be homogeneous non empty standard-ins set st S is J/A-independent holds for I be Element of S, x st x in ( dom ( JumpPart I)) holds NAT c= (( product" ( JumpParts ( InsCode I))) . x)

    proof

      let S be homogeneous non empty standard-ins set such that

       A1: S is J/A-independent;

      consider D0 be non empty set such that

       A2: S c= [: NAT , ( NAT * ), (D0 * ):] by Def1;

      let I be Element of S, x be set such that

       A3: x in ( dom ( JumpPart I));

      

       A4: ( JumpPart I) in ( JumpParts ( InsCode I));

      then ( dom ( product" ( JumpParts ( InsCode I)))) = ( dom ( JumpPart I)) by CARD_3: 100;

      then

       A5: (( product" ( JumpParts ( InsCode I))) . x) = the set of all (f . x) where f be Element of ( JumpParts ( InsCode I)) by A3, CARD_3: 74;

      let e be object;

      assume e in NAT ;

      then

      reconsider e as Element of NAT ;

      set g = (( JumpPart I) +* (x,e));

      

       A6: ( dom g) = ( dom ( JumpPart I)) by FUNCT_7: 30;

      I in S;

      then [( InsCode I), ( JumpPart I), ( AddressPart I)] in S by A2, RECDEF_2: 3;

      then

      reconsider J = [( InsCode I), g, ( AddressPart I)] as Element of S by A4, A1, A6;

      ( InsCode J) = ( InsCode I);

      then ( JumpPart J) in ( JumpParts ( InsCode I));

      then

      reconsider g as Element of ( JumpParts ( InsCode I));

      e = (g . x) by A3, FUNCT_7: 31;

      hence thesis by A5;

    end;

    theorem :: COMPOS_0:1

    

     Th1: for S be standard-ins non empty set holds for I,J be Element of S st ( InsCode I) = ( InsCode J) & ( JumpPart I) = ( JumpPart J) & ( AddressPart I) = ( AddressPart J) holds I = J

    proof

      let S be standard-ins non empty set;

      let I,J be Element of S;

      consider X be non empty set such that

       A1: S c= [: NAT , ( NAT * ), (X * ):] by Def1;

      

       A2: I in S;

      J in S;

      hence thesis by A2, A1, RECDEF_2: 10;

    end;

    reserve y for set;

    registration

      let S be homogeneous J/A-independent standard-ins non empty set;

      let T be InsType of S;

      cluster ( JumpParts T) -> product-like;

      coherence

      proof

        consider y be object such that

         A1: [T, y] in ( proj1 S) by XTUPLE_0:def 12;

        consider z be object such that

         A2: [ [T, y], z] in S by A1, XTUPLE_0:def 12;

        reconsider I = [T, y, z] as Element of S by A2;

        

         A3: ( InsCode I) = T;

        

         A4: ( JumpPart I) = y;

        set f = (( dom ( JumpPart I)) --> NAT );

        

         A5: ( dom f) = ( dom ( JumpPart I)) by FUNCOP_1: 13;

        for x be object holds x in ( JumpParts T) iff ex g be Function st x = g & ( dom g) = ( dom f) & for y be object st y in ( dom f) holds (g . y) in (f . y)

        proof

          let x be object;

          thus x in ( JumpParts T) implies ex g be Function st x = g & ( dom g) = ( dom f) & for y be object st y in ( dom f) holds (g . y) in (f . y)

          proof

            assume x in ( JumpParts T);

            then

            consider K be Element of S such that

             A6: x = ( JumpPart K) and

             A7: ( InsCode K) = T;

            take g = ( JumpPart K);

            thus x = g by A6;

            thus

             A8: ( dom g) = ( dom f) by A7, A3, Def5, A5;

            let y be object;

            assume

             A9: y in ( dom f);

            then (f . y) = NAT by A5, FUNCOP_1: 7;

            hence (g . y) in (f . y) by A8, A9, FUNCT_1: 102;

          end;

          given g be Function such that

           A10: x = g and

           A11: ( dom g) = ( dom f) and

           A12: for y be object st y in ( dom f) holds (g . y) in (f . y);

          

           A13: ( dom g) = ( dom ( JumpPart I)) by A11, FUNCOP_1: 13;

          set J = [T, g, z];

          

           A14: y in ( JumpParts T) by A4, A3;

          then

           A15: ( dom g) = ( dom ( product" ( JumpParts T))) by A13, CARD_3: 100;

          

           A16: for x be object st x in ( dom ( product" ( JumpParts T))) holds (g . x) in (( product" ( JumpParts T)) . x)

          proof

            let x be object;

            assume

             A17: x in ( dom ( product" ( JumpParts T)));

            

             A18: NAT c= (( product" ( JumpParts ( InsCode I))) . x) by A17, A15, A13, Lm3;

            (f . x) = NAT by A15, A13, A17, FUNCOP_1: 7;

            then (g . x) in NAT by A12, A15, A17, A11;

            hence (g . x) in (( product" ( JumpParts T)) . x) by A18;

          end;

          

           A19: g is natural-valued

          proof

            let x be object;

            assume

             A20: x in ( dom g);

            then

             A21: (( product" ( JumpParts ( InsCode I))) . x) c= NAT by Lm2, A13;

            (g . x) in (( product" ( JumpParts T)) . x) by A15, A16, A20;

            hence (g . x) is natural by A21;

          end;

          reconsider J as Element of S by A14, Def6, A19, A13;

          

           A22: ( InsCode J) = T;

          g = ( JumpPart J);

          hence x in ( JumpParts T) by A22, A10;

        end;

        then ( JumpParts T) = ( product f) by CARD_3:def 5;

        hence ( JumpParts T) is product-like;

      end;

    end

    definition

      let S be standard-ins set;

      let I be Element of S;

      :: COMPOS_0:def8

      attr I is ins-loc-free means

      : Def7: ( JumpPart I) is empty;

    end

    registration

      let S be standard-ins non empty set;

      let I be Element of S;

      cluster ( JumpPart I) -> natural-valued;

      coherence ;

    end

    definition

      let S be homogeneous J/A-independent standard-ins non empty set;

      let I be Element of S;

      let k be Nat;

      :: COMPOS_0:def9

      func IncAddr (I,k) -> Element of S means

      : Def8: ( InsCode it ) = ( InsCode I) & ( AddressPart it ) = ( AddressPart I) & ( JumpPart it ) = (k + ( JumpPart I));

      existence

      proof

        consider D0 be non empty set such that

         A1: S c= [: NAT , ( NAT * ), (D0 * ):] by Def1;

        set p = (k + ( JumpPart I));

        set f = ( product" ( JumpParts ( InsCode I)));

        

         A2: ( JumpPart I) in ( JumpParts ( InsCode I));

        

         A3: ( JumpParts ( InsCode I)) = ( product f) by CARD_3: 78;

        

         A4: ( dom p) = ( dom ( JumpPart I)) by VALUED_1:def 2;

        

        then

         A5: ( dom p) = ( DOM ( JumpParts ( InsCode I))) by A2, CARD_3: 108

        .= ( dom f) by CARD_3:def 12;

        for z be object st z in ( dom p) holds (p . z) in (f . z)

        proof

          let z be object;

          assume

           A6: z in ( dom p);

          reconsider z as Element of NAT by A6;

          

           A7: (f . z) c= NAT by A6, A4, Lm2;

           NAT c= (f . z) by A6, A4, Lm3;

          then

           A8: (f . z) = NAT by A7;

          reconsider il = (( JumpPart I) . z) as Element of NAT by ORDINAL1:def 12;

          (p . z) = (k + il) by A6, VALUED_1:def 2;

          hence thesis by A8;

        end;

        then p in ( JumpParts ( InsCode I)) by A3, A5, CARD_3: 9;

        then

        consider II be Element of S such that

         A9: p = ( JumpPart II) and ( InsCode I) = ( InsCode II);

        

         A10: ( JumpPart I) in ( JumpParts ( InsCode I));

         [( InsCode I), ( JumpPart I), ( AddressPart I)] = I by A1, RECDEF_2: 3;

        then

        reconsider IT = [( InsCode I), ( JumpPart II), ( AddressPart I)] as Element of S by A10, Def6, A4, A9;

        take IT;

        thus ( InsCode IT) = ( InsCode I);

        thus ( AddressPart IT) = ( AddressPart I);

        thus ( JumpPart IT) = (k + ( JumpPart I)) by A9;

      end;

      uniqueness by Th1;

    end

    ::$Canceled

    theorem :: COMPOS_0:3

    for S be homogeneous J/A-independent standard-ins non empty set, I be Element of S holds ( IncAddr (I, 0 )) = I

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I be Element of S;

      

       A1: ( InsCode ( IncAddr (I, 0 ))) = ( InsCode I) by Def8;

      

       A2: ( AddressPart ( IncAddr (I, 0 ))) = ( AddressPart I) by Def8;

      

       A3: ( JumpPart ( IncAddr (I, 0 ))) = ( 0 qua Nat + ( JumpPart I)) by Def8;

      then

       A4: ( dom ( JumpPart I)) = ( dom ( JumpPart ( IncAddr (I, 0 )))) by VALUED_1:def 2;

      for k be Nat st k in ( dom ( JumpPart I)) holds (( JumpPart ( IncAddr (I, 0 ))) . k) = (( JumpPart I) . k)

      proof

        let k be Nat;

        assume k in ( dom ( JumpPart I));

        

        hence (( JumpPart ( IncAddr (I, 0 ))) . k) = ( 0 qua Nat + (( JumpPart I) . k)) by A4, A3, VALUED_1:def 2

        .= (( JumpPart I) . k);

      end;

      then ( JumpPart ( IncAddr (I, 0 ))) = ( JumpPart I) by A4;

      hence thesis by A1, A2, Th1;

    end;

    theorem :: COMPOS_0:4

    

     Th3: for S be homogeneous J/A-independent standard-ins non empty set, I be Element of S st I is ins-loc-free holds ( IncAddr (I,k)) = I

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I be Element of S such that

       A1: ( JumpPart I) is empty;

      set f = ( IncAddr (I,k));

      

       A2: ( InsCode f) = ( InsCode I) by Def8;

      

       A3: ( AddressPart f) = ( AddressPart I) by Def8;

      

       A4: ( JumpPart f) = (k + ( JumpPart I)) by Def8;

      ( JumpPart f) = ( JumpPart I) by A1, A4;

      hence thesis by A2, A3, Th1;

    end;

    theorem :: COMPOS_0:5

    for S be homogeneous J/A-independent standard-ins non empty set, I be Element of S holds ( JumpParts ( InsCode I)) = ( JumpParts ( InsCode ( IncAddr (I,k))))

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I be Element of S;

      set A = { ( JumpPart J) where J be Element of S : ( InsCode I) = ( InsCode J) }, B = { ( JumpPart J) where J be Element of S : ( InsCode ( IncAddr (I,k))) = ( InsCode J) };

      A = B

      proof

        hereby

          let a be object;

          assume a in A;

          then

          consider J be Element of S such that

           A1: a = ( JumpPart J) and

           A2: ( InsCode J) = ( InsCode I);

          ( InsCode J) = ( InsCode ( IncAddr (I,k))) by A2, Def8;

          hence a in B by A1;

        end;

        let a be object;

        assume a in B;

        then

        consider J be Element of S such that

         A3: a = ( JumpPart J) and

         A4: ( InsCode J) = ( InsCode ( IncAddr (I,k)));

        ( InsCode J) = ( InsCode I) by A4, Def8;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: COMPOS_0:6

    

     Th5: for S be homogeneous J/A-independent standard-ins non empty set, I,J be Element of S st ex k be Nat st ( IncAddr (I,k)) = ( IncAddr (J,k)) holds I = J

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I,J be Element of S;

      given k be Nat such that

       A1: ( IncAddr (I,k)) = ( IncAddr (J,k));

      

       A2: ( InsCode I) = ( InsCode ( IncAddr (I,k))) by Def8

      .= ( InsCode J) by A1, Def8;

      

       A3: ( AddressPart I) = ( AddressPart ( IncAddr (I,k))) by Def8

      .= ( AddressPart J) by A1, Def8;

      

       A4: ( JumpPart ( IncAddr (I,k))) = (k + ( JumpPart I)) by Def8;

      then

       A5: ( dom ( JumpPart I)) = ( dom ( JumpPart ( IncAddr (I,k)))) by VALUED_1:def 2;

      

       A6: ( JumpPart ( IncAddr (J,k))) = (k + ( JumpPart J)) by Def8;

      then

       A7: ( dom ( JumpPart J)) = ( dom ( JumpPart ( IncAddr (J,k)))) by VALUED_1:def 2;

      

       A8: ( dom ( JumpPart I)) = ( dom ( JumpPart J)) by A2, Def5;

      for x be object st x in ( dom ( JumpPart I)) holds (( JumpPart I) . x) = (( JumpPart J) . x)

      proof

        let x be object;

        assume

         A9: x in ( dom ( JumpPart I));

        

         A10: (( JumpPart ( IncAddr (I,k))) . x) = (k + (( JumpPart I) . x)) by A4, A5, A9, VALUED_1:def 2;

        

         A11: (( JumpPart ( IncAddr (J,k))) . x) = (k + (( JumpPart J) . x)) by A6, A8, A9, A7, VALUED_1:def 2;

        thus thesis by A1, A10, A11;

      end;

      then ( JumpPart I) = ( JumpPart J) by A8;

      hence thesis by A2, A3, Th1;

    end;

    theorem :: COMPOS_0:7

    for S be homogeneous J/A-independent standard-ins non empty set, I be Element of S holds ( IncAddr (( IncAddr (I,k)),m)) = ( IncAddr (I,(k + m)))

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I be Element of S;

      

       A1: ( InsCode ( IncAddr (( IncAddr (I,k)),m))) = ( InsCode ( IncAddr (I,k))) by Def8

      .= ( InsCode I) by Def8

      .= ( InsCode ( IncAddr (I,(k + m)))) by Def8;

      

       A2: ( AddressPart ( IncAddr (( IncAddr (I,k)),m))) = ( AddressPart ( IncAddr (I,k))) by Def8

      .= ( AddressPart I) by Def8

      .= ( AddressPart ( IncAddr (I,(k + m)))) by Def8;

      

       A3: ( JumpPart ( IncAddr (( IncAddr (I,k)),m))) = (m + ( JumpPart ( IncAddr (I,k)))) by Def8;

      

       A4: ( JumpPart ( IncAddr (I,k))) = (k + ( JumpPart I)) by Def8;

      

       A5: ( JumpPart ( IncAddr (I,(k + m)))) = ((k + m) + ( JumpPart I)) by Def8;

      

      then

       A6: ( dom ( JumpPart ( IncAddr (I,(k + m))))) = ( dom ( JumpPart I)) by VALUED_1:def 2

      .= ( dom ( JumpPart ( IncAddr (I,k)))) by A4, VALUED_1:def 2

      .= ( dom ( JumpPart ( IncAddr (( IncAddr (I,k)),m)))) by A3, VALUED_1:def 2;

      for n be object st n in ( dom ( JumpPart ( IncAddr (( IncAddr (I,k)),m)))) holds (( JumpPart ( IncAddr (( IncAddr (I,k)),m))) . n) = (( JumpPart ( IncAddr (I,(k + m)))) . n)

      proof

        let n be object;

        assume

         A7: n in ( dom ( JumpPart ( IncAddr (( IncAddr (I,k)),m))));

        then

         A8: n in ( dom ( JumpPart ( IncAddr (I,k)))) by A3, VALUED_1:def 2;

        then

         A9: n in ( dom ( JumpPart I)) by A4, VALUED_1:def 2;

        

         A10: (( JumpPart ( IncAddr (I,k))) . n) = (k + (( JumpPart I) . n)) by A4, A8, VALUED_1:def 2;

        

         A11: (( JumpPart ( IncAddr (( IncAddr (I,k)),m))) . n) = (m + (( JumpPart ( IncAddr (I,k))) . n)) by A7, A3, VALUED_1:def 2;

        n in ( dom ( JumpPart ( IncAddr (I,(k + m))))) by A5, A9, VALUED_1:def 2;

        then (( JumpPart ( IncAddr (I,(k + m)))) . n) = ((k + m) + (( JumpPart I) . n)) by A5, VALUED_1:def 2;

        hence thesis by A11, A10;

      end;

      then ( JumpPart ( IncAddr (( IncAddr (I,k)),m))) = ( JumpPart ( IncAddr (I,(k + m)))) by A6;

      hence thesis by A1, A2, Th1;

    end;

    theorem :: COMPOS_0:8

    for S be homogeneous J/A-independent standard-ins non empty set, I be Element of S, x be set st x in ( dom ( JumpPart I)) holds (( JumpPart I) . x) in (( product" ( JumpParts ( InsCode I))) . x)

    proof

      let S be homogeneous J/A-independent standard-ins non empty set, I be Element of S, x be set such that

       A1: x in ( dom ( JumpPart I));

      

       A2: ( JumpPart I) in ( JumpParts ( InsCode I));

      

       A3: ( dom ( product" ( JumpParts ( InsCode I)))) = ( DOM ( JumpParts ( InsCode I))) by CARD_3:def 12

      .= ( dom ( JumpPart I)) by A2, CARD_3: 108;

      (( JumpPart I) . x) in ( pi (( JumpParts ( InsCode I)),x)) by A2, CARD_3:def 6;

      hence thesis by A1, A3, CARD_3:def 12;

    end;

    registration

      cluster { [ 0 , {} , {} ], [1, {} , {} ]} -> standard-ins;

      coherence

      proof

        take { {} };

        

         A1: { {} } c= ( { {} } * ) by FINSEQ_1: 49, ZFMISC_1: 31;

        

         A2: { {} } c= ( NAT * ) by FINSEQ_1: 49, ZFMISC_1: 31;

         { [ 0 , {} , {} ]} = [: { 0 }, { {} }, { {} }:] by MCART_1: 35;

        then

         A3: { [ 0 , {} , {} ]} c= [: NAT , ( NAT * ), ( { {} } * ):] by A1, A2, MCART_1: 73;

         { [1, {} , {} ]} = [: {1}, { {} }, { {} }:] by MCART_1: 35;

        then

         A4: { [1, {} , {} ]} c= [: NAT , ( NAT * ), ( { {} } * ):] by A1, A2, MCART_1: 73;

        ( { [ 0 , {} , {} ]} \/ { [1, {} , {} ]}) = { [ 0 , {} , {} ], [1, 0 , 0 ]} by ENUMSET1: 1;

        hence thesis by A3, A4, XBOOLE_1: 8;

      end;

    end

    theorem :: COMPOS_0:9

    

     Th8: for x be Element of { [ 0 , {} , {} ], [1, {} , {} ]} holds ( JumpPart x) = {}

    proof

      let x be Element of { [ 0 , {} , {} ], [1, {} , {} ]};

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

      hence thesis;

    end;

    

     Lm4: for T be InsType of { [ 0 , {} , {} ], [1, {} , {} ]} holds ( JumpParts T) = { 0 }

    proof

      let T be InsType of { [ 0 , {} , {} ], [1, {} , {} ]};

      set A = { ( JumpPart I) where I be Element of { [ 0 , {} , {} ], [1, {} , {} ]} : ( InsCode I) = T };

       { 0 } = A

      proof

        hereby

          let a be object;

          assume a in { 0 };

          then

           A1: a = 0 by TARSKI:def 1;

          

           A2: ( InsCodes { [ 0 , {} , {} ]}) = { 0 } & ( InsCodes { [1, {} , {} ]}) = {1} by MCART_1: 92;

          ( InsCodes { [ 0 , {} , {} ], [1, {} , {} ]}) = ( proj1_3 ( { [ 0 , {} , {} ]} \/ { [1, {} , {} ]})) by ENUMSET1: 1

          .= (( InsCodes { [ 0 , {} , {} ]}) \/ ( InsCodes { [1, {} , {} ]})) by XTUPLE_0: 31;

          then T in { 0 } or T in {1} by A2, XBOOLE_0:def 3;

          then

           A3: T = 0 or T = 1 by TARSKI:def 1;

          reconsider I = [ 0 , 0 , 0 ], J = [1, 0 , 0 ] as Element of { [ 0 , {} , {} ], [1, {} , {} ]} by TARSKI:def 2;

          

           A4: ( JumpPart I) = 0 & ( JumpPart J) = 0 ;

          ( InsCode I) = 0 & ( InsCode J) = 1;

          hence a in A by A1, A3, A4;

        end;

        let a be object;

        assume a in A;

        then

        consider I be Element of { [ 0 , {} , {} ], [1, {} , {} ]} such that

         A5: a = ( JumpPart I) & ( InsCode I) = T;

        I = [ 0 , {} , {} ] or I = [1, {} , {} ] by TARSKI:def 2;

        then a = 0 by A5;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      cluster { [ 0 , {} , {} ], [1, {} , {} ]} -> J/A-independent homogeneous;

      coherence

      proof

        set S = { [ 0 , {} , {} ], [1, {} , {} ]};

        thus S is J/A-independent

        proof

          let T be InsType of S, f1,f2 be natural-valued Function such that

           A1: f1 in ( JumpParts T) and

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

          let p be object;

          

           A3: f1 in { 0 } by A1, Lm4;

          f1 = 0 & f2 = 0 by A3, A2, CARD_3: 10;

          hence thesis;

        end;

        let I,J be Element of S such that ( InsCode I) = ( InsCode J);

        ( JumpPart I) = {} & ( JumpPart J) = {} by Th8;

        hence thesis;

      end;

    end

    theorem :: COMPOS_0:10

    for S be standard-ins non empty set holds for T be InsType of S holds ex I be Element of S st ( InsCode I) = T

    proof

      let S be standard-ins non empty set;

      let T be InsType of S;

      consider y be object such that

       A1: [T, y] in ( proj1 S) by XTUPLE_0:def 12;

      consider z be object such that

       A2: [ [T, y], z] in S by A1, XTUPLE_0:def 12;

      reconsider I = [ [T, y], z] as Element of S by A2;

      take I;

      thus ( InsCode I) = T;

    end;

    theorem :: COMPOS_0:11

    for S be homogeneous standard-ins non empty set holds for I be Element of S st ( JumpPart I) = {} holds ( JumpParts ( InsCode I)) = { 0 }

    proof

      let S be homogeneous standard-ins non empty set;

      let I be Element of S;

      assume

       A1: ( JumpPart I) = {} ;

      set T = ( InsCode I);

      hereby

        let a be object;

        assume a in ( JumpParts T);

        then

        consider II be Element of S such that

         A2: a = ( JumpPart II) and

         A3: ( InsCode II) = T;

        ( dom ( JumpPart II)) = ( dom ( JumpPart I)) by A3, Def5;

        then a = 0 by A1, A2;

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

      end;

      let a be object;

      assume a in { 0 };

      then a = 0 by TARSKI:def 1;

      hence a in ( JumpParts T) by A1;

    end;

    begin

    definition

      let X be set;

      :: COMPOS_0:def10

      attr X is with_halt means

      : Def9: [ 0 , {} , {} ] in X;

    end

    registration

      cluster with_halt -> non empty for set;

      coherence ;

    end

    registration

      cluster { [ 0 , {} , {} ]} -> with_halt;

      coherence by TARSKI:def 1;

      cluster { [ 0 , {} , {} ], [1, {} , {} ]} -> with_halt;

      coherence by TARSKI:def 2;

    end

    registration

      cluster with_halt standard-ins for set;

      existence

      proof

        take S = { [ 0 , {} , {} ]};

        thus thesis;

      end;

    end

    registration

      cluster J/A-independent homogeneous for with_halt standard-ins set;

      existence

      proof

        take S = { [ 0 , {} , {} ]};

        thus thesis;

      end;

    end

    definition

      let S be with_halt set;

      :: COMPOS_0:def11

      func halt S -> Element of S equals [ 0 , {} , {} ];

      coherence by Def9;

    end

    registration

      let S be with_halt standard-ins set;

      cluster ( halt S) -> ins-loc-free;

      coherence ;

    end

    registration

      let S be with_halt standard-ins set;

      cluster ins-loc-free for Element of S;

      existence

      proof

        take ( halt S);

        thus thesis;

      end;

    end

    registration

      let S be with_halt standard-ins set;

      let I be ins-loc-free Element of S;

      cluster ( JumpPart I) -> empty;

      coherence by Def7;

    end

    theorem :: COMPOS_0:12

    for S be homogeneous J/A-independent standard-ins non empty with_halt set, I be Element of S st ( IncAddr (I,k)) = ( halt S) holds I = ( halt S)

    proof

      let S be homogeneous J/A-independent standard-ins non empty with_halt set, I be Element of S;

      assume ( IncAddr (I,k)) = ( halt S);

      then ( IncAddr (I,k)) = ( IncAddr (( halt S),k)) by Th3;

      hence thesis by Th5;

    end;

    definition

      let S be homogeneous J/A-independent standard-ins non empty with_halt set;

      let i be Element of S;

      :: COMPOS_0:def12

      attr i is No-StopCode means i <> ( halt S);

    end

    begin

    definition

      mode Instructions is J/A-independent homogeneous with_halt standard-ins set;

    end

    registration

      cluster non trivial for Instructions;

      existence

      proof

        take { [ 0 , {} , {} ], [1, {} , {} ]};

         [ 0 , {} , {} ] <> [1, {} , {} ] by XTUPLE_0: 3;

        hence thesis by CHAIN_1: 3;

      end;

    end