abcmiz_a.miz



    begin

    reserve i,j for Nat;

    ::$Canceled

    scheme :: ABCMIZ_A:sch1

    MinimalElement { X() -> finite non empty set , R[ set, set] } :

ex x be set st x in X() & for y be set st y in X() holds not R[y, x]

      provided

       A1: for x,y be set st x in X() & y in X() & R[x, y] holds not R[y, x]

       and

       A2: for x,y,z be set st x in X() & y in X() & z in X() & R[x, y] & R[y, z] holds R[x, z];

      assume

       A3: for x be set st x in X() holds ex y be set st y in X() & R[y, x];

      set n = ( card X());

      set x0 = the Element of X();

      defpred P[ Nat, set, set] means $2 in X() implies $3 in X() & R[$3, $2];

      

       A4: for m be Nat st 1 <= m & m < (n + 1) holds for x be set holds ex y be set st P[m, x, y]

      proof

        let m be Nat;

        assume 1 <= m & m < (n + 1);

        let x be set;

        per cases ;

          suppose

           A5: x nin X();

          set y = the set;

          take y;

          thus P[m, x, y] by A5;

        end;

          suppose x in X();

          then

          consider y be set such that

           A6: y in X() & R[y, x] by A3;

          take y;

          thus thesis by A6;

        end;

      end;

      consider p be FinSequence such that

       A7: ( len p) = (n + 1) and

       A8: (p . 1) = x0 or (n + 1) = 0 and

       A9: for i be Nat st 1 <= i & i < (n + 1) holds P[i, (p . i), (p . (i + 1))] from RECDEF_1:sch 3( A4);

      defpred Q[ Nat] means $1 in ( dom p) implies (p . $1) in X();

      

       A10: Q[ 0 ] by FINSEQ_3: 25;

       A11:

      now

        let i be Nat;

        assume

         A12: Q[i];

        thus Q[(i + 1)]

        proof

          assume (i + 1) in ( dom p);

          then (i + 1) <= (n + 1) by A7, FINSEQ_3: 25;

          then

           A13: i < (n + 1) by NAT_1: 13;

          per cases ;

            suppose i = 0 ;

            hence thesis by A8;

          end;

            suppose i > 0 ;

            then i >= ( 0 + 1) & i is Element of NAT by NAT_1: 13, ORDINAL1:def 12;

            hence thesis by A12, A7, A9, A13, FINSEQ_3: 25;

          end;

        end;

      end;

      

       A14: for i be Nat holds Q[i] from NAT_1:sch 2( A10, A11);

      

       A15: ( rng p) c= X()

      proof

        let x be object;

        assume x in ( rng p);

        then ex i be object st i in ( dom p) & x = (p . i) by FUNCT_1:def 3;

        hence thesis by A14;

      end;

      

       A16: for i,j be Nat st 1 <= i & i < j & j <= (n + 1) holds R[(p . j), (p . i)]

      proof

        let i,j be Nat;

        assume

         A17: 1 <= i;

        assume

         A18: i < j;

        then (i + 1) <= j by NAT_1: 13;

        then

        consider k be Nat such that

         A19: j = ((i + 1) + k) by NAT_1: 10;

        assume

         A20: j <= (n + 1);

        then i <= (n + 1) by A18, XXREAL_0: 2;

        then

         A21: i in ( dom p) by A17, A7, FINSEQ_3: 25;

        defpred S[ Nat] means ((i + 1) + $1) <= (n + 1) implies R[(p . ((i + 1) + $1)), (p . i)];

        

         A22: S[ 0 ]

        proof

          assume ((i + 1) + 0 ) <= (n + 1);

          then

           A23: i < (n + 1) by NAT_1: 13;

          (p . i) in X() & i is Element of NAT by A14, A21;

          hence R[(p . ((i + 1) + 0 )), (p . i)] by A9, A17, A23;

        end;

         A24:

        now

          let k be Nat;

          assume

           A25: S[k];

          thus S[(k + 1)]

          proof

            assume

             A26: ((i + 1) + (k + 1)) <= (n + 1);

            

             A27: ((i + 1) + (k + 1)) = (((i + 1) + k) + 1);

            then

             A28: ((i + 1) + k) < (n + 1) by A26, NAT_1: 13;

            

             A29: (p . i) in X() by A14, A21;

            ((i + 1) + k) = (1 + (i + k));

            then

             A30: 1 <= ((i + 1) + k) by NAT_1: 11;

            then ((i + 1) + k) in ( dom p) by A7, A28, FINSEQ_3: 25;

            then

             A31: (p . ((i + 1) + k)) in X() & ((i + 1) + k) is Element of NAT by A14;

            then (p . ((i + 1) + (k + 1))) in X() & R[(p . ((i + 1) + (k + 1))), (p . ((i + 1) + k))] by A9, A28, A27, A30;

            hence R[(p . ((i + 1) + (k + 1))), (p . i)] by A2, A28, A25, A31, A29;

          end;

        end;

        for k be Nat holds S[k] from NAT_1:sch 2( A22, A24);

        hence R[(p . j), (p . i)] by A19, A20;

      end;

      

       A32: ( dom p) = ( Seg (n + 1)) & ( card ( Seg (n + 1))) = (n + 1) by A7, FINSEQ_1: 57, FINSEQ_1:def 3;

      ( Segm ( card ( rng p))) c= ( Segm ( card X())) by A15, CARD_1: 11;

      then ( card ( rng p)) <= n & n < (n + 1) by NAT_1: 19, NAT_1: 39;

      then not (( dom p),( rng p)) are_equipotent by A32, CARD_1: 5;

      then not p is one-to-one by WELLORD2:def 4;

      then

      consider i,j be object such that

       A33: i in ( dom p) & j in ( dom p) & (p . i) = (p . j) & i <> j;

      reconsider i, j as Nat by A33;

      

       A34: 1 <= i & 1 <= j & i <= (n + 1) & j <= (n + 1) by A7, A33, FINSEQ_3: 25;

      (p . i) in ( rng p) by A33, FUNCT_1:def 3;

      then

       A35: (p . i) in X() by A15;

      i < j or j < i by A33, XXREAL_0: 1;

      then R[(p . i), (p . i)] by A16, A33, A34;

      hence contradiction by A1, A35;

    end;

    scheme :: ABCMIZ_A:sch2

    FiniteC { X() -> finite set , P[ set] } :

P[X()]

      provided

       A1: for A be Subset of X() st for B be set st B c< A holds P[B] holds P[A];

      defpred Q[ Nat] means for A be Subset of X() st ( card A) = $1 holds P[A];

      

       A2: for n be Nat st for i be Nat st i < n holds Q[i] holds Q[n]

      proof

        let n be Nat such that

         A3: for i be Nat st i < n holds Q[i];

        let A be Subset of X() such that

         A4: ( card A) = n;

        now

          let B be set such that

           A5: B c< A;

          B c= A by A5;

          then

          reconsider B9 = B as Subset of X() by XBOOLE_1: 1;

          ( card B9) < n by A4, A5, TREES_1: 6;

          hence P[B] by A3;

        end;

        hence thesis by A1;

      end;

      for n be Nat holds Q[n] from NAT_1:sch 4( A2);

      then Q[( card X())] & ( [#] X()) = X();

      hence thesis;

    end;

    scheme :: ABCMIZ_A:sch3

    Numeration { X() -> finite set , R[ set, set] } :

ex s be one-to-one FinSequence st ( rng s) = X() & for i, j st i in ( dom s) & j in ( dom s) & R[(s . i), (s . j)] holds i < j

      provided

       A1: for x,y be set st x in X() & y in X() & R[x, y] holds not R[y, x]

       and

       A2: for x,y,z be set st x in X() & y in X() & z in X() & R[x, y] & R[y, z] holds R[x, z];

      defpred P[ set] means ex s be one-to-one FinSequence st ( rng s) = $1 & for i, j st i in ( dom s) & j in ( dom s) & R[(s . i), (s . j)] holds i < j;

      

       A3: P[ {} ]

      proof

        reconsider s = {} as one-to-one FinSequence;

        take s;

        thus thesis;

      end;

      

       A4: for A be Subset of X() st for B be set st B c< A holds P[B] holds P[A]

      proof

        let A be Subset of X() such that

         A5: for B be set st B c< A holds P[B];

        per cases ;

          suppose A is empty;

          hence P[A] by A3;

        end;

          suppose A is non empty;

          then

          reconsider A9 = A as non empty finite set;

          

           A6: for x,y be set st x in A9 & y in A9 & R[x, y] holds not R[y, x] by A1;

          

           A7: for x,y,z be set st x in A9 & y in A9 & z in A9 & R[x, y] & R[y, z] holds R[x, z] by A2;

          consider x be set such that

           A8: x in A9 & for y be set st y in A9 holds not R[y, x] from MinimalElement( A6, A7);

          set B = (A \ {x});

          

           A9: x nin B & B c= A by ZFMISC_1: 56;

          then B c< A by A8;

          then

          consider s be one-to-one FinSequence such that

           A10: ( rng s) = B and

           A11: for i, j st i in ( dom s) & j in ( dom s) & R[(s . i), (s . j)] holds i < j by A5;

           <*x*> is one-to-one & ( rng <*x*>) = {x} & {x} misses B by FINSEQ_1: 39, FINSEQ_3: 93, XBOOLE_1: 79;

          then

          reconsider s9 = ( <*x*> ^ s) as one-to-one FinSequence by A10, FINSEQ_3: 91;

          

           A12: {x} c= A by A8, ZFMISC_1: 31;

          

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

          thus P[A]

          proof

            take s9;

            

            thus ( rng s9) = (( rng <*x*>) \/ ( rng s)) by FINSEQ_1: 31

            .= ( {x} \/ B) by A10, FINSEQ_1: 38

            .= A by A12, XBOOLE_1: 45;

            let i, j such that

             A14: i in ( dom s9) & j in ( dom s9) & R[(s9 . i), (s9 . j)];

            

             A15: ( dom <*x*>) = ( Seg 1) by FINSEQ_1: 38;

            per cases by A13, A14, FINSEQ_1: 25;

              suppose i in ( dom <*x*>) & j in ( dom <*x*>);

              then i = 1 & j = 1 by A15, FINSEQ_1: 2, TARSKI:def 1;

              then (s9 . i) = x & (s9 . j) = x by FINSEQ_1: 41;

              hence i < j by A8, A14;

            end;

              suppose

               A16: i in ( dom <*x*>) & ex n be Nat st n in ( dom s) & j = (1 + n);

              then

               A17: i = 1 by A15, FINSEQ_1: 2, TARSKI:def 1;

              consider n be Nat such that

               A18: n in ( dom s) & j = (1 + n) by A16;

              1 <= n by A18, FINSEQ_3: 25;

              hence i < j by A17, A18, NAT_1: 13;

            end;

              suppose

               A19: j in ( dom <*x*>) & ex n be Nat st n in ( dom s) & i = (1 + n);

              then j = 1 by A15, FINSEQ_1: 2, TARSKI:def 1;

              then

               A20: (s9 . j) = x by FINSEQ_1: 41;

              consider n be Nat such that

               A21: n in ( dom s) & i = (1 + n) by A19;

              (s9 . i) = (s . n) by A13, A21, FINSEQ_1:def 7;

              then (s9 . i) in ( rng s) by A21, FUNCT_1:def 3;

              hence i < j by A8, A14, A20, A9, A10;

            end;

              suppose (ex n be Nat st n in ( dom s) & i = (1 + n)) & ex n be Nat st n in ( dom s) & j = (1 + n);

              then

              consider ni,nj be Nat such that

               A22: ni in ( dom s) & i = (1 + ni) & nj in ( dom s) & j = (1 + nj);

              (s9 . i) = (s . ni) & (s9 . j) = (s . nj) by A13, A22, FINSEQ_1:def 7;

              then ni < nj by A11, A14, A22;

              hence i < j by A22, XREAL_1: 6;

            end;

          end;

        end;

      end;

      thus P[X()] from FiniteC( A4);

    end;

    theorem :: ABCMIZ_A:2

    

     Th2: for x be variable holds ( varcl ( vars x)) = ( vars x)

    proof

      let x be variable;

      x in Vars ;

      then

      consider A be Subset of Vars , j be Element of NAT such that

       A1: x = [( varcl A), j] & A is finite by ABCMIZ_1: 18;

      ( vars x) = ( varcl A) by A1;

      hence thesis;

    end;

    theorem :: ABCMIZ_A:3

    

     Th3: for C be initialized ConstructorSignature holds for e be expression of C holds e is compound iff not ex x be Element of Vars st e = (x -term C)

    proof

      let C be initialized ConstructorSignature;

      let e be expression of C;

      (ex x be variable st e = (x -term C)) or (ex c be constructor OperSymbol of C st ex p be FinSequence of ( QuasiTerms C) st ( len p) = ( len ( the_arity_of c)) & e = (c -trm p)) or (ex a be expression of C, ( an_Adj C) st e = (( non_op C) term a)) or (ex a be expression of C, ( an_Adj C) st ex t be expression of C, ( a_Type C) st e = (( ast C) term (a,t))) by ABCMIZ_1: 53;

      hence thesis;

    end;

    begin

    registration

      cluster empty for quasi-loci;

      existence by ABCMIZ_1: 29;

    end

    definition

      let C be ConstructorSignature;

      :: ABCMIZ_A:def1

      attr C is standardized means

      : Def1: for o be OperSymbol of C st o is constructor holds o in Constructors & (o `1 ) = ( the_result_sort_of o) & ( card ((o `2 ) `1 )) = ( len ( the_arity_of o));

    end

    theorem :: ABCMIZ_A:4

    

     Th4: for C be ConstructorSignature st C is standardized holds for o be OperSymbol of C holds o is constructor iff o in Constructors

    proof

      let C be ConstructorSignature such that

       A1: C is standardized;

      let o be OperSymbol of C;

      thus o is constructor implies o in Constructors by A1;

      assume o in Constructors ;

      then not o in { * , non_op } by ABCMIZ_1: 39, XBOOLE_0: 3;

      hence o <> * & o <> non_op by TARSKI:def 2;

    end;

    registration

      cluster MaxConstrSign -> standardized;

      coherence

      proof

        let o be OperSymbol of MaxConstrSign ;

        

         A1: the carrier' of MaxConstrSign = ( { * , non_op } \/ Constructors ) by ABCMIZ_1:def 24;

        assume

         A2: o is constructor;

        then

         A3: (the ResultSort of MaxConstrSign . o) = (o `1 ) & ( card (the Arity of MaxConstrSign . o)) = ( card ((o `2 ) `1 )) by ABCMIZ_1:def 24;

        o <> * & o <> non_op by A2;

        then not o in { * , non_op } by TARSKI:def 2;

        hence thesis by A3, A1, XBOOLE_0:def 3;

      end;

    end

    registration

      cluster initialized standardized strict for ConstructorSignature;

      existence

      proof

        take MaxConstrSign ;

        thus thesis;

      end;

    end

    definition

      let C be initialized standardized ConstructorSignature;

      let c be constructor OperSymbol of C;

      :: ABCMIZ_A:def2

      func loci_of c -> quasi-loci equals ((c `2 ) `1 );

      coherence

      proof

        reconsider c as Element of Constructors by Th4;

        ( loci_of c) is quasi-loci;

        hence thesis;

      end;

    end

    registration

      let C be ConstructorSignature;

      cluster constructor for Subsignature of C;

      existence

      proof

        reconsider S = C as Subsignature of C by INSTALG1: 15;

        take S;

        thus thesis;

      end;

    end

    registration

      let C be initialized ConstructorSignature;

      cluster initialized for constructor Subsignature of C;

      existence

      proof

        reconsider S = C as constructor Subsignature of C by INSTALG1: 15;

        take S;

        thus thesis;

      end;

    end

    registration

      let C be standardized ConstructorSignature;

      cluster -> standardized for constructor Subsignature of C;

      coherence

      proof

        let S be constructor Subsignature of C;

        let o be OperSymbol of S such that

         A1: o <> * & o <> non_op ;

        

         A2: the carrier' of S c= the carrier' of C by INSTALG1: 10;

        reconsider c = o as OperSymbol of C by A2;

        

         A3: c is constructor by A1;

        the Arity of S = (the Arity of C | the carrier' of S) & the ResultSort of S = (the ResultSort of C | the carrier' of S) by INSTALG1: 12;

        then ( the_result_sort_of c) = ( the_result_sort_of o) & ( the_arity_of c) = ( the_arity_of o) by FUNCT_1: 49;

        hence thesis by A3, Def1;

      end;

    end

    theorem :: ABCMIZ_A:5

    for S1,S2 be standardized ConstructorSignature st the carrier' of S1 = the carrier' of S2 holds the ManySortedSign of S1 = the ManySortedSign of S2

    proof

      let S1,S2 be standardized ConstructorSignature such that

       A1: the carrier' of S1 = the carrier' of S2;

      

       A2: the carrier of S1 = 3 & the carrier of S2 = 3 by ABCMIZ_1:def 9, YELLOW11: 1;

      now

        let o be OperSymbol of S1;

        reconsider o2 = o as OperSymbol of S2 by A1;

        per cases ;

          suppose o = * or o = non_op ;

          then (the Arity of S1 . o) = <* an_Adj *> & (the Arity of S2 . o) = <* an_Adj *> or (the Arity of S1 . o) = <* an_Adj , a_Type *> & (the Arity of S2 . o) = <* an_Adj , a_Type *> by ABCMIZ_1:def 9;

          hence (the Arity of S1 . o) = (the Arity of S2 . o);

        end;

          suppose o is constructor & o2 is constructor;

          then ( card ((o `2 ) `1 )) = ( len ( the_arity_of o)) & ( card ((o `2 ) `1 )) = ( len ( the_arity_of o2)) & ( the_arity_of o) = (( len ( the_arity_of o)) |-> a_Term ) & ( the_arity_of o2) = (( len ( the_arity_of o2)) |-> a_Term ) by Def1, ABCMIZ_1: 37;

          

          hence (the Arity of S1 . o) = ( the_arity_of o2)

          .= (the Arity of S2 . o);

        end;

      end;

      then

       A3: the Arity of S1 = the Arity of S2 by A1, A2, FUNCT_2: 63;

      now

        let o be OperSymbol of S1;

        reconsider o2 = o as OperSymbol of S2 by A1;

        per cases ;

          suppose o = * or o = non_op ;

          then (the ResultSort of S1 . o) = a_Type & (the ResultSort of S2 . o) = a_Type or (the ResultSort of S1 . o) = an_Adj & (the ResultSort of S2 . o) = an_Adj by ABCMIZ_1:def 9;

          hence (the ResultSort of S1 . o) = (the ResultSort of S2 . o);

        end;

          suppose o is constructor & o2 is constructor;

          then ( the_result_sort_of o) = (o `1 ) & ( the_result_sort_of o2) = (o `1 ) by Def1;

          

          hence (the ResultSort of S1 . o) = ( the_result_sort_of o2)

          .= (the ResultSort of S2 . o);

        end;

      end;

      hence thesis by A1, A2, A3, FUNCT_2: 63;

    end;

    theorem :: ABCMIZ_A:6

    for C be ConstructorSignature holds C is standardized iff C is Subsignature of MaxConstrSign

    proof

      let C be ConstructorSignature;

      

       A1: the carrier' of MaxConstrSign = ( { * , non_op } \/ Constructors ) by ABCMIZ_1:def 24;

      

       A2: ( dom the Arity of MaxConstrSign ) = the carrier' of MaxConstrSign by FUNCT_2:def 1;

      

       A3: ( dom the ResultSort of MaxConstrSign ) = the carrier' of MaxConstrSign by FUNCT_2:def 1;

      thus C is standardized implies C is Subsignature of MaxConstrSign

      proof

        assume

         A4: for o be OperSymbol of C st o is constructor holds o in Constructors & (o `1 ) = ( the_result_sort_of o) & ( card ((o `2 ) `1 )) = ( len ( the_arity_of o));

        

         A5: the carrier of C = 3 & the carrier of MaxConstrSign = 3 by ABCMIZ_1:def 9, YELLOW11: 1;

        

         A6: the Arity of C c= the Arity of MaxConstrSign

        proof

          let x,y be object;

          assume

           A7: [x, y] in the Arity of C;

          then

          reconsider x as OperSymbol of C by ZFMISC_1: 87;

          x = * or x = non_op or x is constructor;

          then x in { * , non_op } or x in Constructors by A4, TARSKI:def 2;

          then

          reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def 3;

          

           A8: y = (the Arity of C . x) by A7, FUNCT_1: 1;

          per cases ;

            suppose x = * or x = non_op ;

            then c = * & y = <* an_Adj , a_Type *> or c = non_op & y = <* an_Adj *> by A8, ABCMIZ_1:def 9;

            then y = (the Arity of MaxConstrSign . c) by ABCMIZ_1:def 9;

            hence thesis by A2, FUNCT_1:def 2;

          end;

            suppose

             A9: x is constructor;

            then

             A10: x <> * & x <> non_op ;

            then

             A11: c is constructor;

            reconsider y as set by TARSKI: 1;

            ( card ((x `2 ) `1 )) = ( len ( the_arity_of x)) by A4, A9

            .= ( card y) by A7, FUNCT_1: 1;

            then

             A12: ( card y) = ( card (the Arity of MaxConstrSign . c)) by A11, ABCMIZ_1:def 24;

            y in ( { a_Term } * ) & (the Arity of MaxConstrSign . c) in ( { a_Term } * ) by A8, A10, ABCMIZ_1:def 9;

            then y = (the Arity of MaxConstrSign . c) by A12, ABCMIZ_1: 6;

            hence thesis by A2, FUNCT_1:def 2;

          end;

        end;

        the ResultSort of C c= the ResultSort of MaxConstrSign

        proof

          let x,y be object;

          assume

           A13: [x, y] in the ResultSort of C;

          then

          reconsider x as OperSymbol of C by ZFMISC_1: 87;

          x is constructor or x = * or x = non_op ;

          then x in { * , non_op } or x in Constructors by A4, TARSKI:def 2;

          then

          reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def 3;

          

           A14: y = (the ResultSort of C . x) by A13, FUNCT_1: 1;

          per cases ;

            suppose x = * or x = non_op ;

            then c = * & y = a_Type or c = non_op & y = an_Adj by A14, ABCMIZ_1:def 9;

            then y = (the ResultSort of MaxConstrSign . c) by ABCMIZ_1:def 9;

            hence thesis by A3, FUNCT_1:def 2;

          end;

            suppose

             A15: x is constructor & c is constructor;

            

            then (x `1 ) = ( the_result_sort_of x) by A4

            .= y by A13, FUNCT_1: 1;

            

            then y = ( the_result_sort_of c) by A15, Def1

            .= (the ResultSort of MaxConstrSign . c);

            hence thesis by A3, FUNCT_1:def 2;

          end;

        end;

        hence thesis by A5, A6, INSTALG1: 13;

      end;

      assume

       A16: C is Subsignature of MaxConstrSign ;

      let o be OperSymbol of C such that

       A17: o <> * & o <> non_op ;

      the carrier' of C c= the carrier' of MaxConstrSign & o in the carrier' of C by A16, INSTALG1: 10;

      then

      reconsider c = o as OperSymbol of MaxConstrSign ;

      

       A18: c is constructor by A17;

       not c in { * , non_op } by A17, TARSKI:def 2;

      hence o in Constructors by A1, XBOOLE_0:def 3;

      

      thus (o `1 ) = (the ResultSort of MaxConstrSign . c) by A18, ABCMIZ_1:def 24

      .= ((the ResultSort of MaxConstrSign | the carrier' of C) . o) by FUNCT_1: 49

      .= (the ResultSort of C . o) by A16, INSTALG1: 12

      .= ( the_result_sort_of o);

      

      thus ( card ((o `2 ) `1 )) = ( card (the Arity of MaxConstrSign . c)) by A18, ABCMIZ_1:def 24

      .= ( card ((the Arity of MaxConstrSign | the carrier' of C) . o)) by FUNCT_1: 49

      .= ( card (the Arity of C . o)) by A16, INSTALG1: 12

      .= ( len ( the_arity_of o));

    end;

    registration

      let C be initialized ConstructorSignature;

      cluster non compound for quasi-term of C;

      existence

      proof

        set x = the Element of Vars ;

        take (x -term C);

        thus thesis;

      end;

    end

    registration

      cluster -> pair for Element of Vars ;

      coherence

      proof

        let x be Element of Vars ;

         Vars = { [( varcl A), j] where A be Subset of Vars , j be Element of NAT : A is finite } & x in Vars by ABCMIZ_1: 18;

        then ex A be Subset of Vars , j be Element of NAT st x = [( varcl A), j] & A is finite;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_A:7

    

     Th7: for x be Element of Vars st ( vars x) is natural holds ( vars x) = 0

    proof

      let x be Element of Vars ;

      assume (x `1 ) is natural;

      then

      reconsider n = (x `1 ) as Element of NAT ;

       Vars = { [( varcl A), j] where A be Subset of Vars , j be Element of NAT : A is finite } & x in Vars by ABCMIZ_1: 18;

      then

      consider A be Subset of Vars , j be Element of NAT such that

       A1: x = [( varcl A), j] & A is finite;

      set i = the Element of n;

      assume

       A2: (x `1 ) <> 0 ;

      then

       A3: i in n;

      reconsider i as Element of NAT by A2, ORDINAL1: 10;

      n = ( varcl A) & ( vars x) c= Vars by A1;

      then i in Vars by A3;

      hence thesis;

    end;

    theorem :: ABCMIZ_A:8

    

     Th8: Vars misses Constructors

    proof

      assume Vars meets Constructors ;

      then

      consider x be object such that

       A1: x in Vars & x in Constructors by XBOOLE_0: 3;

      reconsider x as Element of Vars by A1;

      consider A be Subset of Vars , j be Element of NAT such that

       A2: x = [( varcl A), j] & A is finite by A1, ABCMIZ_1: 18;

      x in ( Modes \/ Attrs ) or x in Funcs by A1, XBOOLE_0:def 3;

      then x in Modes or x in Attrs or x in Funcs by XBOOLE_0:def 3;

      then (x `2 ) in [: QuasiLoci , NAT :] & (x `2 ) = j by A2, MCART_1: 10;

      then ex a,b be object st a in QuasiLoci & b in NAT & [a, b] = j by ZFMISC_1:def 2;

      hence thesis;

    end;

    theorem :: ABCMIZ_A:9

    for x be Element of Vars holds x <> * & x <> non_op ;

    theorem :: ABCMIZ_A:10

    

     Th10: for C be standardized ConstructorSignature holds Vars misses the carrier' of C

    proof

      let C be standardized ConstructorSignature;

      assume Vars meets the carrier' of C;

      then

      consider x be object such that

       A1: x in Vars & x in the carrier' of C by XBOOLE_0: 3;

      reconsider x as Element of Vars by A1;

      reconsider c = x as OperSymbol of C by A1;

      x = * or x = non_op or c is constructor;

      then x = * or x = non_op or x in Constructors & Vars misses Constructors by Th8, Def1;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: ABCMIZ_A:11

    

     Th11: for C be initialized standardized ConstructorSignature holds for e be expression of C holds (ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ]) or (ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op ))

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      set X = ( MSVars C);

      set Y = (X (\/) (the carrier of C --> { 0 }));

      reconsider q = e as Term of C, Y by MSAFREE3: 8;

      per cases by MSATERM: 2;

        suppose ex s be SortSymbol of C, v be Element of (Y . s) st (q . {} ) = [v, s];

        then

        consider s be SortSymbol of C, v be Element of (Y . s) such that

         A1: (q . {} ) = [v, s];

        consider z be object such that

         A2: z in ( dom the Sorts of ( Free (C,X))) & e in (the Sorts of ( Free (C,X)) . z) by CARD_5: 2;

        reconsider z as SortSymbol of C by A2;

        the carrier of C = { a_Type , an_Adj , a_Term } by ABCMIZ_1:def 9;

        then

         A3: z = a_Type or z = an_Adj or z = a_Term by ENUMSET1:def 1;

        

         A4: q = ( root-tree [v, s]) by A1, MSATERM: 5;

        then

         A5: ( the_sort_of q) = s by MSATERM: 14;

        

         A6: the Sorts of ( Free (C,X)) = (C -Terms (X,Y)) by MSAFREE3: 24;

        then the Sorts of ( Free (C,X)) c= the Sorts of ( FreeMSA Y) by PBOOLE:def 18;

        then (the Sorts of ( Free (C,X)) . z) c= (the Sorts of ( FreeMSA Y) . z) & ( FreeMSA Y) = MSAlgebra (# ( FreeSort Y), ( FreeOper Y) #);

        then q in (the Sorts of ( FreeMSA Y) . z) & (the Sorts of ( FreeMSA Y) . z) = ( FreeSort (Y,z)) by A2, MSAFREE:def 11;

        then

         A7: s = z by A5, MSATERM:def 5;

        then v in (( MSVars C) . z) by A4, A2, A6, MSAFREE3: 18;

        then

         A8: v in Vars & z = a_Term by A3, ABCMIZ_1:def 25;

        then

        reconsider x = v as Element of Vars ;

        e = (x -term C) by A1, A7, A8, MSATERM: 5;

        hence thesis by A1, A7, A8;

      end;

        suppose (q . {} ) in [:the carrier' of C, {the carrier of C}:];

        then

        consider o,s be object such that

         A9: o in the carrier' of C & s in {the carrier of C} & (q . {} ) = [o, s] by ZFMISC_1:def 2;

        reconsider o as OperSymbol of C by A9;

        o is constructor iff o <> * & o <> non_op ;

        then s = the carrier of C & (o in Constructors or o = * or o = non_op ) by A9, Def1, TARSKI:def 1;

        hence thesis by A9;

      end;

    end;

    registration

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      cluster (e . {} ) -> pair;

      coherence

      proof

        (ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ]) or (ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op )) by Th11;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_A:12

    

     Th12: for C be initialized ConstructorSignature holds for e be expression of C holds for o be OperSymbol of C st (e . {} ) = [o, the carrier of C] holds e is expression of C, ( the_result_sort_of o)

    proof

      let C be initialized ConstructorSignature;

      let e be expression of C;

      let o be OperSymbol of C such that

       A1: (e . {} ) = [o, the carrier of C];

      set X = ( MSVars C), Y = (X (\/) (the carrier of C --> { 0 }));

      reconsider t = e as Term of C, Y by MSAFREE3: 8;

      ( variables_in t) c= X by MSAFREE3: 27;

      then e in { t1 where t1 be Term of C, Y : ( the_sort_of t1) = ( the_sort_of t) & ( variables_in t1) c= X };

      then e in ((C -Terms (X,Y)) . ( the_sort_of t)) by MSAFREE3:def 5;

      then

       A2: e in (the Sorts of ( Free (C,X)) . ( the_sort_of t)) by MSAFREE3: 24;

      ( the_sort_of t) = ( the_result_sort_of o) by A1, MSATERM: 17;

      hence thesis by A2, ABCMIZ_1:def 28;

    end;

    theorem :: ABCMIZ_A:13

    

     Th13: for C be initialized standardized ConstructorSignature holds for e be expression of C holds (((e . {} ) `1 ) = * implies e is expression of C, ( a_Type C)) & (((e . {} ) `1 ) = non_op implies e is expression of C, ( an_Adj C))

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      per cases by Th11;

        suppose ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ];

        then

        consider x be Element of Vars such that

         A1: e = (x -term C) & (e . {} ) = [x, a_Term ];

        thus thesis by A1;

      end;

        suppose (ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op ));

        then

        consider o be OperSymbol of C such that

         A2: (e . {} ) = [o, the carrier of C];

        set X = ( MSVars C), Y = (X (\/) (the carrier of C --> { 0 }));

        reconsider t = e as Term of C, Y by MSAFREE3: 8;

        ( variables_in t) c= X by MSAFREE3: 27;

        then e in { t1 where t1 be Term of C, Y : ( the_sort_of t1) = ( the_sort_of t) & ( variables_in t1) c= X };

        then e in ((C -Terms (X,Y)) . ( the_sort_of t)) by MSAFREE3:def 5;

        then

         A3: e in (the Sorts of ( Free (C,X)) . ( the_sort_of t)) by MSAFREE3: 24;

        

         A4: ( the_result_sort_of ( non_op C)) = ( an_Adj C) & ( the_result_sort_of ( ast C)) = ( a_Type C) by ABCMIZ_1: 38;

        

         A5: ((e . {} ) `1 ) = o & ( non_op C) = non_op & ( ast C) = * by A2;

        ( the_sort_of t) = ( the_result_sort_of o) by A2, MSATERM: 17;

        hence thesis by A3, A4, A5, ABCMIZ_1:def 28;

      end;

    end;

    theorem :: ABCMIZ_A:14

    

     Th14: for C be initialized standardized ConstructorSignature holds for e be expression of C holds ((e . {} ) `1 ) in Vars & ((e . {} ) `2 ) = a_Term & e is quasi-term of C or ((e . {} ) `2 ) = the carrier of C & (((e . {} ) `1 ) in Constructors & ((e . {} ) `1 ) in the carrier' of C or ((e . {} ) `1 ) = * or ((e . {} ) `1 ) = non_op )

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      per cases by Th11;

        suppose ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ];

        then

        consider x be Element of Vars such that

         A1: e = (x -term C) & (e . {} ) = [x, a_Term ];

        thus thesis by A1;

      end;

        suppose ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op );

        then

        consider o be OperSymbol of C such that

         A2: (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op );

        thus thesis by A2;

      end;

    end;

    theorem :: ABCMIZ_A:15

    for C be initialized standardized ConstructorSignature holds for e be expression of C st ((e . {} ) `1 ) in Constructors holds e in (the Sorts of ( Free (C,( MSVars C))) . (((e . {} ) `1 ) `1 ))

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      assume

       A1: ((e . {} ) `1 ) in Constructors ;

      per cases by Th11;

        suppose ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ];

        then

        consider x be Element of Vars such that

         A2: e = (x -term C) & (e . {} ) = [x, a_Term ];

        ((e . {} ) `1 ) = x by A2;

        hence thesis by A1, Th8, XBOOLE_0: 3;

      end;

        suppose ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op );

        then

        consider o be OperSymbol of C such that

         A3: (e . {} ) = [o, the carrier of C];

        

         A4: ((e . {} ) `1 ) = o by A3;

         * in { * , non_op } & non_op in { * , non_op } by TARSKI:def 2;

        then o <> * & o <> non_op by A1, A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        then

         A5: o is constructor;

        set X = ( MSVars C);

        reconsider t = e as Term of C, (X (\/) (the carrier of C --> { 0 })) by MSAFREE3: 8;

        

         A6: ( the_sort_of t) = ( the_result_sort_of o) by A3, MSATERM: 17

        .= (o `1 ) by A5, Def1;

        ( variables_in t) c= X by MSAFREE3: 27;

        then e in { t1 where t1 be Term of C, (X (\/) (the carrier of C --> { 0 })) : ( the_sort_of t1) = ( the_sort_of t) & ( variables_in t1) c= X };

        then e in ((C -Terms (X,(X (\/) (the carrier of C --> { 0 })))) . ( the_sort_of t)) by MSAFREE3:def 5;

        hence e in (the Sorts of ( Free (C,( MSVars C))) . (((e . {} ) `1 ) `1 )) by A4, A6, MSAFREE3: 23;

      end;

    end;

    theorem :: ABCMIZ_A:16

    for C be initialized standardized ConstructorSignature holds for e be expression of C holds not ((e . {} ) `1 ) in Vars iff ((e . {} ) `1 ) is OperSymbol of C

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C;

      

       A1: ((e . {} ) `1 ) in Vars or ((e . {} ) `1 ) in the carrier' of C or ((e . {} ) `1 ) = ( ast C) or ((e . {} ) `1 ) = ( non_op C) by Th14;

       Vars misses the carrier' of C by Th10;

      hence not ((e . {} ) `1 ) in Vars iff ((e . {} ) `1 ) is OperSymbol of C by A1, XBOOLE_0: 3;

    end;

    theorem :: ABCMIZ_A:17

    

     Th17: for C be initialized standardized ConstructorSignature holds for e be expression of C st ((e . {} ) `1 ) in Vars holds ex x be Element of Vars st x = ((e . {} ) `1 ) & e = (x -term C)

    proof

      let C be initialized standardized ConstructorSignature;

      let t be expression of C such that

       A1: ((t . {} ) `1 ) in Vars ;

      set X = ( MSVars C);

      set V = (X (\/) (the carrier of C --> { 0 }));

      reconsider q = t as Term of C, V by MSAFREE3: 8;

      per cases by MSATERM: 2;

        suppose (q . {} ) in [:the carrier' of C, {the carrier of C}:];

        then ((q . {} ) `1 ) in the carrier' of C & the carrier' of C misses Vars by Th10, MCART_1: 10;

        hence thesis by A1, XBOOLE_0: 3;

      end;

        suppose ex s be SortSymbol of C, v be Element of (V . s) st (q . {} ) = [v, s];

        then

        consider s be SortSymbol of C, v be Element of (V . s) such that

         A2: (t . {} ) = [v, s];

        

         A3: q = ( root-tree [v, s]) by A2, MSATERM: 5;

        reconsider x = v as Element of Vars by A1, A2;

        take x;

        the carrier of C = { a_Type , an_Adj , a_Term } by ABCMIZ_1:def 9;

        then

         A4: s = a_Term or s = a_Type or s = an_Adj by ENUMSET1:def 1;

        ((the carrier of C --> { 0 }) . s) = { 0 };

        then (V . s) = ((X . s) \/ { 0 }) by PBOOLE:def 4;

        then

         A5: s = a_Term or (V . s) = ( {} \/ { 0 }) by A4, ABCMIZ_1:def 25;

        v in (V . s) & x <> 0 ;

        hence thesis by A2, A3, A5;

      end;

    end;

    theorem :: ABCMIZ_A:18

    

     Th18: for C be initialized standardized ConstructorSignature holds for e be expression of C st ((e . {} ) `1 ) = * holds ex a be expression of C, ( an_Adj C), q be expression of C, ( a_Type C) st e = ( [ * , 3] -tree (a,q))

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C such that

       A1: ((e . {} ) `1 ) = * ;

       not ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ] by A1;

      then

      consider o be OperSymbol of C such that

       A2: (e . {} ) = [o, the carrier of C] and o in Constructors or o = * or o = non_op by Th11;

      set Y = (( MSVars C) (\/) (the carrier of C --> { 0 }));

      reconsider t = e as Term of C, (( MSVars C) (\/) (the carrier of C --> { 0 })) by MSAFREE3: 8;

      consider aa be ArgumentSeq of ( Sym (o,(( MSVars C) (\/) (the carrier of C --> { 0 })))) such that

       A3: t = ( [o, the carrier of C] -tree aa) by A2, MSATERM: 10;

      

       A4: * = ( [o, the carrier of C] `1 ) by A1, A3, TREES_4:def 4

      .= o;

      

       A5: ( the_arity_of ( ast C)) = <*( an_Adj C), ( a_Type C)*> by ABCMIZ_1: 38;

      

       A6: ( len aa) = ( len ( the_arity_of o)) by MSATERM: 22

      .= 2 by A4, A5, FINSEQ_1: 44;

      then ( dom aa) = ( Seg 2) by FINSEQ_1:def 3;

      then

       A7: 1 in ( dom aa) & 2 in ( dom aa);

      then

      reconsider t1 = (aa . 1), t2 = (aa . 2) as Term of C, (( MSVars C) (\/) (the carrier of C --> { 0 })) by MSATERM: 22;

      

       A8: ( len ( doms aa)) = ( len aa) by TREES_3: 38;

      (( doms aa) . 1) = ( dom t1) & (( doms aa) . 2) = ( dom t2) by A7, FUNCT_6: 22;

      then

       A9: 0 < 2 & ( 0 + 1) = 1 & 1 < 2 & (1 + 1) = 2 & {} in (( doms aa) . 1) & {} in (( doms aa) . 2) & ( <* 0 *> ^ ( <*> NAT )) = <* 0 *> & ( <*1*> ^ ( <*> NAT )) = <*1*> by FINSEQ_1: 34, TREES_1: 22;

      ( dom t) = ( tree ( doms aa)) by A3, TREES_4: 10;

      then

      reconsider 00 = <* 0 *>, 01 = <*1*> as Element of ( dom t) by A6, A8, A9, TREES_3:def 15;

       0 < 2 & 1 = ( 0 + 1) & 1 < 2 & 2 = (1 + 1) & aa is DTree-yielding;

      then t1 = (t | 00) & t2 = (t | 01) by A3, A6, TREES_4:def 4;

      then

       A10: t1 is expression of C & t2 is expression of C & ( variables_in t1) c= ( variables_in t) & ( variables_in t2) c= ( variables_in t) by MSAFREE3: 32, MSAFREE3: 33;

      then

       A11: ( variables_in t1) c= ( MSVars C) & ( variables_in t2) c= ( MSVars C) by MSAFREE3: 27;

      ( the_sort_of t1) = (( the_arity_of o) . 1) by A7, MSATERM: 23

      .= ( an_Adj C) by A4, A5, FINSEQ_1: 44;

      then t1 in { s where s be Term of C, Y : ( the_sort_of s) = ( an_Adj C) & ( variables_in s) c= ( MSVars C) } by A11;

      then t1 in ((C -Terms (( MSVars C),Y)) . ( an_Adj C)) by MSAFREE3:def 5;

      then t1 in (the Sorts of ( Free (C,( MSVars C))) . ( an_Adj C)) by MSAFREE3: 24;

      then

      reconsider a = t1 as expression of C, ( an_Adj C) by A10, ABCMIZ_1:def 28;

      ( the_sort_of t2) = (( the_arity_of o) . 2) by A7, MSATERM: 23

      .= ( a_Type C) by A4, A5, FINSEQ_1: 44;

      then t2 in { s where s be Term of C, Y : ( the_sort_of s) = ( a_Type C) & ( variables_in s) c= ( MSVars C) } by A11;

      then t2 in ((C -Terms (( MSVars C),Y)) . ( a_Type C)) by MSAFREE3:def 5;

      then t2 in (the Sorts of ( Free (C,( MSVars C))) . ( a_Type C)) by MSAFREE3: 24;

      then

      reconsider q = t2 as expression of C, ( a_Type C) by A10, ABCMIZ_1:def 28;

      take a, q;

      

       A12: the carrier of C = 3 by ABCMIZ_1:def 9, YELLOW11: 1;

      aa = <*a, q*> by A6, FINSEQ_1: 44;

      hence thesis by A3, A4, A12, TREES_4:def 6;

    end;

    theorem :: ABCMIZ_A:19

    

     Th19: for C be initialized standardized ConstructorSignature holds for e be expression of C st ((e . {} ) `1 ) = non_op holds ex a be expression of C, ( an_Adj C) st e = ( [ non_op , 3] -tree a)

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C such that

       A1: ((e . {} ) `1 ) = non_op ;

       not ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ] by A1;

      then

      consider o be OperSymbol of C such that

       A2: (e . {} ) = [o, the carrier of C] and o in Constructors or o = * or o = non_op by Th11;

      set Y = (( MSVars C) (\/) (the carrier of C --> { 0 }));

      reconsider t = e as Term of C, (( MSVars C) (\/) (the carrier of C --> { 0 })) by MSAFREE3: 8;

      consider aa be ArgumentSeq of ( Sym (o,(( MSVars C) (\/) (the carrier of C --> { 0 })))) such that

       A3: t = ( [o, the carrier of C] -tree aa) by A2, MSATERM: 10;

      

       A4: non_op = ( [o, the carrier of C] `1 ) by A1, A3, TREES_4:def 4

      .= o;

      

       A5: ( the_arity_of ( non_op C)) = <*( an_Adj C)*> by ABCMIZ_1: 38;

      

       A6: ( len aa) = ( len ( the_arity_of o)) by MSATERM: 22

      .= 1 by A4, A5, FINSEQ_1: 40;

      then ( dom aa) = ( Seg 1) by FINSEQ_1:def 3;

      then

       A7: 1 in ( dom aa);

      then

      reconsider t1 = (aa . 1) as Term of C, (( MSVars C) (\/) (the carrier of C --> { 0 })) by MSATERM: 22;

      

       A8: ( len ( doms aa)) = ( len aa) by TREES_3: 38;

      (( doms aa) . 1) = ( dom t1) by A7, FUNCT_6: 22;

      then

       A9: 0 < 1 & ( 0 + 1) = 1 & {} in (( doms aa) . 1) & ( <* 0 *> ^ ( <*> NAT )) = <* 0 *> by FINSEQ_1: 34, TREES_1: 22;

      ( dom t) = ( tree ( doms aa)) by A3, TREES_4: 10;

      then

      reconsider 00 = <* 0 *> as Element of ( dom t) by A6, A8, A9, TREES_3:def 15;

      t1 = (t | 00) by A3, A6, A9, TREES_4:def 4;

      then

       A10: t1 is expression of C & ( variables_in t1) c= ( variables_in t) by MSAFREE3: 32, MSAFREE3: 33;

      then

       A11: ( variables_in t1) c= ( MSVars C) by MSAFREE3: 27;

      ( the_sort_of t1) = (( the_arity_of o) . 1) by A7, MSATERM: 23

      .= ( an_Adj C) by A4, A5, FINSEQ_1: 40;

      then t1 in { s where s be Term of C, Y : ( the_sort_of s) = ( an_Adj C) & ( variables_in s) c= ( MSVars C) } by A11;

      then t1 in ((C -Terms (( MSVars C),Y)) . ( an_Adj C)) by MSAFREE3:def 5;

      then t1 in (the Sorts of ( Free (C,( MSVars C))) . ( an_Adj C)) by MSAFREE3: 24;

      then

      reconsider a = t1 as expression of C, ( an_Adj C) by A10, ABCMIZ_1:def 28;

      take a;

      

       A12: the carrier of C = 3 by ABCMIZ_1:def 9, YELLOW11: 1;

      aa = <*a*> by A6, FINSEQ_1: 40;

      hence thesis by A3, A4, A12, TREES_4:def 5;

    end;

    theorem :: ABCMIZ_A:20

    

     Th20: for C be initialized standardized ConstructorSignature holds for e be expression of C st ((e . {} ) `1 ) in Constructors holds ex o be OperSymbol of C st o = ((e . {} ) `1 ) & ( the_result_sort_of o) = (o `1 ) & e is expression of C, ( the_result_sort_of o)

    proof

      let C be initialized standardized ConstructorSignature;

      let e be expression of C such that

       A1: ((e . {} ) `1 ) in Constructors ;

      per cases by Th11;

        suppose ex x be Element of Vars st e = (x -term C) & (e . {} ) = [x, a_Term ];

        then

        consider x be Element of Vars such that

         A2: e = (x -term C) & (e . {} ) = [x, a_Term ];

        ((e . {} ) `1 ) = x & x in Vars by A2;

        hence thesis by A1, Th8, XBOOLE_0: 3;

      end;

        suppose ex o be OperSymbol of C st (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op );

        then

        consider o be OperSymbol of C such that

         A3: (e . {} ) = [o, the carrier of C] & (o in Constructors or o = * or o = non_op );

        take o;

        

         A4: ((e . {} ) `1 ) = o & ((e . {} ) `2 ) = the carrier of C by A3;

         * in { * , non_op } & non_op in { * , non_op } by TARSKI:def 2;

        then o <> * & o <> non_op by A1, A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        then o is constructor;

        hence o = ((e . {} ) `1 ) & ( the_result_sort_of o) = (o `1 ) by A3, Def1;

        set X = ( MSVars C);

        set V = (X (\/) (the carrier of C --> { 0 }));

        reconsider q = e as Term of C, V by MSAFREE3: 8;

        

         A5: ( variables_in q) c= X by MSAFREE3: 27;

        

         A6: ( the_sort_of q) = ( the_result_sort_of o) by A3, MSATERM: 17;

        (the Sorts of ( Free (C,( MSVars C))) . ( the_result_sort_of o)) = ((C -Terms (X,V)) . ( the_result_sort_of o)) by MSAFREE3: 24

        .= { a where a be Term of C, V : ( the_sort_of a) = ( the_result_sort_of o) & ( variables_in a) c= X } by MSAFREE3:def 5;

        hence e in (the Sorts of ( Free (C,( MSVars C))) . ( the_result_sort_of o)) by A5, A6;

      end;

    end;

    theorem :: ABCMIZ_A:21

    

     Th21: for C be initialized standardized ConstructorSignature holds for t be quasi-term of C holds t is compound iff ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Term

    proof

      let C be initialized standardized ConstructorSignature;

      set X = ( MSVars C);

      set V = (X (\/) (the carrier of C --> { 0 }));

      let t be quasi-term of C;

      (C -Terms (X,V)) c= the Sorts of ( FreeMSA V) & the Sorts of ( Free (C,X)) = (C -Terms (X,V)) by MSAFREE3: 24, PBOOLE:def 18;

      then

       A1: ( FreeMSA V) = MSAlgebra (# ( FreeSort V), ( FreeOper V) #) & ((C -Terms (X,V)) . ( a_Term C)) c= (the Sorts of ( FreeMSA V) . ( a_Term C)) & t in ((C -Terms (X,V)) . ( a_Term C)) by ABCMIZ_1:def 28;

      then t in (( FreeSort V) . ( a_Term C));

      then

       A2: t in ( FreeSort (V,( a_Term C))) by MSAFREE:def 11;

      

       A3: (( MSVars C) . a_Term ) = Vars & ( a_Term C) = a_Term & a_Term = 2 by ABCMIZ_1:def 25;

      reconsider q = t as Term of C, V by MSAFREE3: 8;

      per cases by MSATERM: 2;

        suppose ex s be SortSymbol of C, v be Element of (V . s) st (q . {} ) = [v, s];

        then

        consider s be SortSymbol of C, v be Element of (V . s) such that

         A4: (t . {} ) = [v, s];

        

         A5: q = ( root-tree [v, s]) & ( the_sort_of q) = ( a_Term C) by A2, A4, MSATERM: 5, MSATERM:def 5;

        then

         A6: ( a_Term C) = s & ((t . {} ) `1 ) = v by A4, MSATERM: 14;

        then

        reconsider x = v as Element of Vars by A3, A5, A1, MSAFREE3: 18;

        q = (x -term C) & ( vars x) <> 2 by A5, A6, Th7;

        hence thesis by A6;

      end;

        suppose (q . {} ) in [:the carrier' of C, {the carrier of C}:];

        then

        consider o,k be object such that

         A7: o in the carrier' of C & k in {the carrier of C} & (q . {} ) = [o, k] by ZFMISC_1:def 2;

        reconsider o as OperSymbol of C by A7;

        k = the carrier of C by A7, TARSKI:def 1;

        

        then

         A8: ( the_result_sort_of o) = ( the_sort_of q) by A7, MSATERM: 17

        .= ( a_Term C) by A1, MSAFREE3: 17;

        then o <> ( ast C) & o <> ( non_op C) by ABCMIZ_1: 38;

        then

         A9: o is constructor;

        

        then

         A10: ( a_Term C) = (o `1 ) by A8, Def1

        .= (((q . {} ) `1 ) `1 ) by A7;

        

         A11: ((q . {} ) `1 ) = o by A7;

        now

          given x be Element of Vars such that

           A12: q = (x -term C);

          (q . {} ) = [x, a_Term ] by A12, TREES_4: 3;

          then k = a_Term by A7, XTUPLE_0: 1;

          then 2 = the carrier of C by A7, TARSKI:def 1;

          hence contradiction by ABCMIZ_1:def 9, YELLOW11: 1;

        end;

        hence thesis by A9, A10, A11, Th3, Def1;

      end;

    end;

    theorem :: ABCMIZ_A:22

    

     Th22: for C be initialized standardized ConstructorSignature holds for t be expression of C holds t is non compound quasi-term of C iff ((t . {} ) `1 ) in Vars

    proof

      let C be initialized standardized ConstructorSignature;

      let t be expression of C;

      now

        assume t is non compound quasi-term of C;

        then

        consider x be Element of Vars such that

         A1: t = (x -term C) by Th3;

        (t . {} ) = [x, a_Term ] & x in Vars by A1, TREES_4: 3;

        hence ((t . {} ) `1 ) in Vars ;

      end;

      assume ((t . {} ) `1 ) in Vars ;

      then ex x be Element of Vars st x = ((t . {} ) `1 ) & t = (x -term C) by Th17;

      hence thesis;

    end;

    theorem :: ABCMIZ_A:23

    for C be initialized standardized ConstructorSignature holds for t be expression of C holds t is quasi-term of C iff ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Term or ((t . {} ) `1 ) in Vars

    proof

      let C be initialized standardized ConstructorSignature;

      let t be expression of C;

      hereby

        assume t is quasi-term of C;

        then

        reconsider tr = t as quasi-term of C;

        tr is compound or tr is non compound;

        hence ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Term or ((t . {} ) `1 ) in Vars by Th21, Th22;

      end;

      assume that

       A1: ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Term or ((t . {} ) `1 ) in Vars and

       A2: not t is quasi-term of C;

      

       A3: ((t . {} ) `1 ) in Vars implies ex x be Element of Vars st x = ((t . {} ) `1 ) & t = (x -term C) by Th17;

      then ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Term by A1, A2;

      then ex o be OperSymbol of C st o = ((t . {} ) `1 ) & ( the_result_sort_of o) = (o `1 ) & t is expression of C, ( the_result_sort_of o) by Th20;

      hence thesis by A2, A3, A1;

    end;

    theorem :: ABCMIZ_A:24

    

     Th24: for C be initialized standardized ConstructorSignature holds for a be expression of C holds a is positive quasi-adjective of C iff ((a . {} ) `1 ) in Constructors & (((a . {} ) `1 ) `1 ) = an_Adj

    proof

      let C be initialized standardized ConstructorSignature;

      set X = ( MSVars C);

      set V = (X (\/) (the carrier of C --> { 0 }));

      let t be expression of C;

      consider A be MSSubset of ( FreeMSA V) such that

       A1: ( Free (C,X)) = ( GenMSAlg A) & A = (( Reverse V) "" X) by MSAFREE3:def 1;

      the Sorts of ( Free (C,X)) is MSSubset of ( FreeMSA V) by A1, MSUALG_2:def 9;

      then the Sorts of ( Free (C,X)) c= the Sorts of ( FreeMSA V) by PBOOLE:def 18;

      then

       A2: (the Sorts of ( Free (C,( MSVars C))) . ( an_Adj C)) c= (the Sorts of ( FreeMSA V) . ( an_Adj C));

      per cases by Th14;

        suppose ((t . {} ) `1 ) in Vars & ((t . {} ) `2 ) = a_Term & t is quasi-term of C;

        hence thesis by Th8, ABCMIZ_1: 77, XBOOLE_0: 3;

      end;

        suppose that

         A3: ((t . {} ) `2 ) = the carrier of C and

         A4: ((t . {} ) `1 ) in Constructors and

         A5: ((t . {} ) `1 ) in the carrier' of C;

        reconsider o = ((t . {} ) `1 ) as OperSymbol of C by A5;

        reconsider tt = t as Term of C, V by MSAFREE3: 8;

         not o in { * , non_op } by A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        then o <> * & o <> non_op by TARSKI:def 2;

        then o is constructor;

        then

         A6: (o `1 ) = ( the_result_sort_of o) by Def1;

        

         A7: (t . {} ) = [o, ((t . {} ) `2 )];

        then

         A8: ( the_sort_of tt) = ( the_result_sort_of o) by A3, MSATERM: 17;

        hereby

          assume t is positive quasi-adjective of C;

          then

           A9: t in (the Sorts of ( Free (C,( MSVars C))) . ( an_Adj C)) by ABCMIZ_1:def 28;

          thus ((t . {} ) `1 ) in Constructors by A4;

          assume (((t . {} ) `1 ) `1 ) <> an_Adj ;

          hence contradiction by A2, A9, A6, A8, MSAFREE3: 7;

        end;

        assume ((t . {} ) `1 ) in Constructors ;

        assume (((t . {} ) `1 ) `1 ) = an_Adj ;

        then

        reconsider t as expression of C, ( an_Adj C) by A3, A6, A7, Th12;

        t is positive

        proof

          given a be expression of C, ( an_Adj C) such that

           A10: t = (( non_op C) term a);

          t = ( [ non_op , the carrier of C] -tree <*a*>) by A10, ABCMIZ_1: 43;

          then (t . {} ) = [ non_op , the carrier of C] by TREES_4:def 4;

          then ((t . {} ) `1 ) = non_op ;

          then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

          hence thesis by A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        end;

        hence thesis;

      end;

        suppose

         A11: ((t . {} ) `1 ) = * ;

        then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

        then

         A12: not ((t . {} ) `1 ) in Constructors by ABCMIZ_1: 39, XBOOLE_0: 3;

        consider a be expression of C, ( an_Adj C), q be expression of C, ( a_Type C) such that

         A13: t = ( [ * , 3] -tree (a,q)) by A11, Th18;

        t = ( [ * , 3] -tree <*a, q*>) by A13, TREES_4:def 6;

        then (t . {} ) = [ * , 3] by TREES_4:def 4;

        then ((t . {} ) `1 ) = * ;

        then t is expression of C, ( a_Type C) & ( a_Type C) = a_Type & a_Type = 0 & ( an_Adj C) = an_Adj & an_Adj = 1 by Th13;

        hence thesis by A12, ABCMIZ_1: 48;

      end;

        suppose

         A14: ((t . {} ) `1 ) = non_op ;

        then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

        then

         A15: not ((t . {} ) `1 ) in Constructors by ABCMIZ_1: 39, XBOOLE_0: 3;

        consider a be expression of C, ( an_Adj C) such that

         A16: t = ( [ non_op , 3] -tree a) by A14, Th19;

        t = ( [ non_op , 3] -tree <*a*>) by A16, TREES_4:def 5

        .= ( [ non_op , the carrier of C] -tree <*a*>) by ABCMIZ_1:def 9, YELLOW11: 1

        .= (( non_op C) term a) by ABCMIZ_1: 43;

        hence thesis by A15, ABCMIZ_1:def 37;

      end;

    end;

    theorem :: ABCMIZ_A:25

    for C be initialized standardized ConstructorSignature holds for a be quasi-adjective of C holds a is negative iff ((a . {} ) `1 ) = non_op

    proof

      let C be initialized standardized ConstructorSignature;

      let t be quasi-adjective of C;

      per cases ;

        suppose

         A1: t is positive expression of C, ( an_Adj C);

        then ((t . {} ) `1 ) in Constructors & non_op in { * , non_op } by Th24, TARSKI:def 2;

        hence thesis by A1, ABCMIZ_1: 39, XBOOLE_0: 3;

      end;

        suppose

         A2: t is negative expression of C, ( an_Adj C);

        then

        consider a be expression of C, ( an_Adj C) such that

         A3: a is positive & t = (( non_op C) term a) by ABCMIZ_1:def 38;

        t = ( [ non_op , the carrier of C] -tree <*a*>) by A3, ABCMIZ_1: 43;

        then (t . {} ) = [ non_op , the carrier of C] by TREES_4:def 4;

        hence thesis by A2;

      end;

    end;

    theorem :: ABCMIZ_A:26

    for C be initialized standardized ConstructorSignature holds for t be expression of C holds t is pure expression of C, ( a_Type C) iff ((t . {} ) `1 ) in Constructors & (((t . {} ) `1 ) `1 ) = a_Type

    proof

      let C be initialized standardized ConstructorSignature;

      set X = ( MSVars C);

      set V = (X (\/) (the carrier of C --> { 0 }));

      let t be expression of C;

      consider A be MSSubset of ( FreeMSA V) such that

       A1: ( Free (C,X)) = ( GenMSAlg A) & A = (( Reverse V) "" X) by MSAFREE3:def 1;

      the Sorts of ( Free (C,X)) is MSSubset of ( FreeMSA V) by A1, MSUALG_2:def 9;

      then the Sorts of ( Free (C,X)) c= the Sorts of ( FreeMSA V) by PBOOLE:def 18;

      then

       A2: (the Sorts of ( Free (C,( MSVars C))) . ( a_Type C)) c= (the Sorts of ( FreeMSA V) . ( a_Type C));

      per cases by Th14;

        suppose ((t . {} ) `1 ) in Vars & ((t . {} ) `2 ) = a_Term & t is quasi-term of C;

        hence thesis by Th8, ABCMIZ_1: 48, XBOOLE_0: 3;

      end;

        suppose that

         A3: ((t . {} ) `2 ) = the carrier of C and

         A4: ((t . {} ) `1 ) in Constructors and

         A5: ((t . {} ) `1 ) in the carrier' of C;

        reconsider o = ((t . {} ) `1 ) as OperSymbol of C by A5;

        reconsider tt = t as Term of C, V by MSAFREE3: 8;

         not o in { * , non_op } by A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        then o <> * & o <> non_op by TARSKI:def 2;

        then o is constructor;

        then

         A6: (o `1 ) = ( the_result_sort_of o) by Def1;

        

         A7: (t . {} ) = [o, ((t . {} ) `2 )];

        then

         A8: ( the_sort_of tt) = ( the_result_sort_of o) by A3, MSATERM: 17;

        now

          assume t is pure expression of C, ( a_Type C);

          then

           A9: t in (the Sorts of ( Free (C,( MSVars C))) . ( a_Type C)) by ABCMIZ_1:def 28;

          thus ((t . {} ) `1 ) in Constructors by A4;

          assume (((t . {} ) `1 ) `1 ) <> a_Type ;

          hence contradiction by A2, A9, A6, A8, MSAFREE3: 7;

        end;

        assume ((t . {} ) `1 ) in Constructors ;

        assume (((t . {} ) `1 ) `1 ) = a_Type ;

        then

        reconsider t as expression of C, ( a_Type C) by A3, A7, Th12, A6;

        t is pure

        proof

          given a be expression of C, ( an_Adj C), q be expression of C, ( a_Type C) such that

           A10: t = (( ast C) term (a,q));

          t = ( [ * , the carrier of C] -tree <*a, q*>) by A10, ABCMIZ_1: 46;

          then (t . {} ) = [ * , the carrier of C] by TREES_4:def 4;

          then ((t . {} ) `1 ) = * ;

          then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

          hence thesis by A4, ABCMIZ_1: 39, XBOOLE_0: 3;

        end;

        hence thesis;

      end;

        suppose

         A11: ((t . {} ) `1 ) = * ;

        then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

        then

         A12: not ((t . {} ) `1 ) in Constructors by ABCMIZ_1: 39, XBOOLE_0: 3;

        consider a be expression of C, ( an_Adj C), q be expression of C, ( a_Type C) such that

         A13: t = ( [ * , 3] -tree (a,q)) by A11, Th18;

        t = ( [ * , 3] -tree <*a, q*>) by A13, TREES_4:def 6

        .= ( [ * , the carrier of C] -tree <*a, q*>) by ABCMIZ_1:def 9, YELLOW11: 1

        .= (( ast C) term (a,q)) by ABCMIZ_1: 46;

        hence thesis by A12, ABCMIZ_1:def 41;

      end;

        suppose

         A14: ((t . {} ) `1 ) = non_op ;

        then ((t . {} ) `1 ) in { * , non_op } by TARSKI:def 2;

        then

         A15: not ((t . {} ) `1 ) in Constructors by ABCMIZ_1: 39, XBOOLE_0: 3;

        consider a be expression of C, ( an_Adj C) such that

         A16: t = ( [ non_op , 3] -tree a) by A14, Th19;

        t = ( [ non_op , 3] -tree <*a*>) by A16, TREES_4:def 5;

        then (t . {} ) = [ non_op , 3] by TREES_4:def 4;

        then ((t . {} ) `1 ) = non_op ;

        then t is expression of C, ( an_Adj C) by Th13;

        hence thesis by A15, ABCMIZ_1: 48;

      end;

    end;

    begin

    reserve i,j for Nat,

x for variable,

l for quasi-loci;

    set MC = MaxConstrSign ;

    definition

      mode expression is expression of MaxConstrSign ;

      mode valuation is valuation of MaxConstrSign ;

      mode quasi-adjective is quasi-adjective of MaxConstrSign ;

      :: ABCMIZ_A:def3

      func QuasiAdjs -> Subset of ( Free ( MaxConstrSign ,( MSVars MaxConstrSign ))) equals ( QuasiAdjs MaxConstrSign );

      coherence ;

      mode quasi-term is quasi-term of MaxConstrSign ;

      :: ABCMIZ_A:def4

      func QuasiTerms -> Subset of ( Free ( MaxConstrSign ,( MSVars MaxConstrSign ))) equals ( QuasiTerms MaxConstrSign );

      coherence ;

      mode quasi-type is quasi-type of MaxConstrSign ;

      :: ABCMIZ_A:def5

      func QuasiTypes -> set equals ( QuasiTypes MaxConstrSign );

      coherence ;

    end

    registration

      cluster QuasiAdjs -> non empty;

      coherence ;

      cluster QuasiTerms -> non empty;

      coherence ;

      cluster QuasiTypes -> non empty;

      coherence ;

    end

    definition

      :: original: Modes

      redefine

      func Modes -> non empty Subset of Constructors ;

      coherence

      proof

         Modes c= ( Modes \/ Attrs ) & ( Modes \/ Attrs ) c= Constructors by XBOOLE_1: 7;

        hence thesis by XBOOLE_1: 1;

      end;

      :: original: Attrs

      redefine

      func Attrs -> non empty Subset of Constructors ;

      coherence

      proof

         Attrs c= ( Modes \/ Attrs ) & ( Modes \/ Attrs ) c= Constructors by XBOOLE_1: 7;

        hence thesis by XBOOLE_1: 1;

      end;

      :: original: Funcs

      redefine

      func Funcs -> non empty Subset of Constructors ;

      coherence by XBOOLE_1: 7;

    end

    reserve C for initialized ConstructorSignature,

c for constructor OperSymbol of C;

    definition

      :: ABCMIZ_A:def6

      func set-constr -> Element of Modes equals [ a_Type , [ {} , 0 ]];

      coherence

      proof

         a_Type in { a_Type } & [ {} , 0 ] in [: QuasiLoci , NAT :] by ABCMIZ_1: 29, TARSKI:def 1, ZFMISC_1:def 2;

        hence thesis by ZFMISC_1:def 2;

      end;

    end

    theorem :: ABCMIZ_A:27

    ( kind_of set-constr ) = a_Type & ( loci_of set-constr ) = {} & ( index_of set-constr ) = 0 ;

    theorem :: ABCMIZ_A:28

    

     Th28: Constructors = [: { a_Type , an_Adj , a_Term }, [: QuasiLoci , NAT :]:]

    proof

      

      thus Constructors = (( [: { a_Type }, [: QuasiLoci , NAT :]:] \/ [: { an_Adj }, [: QuasiLoci , NAT :]:]) \/ Funcs )

      .= ( [:( { a_Type } \/ { an_Adj }), [: QuasiLoci , NAT :]:] \/ Funcs ) by ZFMISC_1: 97

      .= ( [: { a_Type , an_Adj }, [: QuasiLoci , NAT :]:] \/ Funcs ) by ENUMSET1: 1

      .= [:( { a_Type , an_Adj } \/ { a_Term }), [: QuasiLoci , NAT :]:] by ZFMISC_1: 97

      .= [: { a_Type , an_Adj , a_Term }, [: QuasiLoci , NAT :]:] by ENUMSET1: 3;

    end;

    theorem :: ABCMIZ_A:29

    

     Th29: [( rng l), i] in Vars & (l ^ <* [( rng l), i]*>) is quasi-loci

    proof

      ( varcl ( rng l)) = ( rng l) by ABCMIZ_1: 33;

      hence [( rng l), i] in Vars by ABCMIZ_1: 17;

      then

      reconsider x = [( rng l), i] as variable;

      ( rng l) in {( rng l), i} & {( rng l), i} in x by TARSKI:def 2;

      then ( vars x) = ( rng l) & x nin ( rng l) by XREGULAR: 7;

      hence thesis by ABCMIZ_1: 31;

    end;

    theorem :: ABCMIZ_A:30

    

     Th30: ex l st ( len l) = i

    proof

      defpred P[ Nat] means ex l st ( len l) = $1;

      ( <*> Vars ) is quasi-loci & ( len ( <*> Vars )) = 0 by ABCMIZ_1: 29;

      then

       A1: P[ 0 ];

      

       A2: P[j] implies P[(j + 1)]

      proof

        given l such that

         A3: ( len l) = j;

        reconsider l1 = (l ^ <* [( rng l), 1]*>) as quasi-loci by Th29;

        take l1;

        thus thesis by A3, FINSEQ_2: 16;

      end;

       P[j] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: ABCMIZ_A:31

    

     Th31: for X be finite Subset of Vars holds ex l st ( rng l) = ( varcl X)

    proof

      let X be finite Subset of Vars ;

      reconsider Y = ( varcl X) as finite Subset of Vars by ABCMIZ_1: 24;

      defpred R[ set, set] means $1 in ($2 `1 );

      

       A1: for x,y be set st x in Y & y in Y & R[x, y] holds not R[y, x]

      proof

        let x,y be set such that

         A2: x in Y & y in Y & R[x, y] & R[y, x];

        x in Vars by A2;

        then

        consider A be Subset of Vars , j be Element of NAT such that

         A3: x = [( varcl A), j] & A is finite by ABCMIZ_1: 18;

        y in Vars by A2;

        then

        consider B be Subset of Vars , k be Element of NAT such that

         A4: y = [( varcl B), k] & B is finite by ABCMIZ_1: 18;

        

         A5: y in ( varcl A) & x in ( varcl B) by A2, A3, A4;

        

         A6: ( varcl A) in {( varcl A)} & ( varcl B) in {( varcl B)} by TARSKI:def 1;

         {( varcl A)} in x & {( varcl B)} in y by A4, A3, TARSKI:def 2;

        hence thesis by A5, A6, XREGULAR: 10;

      end;

      

       A7: for x,y,z be set st x in Y & y in Y & z in Y & R[x, y] & R[y, z] holds R[x, z]

      proof

        let x,y,z be set such that

         A8: x in Y & y in Y & z in Y & R[x, y] & R[y, z];

        y in Vars by A8;

        then

        consider B be Subset of Vars , k be Element of NAT such that

         A9: y = [( varcl B), k] & B is finite by ABCMIZ_1: 18;

        z in Vars by A8;

        then

        consider C be Subset of Vars , j be Element of NAT such that

         A10: z = [( varcl C), j] & C is finite by ABCMIZ_1: 18;

        

         A11: (z `1 ) = ( varcl C) & (y `1 ) = ( varcl B) by A10, A9;

        then ( varcl B) c= ( varcl C) by A8, A9, ABCMIZ_1:def 1;

        hence R[x, z] by A11, A8;

      end;

      consider l be one-to-one FinSequence such that

       A12: ( rng l) = Y and

       A13: for i, j st i in ( dom l) & j in ( dom l) & R[(l . i), (l . j)] holds i < j from Numeration( A1, A7);

      reconsider l as one-to-one FinSequence of Vars by A12, FINSEQ_1:def 4;

      now

        let i be Nat, x be variable;

        assume

         A14: i in ( dom l) & x = (l . i);

        let y be variable;

        assume

         A15: y in ( vars x);

        x in Vars ;

        then

        consider A be Subset of Vars , j be Element of NAT such that

         A16: x = [( varcl A), j] & A is finite by ABCMIZ_1: 18;

        x in ( rng l) & ( vars x) = ( varcl A) by A14, A16, FUNCT_1:def 3;

        then ( vars x) c= Y by A12, A16, ABCMIZ_1:def 1;

        then

        consider a be object such that

         A17: a in ( dom l) & y = (l . a) by A12, A15, FUNCT_1:def 3;

        reconsider a as Nat by A17;

        take a;

        thus a in ( dom l) & a < i & y = (l . a) by A13, A14, A15, A17;

      end;

      then

      reconsider l as quasi-loci by ABCMIZ_1: 30;

      take l;

      thus ( rng l) = ( varcl X) by A12;

    end;

    theorem :: ABCMIZ_A:32

    

     Th32: for S be non empty non void ManySortedSign holds for Y be non empty-yielding ManySortedSet of the carrier of S holds for X,o be set, p be DTree-yielding FinSequence st ex C st X = ( Union the Sorts of ( Free (S,Y))) holds (o -tree p) in X implies p is FinSequence of X

    proof

      let S be non empty non void ManySortedSign;

      let Y be non empty-yielding ManySortedSet of the carrier of S;

      let X,o be set;

      let p be DTree-yielding FinSequence;

      given C such that

       A1: X = ( Union the Sorts of ( Free (S,Y)));

      assume (o -tree p) in X;

      then

      reconsider e = (o -tree p) as Element of ( Free (S,Y)) by A1;

      ( rng p) c= X

      proof

        let z be object;

        assume z in ( rng p);

        then

        consider i be object such that

         A2: i in ( dom p) & z = (p . i) by FUNCT_1:def 3;

        reconsider i as Nat by A2;

        reconsider ppi = (p . i) as DecoratedTree by A2, TREES_3: 24;

        

         A3: 1 <= i & i <= ( len p) by A2, FINSEQ_3: 25;

        then

         A4: ((i -' 1) + 1) = i by XREAL_1: 235;

        then

         A5: (i -' 1) < ( len p) by A3, NAT_1: 13;

        

         A6: ( len ( doms p)) = ( len p) by TREES_3: 38;

        

         A7: (( doms p) . i) = ( dom ppi) by A2, FUNCT_6: 22;

        

         A8: ( dom e) = ( tree ( doms p)) by TREES_4: 10;

        ( <*(i -' 1)*> ^ ( <*> NAT )) = <*(i -' 1)*> & ( <*> NAT ) in ( dom ppi) by FINSEQ_1: 34, TREES_1: 22;

        then

        reconsider q = <*(i -' 1)*> as Element of ( dom e) by A4, A5, A6, A7, A8, TREES_3:def 15;

        (e | q) = z by A2, A4, A5, TREES_4:def 4;

        then z is Element of ( Free (S,Y)) by MSAFREE3: 33;

        hence thesis by A1;

      end;

      hence p is FinSequence of X by FINSEQ_1:def 4;

    end;

    definition

      let C;

      let e be expression of C;

      :: ABCMIZ_A:def7

      mode subexpression of e -> expression of C means it in ( Subtrees e);

      existence by TREES_9: 11;

      :: ABCMIZ_A:def8

      func constrs e -> set equals (( proj1 ( rng e)) /\ the set of all o where o be constructor OperSymbol of C);

      coherence ;

    end

    definition

      let S be non empty non void ManySortedSign;

      let X be non empty-yielding ManySortedSet of the carrier of S;

      let e be Element of ( Free (S,X));

      :: ABCMIZ_A:def9

      func main-constr e -> set equals

      : Def9: ((e . {} ) `1 ) if e is compound

      otherwise {} ;

      correctness ;

      :: ABCMIZ_A:def10

      func args e -> DTree-yielding FinSequence means

      : ARGS: e = ((e . {} ) -tree it );

      existence

      proof

        consider v be set, p be DTree-yielding FinSequence such that

         A1: e = (v -tree p) by TREES_9: 8;

        

         A2: v = (e . {} ) by A1, TREES_4:def 4;

        thus thesis by A1, A2;

      end;

      uniqueness by TREES_4: 15;

    end

    definition

      let S be non empty non void ManySortedSign;

      let X be non empty-yielding ManySortedSet of the carrier of S;

      let e be Element of ( Free (S,X));

      :: original: args

      redefine

      func args e -> FinSequence of ( Free (S,X)) ;

      coherence

      proof

        

         A1: e = ((e . {} ) -tree ( args e)) by ARGS;

        ( args e) is FinSequence of ( Free (S,X)) by A1, Th32;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_A:33

    

     Th33: for C holds for e be expression of C holds e is subexpression of e

    proof

      let C be initialized ConstructorSignature;

      let e be expression of C;

      thus e in ( Subtrees e) by TREES_9: 11;

    end;

    theorem :: ABCMIZ_A:34

    ( main-constr (x -term C)) = {} by Def9;

    theorem :: ABCMIZ_A:35

    

     Th35: for c be constructor OperSymbol of C holds for p be FinSequence of ( QuasiTerms C) st ( len p) = ( len ( the_arity_of c)) holds ( main-constr (c -trm p)) = c

    proof

      let c be constructor OperSymbol of C;

      let p be FinSequence of ( QuasiTerms C);

      assume ( len p) = ( len ( the_arity_of c));

      then (c -trm p) = ( [c, the carrier of C] -tree p) by ABCMIZ_1:def 35;

      then ((c -trm p) . {} ) = [c, the carrier of C] by TREES_4:def 4;

      

      hence ( main-constr (c -trm p)) = ( [c, the carrier of C] `1 ) by Def9

      .= c;

    end;

    definition

      let C;

      let e be expression of C;

      :: ABCMIZ_A:def11

      attr e is constructor means

      : Def11: e is compound & ( main-constr e) is constructor OperSymbol of C;

    end

    registration

      let C;

      cluster constructor -> compound for expression of C;

      coherence ;

    end

    registration

      let C;

      cluster constructor for expression of C;

      existence

      proof

        consider m,a be OperSymbol of C such that

         A1: ( the_result_sort_of m) = a_Type & ( the_arity_of m) = {} & ( the_result_sort_of a) = an_Adj & ( the_arity_of a) = {} by ABCMIZ_1:def 12;

        ( the_arity_of ( ast C)) = <*( an_Adj C), ( a_Type C)*> & ( the_arity_of ( non_op C)) = <*( an_Adj C)*> by ABCMIZ_1: 38;

        then

        reconsider m as constructor OperSymbol of C by A1, ABCMIZ_1:def 11;

        set p = ( <*> ( QuasiTerms C));

        take e = (m -trm p);

        thus e is compound;

        ( len p) = ( len ( the_arity_of m)) by A1;

        hence thesis by Th35;

      end;

    end

    registration

      let C;

      let e be constructor expression of C;

      cluster constructor for subexpression of e;

      existence

      proof

        e is subexpression of e by Th33;

        hence thesis;

      end;

    end

    registration

      let S be non void Signature;

      let X be non empty-yielding ManySortedSet of S;

      let t be Element of ( Free (S,X));

      cluster ( rng t) -> Relation-like;

      coherence

      proof

        set Z = (the carrier of S --> { 0 });

        set Y = (X (\/) Z);

        t is Term of S, Y by MSAFREE3: 8;

        then ( rng t) c= the carrier of ( DTConMSA Y) by RELAT_1:def 19;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_A:36

    for e be constructor expression of C holds ( main-constr e) in ( constrs e)

    proof

      let e be constructor expression of C;

      

       A1: ( main-constr e) = ((e . {} ) `1 ) by Def9;

       {} in ( dom e) by TREES_1: 22;

      then (e . {} ) in ( rng e) by FUNCT_1:def 3;

      then

       A2: ( main-constr e) in ( proj1 ( rng e)) by A1, MCART_1: 86;

      ( main-constr e) is constructor OperSymbol of C by Def11;

      then ( main-constr e) in the set of all c;

      hence ( main-constr e) in ( constrs e) by A2, XBOOLE_0:def 4;

    end;

    begin

    reserve a,a9 for quasi-adjective,

t,t1,t2 for quasi-term,

T for quasi-type,

c for Element of Constructors ;

    definition

      let C be non void Signature;

      :: ABCMIZ_A:def12

      attr C is arity-rich means

      : Def12: for n be Nat, s be SortSymbol of C holds { o where o be OperSymbol of C : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = n } is infinite;

      let o be OperSymbol of C;

      :: ABCMIZ_A:def13

      attr o is nullary means

      : Def13: ( the_arity_of o) = {} ;

      :: ABCMIZ_A:def14

      attr o is unary means

      : Def14: ( len ( the_arity_of o)) = 1;

      :: ABCMIZ_A:def15

      attr o is binary means

      : Def15: ( len ( the_arity_of o)) = 2;

    end

    theorem :: ABCMIZ_A:37

    

     Th37: for C be non void Signature holds for o be OperSymbol of C holds (o is nullary implies not o is unary) & (o is nullary implies not o is binary) & (o is unary implies not o is binary);

    registration

      let C be ConstructorSignature;

      cluster ( non_op C) -> unary;

      coherence

      proof

        ( the_arity_of ( non_op C)) = <*( an_Adj C)*> by ABCMIZ_1: 38;

        hence ( len ( the_arity_of ( non_op C))) = 1 by FINSEQ_1: 39;

      end;

      cluster ( ast C) -> binary;

      coherence

      proof

        ( the_arity_of ( ast C)) = <*( an_Adj C), ( a_Type C)*> by ABCMIZ_1: 38;

        hence ( len ( the_arity_of ( ast C))) = 2 by FINSEQ_1: 44;

      end;

    end

    registration

      let C be ConstructorSignature;

      cluster nullary -> constructor for OperSymbol of C;

      coherence

      proof

        let o be OperSymbol of C such that

         A1: ( the_arity_of o) = {} ;

        ( the_arity_of ( ast C)) = <*( an_Adj C), ( a_Type C)*> & ( the_arity_of ( non_op C)) = <*( an_Adj C)*> by ABCMIZ_1: 38;

        hence o <> * & o <> non_op by A1;

      end;

    end

    theorem :: ABCMIZ_A:38

    

     Th38: for C be ConstructorSignature holds C is initialized iff ex m be OperSymbol of ( a_Type C), a be OperSymbol of ( an_Adj C) st m is nullary & a is nullary

    proof

      let C be ConstructorSignature;

      hereby

        assume C is initialized;

        then

        consider m,a be OperSymbol of C such that

         A1: ( the_result_sort_of m) = a_Type & ( the_arity_of m) = {} & ( the_result_sort_of a) = an_Adj & ( the_arity_of a) = {} ;

        reconsider m as OperSymbol of ( a_Type C) by A1, ABCMIZ_1:def 32;

        reconsider a as OperSymbol of ( an_Adj C) by A1, ABCMIZ_1:def 32;

        take m, a;

        thus m is nullary by A1;

        thus a is nullary by A1;

      end;

      given m be OperSymbol of ( a_Type C), a be OperSymbol of ( an_Adj C) such that

       A2: m is nullary & a is nullary;

      take m, a;

      ( the_result_sort_of ( non_op C)) = ( an_Adj C) & ( the_result_sort_of ( ast C)) = ( a_Type C) by ABCMIZ_1: 38;

      hence thesis by A2, ABCMIZ_1:def 32;

    end;

    registration

      let C be initialized ConstructorSignature;

      cluster nullary constructor for OperSymbol of ( a_Type C);

      existence

      proof

        consider m be OperSymbol of ( a_Type C), a be OperSymbol of ( an_Adj C) such that

         A1: m is nullary & a is nullary by Th38;

        take m;

        thus thesis by A1;

      end;

      cluster nullary constructor for OperSymbol of ( an_Adj C);

      existence

      proof

        consider m be OperSymbol of ( a_Type C), a be OperSymbol of ( an_Adj C) such that

         A2: m is nullary & a is nullary by Th38;

        take a;

        thus thesis by A2;

      end;

    end

    registration

      let C be initialized ConstructorSignature;

      cluster nullary constructor for OperSymbol of C;

      existence

      proof

        set o = the nullary constructor OperSymbol of ( a_Type C);

        take o;

        thus thesis;

      end;

    end

    registration

      cluster arity-rich -> with_an_operation_for_each_sort for non void Signature;

      coherence

      proof

        let S be non void Signature such that

         A1: for n be Nat, s be SortSymbol of S holds { o where o be OperSymbol of S : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = n } is infinite;

        let v be object;

        assume v in the carrier of S;

        then

        reconsider v as SortSymbol of S;

        set A = { o where o be OperSymbol of S : ( the_result_sort_of o) = v & ( len ( the_arity_of o)) = 0 };

        reconsider A as infinite set by A1;

        set a = the Element of A;

        a in A;

        then

        consider o be OperSymbol of S such that

         A2: a = o & ( the_result_sort_of o) = v & ( len ( the_arity_of o)) = 0 ;

        thus thesis by A2, FUNCT_2: 4;

      end;

      cluster arity-rich -> initialized for ConstructorSignature;

      coherence

      proof

        let C be ConstructorSignature such that

         A3: C is arity-rich;

        set Xt = { o where o be OperSymbol of C : ( the_result_sort_of o) = ( a_Type C) & ( len ( the_arity_of o)) = 0 };

        set x = the Element of Xt;

        Xt is infinite set by A3;

        then x in Xt;

        then

        consider m be OperSymbol of C such that

         A4: x = m & ( the_result_sort_of m) = ( a_Type C) & ( len ( the_arity_of m)) = 0 ;

        set Xa = { o where o be OperSymbol of C : ( the_result_sort_of o) = ( an_Adj C) & ( len ( the_arity_of o)) = 0 };

        set x = the Element of Xa;

        Xa is infinite set by A3;

        then x in Xa;

        then

        consider a be OperSymbol of C such that

         A5: x = a & ( the_result_sort_of a) = ( an_Adj C) & ( len ( the_arity_of a)) = 0 ;

        take m, a;

        thus thesis by A4, A5;

      end;

    end

    registration

      cluster MaxConstrSign -> arity-rich;

      coherence

      proof

        set C = MaxConstrSign ;

        let n be Nat, s be SortSymbol of C;

        

         A1: the carrier of C = { 0 , 1, 2} by ABCMIZ_1:def 9;

        set X = { o where o be OperSymbol of C : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = n };

        consider l be quasi-loci such that

         A2: ( len l) = n by Th30;

        deffunc F( object) = [s, [l, $1]];

        consider f be Function such that

         A3: ( dom f) = NAT & for i be object st i in NAT holds (f . i) = F(i) from FUNCT_1:sch 3;

        f is one-to-one

        proof

          let i,j be object;

          assume i in ( dom f) & j in ( dom f);

          then

          reconsider i, j as Element of NAT by A3;

          (f . i) = F(i) & (f . j) = F(j) by A3;

          then (f . i) = (f . j) implies [l, i] = [l, j] by XTUPLE_0: 1;

          hence thesis by XTUPLE_0: 1;

        end;

        then

         A4: ( rng f) is infinite by A3, CARD_1: 59;

        ( rng f) c= X

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A5: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A3, A5;

          

           A6: [l, x] in [: QuasiLoci , NAT :] & y = F(x) by A3, A5;

          then y in Constructors by A1, Th28, ZFMISC_1:def 2;

          then y in ( { * , non_op } \/ Constructors ) by XBOOLE_0:def 3;

          then

          reconsider y as OperSymbol of C by ABCMIZ_1:def 24;

          

           A7: y is constructor by A6;

          

          then

           A8: ( the_result_sort_of y) = (y `1 ) by ABCMIZ_1:def 24

          .= s by A6;

          ( len ( the_arity_of y)) = ( card ((y `2 ) `1 )) by A7, ABCMIZ_1:def 24

          .= ( card ( [l, x] `1 )) by A6

          .= ( len l);

          hence thesis by A2, A8;

        end;

        hence X is infinite by A4;

      end;

    end

    registration

      cluster arity-rich initialized for ConstructorSignature;

      existence

      proof

        take MaxConstrSign ;

        thus thesis;

      end;

    end

    registration

      let C be arity-rich ConstructorSignature;

      let s be SortSymbol of C;

      cluster nullary constructor for OperSymbol of s;

      existence

      proof

        set X = { o where o be OperSymbol of C : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = 0 };

        X is infinite by Def12;

        then

        consider m1,m2 be object such that

         A1: m1 in X & m2 in X & m1 <> m2 by ZFMISC_1:def 10;

        consider o1 be OperSymbol of C such that

         A2: m1 = o1 & ( the_result_sort_of o1) = s & ( len ( the_arity_of o1)) = 0 by A1;

        reconsider m1 as OperSymbol of s by A2, ABCMIZ_1:def 32;

        ( the_arity_of m1) = {} by A2;

        then m1 is nullary;

        hence thesis;

      end;

      cluster unary constructor for OperSymbol of s;

      existence

      proof

        set X = { o where o be OperSymbol of C : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = 1 };

        X is infinite by Def12;

        then

        consider m1,m2 be object such that

         A3: m1 in X & m2 in X & m1 <> m2 by ZFMISC_1:def 10;

        consider o1 be OperSymbol of C such that

         A4: m1 = o1 & ( the_result_sort_of o1) = s & ( len ( the_arity_of o1)) = 1 by A3;

        consider o2 be OperSymbol of C such that

         A5: m2 = o2 & ( the_result_sort_of o2) = s & ( len ( the_arity_of o2)) = 1 by A3;

        reconsider m1, m2 as OperSymbol of s by A4, A5, ABCMIZ_1:def 32;

        

         A6: m1 is unary & m2 is unary by A4, A5;

        then

         A7: m1 <> ( ast C) & m2 <> ( ast C) by Th37;

        m1 <> non_op or m2 <> non_op by A3;

        then m1 is constructor or m2 is constructor by A7;

        hence thesis by A6;

      end;

      cluster binary constructor for OperSymbol of s;

      existence

      proof

        set X = { o where o be OperSymbol of C : ( the_result_sort_of o) = s & ( len ( the_arity_of o)) = 2 };

        X is infinite by Def12;

        then

        consider m1,m2 be object such that

         A8: m1 in X & m2 in X & m1 <> m2 by ZFMISC_1:def 10;

        consider o1 be OperSymbol of C such that

         A9: m1 = o1 & ( the_result_sort_of o1) = s & ( len ( the_arity_of o1)) = 2 by A8;

        consider o2 be OperSymbol of C such that

         A10: m2 = o2 & ( the_result_sort_of o2) = s & ( len ( the_arity_of o2)) = 2 by A8;

        reconsider m1, m2 as OperSymbol of s by A9, A10, ABCMIZ_1:def 32;

        

         A11: m1 is binary & m2 is binary by A9, A10;

        then

         A12: m1 <> ( non_op C) & m2 <> ( non_op C) by Th37;

        m1 <> * or m2 <> * by A8;

        then m1 is constructor or m2 is constructor by A12;

        hence thesis by A11;

      end;

    end

    registration

      let C be arity-rich ConstructorSignature;

      cluster unary constructor for OperSymbol of C;

      existence

      proof

        set o = the unary constructor OperSymbol of ( a_Type C);

        take o;

        thus thesis;

      end;

      cluster binary constructor for OperSymbol of C;

      existence

      proof

        set o = the binary constructor OperSymbol of ( a_Type C);

        take o;

        thus thesis;

      end;

    end

    theorem :: ABCMIZ_A:39

    

     Th39: for o be nullary OperSymbol of C holds ( [o, the carrier of C] -tree {} ) is expression of C, ( the_result_sort_of o)

    proof

      let o be nullary OperSymbol of C;

      set X = ( MSVars C);

      set Z = (the carrier of C --> { 0 });

      set Y = (X (\/) Z);

      

       A1: ( the_arity_of o) = {} by Def13;

      

       A2: the Sorts of ( Free (C,X)) = (C -Terms (X,Y)) by MSAFREE3: 24;

      for i be Nat st i in ( dom {} ) holds ex t be Term of C, Y st t = ( {} . i) & ( the_sort_of t) = (( the_arity_of o) . i);

      then

      reconsider p = {} as ArgumentSeq of ( Sym (o,Y)) by A1, MSATERM: 24;

      

       A3: ( variables_in (( Sym (o,Y)) -tree p)) c= X

      proof

        let s be object;

        assume s in the carrier of C;

        then

        reconsider s9 = s as SortSymbol of C;

        let x be object;

        assume x in (( variables_in (( Sym (o,Y)) -tree p)) . s);

        then ex t be DecoratedTree st t in ( rng p) & x in ((C variables_in t) . s9) by MSAFREE3: 11;

        hence thesis;

      end;

      set s9 = ( the_result_sort_of o);

      

       A4: ( the_sort_of (( Sym (o,Y)) -tree p)) = ( the_result_sort_of o) by MSATERM: 20;

      (the Sorts of ( Free (C,X)) . s9) = { t where t be Term of C, Y : ( the_sort_of t) = s9 & ( variables_in t) c= X } by A2, MSAFREE3:def 5;

      then ( [o, the carrier of C] -tree {} ) in (the Sorts of ( Free (C,X)) . s9) by A3, A4;

      hence thesis by ABCMIZ_1: 41;

    end;

    definition

      let C be initialized ConstructorSignature;

      let m be nullary constructor OperSymbol of ( a_Type C);

      :: original: term

      redefine

      func m term -> pure expression of C, ( a_Type C) ;

      coherence

      proof

        set T = (m term );

        ( the_arity_of m) = 0 by Def13;

        then ( len ( the_arity_of m)) = 0 ;

        then

         A1: T = ( [m, the carrier of C] -tree {} ) by ABCMIZ_1:def 29;

        ex m,a be OperSymbol of C st ( the_result_sort_of m) = a_Type & ( the_arity_of m) = {} & ( the_result_sort_of a) = an_Adj & ( the_arity_of a) = {} by ABCMIZ_1:def 12;

        then ( the_result_sort_of m) = ( a_Type C) by ABCMIZ_1:def 32;

        then

        reconsider T as expression of C, ( a_Type C) by A1, Th39;

        T is pure

        proof

          given a be expression of C, ( an_Adj C), t be expression of C, ( a_Type C) such that

           A2: T = (( ast C) term (a,t));

          T = ( [ * , the carrier of C] -tree <*a, t*>) by A2, ABCMIZ_1: 46;

          hence thesis by A1, TREES_4: 15;

        end;

        hence thesis;

      end;

    end

    definition

      let c be Element of Constructors ;

      :: ABCMIZ_A:def16

      func @ c -> constructor OperSymbol of MaxConstrSign equals c;

      coherence

      proof

         * in { * , non_op } & non_op in { * , non_op } & the carrier' of MC = ( { * , non_op } \/ Constructors ) by ABCMIZ_1:def 24, TARSKI:def 2;

        then c <> * & c <> non_op & c in the carrier' of MC by ABCMIZ_1: 39, XBOOLE_0: 3, XBOOLE_0:def 3;

        hence thesis by ABCMIZ_1:def 11;

      end;

    end

    definition

      let m be Element of Modes ;

      :: original: @

      redefine

      func @ m -> constructor OperSymbol of ( a_Type MaxConstrSign ) ;

      coherence

      proof

        

         A1: (m `1 ) in { a_Type } by MCART_1: 10;

        ( the_result_sort_of ( @ m)) = (m `1 ) by ABCMIZ_1:def 24

        .= a_Type by A1, TARSKI:def 1;

        hence thesis by ABCMIZ_1:def 32;

      end;

    end

    registration

      cluster ( @ set-constr ) -> nullary;

      coherence

      proof

        ( len ( the_arity_of ( @ set-constr ))) = ( card (( set-constr `2 ) `1 )) by ABCMIZ_1:def 24

        .= ( card ( [ {} , 0 ] `1 ))

        .= ( card 0 );

        hence ( the_arity_of ( @ set-constr )) = {} ;

      end;

    end

    theorem :: ABCMIZ_A:40

    ( the_arity_of ( @ set-constr )) = {} by Def13;

    definition

      :: ABCMIZ_A:def17

      func set-type -> quasi-type equals (( {} ( QuasiAdjs MaxConstrSign )) ast (( @ set-constr ) term ));

      coherence ;

    end

    theorem :: ABCMIZ_A:41

    ( adjs set-type ) = {} & ( the_base_of set-type ) = (( @ set-constr ) term );

    definition

      let l be FinSequence of Vars ;

      :: ABCMIZ_A:def18

      func args l -> FinSequence of ( QuasiTerms MaxConstrSign ) means

      : Def18: ( len it ) = ( len l) & for i st i in ( dom l) holds (it . i) = ((l /. i) -term MaxConstrSign );

      existence

      proof

        deffunc F( Nat) = ((l /. $1) -term MaxConstrSign );

        consider g be FinSequence such that

         A1: ( len g) = ( len l) and

         A2: for i st i in ( dom g) holds (g . i) = F(i) from FINSEQ_1:sch 2;

        

         A3: ( dom g) = ( dom l) by A1, FINSEQ_3: 29;

        ( rng g) c= ( QuasiTerms MaxConstrSign )

        proof

          let j be object;

          assume j in ( rng g);

          then

          consider z be object such that

           A4: z in ( dom g) & j = (g . z) by FUNCT_1:def 3;

          reconsider z as Nat by A4;

          j = F(z) by A2, A4;

          hence thesis by ABCMIZ_1: 49;

        end;

        then

        reconsider g as FinSequence of ( QuasiTerms MaxConstrSign ) by FINSEQ_1:def 4;

        take g;

        thus thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let a1,a2 be FinSequence of ( QuasiTerms MaxConstrSign ) such that

         A5: ( len a1) = ( len l) and

         A6: for i st i in ( dom l) holds (a1 . i) = ((l /. i) -term MaxConstrSign ) and

         A7: ( len a2) = ( len l) and

         A8: for i st i in ( dom l) holds (a2 . i) = ((l /. i) -term MaxConstrSign );

        

         A9: ( dom a1) = ( dom l) & ( dom a2) = ( dom l) by A5, A7, FINSEQ_3: 29;

        now

          let i;

          assume i in ( dom a1);

          then (a1 . i) = ((l /. i) -term MaxConstrSign ) & (a2 . i) = ((l /. i) -term MaxConstrSign ) by A6, A8, A9;

          hence (a1 . i) = (a2 . i);

        end;

        hence thesis by A9;

      end;

    end

    definition

      let c;

      :: ABCMIZ_A:def19

      func base_exp_of c -> expression equals (( @ c) -trm ( args ( loci_of c)));

      coherence ;

    end

    theorem :: ABCMIZ_A:42

    

     Th42: for o be OperSymbol of MaxConstrSign holds o is constructor iff o in Constructors

    proof

      let o be OperSymbol of MaxConstrSign ;

      

       A1: the carrier' of MaxConstrSign = ( { * , non_op } \/ Constructors ) by ABCMIZ_1:def 24;

      o is constructor iff o nin { * , non_op } by TARSKI:def 2;

      hence thesis by A1, ABCMIZ_1: 39, XBOOLE_0: 3, XBOOLE_0:def 3;

    end;

    theorem :: ABCMIZ_A:43

    for m be nullary OperSymbol of MaxConstrSign holds ( main-constr (m term )) = m

    proof

      set C = MaxConstrSign ;

      let m be nullary OperSymbol of C;

      ( the_arity_of m) = 0 by Def13;

      then ( len ( the_arity_of m)) = 0 & ( len {} ) = 0 ;

      then

       A1: (m term ) = ( [m, the carrier of C] -tree {} ) & (m -trm ( <*> ( QuasiTerms C))) = ( [m, the carrier of C] -tree {} ) by ABCMIZ_1:def 29, ABCMIZ_1:def 35;

      

      hence ( main-constr (m term )) = (((m term ) . {} ) `1 ) by Def9

      .= ( [m, the carrier of C] `1 ) by A1, TREES_4:def 4

      .= m;

    end;

    theorem :: ABCMIZ_A:44

    for m be unary constructor OperSymbol of MaxConstrSign holds for t holds ( main-constr (m term t)) = m

    proof

      set C = MaxConstrSign ;

      let m be unary constructor OperSymbol of C;

      let t;

      reconsider w = t as Element of ( QuasiTerms C) by ABCMIZ_1: 49;

      reconsider p = <*w*> as FinSequence of ( QuasiTerms C);

      

       A1: ( len ( the_arity_of m)) = 1 by Def14;

      

      then ( the_arity_of m) = (1 |-> a_Term ) by ABCMIZ_1: 37

      .= <* a_Term *> by FINSEQ_2: 59;

      then ( len p) = 1 & (( the_arity_of m) . 1) = ( a_Term C) by FINSEQ_1: 40;

      then

       A2: (m term t) = ( [m, the carrier of C] -tree <*t*>) & (m -trm p) = ( [m, the carrier of C] -tree <*t*>) by A1, ABCMIZ_1:def 30, ABCMIZ_1:def 35;

      

      hence ( main-constr (m term t)) = (((m term t) . {} ) `1 ) by Def9

      .= ( [m, the carrier of C] `1 ) by A2, TREES_4:def 4

      .= m;

    end;

    theorem :: ABCMIZ_A:45

    for a holds ( main-constr (( non_op MaxConstrSign ) term a)) = non_op

    proof

      set C = MaxConstrSign ;

      set m = ( non_op C);

      let a;

      

       A1: ( len ( the_arity_of m)) = 1 by Def14;

      ( the_arity_of m) = <* an_Adj *> by ABCMIZ_1: 38;

      then (( the_arity_of m) . 1) = ( an_Adj C) by FINSEQ_1: 40;

      then

       A2: (m term a) = ( [m, the carrier of C] -tree <*a*>) by A1, ABCMIZ_1:def 30;

      

      thus ( main-constr (m term a)) = (((m term a) . {} ) `1 ) by Def9

      .= ( [m, the carrier of C] `1 ) by A2, TREES_4:def 4

      .= non_op ;

    end;

    theorem :: ABCMIZ_A:46

    for m be binary constructor OperSymbol of MaxConstrSign holds for t1, t2 holds ( main-constr (m term (t1,t2))) = m

    proof

      set C = MaxConstrSign ;

      let m be binary constructor OperSymbol of C;

      let t1, t2;

      reconsider w1 = t1, w2 = t2 as Element of ( QuasiTerms C) by ABCMIZ_1: 49;

      reconsider p = <*w1, w2*> as FinSequence of ( QuasiTerms C);

      

       A1: ( len ( the_arity_of m)) = 2 by Def15;

      

      then ( the_arity_of m) = (2 |-> a_Term ) by ABCMIZ_1: 37

      .= <* a_Term , a_Term *> by FINSEQ_2: 61;

      then (( the_arity_of m) . 1) = ( a_Term C) & (( the_arity_of m) . 2) = ( a_Term C) & ( len p) = 2 by FINSEQ_1: 44;

      then

       A2: (m term (t1,t2)) = ( [m, the carrier of C] -tree <*t1, t2*>) & (m -trm p) = ( [m, the carrier of C] -tree p) by A1, ABCMIZ_1:def 31, ABCMIZ_1:def 35;

      

      hence ( main-constr (m term (t1,t2))) = (((m term (t1,t2)) . {} ) `1 ) by Def9

      .= ( [m, the carrier of C] `1 ) by A2, TREES_4:def 4

      .= m;

    end;

    theorem :: ABCMIZ_A:47

    for q be expression of MaxConstrSign , ( a_Type MaxConstrSign ) holds for a holds ( main-constr (( ast MaxConstrSign ) term (a,q))) = *

    proof

      set C = MaxConstrSign ;

      set m = ( ast C);

      let q be expression of MaxConstrSign , ( a_Type MaxConstrSign );

      let a;

      

       A1: ( len ( the_arity_of m)) = 2 by Def15;

      ( the_arity_of m) = <*( an_Adj C), ( a_Type C)*> by ABCMIZ_1: 38;

      then (( the_arity_of m) . 1) = ( an_Adj C) & (( the_arity_of m) . 2) = ( a_Type C) by FINSEQ_1: 44;

      then

       A2: (m term (a,q)) = ( [m, the carrier of C] -tree <*a, q*>) by A1, ABCMIZ_1:def 31;

      

      thus ( main-constr (m term (a,q))) = (((m term (a,q)) . {} ) `1 ) by Def9

      .= ( [m, the carrier of C] `1 ) by A2, TREES_4:def 4

      .= * ;

    end;

    definition

      let T be quasi-type;

      :: ABCMIZ_A:def20

      func constrs T -> set equals (( constrs ( the_base_of T)) \/ ( union { ( constrs a) : a in ( adjs T) }));

      coherence ;

    end

    theorem :: ABCMIZ_A:48

    for q be pure expression of MaxConstrSign , ( a_Type MaxConstrSign ) holds for A be finite Subset of ( QuasiAdjs MaxConstrSign ) holds ( constrs (A ast q)) = (( constrs q) \/ ( union { ( constrs a) : a in A }));

    theorem :: ABCMIZ_A:49

    ( constrs (a ast T)) = (( constrs a) \/ ( constrs T))

    proof

      set A = { ( constrs a9) : a9 in ( {a} \/ ( adjs T)) };

      set B = { ( constrs a9) : a9 in ( adjs T) };

      

       A1: A = (B \/ {( constrs a)})

      proof

        thus A c= (B \/ {( constrs a)})

        proof

          let z be object;

          assume z in A;

          then

          consider a9 such that

           A2: z = ( constrs a9) & a9 in ( {a} \/ ( adjs T));

          a9 in {a} or a9 in ( adjs T) by A2, XBOOLE_0:def 3;

          then a9 = a or a9 in ( adjs T) by TARSKI:def 1;

          then z in {( constrs a)} or z in B by A2, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

        let z be object;

        assume

         A3: z in (B \/ {( constrs a)});

        

         A4: a in {a} by TARSKI:def 1;

        per cases by A3, XBOOLE_0:def 3;

          suppose z in B;

          then

          consider a9 such that

           A5: z = ( constrs a9) & a9 in ( adjs T);

          a9 in ( {a} \/ ( adjs T)) by A5, XBOOLE_0:def 3;

          hence thesis by A5;

        end;

          suppose z in {( constrs a)};

          then z = ( constrs a) & a in ( {a} \/ ( adjs T)) by A4, TARSKI:def 1, XBOOLE_0:def 3;

          hence thesis;

        end;

      end;

      

      thus ( constrs (a ast T)) = (( constrs ( the_base_of (a ast T))) \/ ( union A))

      .= (( constrs ( the_base_of T)) \/ ( union A))

      .= (( constrs ( the_base_of T)) \/ (( union {( constrs a)}) \/ ( union B))) by A1, ZFMISC_1: 78

      .= (( constrs ( the_base_of T)) \/ (( constrs a) \/ ( union B))) by ZFMISC_1: 25

      .= ((( constrs ( the_base_of T)) \/ ( constrs a)) \/ ( union B)) by XBOOLE_1: 4

      .= (( constrs a) \/ (( constrs ( the_base_of T)) \/ ( union B))) by XBOOLE_1: 4

      .= (( constrs a) \/ ( constrs T));

    end;

    begin

    definition

      let C be initialized ConstructorSignature;

      let t,p be expression of C;

      :: ABCMIZ_A:def21

      pred t matches_with p means ex f be valuation of C st t = (p at f);

      reflexivity

      proof

        let t be expression of C;

        take f = the empty valuation of C;

        thus (t at f) = t by ABCMIZ_1: 139;

      end;

    end

    theorem :: ABCMIZ_A:50

    for t1,t2,t3 be expression of C st t1 matches_with t2 & t2 matches_with t3 holds t1 matches_with t3

    proof

      let t1,t2,t3 be expression of C;

      given f1 be valuation of C such that

       A1: t1 = (t2 at f1);

      given f2 be valuation of C such that

       A2: t2 = (t3 at f2);

      take (f2 at f1);

      thus thesis by A1, A2, ABCMIZ_1: 149;

    end;

    definition

      let C be initialized ConstructorSignature;

      let A,B be Subset of ( QuasiAdjs C);

      :: ABCMIZ_A:def22

      pred A matches_with B means ex f be valuation of C st (B at f) c= A;

      reflexivity

      proof

        let t be Subset of ( QuasiAdjs C);

        take f = the empty valuation of C;

        let x be object;

        assume x in (t at f);

        then ex a be quasi-adjective of C st x = (a at f) & a in t;

        hence x in t by ABCMIZ_1: 139;

      end;

    end

    theorem :: ABCMIZ_A:51

    for A1,A2,A3 be Subset of ( QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds A1 matches_with A3

    proof

      let t1,t2,t3 be Subset of ( QuasiAdjs C);

      given f1 be valuation of C such that

       A1: (t2 at f1) c= t1;

      given f2 be valuation of C such that

       A2: (t3 at f2) c= t2;

      take (f2 at f1);

      ((t3 at f2) at f1) c= (t2 at f1) by A2, ABCMIZ_1: 146;

      then ((t3 at f2) at f1) c= t1 by A1;

      hence thesis by ABCMIZ_1: 150;

    end;

    definition

      let C be initialized ConstructorSignature;

      let T,P be quasi-type of C;

      :: ABCMIZ_A:def23

      pred T matches_with P means ex f be valuation of C st (( adjs P) at f) c= ( adjs T) & (( the_base_of P) at f) = ( the_base_of T);

      reflexivity

      proof

        let t be quasi-type of C;

        take f = the empty valuation of C;

        thus (( adjs t) at f) c= ( adjs t)

        proof

          let x be object;

          assume x in (( adjs t) at f);

          then ex a be quasi-adjective of C st x = (a at f) & a in ( adjs t);

          hence x in ( adjs t) by ABCMIZ_1: 139;

        end;

        thus thesis by ABCMIZ_1: 139;

      end;

    end

    theorem :: ABCMIZ_A:52

    for T1,T2,T3 be quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds T1 matches_with T3

    proof

      let t1,t2,t3 be quasi-type of C;

      given f1 be valuation of C such that

       A1: (( adjs t2) at f1) c= ( adjs t1) & (( the_base_of t2) at f1) = ( the_base_of t1);

      given f2 be valuation of C such that

       A2: (( adjs t3) at f2) c= ( adjs t2) & (( the_base_of t3) at f2) = ( the_base_of t2);

      take (f2 at f1);

      ((( adjs t3) at f2) at f1) c= (( adjs t2) at f1) by A2, ABCMIZ_1: 146;

      then ((( adjs t3) at f2) at f1) c= ( adjs t1) by A1;

      hence thesis by A1, A2, ABCMIZ_1: 149, ABCMIZ_1: 150;

    end;

    definition

      let C be initialized ConstructorSignature;

      let t1,t2 be expression of C;

      let f be valuation of C;

      ::$Notion-Name

      :: ABCMIZ_A:def24

      pred f unifies t1,t2 means (t1 at f) = (t2 at f);

    end

    theorem :: ABCMIZ_A:53

    for t1,t2 be expression of C holds for f be valuation of C st f unifies (t1,t2) holds f unifies (t2,t1);

    definition

      let C be initialized ConstructorSignature;

      let t1,t2 be expression of C;

      :: ABCMIZ_A:def25

      pred t1,t2 are_unifiable means ex f be valuation of C st f unifies (t1,t2);

      reflexivity

      proof

        let t be expression of C;

        set f = the valuation of C;

        take f;

        thus (t at f) = (t at f);

      end;

      symmetry

      proof

        let t1,t2 be expression of C;

        given f be valuation of C such that

         A1: f unifies (t1,t2);

        take f;

        thus (t2 at f) = (t1 at f) by A1;

      end;

    end

    definition

      let C be initialized ConstructorSignature;

      let t1,t2 be expression of C;

      :: ABCMIZ_A:def26

      pred t1,t2 are_weakly-unifiable means ex g be irrelevant one-to-one valuation of C st ( variables_in t2) c= ( dom g) & (t1,(t2 at g)) are_unifiable ;

      reflexivity

      proof

        let t be expression of C;

        take (C idval ( variables_in t));

        thus thesis by ABCMIZ_1: 131, ABCMIZ_1: 137;

      end;

    end

    theorem :: ABCMIZ_A:54

    for t1,t2 be expression of C st (t1,t2) are_unifiable holds (t1,t2) are_weakly-unifiable

    proof

      let t1,t2 be expression of C;

      given f be valuation of C such that

       A1: f unifies (t1,t2);

      take g = (C idval ( variables_in t2));

      thus ( variables_in t2) c= ( dom g) by ABCMIZ_1: 131;

      take f;

      thus f unifies (t1,(t2 at g)) by A1, ABCMIZ_1: 137;

    end;

    definition

      let C be initialized ConstructorSignature;

      let t,t1,t2 be expression of C;

      :: ABCMIZ_A:def27

      pred t is_a_unification_of t1,t2 means ex f be valuation of C st f unifies (t1,t2) & t = (t1 at f);

    end

    theorem :: ABCMIZ_A:55

    for t1,t2,t be expression of C st t is_a_unification_of (t1,t2) holds t is_a_unification_of (t2,t1)

    proof

      let t1,t2,t be expression of C;

      given f be valuation of C such that

       A1: f unifies (t1,t2) & t = (t1 at f);

      take f;

      thus f unifies (t2,t1) & t = (t2 at f) by A1;

    end;

    theorem :: ABCMIZ_A:56

    for t1,t2,t be expression of C st t is_a_unification_of (t1,t2) holds t matches_with t1 & t matches_with t2

    proof

      let t1,t2,t be expression of C;

      given f be valuation of C such that

       A1: f unifies (t1,t2) & t = (t1 at f);

      thus ex f be valuation of C st t = (t1 at f) by A1;

      take f;

      thus t = (t2 at f) by A1;

    end;

    definition

      let C be initialized ConstructorSignature;

      let t,t1,t2 be expression of C;

      :: ABCMIZ_A:def28

      pred t is_a_general-unification_of t1,t2 means t is_a_unification_of (t1,t2) & for u be expression of C st u is_a_unification_of (t1,t2) holds u matches_with t;

    end

    begin

    theorem :: ABCMIZ_A:57

    

     Th57: for n be Nat holds for s be SortSymbol of MaxConstrSign holds ex m be constructor OperSymbol of s st ( len ( the_arity_of m)) = n

    proof

      set C = MaxConstrSign ;

      let n be Nat;

      let s be SortSymbol of C;

      deffunc F( Nat) = [ {} , $1];

      consider l be FinSequence such that

       A1: ( len l) = n and

       A2: for i st i in ( dom l) holds (l . i) = F(i) from FINSEQ_1:sch 2;

      

       A3: l is one-to-one

      proof

        let i,j be object such that

         A4: i in ( dom l) & j in ( dom l) & (l . i) = (l . j);

        reconsider i, j as Nat by A4;

        (l . i) = F(i) & (l . i) = F(j) by A2, A4;

        then i = ( F(j) `2 );

        hence thesis;

      end;

      ( rng l) c= Vars

      proof

        let z be object;

        assume z in ( rng l);

        then

        consider a be object such that

         A5: a in ( dom l) & z = (l . a) by FUNCT_1:def 3;

        reconsider a as Nat by A5;

        z = F(a) by A2, A5;

        hence thesis by ABCMIZ_1: 25;

      end;

      then

      reconsider l as one-to-one FinSequence of Vars by A3, FINSEQ_1:def 4;

      for i be Nat, x be variable st i in ( dom l) & x = (l . i) holds for y be variable st y in ( vars x) holds ex j be Nat st j in ( dom l) & j < i & y = (l . j)

      proof

        let i, x;

        assume i in ( dom l) & x = (l . i);

        then x = F(i) by A2;

        hence thesis;

      end;

      then

      reconsider l as quasi-loci by ABCMIZ_1: 30;

      set m = [s, [l, 0 ]];

      the carrier of C = { a_Type , an_Adj , a_Term } by ABCMIZ_1:def 9;

      then

       A6: m in Constructors by Th28;

      then m in ( { * , non_op } \/ Constructors ) by XBOOLE_0:def 3;

      then

      reconsider m as constructor OperSymbol of C by A6, Th42, ABCMIZ_1:def 24;

      ( the_result_sort_of m) = (m `1 ) by ABCMIZ_1:def 24

      .= s;

      then

      reconsider m as constructor OperSymbol of s by ABCMIZ_1:def 32;

      take m;

      

      thus ( len ( the_arity_of m)) = ( card ((m `2 ) `1 )) by ABCMIZ_1:def 24

      .= ( card ( [l, 0 ] `1 ))

      .= ( card l)

      .= n by A1;

    end;

    theorem :: ABCMIZ_A:58

    

     Th58: for l holds for s be SortSymbol of MaxConstrSign holds for m be constructor OperSymbol of s st ( len ( the_arity_of m)) = ( len l) holds ( variables_in (m -trm ( args l))) = ( rng l)

    proof

      let l;

      set X = ( rng l);

      set n = ( len l);

      set C = MaxConstrSign ;

      let s be SortSymbol of C;

      let m be constructor OperSymbol of s such that

       A1: ( len ( the_arity_of m)) = n;

      set p = ( args l);

      set Y = { ( variables_in t) where t be quasi-term of C : t in ( rng p) };

      

       A2: ( len p) = ( len ( the_arity_of m)) by A1, Def18;

      then

       A3: ( variables_in (m -trm p)) = ( union Y) by ABCMIZ_1: 90;

      

       A4: ( dom p) = ( dom l) by A1, A2, FINSEQ_3: 29;

      thus ( variables_in (m -trm p)) c= X

      proof

        let s be object;

        assume s in ( variables_in (m -trm p));

        then

        consider A be set such that

         A5: s in A & A in Y by A3, TARSKI:def 4;

        consider t be quasi-term of C such that

         A6: A = ( variables_in t) & t in ( rng p) by A5;

        consider z be object such that

         A7: z in ( dom p) & t = (p . z) by A6, FUNCT_1:def 3;

        reconsider z as Element of NAT by A7;

        (l . z) = (l /. z) by A4, A7, PARTFUN1:def 6;

        then

         A8: (l /. z) in X by A4, A7, FUNCT_1:def 3;

        (p . z) = ((l /. z) -term C) by A4, A7, Def18;

        then A = {(l /. z)} by A6, A7, ABCMIZ_1: 86;

        hence thesis by A5, A8, TARSKI:def 1;

      end;

      let s be object;

      assume s in X;

      then

      consider z be object such that

       A9: z in ( dom l) & s = (l . z) by FUNCT_1:def 3;

      reconsider z as Element of NAT by A9;

      set t = ((l /. z) -term C);

      (p . z) = t & (l . z) = (l /. z) by A9, Def18, PARTFUN1:def 6;

      then ( variables_in t) = {s} & t in ( rng p) by A4, A9, ABCMIZ_1: 86, FUNCT_1:def 3;

      then s in {s} & {s} in Y by TARSKI:def 1;

      hence thesis by A3, TARSKI:def 4;

    end;

    theorem :: ABCMIZ_A:59

    

     Th59: for X be finite Subset of Vars st ( varcl X) = X holds for s be SortSymbol of MaxConstrSign holds ex m be constructor OperSymbol of s st ex p be FinSequence of ( QuasiTerms MaxConstrSign ) st ( len p) = ( len ( the_arity_of m)) & ( vars (m -trm p)) = X

    proof

      let X be finite Subset of Vars ;

      assume

       A1: ( varcl X) = X;

      then

      consider l such that

       A2: ( rng l) = X by Th31;

      set n = ( len l);

      set C = MaxConstrSign ;

      let s be SortSymbol of C;

      consider m be constructor OperSymbol of s such that

       A3: ( len ( the_arity_of m)) = n by Th57;

      take m;

      set p = ( args l);

      take p;

      thus ( len p) = ( len ( the_arity_of m)) by A3, Def18;

      thus thesis by A1, A2, A3, Th58;

    end;

    definition

      let d be PartFunc of Vars , QuasiTypes ;

      :: ABCMIZ_A:def29

      attr d is even means for x, T st x in ( dom d) & T = (d . x) holds ( vars T) = ( vars x);

    end

    definition

      let l be quasi-loci;

      :: ABCMIZ_A:def30

      mode type-distribution of l -> PartFunc of Vars , QuasiTypes means

      : Def30: ( dom it ) = ( rng l) & it is even;

      existence

      proof

        defpred P[ object, object] means ex x, T st $1 = x & $2 = T & ( vars T) = ( vars x);

        

         A1: for z be object st z in ( rng l) holds ex y be object st P[z, y]

        proof

          set C = MaxConstrSign ;

          let z be object;

          assume z in ( rng l);

          then

          reconsider x = z as variable;

          ( varcl ( vars x)) = ( vars x) by Th2;

          then

          consider m be constructor OperSymbol of ( a_Type C), p be FinSequence of ( QuasiTerms C) such that

           A2: ( len p) = ( len ( the_arity_of m)) & ( vars (m -trm p)) = ( vars x) by Th59;

          ( a_Type C) in the carrier of C & the carrier of C c= ( rng the ResultSort of C) by ABCMIZ_1:def 54;

          then

          consider o be object such that

           A3: o in ( dom the ResultSort of C) & ( a_Type C) = (the ResultSort of C . o) by FUNCT_1:def 3;

          reconsider o as OperSymbol of C by A3;

          ( the_result_sort_of o) = ( a_Type C) by A3;

          then ( the_result_sort_of m) = ( a_Type C) by ABCMIZ_1:def 32;

          then

          reconsider q = (m -trm p) as pure expression of C, ( a_Type C) by A2, ABCMIZ_1: 75;

          set B = ( {} ( QuasiAdjs C));

          reconsider T = (B ast q) as quasi-type;

          take T, x, T;

          thus thesis by A2, ABCMIZ_1: 106;

        end;

        consider f be Function such that

         A4: ( dom f) = ( rng l) and

         A5: for z be object st z in ( rng l) holds P[z, (f . z)] from CLASSES1:sch 1( A1);

        ( rng f) c= QuasiTypes

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider z be object such that

           A6: z in ( dom f) & y = (f . z) by FUNCT_1:def 3;

           P[z, y] by A4, A5, A6;

          hence thesis by ABCMIZ_1:def 43;

        end;

        then

        reconsider f as PartFunc of Vars , QuasiTypes by A4, RELSET_1: 4;

        take f;

        thus ( dom f) = ( rng l) by A4;

        let x, T;

        assume x in ( dom f) & T = (f . x);

        then P[x, T] by A4, A5;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_A:60

    for l be empty quasi-loci holds {} is type-distribution of l

    proof

      let l be empty quasi-loci;

      reconsider d = {} as PartFunc of Vars , QuasiTypes by RELSET_1: 12;

      ( dom d) = ( rng l) & d is even;

      hence thesis by Def30;

    end;