msafree2.miz



    begin

    definition

      let S be ManySortedSign;

      mode Vertex of S is Element of S;

    end

    definition

      let S be non empty ManySortedSign;

      :: MSAFREE2:def1

      func SortsWithConstants S -> Subset of S equals

      : Def1: { v where v be SortSymbol of S : v is with_const_op } if S is non void

      otherwise {} ;

      coherence

      proof

        hereby

          defpred P[ SortSymbol of S] means $1 is with_const_op;

          assume S is non void;

          { v where v be SortSymbol of S : P[v] } is Subset of S from DOMAIN_1:sch 7;

          hence { v where v be SortSymbol of S : v is with_const_op } is Subset of S;

        end;

        assume S is void;

        thus thesis by SUBSET_1: 1;

      end;

      consistency ;

    end

    definition

      let G be non empty ManySortedSign;

      :: MSAFREE2:def2

      func InputVertices G -> Subset of G equals (the carrier of G \ ( rng the ResultSort of G));

      coherence ;

      :: MSAFREE2:def3

      func InnerVertices G -> Subset of G equals ( rng the ResultSort of G);

      coherence ;

    end

    theorem :: MSAFREE2:1

    for G be void non empty ManySortedSign holds ( InputVertices G) = the carrier of G;

    theorem :: MSAFREE2:2

    

     Th2: for G be non void non empty ManySortedSign, v be Vertex of G st v in ( InputVertices G) holds not ex o be OperSymbol of G st ( the_result_sort_of o) = v

    proof

      let G be non void non empty ManySortedSign, v be Vertex of G;

      assume

       A1: v in ( InputVertices G);

      let o be OperSymbol of G such that

       A2: ( the_result_sort_of o) = v;

      o in the carrier' of G;

      then o in ( dom the ResultSort of G) by FUNCT_2:def 1;

      then v in ( rng the ResultSort of G) by A2, FUNCT_1:def 3;

      hence contradiction by A1, XBOOLE_0:def 5;

    end;

    theorem :: MSAFREE2:3

    

     Th3: for G be non empty ManySortedSign holds ( SortsWithConstants G) c= ( InnerVertices G)

    proof

      let G be non empty ManySortedSign;

      per cases ;

        suppose G is void;

        hence thesis by Def1;

      end;

        suppose

         A1: G is non void;

        let x be object;

        assume

         A2: x in ( SortsWithConstants G);

        ( SortsWithConstants G) = { v where v be SortSymbol of G : v is with_const_op } by A1, Def1;

        then

        consider x9 be SortSymbol of G such that

         A3: x9 = x and

         A4: x9 is with_const_op by A2;

        ex o be OperSymbol of G st (the Arity of G . o) = {} & (the ResultSort of G . o) = x9 by A4;

        hence thesis by A1, A3, FUNCT_2: 4;

      end;

    end;

    theorem :: MSAFREE2:4

    for G be non empty ManySortedSign holds ( InputVertices G) misses ( SortsWithConstants G)

    proof

      let G be non empty ManySortedSign;

      ( InputVertices G) misses ( InnerVertices G) by XBOOLE_1: 79;

      hence thesis by Th3, XBOOLE_1: 63;

    end;

    definition

      let IT be non empty ManySortedSign;

      :: MSAFREE2:def4

      attr IT is with_input_V means

      : Def4: ( InputVertices IT) <> {} ;

    end

    registration

      cluster non void with_input_V for non empty ManySortedSign;

      existence

      proof

         {} in { {} , { {} }} by TARSKI:def 2;

        then

        reconsider g = ( { {} } --> {} ) as Function of { {} }, { {} , { {} }} by FUNCOP_1: 46;

         {} in ( { {} , { {} }} * ) by FINSEQ_1: 49;

        then

        reconsider f = ( { {} } --> {} ) as Function of { {} }, ( { {} , { {} }} * ) by FUNCOP_1: 46;

        take c = ManySortedSign (# { {} , { {} }}, { {} }, f, g #);

        ( rng the ResultSort of c) = { {} } by FUNCOP_1: 8;

        then { {} } in the carrier of c & not { {} } in ( rng the ResultSort of c) by TARSKI:def 2;

        then ( InputVertices c) <> {} by XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    registration

      let G be with_input_V non empty ManySortedSign;

      cluster ( InputVertices G) -> non empty;

      coherence by Def4;

    end

    registration

      let G be non void non empty ManySortedSign;

      cluster ( InnerVertices G) -> non empty;

      coherence

      proof

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

        hence thesis by RELAT_1: 42;

      end;

    end

    definition

      let S be non empty ManySortedSign;

      let MSA be non-empty MSAlgebra over S;

      :: MSAFREE2:def5

      mode InputValues of MSA -> ManySortedSet of ( InputVertices S) means for v be Vertex of S st v in ( InputVertices S) holds (it . v) in (the Sorts of MSA . v);

      existence

      proof

        set e = the Element of ( product the Sorts of MSA);

        set p = (e | ( InputVertices S));

        

         A1: ( dom the Sorts of MSA) = the carrier of S & ex g be Function st e = g & ( dom g) = ( dom the Sorts of MSA) & for x be object st x in ( dom the Sorts of MSA) holds (g . x) in (the Sorts of MSA . x) by CARD_3:def 5, PARTFUN1:def 2;

        reconsider p as ManySortedSet of ( InputVertices S);

        take p;

        let v be Vertex of S;

        assume v in ( InputVertices S);

        then (p . v) = (e . v) by FUNCT_1: 49;

        hence thesis by A1;

      end;

    end

    definition

      let S be non empty ManySortedSign;

      :: MSAFREE2:def6

      attr S is Circuit-like means

      : Def6: for S9 be non void non empty ManySortedSign st S9 = S holds for o1,o2 be OperSymbol of S9 st ( the_result_sort_of o1) = ( the_result_sort_of o2) holds o1 = o2;

    end

    registration

      cluster void -> Circuit-like for non empty ManySortedSign;

      coherence ;

    end

    registration

      cluster non void Circuit-like strict for non empty ManySortedSign;

      existence

      proof

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

        then

        reconsider f = ( { {} } --> {} ) as Function of { {} }, ( { {} } * ) by FUNCOP_1: 46;

        reconsider g = ( { {} } --> {} ) as Function of { {} }, { {} };

        take c = ManySortedSign (# { {} }, { {} }, f, g #);

        c is Circuit-like

        proof

          let S be non void non empty ManySortedSign;

          assume

           A1: S = c;

          let v1,v2 be OperSymbol of S such that ( the_result_sort_of v1) = ( the_result_sort_of v2);

          

          thus v1 = {} by A1, TARSKI:def 1

          .= v2 by A1, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      let IIG be Circuit-like non void non empty ManySortedSign;

      let v be Vertex of IIG;

      :: MSAFREE2:def7

      func action_at v -> OperSymbol of IIG means ( the_result_sort_of it ) = v;

      existence

      proof

        consider x be object such that

         A2: x in ( dom the ResultSort of IIG) and

         A3: (the ResultSort of IIG . x) = v by A1, FUNCT_1:def 3;

        reconsider x as OperSymbol of IIG by A2;

        take x;

        thus thesis by A3;

      end;

      uniqueness by Def6;

    end

    begin

    theorem :: MSAFREE2:5

    for S be non void non empty ManySortedSign, A be MSAlgebra over S, o be OperSymbol of S, p be FinSequence st ( len p) = ( len ( the_arity_of o)) & for k be Nat st k in ( dom p) holds (p . k) in (the Sorts of A . (( the_arity_of o) /. k)) holds p in ( Args (o,A))

    proof

      let S be non void non empty ManySortedSign, A be MSAlgebra over S, o be OperSymbol of S, p be FinSequence such that

       A1: ( len p) = ( len ( the_arity_of o)) and

       A2: for k be Nat st k in ( dom p) holds (p . k) in (the Sorts of A . (( the_arity_of o) /. k));

      set D = (the Sorts of A * ( the_arity_of o));

      

       A3: ( dom p) = ( dom ( the_arity_of o)) by A1, FINSEQ_3: 29;

      ( rng ( the_arity_of o)) c= the carrier of S;

      then ( rng ( the_arity_of o)) c= ( dom the Sorts of A) by PARTFUN1:def 2;

      then

       A4: ( dom p) = ( dom D) by A3, RELAT_1: 27;

       A5:

      now

        let x be object;

        assume

         A6: x in ( dom D);

        then

        reconsider k = x as Nat;

        (D . k) = (the Sorts of A . (( the_arity_of o) . k)) by A6, FUNCT_1: 12

        .= (the Sorts of A . (( the_arity_of o) /. k)) by A3, A4, A6, PARTFUN1:def 6;

        hence (p . x) in (D . x) by A2, A4, A6;

      end;

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

      

      then (((the Sorts of A # ) * the Arity of S) . o) = ((the Sorts of A # ) . ( the_arity_of o)) by FUNCT_1: 13

      .= ( product (the Sorts of A * ( the_arity_of o))) by FINSEQ_2:def 5;

      hence thesis by A4, A5, CARD_3:def 5;

    end;

    definition

      let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over S;

      :: MSAFREE2:def8

      func FreeEnv MSA -> free strict non-empty MSAlgebra over S equals ( FreeMSA the Sorts of MSA);

      coherence by MSAFREE: 17;

    end

    definition

      let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over S;

      :: MSAFREE2:def9

      func Eval MSA -> ManySortedFunction of ( FreeEnv MSA), MSA means it is_homomorphism (( FreeEnv MSA),MSA) & for s be SortSymbol of S, x,y be set st y in ( FreeSort (the Sorts of MSA,s)) & y = ( root-tree [x, s]) & x in (the Sorts of MSA . s) holds ((it . s) . y) = x;

      existence

      proof

        reconsider A = ( FreeGen the Sorts of MSA) as free GeneratorSet of ( FreeEnv MSA) by MSAFREE: 16;

        defpred P[ object, object] means ex s be SortSymbol of S, f be Function of (A . s), (the Sorts of MSA . s) st f = $2 & s = $1 & for x,y be set st y in (A . s) & y = ( root-tree [x, s]) & x in (the Sorts of MSA . s) holds (f . y) = x;

        

         A1: for i be object st i in the carrier of S holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as SortSymbol of S;

          defpred P[ object, object] means $1 = ( root-tree [$2, s]);

          

           A2: for e be object st e in (A . s) holds ex u be object st u in (the Sorts of MSA . s) & P[e, u]

          proof

            let e be object;

            assume e in (A . s);

            then e in ( FreeGen (s,the Sorts of MSA)) by MSAFREE:def 16;

            then

            consider a be set such that

             A3: a in (the Sorts of MSA . s) & e = ( root-tree [a, s]) by MSAFREE:def 15;

            thus thesis by A3;

          end;

          consider j be Function such that

           A4: ( dom j) = (A . s) & ( rng j) c= (the Sorts of MSA . s) & for e be object st e in (A . s) holds P[e, (j . e)] from FUNCT_1:sch 6( A2);

          reconsider f = j as Function of (A . s), (the Sorts of MSA . s) by A4, FUNCT_2:def 1, RELSET_1: 4;

          take j, s;

          take f;

          thus f = j & s = i;

          let x,y be set such that

           A5: y in (A . s) and

           A6: y = ( root-tree [x, s]) and x in (the Sorts of MSA . s);

          y = ( root-tree [(j . y), s]) by A4, A5;

          then [x, s] = [(j . y), s] by A6, TREES_4: 4;

          hence thesis by XTUPLE_0: 1;

        end;

        consider f be ManySortedSet of the carrier of S such that

         A7: for i be object st i in the carrier of S holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        now

          let x be object;

          assume x in ( dom f);

          then x in the carrier of S;

          then P[x, (f . x)] by A7;

          hence (f . x) is Function;

        end;

        then

        reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;

        now

          let i be object;

          assume i in the carrier of S;

          then P[i, (f . i)] by A7;

          hence (f . i) is Function of (A . i), (the Sorts of MSA . i);

        end;

        then

        reconsider f as ManySortedFunction of A, the Sorts of MSA by PBOOLE:def 15;

        consider IT be ManySortedFunction of ( FreeEnv MSA), MSA such that

         A8: IT is_homomorphism (( FreeEnv MSA),MSA) and

         A9: (IT || A) = f by MSAFREE:def 5;

        take IT;

        thus IT is_homomorphism (( FreeEnv MSA),MSA) by A8;

        let s be SortSymbol of S, x,y be set;

        

         A10: ex t be SortSymbol of S, g be Function of (A . t), (the Sorts of MSA . t) st g = (f . s) & t = s & for x,y be set st y in (A . t) & y = ( root-tree [x, t]) & x in (the Sorts of MSA . t) holds (g . y) = x by A7;

        assume that y in ( FreeSort (the Sorts of MSA,s)) and

         A11: y = ( root-tree [x, s]) & x in (the Sorts of MSA . s);

        y in ( FreeGen (s,the Sorts of MSA)) by A11, MSAFREE:def 15;

        then

         A12: y in (A . s) by MSAFREE:def 16;

        

        hence ((IT . s) . y) = (((IT . s) | (A . s)) . y) by FUNCT_1: 49

        .= ((f . s) . y) by A9, MSAFREE:def 1

        .= x by A11, A12, A10;

      end;

      uniqueness

      proof

        defpred P[ set, set, set] means $3 = ( root-tree [$2, $1]);

        let IT1,IT2 be ManySortedFunction of ( FreeEnv MSA), MSA;

        reconsider IT19 = IT1, IT29 = IT2 as ManySortedFunction of ( FreeMSA the Sorts of MSA), MSA;

        assume IT1 is_homomorphism (( FreeEnv MSA),MSA);

        then

         A13: IT19 is_homomorphism (( FreeMSA the Sorts of MSA),MSA);

        assume

         A14: for s be SortSymbol of S, x,y be set st y in ( FreeSort (the Sorts of MSA,s)) & y = ( root-tree [x, s]) & x in (the Sorts of MSA . s) holds ((IT1 . s) . y) = x;

        

         A15: for s be SortSymbol of S, x,y be set st y in ( FreeGen (s,the Sorts of MSA)) holds ((IT19 . s) . y) = x iff P[s, x, y]

        proof

          let s be SortSymbol of S, x,y be set;

          assume

           A16: y in ( FreeGen (s,the Sorts of MSA));

          then

          consider a be set such that

           A17: a in (the Sorts of MSA . s) and

           A18: y = ( root-tree [a, s]) by MSAFREE:def 15;

          y in (( FreeSort the Sorts of MSA) . s) by A16;

          then

           A19: y in ( FreeSort (the Sorts of MSA,s)) by MSAFREE:def 11;

          hence ((IT19 . s) . y) = x implies y = ( root-tree [x, s]) by A14, A17, A18;

          assume y = ( root-tree [x, s]);

          then [x, s] = [a, s] by A18, TREES_4: 4;

          then x = a by XTUPLE_0: 1;

          hence thesis by A14, A19, A17, A18;

        end;

        assume IT2 is_homomorphism (( FreeEnv MSA),MSA);

        then

         A20: IT29 is_homomorphism (( FreeMSA the Sorts of MSA),MSA);

        assume

         A21: for s be SortSymbol of S, x,y be set st y in ( FreeSort (the Sorts of MSA,s)) & y = ( root-tree [x, s]) & x in (the Sorts of MSA . s) holds ((IT2 . s) . y) = x;

        

         A22: for s be SortSymbol of S, x,y be set st y in ( FreeGen (s,the Sorts of MSA)) holds ((IT29 . s) . y) = x iff P[s, x, y]

        proof

          let s be SortSymbol of S, x,y be set;

          assume

           A23: y in ( FreeGen (s,the Sorts of MSA));

          then

          consider a be set such that

           A24: a in (the Sorts of MSA . s) and

           A25: y = ( root-tree [a, s]) by MSAFREE:def 15;

          y in (( FreeSort the Sorts of MSA) . s) by A23;

          then

           A26: y in ( FreeSort (the Sorts of MSA,s)) by MSAFREE:def 11;

          hence ((IT29 . s) . y) = x implies y = ( root-tree [x, s]) by A21, A24, A25;

          assume y = ( root-tree [x, s]);

          then [x, s] = [a, s] by A25, TREES_4: 4;

          then x = a by XTUPLE_0: 1;

          hence thesis by A21, A26, A24, A25;

        end;

        IT19 = IT29 from MSAFREE1:sch 3( A13, A15, A20, A22);

        hence thesis;

      end;

    end

    theorem :: MSAFREE2:6

    

     Th6: for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A

    proof

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S;

      reconsider theA = the MSAlgebra of A as non-empty MSAlgebra over S;

      reconsider AA = the Sorts of A as non-empty MSSubset of theA by PBOOLE:def 18;

      set GAA = ( GenMSAlg AA);

      

       A1: the Sorts of GAA is MSSubset of A by MSUALG_2:def 9;

      now

        let B be MSSubset of A such that

         A2: B = the Sorts of GAA;

        reconsider C = B as MSSubset of theA;

        

         A3: C is opers_closed by A2, MSUALG_2:def 9;

         A4:

        now

          let o be OperSymbol of S;

          C is_closed_on o by A3;

          then

           A5: ( rng (( Den (o, the MSAlgebra of A)) | (((C # ) * the Arity of S) . o))) c= ((C * the ResultSort of S) . o);

          thus B is_closed_on o by A5;

        end;

        hence B is opers_closed;

        reconsider OAB = ( Opers (A,B)) as ManySortedFunction of ((C # ) * the Arity of S), (C * the ResultSort of S);

         A6:

        now

          let o be OperSymbol of S;

          

           A7: C is_closed_on o & ( Den (o,A)) = ( Den (o, the MSAlgebra of A)) by A3;

          

          thus (OAB . o) = (o /. B) by MSUALG_2:def 8

          .= (( Den (o,A)) | (((B # ) * the Arity of S) . o)) by A4, MSUALG_2:def 7

          .= (o /. C) by A7, MSUALG_2:def 7;

        end;

        the Charact of GAA = ( Opers (theA,C)) by A2, MSUALG_2:def 9;

        hence the Charact of GAA = ( Opers (A,B)) by A6, MSUALG_2:def 8;

      end;

      then

      reconsider GAA as strict non-empty MSSubAlgebra of A by A1, MSUALG_2:def 9;

      reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def 18;

       A8:

      now

        let U1 be MSSubAlgebra of A;

         A9:

        now

          let B be MSSubset of theA such that

           A10: B = the Sorts of U1;

          reconsider C = B as MSSubset of A;

          

           A11: C is opers_closed by A10, MSUALG_2:def 9;

           A12:

          now

            let o be OperSymbol of S;

            C is_closed_on o by A11;

            then

             A13: ( rng (( Den (o,A)) | (((C # ) * the Arity of S) . o))) c= ((C * the ResultSort of S) . o);

            thus B is_closed_on o by A13;

          end;

          hence B is opers_closed;

          reconsider OAB = ( Opers (theA,B)) as ManySortedFunction of ((C # ) * the Arity of S), (C * the ResultSort of S);

           A14:

          now

            let o be OperSymbol of S;

            

             A15: ( Den (o,A)) = ( Den (o, the MSAlgebra of A));

            

             A16: C is_closed_on o by A11;

            

            thus (OAB . o) = (o /. B) by MSUALG_2:def 8

            .= (( Den (o,A)) | (((B # ) * the Arity of S) . o)) by A12, A15, MSUALG_2:def 7

            .= (o /. C) by A16, MSUALG_2:def 7;

          end;

          the Charact of U1 = ( Opers (A,C)) by A10, MSUALG_2:def 9;

          hence the Charact of U1 = ( Opers (theA,B)) by A14, MSUALG_2:def 8;

        end;

        the Sorts of U1 is MSSubset of the MSAlgebra of A by MSUALG_2:def 9;

        then

        reconsider U2 = U1 as MSSubAlgebra of theA by A9, MSUALG_2:def 9;

        assume BB is MSSubset of U1;

        then GAA is MSSubAlgebra of U2 by MSUALG_2:def 17;

        hence GAA is MSSubAlgebra of U1;

      end;

      BB is MSSubset of ( GenMSAlg AA) by MSUALG_2:def 17;

      then ( GenMSAlg AA) = ( GenMSAlg BB) by A8, MSUALG_2:def 17;

      then the Sorts of ( GenMSAlg BB) = the Sorts of A by MSUALG_2: 21;

      hence thesis by MSAFREE:def 4;

    end;

    definition

      let S be non empty ManySortedSign;

      let IT be MSAlgebra over S;

      :: MSAFREE2:def10

      attr IT is finitely-generated means

      : Def10: for S9 be non void non empty ManySortedSign st S9 = S holds for A be MSAlgebra over S9 st A = IT holds ex G be GeneratorSet of A st G is finite-yielding if not S is void

      otherwise the Sorts of IT is finite-yielding;

      consistency ;

    end

    definition

      let S be non empty ManySortedSign;

      let IT be MSAlgebra over S;

      :: MSAFREE2:def11

      attr IT is finite-yielding means the Sorts of IT is finite-yielding;

    end

    registration

      let S be non empty ManySortedSign;

      cluster finite-yielding -> finitely-generated for non-empty MSAlgebra over S;

      coherence

      proof

        let A be non-empty MSAlgebra over S;

        assume

         A1: A is finite-yielding;

        per cases ;

          case S is non void;

          let S9 be non void non empty ManySortedSign such that

           A2: S9 = S;

          let A9 be MSAlgebra over S9;

          assume A9 = A;

          then

          reconsider G = the Sorts of A as GeneratorSet of A9 by A2, Th6;

          take G;

          thus thesis by A1;

        end;

          case S is void;

          thus thesis by A1;

        end;

      end;

    end

    definition

      let S be non empty ManySortedSign;

      :: MSAFREE2:def12

      func Trivial_Algebra S -> strict MSAlgebra over S means

      : Def12: the Sorts of it = (the carrier of S --> { 0 });

      existence

      proof

        reconsider f = (the carrier of S --> { 0 }) as ManySortedSet of the carrier of S;

        set Ch = the ManySortedFunction of ((f # ) * the Arity of S), (f * the ResultSort of S);

        take MSAlgebra (# f, Ch #);

        thus thesis;

      end;

      uniqueness

      proof

        let A1,A2 be strict MSAlgebra over S such that

         A1: the Sorts of A1 = (the carrier of S --> { 0 }) and

         A2: the Sorts of A2 = (the carrier of S --> { 0 });

        set B = the Sorts of A1;

        

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

        now

          let i be object;

          set A = ((B * the ResultSort of S) . i);

          assume

           A4: i in the carrier' of S;

          

          then

           A5: A = (B . (the ResultSort of S . i)) by A3, FUNCT_1: 13

          .= { 0 } by A1, A4, FUNCOP_1: 7, FUNCT_2: 5;

          then

          reconsider A as non empty set;

          reconsider f1 = (the Charact of A1 . i), f2 = (the Charact of A2 . i) as Function of (((B # ) * the Arity of S) . i), A by A1, A2, A4, PBOOLE:def 15;

          now

            let x be object;

            assume

             A6: x in (((B # ) * the Arity of S) . i);

            then (f1 . x) in A by FUNCT_2: 5;

            then

             A7: (f1 . x) = 0 by A5, TARSKI:def 1;

            (f2 . x) in A by A6, FUNCT_2: 5;

            hence (f1 . x) = (f2 . x) by A5, A7, TARSKI:def 1;

          end;

          hence (the Charact of A1 . i) = (the Charact of A2 . i) by FUNCT_2: 12;

        end;

        hence thesis by A1, A2, PBOOLE: 3;

      end;

    end

    registration

      let S be non empty ManySortedSign;

      cluster finite-yielding non-empty strict for MSAlgebra over S;

      existence

      proof

        take T = ( Trivial_Algebra S);

        

         A1: the Sorts of T = (the carrier of S --> { 0 }) by Def12;

        the Sorts of T is finite-yielding by A1, FUNCOP_1: 7;

        hence T is finite-yielding;

        thus T is non-empty by A1;

        thus thesis;

      end;

    end

    definition

      let IT be non empty ManySortedSign;

      :: MSAFREE2:def13

      attr IT is monotonic means for A be finitely-generated non-empty MSAlgebra over IT holds A is finite-yielding;

    end

    registration

      cluster non void finite monotonic Circuit-like for non empty ManySortedSign;

      existence

      proof

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

        then

        reconsider f = ( { [ {} , { {} }]} --> {} ) as Function of { [ {} , { {} }]}, ( { {} } * ) by FUNCOP_1: 46;

        reconsider g = ( { [ {} , { {} }]} --> {} ) as Function of { [ {} , { {} }]}, { {} };

        take S = ManySortedSign (# { {} }, { [ {} , { {} }]}, f, g #);

        thus S is non void;

        thus S is finite;

        thus S is monotonic

        proof

          reconsider S9 = S as non void non empty ManySortedSign;

          let A be finitely-generated non-empty MSAlgebra over S;

          reconsider A9 = A as non-empty MSAlgebra over S9;

          set s = the SortSymbol of S9;

          consider G be GeneratorSet of A9 such that

           A1: G is finite-yielding by Def10;

          reconsider Gs = (G . s) as finite set by A1;

          set o = the OperSymbol of S9;

          set T = (s .--> ((G . s) \/ {(( Den (o,A9)) . {} )}));

          set O = (o .--> ( Den (o,A9)));

          reconsider G9 = G as MSSubset of A9;

          let i be object;

          

           A2: s = {} by TARSKI:def 1;

          then

          reconsider T as non-empty ManySortedSet of the carrier of S;

          assume i in the carrier of S;

          then

           A3: i = s by A2, TARSKI:def 1;

          reconsider T9 = T as ManySortedSet of the carrier of S9;

          

           A4: ( Args (o,A9)) = ((the Sorts of A9 # ) . (the Arity of S . o)) by FUNCT_2: 15

          .= ((the Sorts of A9 # ) . ( <*> the carrier of S9))

          .= { {} } by PRE_CIRC: 2;

          then

           A5: ( dom ( Den (o,A9))) = { {} } by FUNCT_2:def 1;

           A6:

          now

            let i be object;

            assume

             A7: i in the carrier' of S;

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

            then

             A8: i = o by TARSKI:def 1;

            (((T # ) * the Arity of S) . i) = ((T # ) . (the Arity of S . i)) by A7, FUNCT_2: 15

            .= ((T # ) . ( <*> the carrier of S))

            .= { {} } by PRE_CIRC: 2;

            then

            reconsider Oi = (O . i) as Function of (((T # ) * the Arity of S) . i), ( Result (o,A9)) by A4, A8, FUNCOP_1: 72;

            (O . i) = ( Den (o,A9)) by A8, FUNCOP_1: 72;

            then

             A9: ( rng Oi) = {(( Den (o,A9)) . {} )} by A5, FUNCT_1: 4;

            ((T * the ResultSort of S) . i) = (T . (the ResultSort of S . i)) by A7, FUNCT_2: 15

            .= (T . s) by A2

            .= ((G . s) \/ {(( Den (o,A9)) . {} )}) by FUNCOP_1: 72;

            then ( rng Oi) c= ((T * the ResultSort of S) . i) by A9, XBOOLE_1: 7;

            hence (O . i) is Function of (((T # ) * the Arity of S) . i), ((T * the ResultSort of S) . i) by FUNCT_2: 6;

          end;

          

           A10: o = [ {} , { {} }] by TARSKI:def 1;

          then

          reconsider O as ManySortedFunction of ((T # ) * the Arity of S), (T * the ResultSort of S) by A6, PBOOLE:def 15;

           A11:

          now

            let B be MSSubset of A9;

            assume

             A12: B = the Sorts of MSAlgebra (# T, O #);

            thus

             A13: B is opers_closed

            proof

              let o9 be OperSymbol of S9;

              let x be object;

              assume

               A14: x in ( rng (( Den (o9,A9)) | (((B # ) * the Arity of S9) . o9)));

              

               A15: o9 = o by A10, TARSKI:def 1;

              

               A16: ( dom the ResultSort of S9) = { [ {} , { {} }]} & (the ResultSort of S9 . o) = s by A2;

              

               A17: (( Den (o,A9)) | { {} }) = ( Den (o,A9)) by A5;

              (((B # ) * the Arity of S) . o) = ((B # ) . (the Arity of S . o)) by FUNCT_2: 15

              .= ((T # ) . ( <*> the carrier of S)) by A12

              .= { {} } by PRE_CIRC: 2;

              then ex y be object st y in ( dom ( Den (o,A9))) & x = (( Den (o,A9)) . y) by A15, A17, A14, FUNCT_1:def 3;

              then x = (( Den (o,A9)) . {} ) by A4, TARSKI:def 1;

              then

               A18: x in {(( Den (o,A9)) . {} )} by TARSKI:def 1;

              (B . s) = ((G . s) \/ {(( Den (o,A9)) . {} )}) by A12, FUNCOP_1: 72;

              then x in (B . s) by A18, XBOOLE_0:def 3;

              hence thesis by A15, A16, FUNCT_1: 13;

            end;

            now

              let o9 be OperSymbol of S9;

              (((B # ) * the Arity of S9) . o) = ((B # ) . (the Arity of S9 . o)) by FUNCT_2: 15

              .= ((T # ) . ( <*> the carrier of S9)) by A12

              .= { {} } by PRE_CIRC: 2;

              then (( Den (o,A9)) | (((B # ) * the Arity of S9) . o)) = ( Den (o,A9)) by A5;

              then

               A19: (the Charact of MSAlgebra (# T, O #) . o) = (( Den (o,A9)) | (((B # ) * the Arity of S9) . o)) by FUNCOP_1: 72;

              o9 = o & B is_closed_on o by A10, A13, TARSKI:def 1;

              hence (the Charact of MSAlgebra (# T, O #) . o9) = (o9 /. B) by A19, MSUALG_2:def 7;

            end;

            hence the Charact of MSAlgebra (# T, O #) = ( Opers (A9,B)) by A12, MSUALG_2:def 8;

          end;

          reconsider A99 = MSAlgebra (# T, O #) as non-empty MSAlgebra over S9 by MSUALG_1:def 3;

          

           A20: ( Result (o,A9)) = (the Sorts of A9 . (the ResultSort of S . o)) by FUNCT_2: 15

          .= (the Sorts of A9 . {} );

          T9 c= the Sorts of A9

          proof

            let i be object;

            assume i in the carrier of S9;

            then

             A21: i = {} by TARSKI:def 1;

            then

             A22: (T9 . i) = ((G . s) \/ {(( Den (o,A9)) . {} )}) by A2;

            G c= the Sorts of A9 by PBOOLE:def 18;

            then

             A23: (G . s) c= (the Sorts of A9 . i) by A2, A21;

            ( dom ( Den (o,A9))) = ( Args (o,A9)) by FUNCT_2:def 1;

            then {} in ( dom ( Den (o,A9))) by A4, TARSKI:def 1;

            then (( Den (o,A9)) . {} ) in ( rng ( Den (o,A9))) by FUNCT_1:def 3;

            then {(( Den (o,A9)) . {} )} c= (the Sorts of A9 . i) by A20, A21, ZFMISC_1: 31;

            hence thesis by A22, A23, XBOOLE_1: 8;

          end;

          then the Sorts of MSAlgebra (# T, O #) is MSSubset of A9 by PBOOLE:def 18;

          then

          reconsider A99 as strict MSSubAlgebra of A9 by A11, MSUALG_2:def 9;

           A24:

          now

            let U1 be MSSubAlgebra of A9;

            assume

             A25: G9 is MSSubset of U1;

            now

              ( Constants A9) is MSSubset of U1 by MSUALG_2: 10;

              then ( Constants A9) c= the Sorts of U1 by PBOOLE:def 18;

              then (( Constants A9) . s) c= (the Sorts of U1 . s);

              then

               A26: ( Constants (A9,s)) c= (the Sorts of U1 . s) by MSUALG_2:def 4;

              

               A27: {} in ( dom ( Den (o,A9))) by A5, TARSKI:def 1;

              then (( Den (o,A9)) . {} ) in ( rng ( Den (o,A9))) by FUNCT_1:def 3;

              then

              reconsider b = (( Den (o,A9)) . {} ) as Element of (the Sorts of A9 . s) by A20, TARSKI:def 1;

              let i be object;

              

               A28: (the Arity of S9 . o) = {} & ex X be non empty set st X = (the Sorts of A9 . s) & ( Constants (A9,s)) = { a where a be Element of X : ex o be OperSymbol of S9 st (the Arity of S9 . o) = {} & (the ResultSort of S9 . o) = s & a in ( rng ( Den (o,A9))) } by MSUALG_2:def 3;

              b in ( rng ( Den (o,A9))) by A27, FUNCT_1:def 3;

              then (( Den (o,A9)) . {} ) in ( Constants (A9,s)) by A2, A28;

              then

               A29: {(( Den (o,A9)) . {} )} c= (the Sorts of U1 . s) by A26, ZFMISC_1: 31;

              G c= the Sorts of U1 by A25, PBOOLE:def 18;

              then

               A30: (the Sorts of A99 . s) = ((G . s) \/ {(( Den (o,A9)) . {} )}) & (G . s) c= (the Sorts of U1 . s) by FUNCOP_1: 72;

              assume i in the carrier of S9;

              then i = s by A2, TARSKI:def 1;

              hence (the Sorts of A99 . i) c= (the Sorts of U1 . i) by A30, A29, XBOOLE_1: 8;

            end;

            then the Sorts of A99 c= the Sorts of U1;

            hence A99 is MSSubAlgebra of U1 by MSUALG_2: 8;

          end;

          now

            let i be object;

            assume i in the carrier of S9;

            then

             A31: i = s by A2, TARSKI:def 1;

            (the Sorts of A99 . s) = ((G . s) \/ {(( Den (o,A9)) . {} )}) by FUNCOP_1: 72;

            hence (G9 . i) c= (the Sorts of A99 . i) by A31, XBOOLE_1: 7;

          end;

          then G9 c= the Sorts of A99;

          then G9 is MSSubset of A99 by PBOOLE:def 18;

          

          then (s .--> ((G . s) \/ {(( Den (o,A9)) . {} )})) = the Sorts of ( GenMSAlg G) by A24, MSUALG_2:def 17

          .= the Sorts of A9 by MSAFREE:def 4;

          then (the Sorts of A . i) = (Gs \/ {(( Den (o,A9)) . {} )}) by A3, FUNCOP_1: 72;

          hence thesis;

        end;

        thus S is Circuit-like

        proof

          let S9 be non void non empty ManySortedSign;

          assume

           A32: S9 = S;

          let o1,o2 be OperSymbol of S9 such that ( the_result_sort_of o1) = ( the_result_sort_of o2);

          o1 = [ {} , { {} }] by A32, TARSKI:def 1;

          hence thesis by A32, TARSKI:def 1;

        end;

      end;

    end

    theorem :: MSAFREE2:7

    

     Th7: for S be non void non empty ManySortedSign holds for X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of ( FreeMSA X) . v) holds e is finite DecoratedTree

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of ( FreeMSA X) . v);

      ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then (the Sorts of ( FreeMSA X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

      then

       A1: e in ( TS ( DTConMSA X)) by TARSKI:def 3;

      then

      reconsider e9 = e as DecoratedTree;

      ( dom e9) is finite by A1;

      hence thesis by FINSET_1: 10;

    end;

    theorem :: MSAFREE2:8

    for S be non void non empty ManySortedSign, X be non-empty finite-yielding ManySortedSet of the carrier of S holds ( FreeMSA X) is finitely-generated

    proof

      let S be non void non empty ManySortedSign, X be non-empty finite-yielding ManySortedSet of the carrier of S;

      per cases ;

        case S is non void;

        reconsider G = ( FreeGen X) as GeneratorSet of ( FreeMSA X);

        let S9 be non void non empty ManySortedSign such that

         A1: S9 = S;

        let A be MSAlgebra over S9;

        assume A = ( FreeMSA X);

        then

        reconsider G as GeneratorSet of A by A1;

        take G;

        thus G is finite-yielding

        proof

          let i be object;

          reconsider Gi = (G . i) as set;

          assume i in the carrier of S9;

          then

          reconsider iS = i as SortSymbol of S by A1;

          reconsider Xi = (X . iS) as non empty finite set;

          now

            defpred P[ object, object] means $1 = ( root-tree [$2, i]);

            

             A2: for e be object st e in Gi holds ex u be object st u in Xi & P[e, u]

            proof

              

               A3: Gi = ( FreeGen (iS,X)) by MSAFREE:def 16;

              let e be object;

              assume e in Gi;

              then

              consider u be set such that

               A4: u in Xi & e = ( root-tree [u, i]) by A3, MSAFREE:def 15;

              take u;

              thus thesis by A4;

            end;

            consider f be Function such that

             A5: ( dom f) = Gi and

             A6: ( rng f) c= Xi and

             A7: for e be object st e in Gi holds P[e, (f . e)] from FUNCT_1:sch 6( A2);

            take f;

            f is one-to-one

            proof

              let x1,x2 be object;

              assume that

               A8: x1 in ( dom f) and

               A9: x2 in ( dom f) and

               A10: (f . x1) = (f . x2);

              

              thus x1 = ( root-tree [(f . x2), i]) by A5, A7, A8, A10

              .= x2 by A5, A7, A9;

            end;

            hence ex f be Function st f is one-to-one & ( dom f) = Gi & ( rng f) c= Xi by A5, A6;

          end;

          then ( card Gi) c= ( card Xi) or ( card Gi) in ( card Xi) by CARD_1: 10;

          hence thesis by CARD_2: 49;

        end;

      end;

        case S is void;

        hence thesis;

      end;

    end;

    theorem :: MSAFREE2:9

    for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, v be Vertex of S, e be Element of (the Sorts of ( FreeEnv A) . v) st v in ( InputVertices S) holds ex x be Element of (the Sorts of A . v) st e = ( root-tree [x, v])

    proof

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, v be Vertex of S, e be Element of (the Sorts of ( FreeEnv A) . v);

      ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

      then e in (( FreeSort the Sorts of A) . v);

      then e in ( FreeSort (the Sorts of A,v)) by MSAFREE:def 11;

      then e in { a where a be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v } by MSAFREE:def 10;

      then

      consider a be Element of ( TS ( DTConMSA the Sorts of A)) such that

       A1: a = e and

       A2: (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v;

      assume v in ( InputVertices S);

      then

      consider x be set such that

       A3: x in (the Sorts of A . v) and

       A4: a = ( root-tree [x, v]) by A2, Th2;

      reconsider x as Element of (the Sorts of A . v) by A3;

      take x;

      thus thesis by A1, A4;

    end;

    theorem :: MSAFREE2:10

    

     Th10: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be DTree-yielding FinSequence st ( [o, the carrier of S] -tree p) in (the Sorts of ( FreeMSA X) . ( the_result_sort_of o)) holds ( len p) = ( len ( the_arity_of o))

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be DTree-yielding FinSequence;

      set s = ( the_result_sort_of o);

      assume

       A1: ( [o, the carrier of S] -tree p) in (the Sorts of ( FreeMSA X) . ( the_result_sort_of o));

      ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then ( [o, the carrier of S] -tree p) in ( FreeSort (X,s)) by A1, MSAFREE:def 11;

      then

       A2: ( [o, the carrier of S] -tree p) in { a where a be Element of ( TS ( DTConMSA X)) : (ex x be set st x in (X . s) & a = ( root-tree [x, s])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = s } by MSAFREE:def 10;

      the carrier of S in {the carrier of S} by TARSKI:def 1;

      then [o, the carrier of S] in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 87;

      then

      reconsider nt = [o, the carrier of S] as NonTerminal of ( DTConMSA X) by MSAFREE: 6;

      reconsider O = ( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))) as non empty set;

      reconsider R = ( REL X) as Relation of O, (O * );

      

       A3: ( DTConMSA X) = DTConstrStr (# O, R #) by MSAFREE:def 8;

      then

      reconsider TSDT = ( TS ( DTConMSA X)) as Subset of ( FinTrees O);

      reconsider c = nt as Element of O by A3;

      for x be object st x in TSDT holds x is DecoratedTree of O;

      then

      reconsider TSDT as DTree-set of O by TREES_3:def 6;

      consider a be Element of ( TS ( DTConMSA X)) such that

       A4: a = ( [o, the carrier of S] -tree p) and (ex x be set st x in (X . s) & a = ( root-tree [x, s])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = s by A2;

      (a . {} ) = [o, the carrier of S] by A4, TREES_4:def 4;

      then

      consider ts be FinSequence of ( TS ( DTConMSA X)) such that

       A5: a = (nt -tree ts) and

       A6: nt ==> ( roots ts) by DTCONSTR: 10;

      reconsider ts9 = ts as FinSequence of TSDT;

      reconsider b = ( roots ts9) as FinSequence of O;

      reconsider b as Element of (O * ) by FINSEQ_1:def 11;

       [c, b] in R by A6, A3, LANG1:def 1;

      then

       A7: ( len ( roots ts)) = ( len ( the_arity_of o)) by MSAFREE:def 7;

      reconsider ts as DTree-yielding FinSequence;

      

       A8: ( dom ( roots ts)) = ( dom ts) by TREES_3:def 18;

      ts = p by A4, A5, TREES_4: 15;

      hence thesis by A7, A8, FINSEQ_3: 29;

    end;

    theorem :: MSAFREE2:11

    

     Th11: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be DTree-yielding FinSequence st ( [o, the carrier of S] -tree p) in (the Sorts of ( FreeMSA X) . ( the_result_sort_of o)) holds for i be Nat st i in ( dom ( the_arity_of o)) holds (p . i) in (the Sorts of ( FreeMSA X) . (( the_arity_of o) . i))

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be DTree-yielding FinSequence;

      

       A1: ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      assume

       A2: ( [o, the carrier of S] -tree p) in (the Sorts of ( FreeMSA X) . ( the_result_sort_of o));

      now

        the carrier of S in {the carrier of S} by TARSKI:def 1;

        then [o, the carrier of S] in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 87;

        then

        reconsider nt = [o, the carrier of S] as NonTerminal of ( DTConMSA X) by MSAFREE: 6;

        set rso = ( the_result_sort_of o);

        reconsider ao = ( the_arity_of o) as Element of (the carrier of S * );

        let i be Nat;

        assume

         A3: i in ( dom ( the_arity_of o));

        then (ao . i) in ( rng ao) by FUNCT_1:def 3;

        then

        reconsider s = (ao . i) as SortSymbol of S;

        

         A4: (the Sorts of ( FreeMSA X) . s) = ( FreeSort (X,s)) by A1, MSAFREE:def 11

        .= ( FreeSort (X,(( the_arity_of o) /. i))) by A3, PARTFUN1:def 6;

        ( [o, the carrier of S] -tree p) in ( FreeSort (X,rso)) by A2, A1, MSAFREE:def 11;

        then ( [o, the carrier of S] -tree p) in { a where a be Element of ( TS ( DTConMSA X)) : (ex x be set st x in (X . rso) & a = ( root-tree [x, rso])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = rso } by MSAFREE:def 10;

        then

        consider a be Element of ( TS ( DTConMSA X)) such that

         A5: a = ( [o, the carrier of S] -tree p) and (ex x be set st x in (X . rso) & a = ( root-tree [x, rso])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = rso;

        (a . {} ) = [o, the carrier of S] by A5, TREES_4:def 4;

        then

        consider ts be FinSequence of ( TS ( DTConMSA X)) such that

         A6: a = (nt -tree ts) and

         A7: nt ==> ( roots ts) by DTCONSTR: 10;

        nt = ( Sym (o,X)) by MSAFREE:def 9;

        then

         A8: ts in (((( FreeSort X) # ) * the Arity of S) . o) by A7, MSAFREE: 10;

        ( dom p) = ( Seg ( len p)) & ( dom ( the_arity_of o)) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        then

         A9: i in ( dom p) by A2, A3, Th10;

        reconsider ts as DTree-yielding FinSequence;

        ts = p by A5, A6, TREES_4: 15;

        hence (p . i) in (the Sorts of ( FreeMSA X) . (( the_arity_of o) . i)) by A9, A8, A4, MSAFREE: 9;

      end;

      hence thesis;

    end;

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S;

      cluster -> finite non empty Function-like Relation-like for Element of (the Sorts of ( FreeMSA X) . v);

      coherence

      proof

        let e be Element of (the Sorts of ( FreeMSA X) . v);

        reconsider e9 = e as DecoratedTree by Th7;

        thus e is finite by Th7;

        ( dom e9) is Tree;

        hence e is non empty;

        thus thesis by Th7;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S;

      cluster Function-like Relation-like for Element of (the Sorts of ( FreeMSA X) . v);

      existence

      proof

        set e = the Element of (the Sorts of ( FreeMSA X) . v);

        take e;

        thus thesis;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S;

      cluster -> DecoratedTree-like for Function-like Relation-like Element of (the Sorts of ( FreeMSA X) . v);

      coherence by Th7;

    end

    registration

      let IIG be non void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of IIG, v be Vertex of IIG;

      cluster finite for Element of (the Sorts of ( FreeMSA X) . v);

      existence

      proof

        set e = the Element of (the Sorts of ( FreeMSA X) . v);

        take e;

        thus thesis;

      end;

    end

    theorem :: MSAFREE2:12

    for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S, o be OperSymbol of S, e be Element of (the Sorts of ( FreeMSA X) . v) st (e . {} ) = [o, the carrier of S] holds ex p be DTree-yielding FinSequence st ( len p) = ( len ( the_arity_of o)) & for i be Nat st i in ( dom p) holds (p . i) in (the Sorts of ( FreeMSA X) . (( the_arity_of o) . i))

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S, o be OperSymbol of S, e be Element of (the Sorts of ( FreeMSA X) . v) such that

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

      the carrier of S in {the carrier of S} by TARSKI:def 1;

      then [o, the carrier of S] in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 87;

      then

      reconsider nt = [o, the carrier of S] as NonTerminal of ( DTConMSA X) by MSAFREE: 6;

      ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then (the Sorts of ( FreeMSA X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

      then e in ( FreeSort (X,v));

      then e in { a where a be Element of ( TS ( DTConMSA X)) : (ex x be set st x in (X . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v } by MSAFREE:def 10;

      then

      consider a be Element of ( TS ( DTConMSA X)) such that

       A2: a = e and

       A3: (ex x be set st x in (X . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v;

      consider x be set such that

       A4: x in (X . v) & a = ( root-tree [x, v]) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v by A3;

      consider p be FinSequence of ( TS ( DTConMSA X)) such that

       A5: a = (nt -tree p) and nt ==> ( roots p) by A1, A2, DTCONSTR: 10;

      now

        assume a = ( root-tree [x, v]);

        then

         A6: (a . {} ) = [x, v] by TREES_4: 3;

        

         A7: for X be set holds not X in X;

        (a . {} ) = [o, the carrier of S] by A5, TREES_4:def 4;

        then the carrier of S = v by A6, XTUPLE_0: 1;

        hence contradiction by A7;

      end;

      then

      consider o9 be OperSymbol of S such that

       A8: [o9, the carrier of S] = (a . {} ) and

       A9: ( the_result_sort_of o9) = v by A4;

      

       A10: o = o9 by A1, A2, A8, XTUPLE_0: 1;

      then

       A11: ( len p) = ( len ( the_arity_of o)) by A2, A5, A9, Th10;

      

      then ( dom p) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3

      .= ( dom ( the_arity_of o)) by FINSEQ_1:def 3;

      then for i be Nat st i in ( dom p) holds (p . i) in (the Sorts of ( FreeMSA X) . (( the_arity_of o) . i)) by A2, A5, A9, A10, Th11;

      hence thesis by A11;

    end;

    definition

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of ( FreeMSA X) . v);

      :: MSAFREE2:def14

      func depth e -> Nat means ex dt be finite DecoratedTree, t be finite Tree st dt = e & t = ( dom dt) & it = ( height t);

      existence

      proof

        reconsider dt = e as finite DecoratedTree;

        reconsider domdt = ( dom dt) as finite Tree;

        take ( height domdt), dt, domdt;

        thus thesis;

      end;

      uniqueness ;

    end