msafree3.miz



    begin

    reserve x,y,z for set;

    registration

      let S be non empty non void ManySortedSign;

      let A be non empty MSAlgebra over S;

      cluster ( Union the Sorts of A) -> non empty;

      coherence

      proof

        

         A1: ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

        consider i be object such that

         A2: i in the carrier of S and

         A3: (the Sorts of A . i) is non empty by PBOOLE:def 12;

        set x = the Element of (the Sorts of A . i);

        x in (the Sorts of A . i) by A3;

        hence thesis by A2, A1, CARD_5: 2;

      end;

    end

    definition

      let S be non empty non void ManySortedSign;

      let A be non empty MSAlgebra over S;

      mode Element of A is Element of ( Union the Sorts of A);

    end

    theorem :: MSAFREE3:1

    for I be set, A be ManySortedSet of I holds for F be ManySortedFunction of I st F is "1-1" & A c= ( doms F) holds (F "" (F .:.: A)) = A

    proof

      let I be set, A be ManySortedSet of I;

      let F be ManySortedFunction of I such that

       A1: F is "1-1" and

       A2: A c= ( doms F);

      

       A3: ( dom F) = I by PARTFUN1:def 2;

      now

        let i be object;

        assume

         A4: i in I;

        then

         A5: (F . i) is one-to-one by A1, A3, MSUALG_3:def 2;

        (A . i) c= (( doms F) . i) by A2, A4;

        then

         A6: (A . i) c= ( dom (F . i)) by A3, A4, FUNCT_6: 22;

        

        thus ((F "" (F .:.: A)) . i) = ((F . i) " ((F .:.: A) . i)) by A4, EQUATION:def 1

        .= ((F . i) " ((F . i) .: (A . i))) by A4, PBOOLE:def 20

        .= (A . i) by A6, A5, FUNCT_1: 94;

      end;

      hence thesis;

    end;

    definition

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

      :: MSAFREE3:def1

      func Free (S,X) -> strict MSAlgebra over S means

      : Def1: ex A be MSSubset of ( FreeMSA (X (\/) (the carrier of S --> { 0 }))) st it = ( GenMSAlg A) & A = (( Reverse (X (\/) (the carrier of S --> { 0 }))) "" X);

      uniqueness ;

      existence

      proof

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

        set R = ( Reverse Y);

        (R "" X) is ManySortedSubset of ( FreeGen Y) by EQUATION: 8;

        then

         A1: (R "" X) c= ( FreeGen Y) by PBOOLE:def 18;

        ( FreeGen Y) c= the Sorts of ( FreeMSA Y) by PBOOLE:def 18;

        then (R "" X) c= the Sorts of ( FreeMSA Y) by A1, PBOOLE: 13;

        then

        reconsider Z = (R "" X) as MSSubset of ( FreeMSA Y) by PBOOLE:def 18;

        take ( GenMSAlg Z), Z;

        thus thesis;

      end;

    end

    theorem :: MSAFREE3:2

    

     Th2: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds for s be SortSymbol of S holds [x, s] in the carrier of ( DTConMSA X) iff x in (X . s)

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

      let s be SortSymbol of S;

      

       A1: ( DTConMSA X) = DTConstrStr (# ( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))), ( REL X) #) by MSAFREE:def 8;

      

       A2: ( dom ( coprod X)) = the carrier of S by PARTFUN1:def 2;

      s in the carrier of S;

      then s <> the carrier of S;

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

      then

       A3: not [x, s] in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 87;

      hereby

        assume [x, s] in the carrier of ( DTConMSA X);

        then [x, s] in ( Union ( coprod X)) by A1, A3, XBOOLE_0:def 3;

        then

        consider y be object such that

         A4: y in ( dom ( coprod X)) and

         A5: [x, s] in (( coprod X) . y) by CARD_5: 2;

        (( coprod X) . y) = ( coprod (y,X)) by A4, MSAFREE:def 3;

        then

        consider z such that

         A6: z in (X . y) and

         A7: [x, s] = [z, y] by A4, A5, MSAFREE:def 2;

        x = z by A7, XTUPLE_0: 1;

        hence x in (X . s) by A6, A7, XTUPLE_0: 1;

      end;

      assume x in (X . s);

      then [x, s] in ( coprod (s,X)) by MSAFREE:def 2;

      then [x, s] in (( coprod X) . s) by MSAFREE:def 3;

      then [x, s] in ( Union ( coprod X)) by A2, CARD_5: 2;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: MSAFREE3:3

    

     Th3: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds for s be SortSymbol of S holds x in (X . s) & x in (Y . s) iff ( root-tree [x, s]) in ((( Reverse Y) "" X) . s)

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let s be SortSymbol of S;

      

       A1: (( Reverse Y) . s) = ( Reverse (s,Y)) by MSAFREE:def 18;

      

       A2: ( dom ( Reverse (s,Y))) = ( FreeGen (s,Y)) by FUNCT_2:def 1;

      hereby

        assume that

         A3: x in (X . s) and

         A4: x in (Y . s);

        

         A5: ( root-tree [x, s]) in ( FreeGen (s,Y)) by A4, MSAFREE:def 15;

         [x, s] in the carrier of ( DTConMSA Y) by A4, Th2;

        

        then ((( Reverse Y) . s) . ( root-tree [x, s])) = ( [x, s] `1 ) by A1, A5, MSAFREE:def 17

        .= x;

        then ( root-tree [x, s]) in ((( Reverse Y) . s) " (X . s)) by A1, A2, A3, A5, FUNCT_1:def 7;

        hence ( root-tree [x, s]) in ((( Reverse Y) "" X) . s) by EQUATION:def 1;

      end;

      assume ( root-tree [x, s]) in ((( Reverse Y) "" X) . s);

      then

       A6: ( root-tree [x, s]) in ((( Reverse Y) . s) " (X . s)) by EQUATION:def 1;

      then

       A7: (( Reverse (s,Y)) . ( root-tree [x, s])) in (X . s) by A1, FUNCT_1:def 7;

      

       A8: ( root-tree [x, s]) in ( FreeGen (s,Y)) by A1, A2, A6, FUNCT_1:def 7;

      then

      consider z such that

       A9: z in (Y . s) and

       A10: ( root-tree [x, s]) = ( root-tree [z, s]) by MSAFREE:def 15;

      

       B: ( [z, s] `1 ) = z;

      

       A11: [x, s] = [z, s] by A10, TREES_4: 4;

      then [x, s] in the carrier of ( DTConMSA Y) by A9, Th2;

      then ( [x, s] `1 ) in (X . s) by A8, A7, MSAFREE:def 17;

      hence x in (X . s) & x in (Y . s) by A9, A11, B;

    end;

    theorem :: MSAFREE3:4

    

     Th4: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds for s be SortSymbol of S st x in (X . s) holds ( root-tree [x, s]) in (the Sorts of ( Free (S,X)) . s)

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

      let s be SortSymbol of S such that

       A1: x in (X . s);

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

      consider A be MSSubset of ( FreeMSA Y) such that

       A2: ( Free (S,X)) = ( GenMSAlg A) and

       A3: A = (( Reverse Y) "" X) by Def1;

      A is MSSubset of ( Free (S,X)) by A2, MSUALG_2:def 17;

      then A c= the Sorts of ( Free (S,X)) by PBOOLE:def 18;

      then

       A4: (A . s) c= (the Sorts of ( Free (S,X)) . s);

      X c= Y by PBOOLE: 14;

      then (X . s) c= (Y . s);

      then ( root-tree [x, s]) in (A . s) by A1, A3, Th3;

      hence thesis by A4;

    end;

    theorem :: MSAFREE3:5

    

     Th5: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds for o be OperSymbol of S st ( the_arity_of o) = {} holds ( root-tree [o, the carrier of S]) in (the Sorts of ( Free (S,X)) . ( the_result_sort_of o))

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

      let o be OperSymbol of S such that

       A1: ( the_arity_of o) = {} ;

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

      

       A2: ( Args (o,( FreeMSA Y))) = (((the Sorts of ( FreeMSA Y) # ) * the Arity of S) . o) by MSUALG_1:def 4

      .= ((the Sorts of ( FreeMSA Y) # ) . (the Arity of S . o)) by FUNCT_2: 15

      .= ((the Sorts of ( FreeMSA Y) # ) . ( <*> the carrier of S)) by A1, MSUALG_1:def 1

      .= { {} } by PRE_CIRC: 2;

      then

       A3: ( dom ( Den (o,( FreeMSA Y)))) c= { {} };

      

       A4: ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1;

      then

      reconsider FX = the Sorts of ( Free (S,X)) as MSSubset of ( FreeMSA Y) by MSUALG_2:def 9;

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

      .= ((FX # ) . ( <*> the carrier of S)) by A1, MSUALG_1:def 1

      .= { {} } by PRE_CIRC: 2;

      then

       A5: (( Den (o,( FreeMSA Y))) | (((FX # ) * the Arity of S) . o)) = ( Den (o,( FreeMSA Y))) by A3, RELAT_1: 68;

      set a = the ArgumentSeq of ( Sym (o,Y));

      reconsider a as Element of ( Args (o,( FreeMSA Y))) by INSTALG1: 1;

      a = {} by A2, TARSKI:def 1;

      then ( root-tree [o, the carrier of S]) = ( [o, the carrier of S] -tree a) by TREES_4: 20;

      then (( Den (o,( FreeMSA Y))) . a) = ( root-tree [o, the carrier of S]) by INSTALG1: 3;

      then

       A6: ( root-tree [o, the carrier of S]) in ( rng ( Den (o,( FreeMSA Y)))) by FUNCT_2: 4;

      FX is opers_closed by A4, MSUALG_2:def 9;

      then FX is_closed_on o;

      then

       A7: ( rng (( Den (o,( FreeMSA Y))) | (((FX # ) * the Arity of S) . o))) c= ((FX * the ResultSort of S) . o);

      ((FX * the ResultSort of S) . o) = (FX . (the ResultSort of S . o)) by FUNCT_2: 15

      .= (FX . ( the_result_sort_of o)) by MSUALG_1:def 2;

      hence thesis by A7, A5, A6;

    end;

    registration

      let S be non void Signature;

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

      cluster ( Free (S,X)) -> non empty;

      coherence

      proof

        consider s be object such that

         A1: s in the carrier of S and

         A2: (X . s) is non empty by PBOOLE:def 12;

        reconsider s as SortSymbol of S by A1;

        set x = the Element of (X . s);

        ( root-tree [x, s]) in (the Sorts of ( Free (S,X)) . s) by A2, Th4;

        hence not the Sorts of ( Free (S,X)) is empty-yielding;

      end;

    end

    theorem :: MSAFREE3:6

    for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds x is Element of ( FreeMSA X) iff x is Term of S, X

    proof

      let S be non void Signature;

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

      

       A1: (S -Terms X) = ( TS ( DTConMSA X)) by MSATERM:def 1

      .= ( union ( rng ( FreeSort X))) by MSAFREE: 11

      .= ( Union ( FreeSort X)) by CARD_3:def 4;

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

      hence thesis by A1;

    end;

    theorem :: MSAFREE3:7

    

     Th7: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for s be SortSymbol of S holds for x be Term of S, X holds x in (the Sorts of ( FreeMSA X) . s) iff ( the_sort_of x) = s

    proof

      let S be non void Signature;

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

      let s be SortSymbol of S;

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

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

      hence thesis by MSATERM:def 5;

    end;

    theorem :: MSAFREE3:8

    

     Th8: for S be non void Signature holds for X be non empty-yielding ManySortedSet of the carrier of S holds for x be Element of ( Free (S,X)) holds x is Term of S, (X (\/) (the carrier of S --> { 0 }))

    proof

      let S be non void Signature;

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

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

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

      

       A1: (S -Terms Y) = ( TS ( DTConMSA Y)) by MSATERM:def 1

      .= ( union ( rng ( FreeSort Y))) by MSAFREE: 11

      .= ( Union ( FreeSort Y)) by CARD_3:def 4;

      

       A2: ( FreeMSA Y) = MSAlgebra (# ( FreeSort Y), ( FreeOper Y) #) & ( dom the Sorts of ( FreeMSA Y)) = the carrier of S by MSAFREE:def 14, PARTFUN1:def 2;

      consider y be object such that

       A3: y in ( dom the Sorts of ( Free (S,X))) and

       A4: x in (the Sorts of ( Free (S,X)) . y) by CARD_5: 2;

      ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1;

      then the Sorts of ( Free (S,X)) is MSSubset of ( FreeMSA Y) by MSUALG_2:def 9;

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

      then (the Sorts of ( Free (S,X)) . y) c= (the Sorts of ( FreeMSA Y) . y) by A3;

      hence thesis by A1, A3, A4, A2, CARD_5: 2;

    end;

    registration

      let S be non empty non void ManySortedSign;

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

      cluster -> Relation-like Function-like for Element of ( Free (S,X));

      coherence by Th8;

    end

    registration

      let S be non empty non void ManySortedSign;

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

      cluster -> finite DecoratedTree-like for Element of ( Free (S,X));

      coherence by Th8;

    end

    registration

      let S be non empty non void ManySortedSign;

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

      cluster -> finite-branching for Element of ( Free (S,X));

      coherence ;

    end

    registration

      cluster -> non empty for DecoratedTree;

      coherence by RELAT_1: 38;

    end

    definition

      let S be ManySortedSign;

      let t be non empty Relation;

      :: MSAFREE3:def2

      func S variables_in t -> ManySortedSet of the carrier of S means

      : Def2: for s be object st s in the carrier of S holds (it . s) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s };

      existence

      proof

        deffunc F( object) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = $1 };

        ex f be ManySortedSet of the carrier of S st for i be object st i in the carrier of S holds (f . i) = F(i) from PBOOLE:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let V1,V2 be ManySortedSet of the carrier of S such that

         A1: for s be object st s in the carrier of S holds (V1 . s) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } and

         A2: for s be object st s in the carrier of S holds (V2 . s) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s };

        now

          let s be object;

          assume

           A3: s in the carrier of S;

          

          hence (V1 . s) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } by A1

          .= (V2 . s) by A2, A3;

        end;

        hence thesis;

      end;

    end

    definition

      let S be ManySortedSign;

      let X be ManySortedSet of the carrier of S;

      let t be non empty Relation;

      :: MSAFREE3:def3

      func X variables_in t -> ManySortedSubset of X equals (X (/\) (S variables_in t));

      coherence

      proof

        thus (X (/\) (S variables_in t)) c= X by PBOOLE: 15;

      end;

    end

    theorem :: MSAFREE3:9

    

     Th9: for S be ManySortedSign, X be ManySortedSet of the carrier of S holds for t be non empty Relation, V be ManySortedSubset of X holds V = (X variables_in t) iff for s be set st s in the carrier of S holds (V . s) = ((X . s) /\ { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s })

    proof

      let S be ManySortedSign, X be ManySortedSet of the carrier of S;

      let t be non empty Relation, V be ManySortedSubset of X;

      hereby

        assume

         A1: V = (X variables_in t);

        let s be set;

        assume

         A2: s in the carrier of S;

        then (V . s) = ((X . s) /\ ((S variables_in t) . s)) by A1, PBOOLE:def 5;

        hence (V . s) = ((X . s) /\ { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s }) by A2, Def2;

      end;

      assume

       A3: for s be set st s in the carrier of S holds (V . s) = ((X . s) /\ { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s });

      now

        let s be object;

        assume

         A4: s in the carrier of S;

        

        hence (V . s) = ((X . s) /\ { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s }) by A3

        .= ((X . s) /\ ((S variables_in t) . s)) by A4, Def2;

      end;

      hence thesis by PBOOLE:def 5;

    end;

    theorem :: MSAFREE3:10

    

     Th10: for S be ManySortedSign, s,x be object holds (s in the carrier of S implies ((S variables_in ( root-tree [x, s])) . s) = {x}) & for s9 be object st s9 <> s or not s in the carrier of S holds ((S variables_in ( root-tree [x, s])) . s9) = {}

    proof

      let S be ManySortedSign, s,x be object;

      reconsider t = ( root-tree [x, s]) as DecoratedTree;

      

       A1: ( [x, s] `2 ) = s;

      t = { [ {} , [x, s]]} by TREES_4: 6;

      then

       A2: ( rng t) = { [x, s]} by RELAT_1: 9;

      

       A3: ( [x, s] `1 ) = x;

      hereby

        assume s in the carrier of S;

        then

         A4: ((S variables_in t) . s) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } by Def2;

        thus ((S variables_in ( root-tree [x, s])) . s) = {x}

        proof

          hereby

            let y be object;

            assume y in ((S variables_in ( root-tree [x, s])) . s);

            then

            consider a be Element of ( rng t) such that

             A5: y = (a `1 ) and (a `2 ) = s by A4;

            a = [x, s] by A2, TARSKI:def 1;

            hence y in {x} by A5, TARSKI:def 1;

          end;

           [x, s] in ( rng t) by A2, TARSKI:def 1;

          then x in { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } by A3, A1;

          hence thesis by A4, ZFMISC_1: 31;

        end;

      end;

      let s9 be object such that

       A6: s9 <> s or not s in the carrier of S;

      set y = the Element of ((S variables_in ( root-tree [x, s])) . s9);

      assume

       A7: ((S variables_in ( root-tree [x, s])) . s9) <> {} ;

      then

       A8: y in ((S variables_in t) . s9);

      ( dom (S variables_in t)) = the carrier of S by PARTFUN1:def 2;

      then

       A9: s9 in the carrier of S by A7, FUNCT_1:def 2;

      then ((S variables_in t) . s9) = { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s9 } by Def2;

      then ex a be Element of ( rng t) st y = (a `1 ) & (a `2 ) = s9 by A8;

      hence thesis by A2, A1, A6, A9, TARSKI:def 1;

    end;

    theorem :: MSAFREE3:11

    

     Th11: for S be ManySortedSign, s be set st s in the carrier of S holds for p be DTree-yielding FinSequence holds x in ((S variables_in ( [z, the carrier of S] -tree p)) . s) iff ex t be DecoratedTree st t in ( rng p) & x in ((S variables_in t) . s)

    proof

      let S be ManySortedSign, s be set such that

       A1: s in the carrier of S;

      let p be DTree-yielding FinSequence;

      reconsider q = ( [z, the carrier of S] -tree p) as DecoratedTree;

      

       A2: ((S variables_in q) . s) = { (a `1 ) where a be Element of ( rng q) : (a `2 ) = s } by A1, Def2;

      

       A3: ( dom q) = ( tree ( doms p)) by TREES_4: 10;

      

       A4: ( dom ( doms p)) = ( dom p) by TREES_3: 37;

      then

       A5: ( len p) = ( len ( doms p)) by FINSEQ_3: 29;

      hereby

        assume x in ((S variables_in ( [z, the carrier of S] -tree p)) . s);

        then

        consider a be Element of ( rng q) such that

         A6: x = (a `1 ) and

         A7: (a `2 ) = s by A2;

        consider y be object such that

         A8: y in ( dom q) and

         A9: a = (q . y) by FUNCT_1:def 3;

        reconsider y as Element of ( dom q) by A8;

        (q . {} ) = [z, the carrier of S] & s <> the carrier of S by A1, TREES_4:def 4;

        then y <> {} by A7, A9;

        then

        consider n be Nat, r be FinSequence such that

         A10: n < ( len ( doms p)) and

         A11: r in (( doms p) . (n + 1)) and

         A12: y = ( <*n*> ^ r) by A3, TREES_3:def 15;

        1 <= (n + 1) & (n + 1) <= ( len ( doms p)) by A10, NAT_1: 11, NAT_1: 13;

        then

         A13: (n + 1) in ( dom ( doms p)) by FINSEQ_3: 25;

        then

        reconsider t = (p . (n + 1)) as DecoratedTree by A4, TREES_3: 24;

        reconsider r as FinSequence of NAT by A12, FINSEQ_1: 36;

        take t;

        thus t in ( rng p) by A4, A13, FUNCT_1:def 3;

        

         A14: (( doms p) . (n + 1)) = ( dom t) by A4, A13, FUNCT_6: 22;

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

        

         A15: t = (q | <*n*>) by A5, A10, TREES_4:def 4;

        then ( dom t) = (( dom q) | <*n*>) by TREES_2:def 10;

        then a = (t . r) by A9, A11, A12, A15, A14, TREES_2:def 10;

        then a in ( rng t) by A11, A14, FUNCT_1:def 3;

        then x in { (b `1 ) where b be Element of ( rng t) : (b `2 ) = s } by A6, A7;

        hence x in ((S variables_in t) . s) by A1, Def2;

      end;

      given t be DecoratedTree such that

       A16: t in ( rng p) and

       A17: x in ((S variables_in t) . s);

      consider y be object such that

       A18: y in ( dom p) and

       A19: t = (p . y) by A16, FUNCT_1:def 3;

      reconsider y as Element of NAT by A18;

      y >= 1 by A18, FINSEQ_3: 25;

      then

      consider n be Nat such that

       A20: y = (1 + n) by NAT_1: 10;

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

      y <= ( len p) by A18, FINSEQ_3: 25;

      then

       A21: n < ( len p) by A20, NAT_1: 13;

      then

       A22: t = (q | <*n*>) by A19, A20, TREES_4:def 4;

      

       A23: {} in ( dom t) & ( <*n*> ^ {} ) = <*n*> by FINSEQ_1: 34, TREES_1: 22;

      ( dom t) = (( doms p) . (n + 1)) by A18, A19, A20, FUNCT_6: 22;

      then <*n*> in ( dom q) by A3, A5, A21, A23, TREES_3:def 15;

      then

       A24: ( rng t) c= ( rng q) by A22, TREES_2: 32;

      x in { (b `1 ) where b be Element of ( rng t) : (b `2 ) = s } by A1, A17, Def2;

      then

      consider b be Element of ( rng t) such that

       A25: x = (b `1 ) & (b `2 ) = s;

      b in ( rng t);

      hence thesis by A2, A25, A24;

    end;

    theorem :: MSAFREE3:12

    

     Th12: for S be ManySortedSign holds for X be ManySortedSet of the carrier of S holds for s,x be set holds (x in (X . s) implies ((X variables_in ( root-tree [x, s])) . s) = {x}) & for s9 be set st s9 <> s or not x in (X . s) holds ((X variables_in ( root-tree [x, s])) . s9) = {}

    proof

      let S be ManySortedSign, X be ManySortedSet of the carrier of S;

      let s,x be set;

      reconsider t = ( root-tree [x, s]) as DecoratedTree;

      hereby

        assume

         A1: x in (X . s);

        then

         A2: {x} c= (X . s) by ZFMISC_1: 31;

        ( dom X) = the carrier of S by PARTFUN1:def 2;

        then

         A3: s in the carrier of S by A1, FUNCT_1:def 2;

        then ((S variables_in ( root-tree [x, s])) . s) = {x} by Th10;

        then ((X . s) /\ ((S variables_in ( root-tree [x, s])) . s)) = {x} by A2, XBOOLE_1: 28;

        hence ((X variables_in ( root-tree [x, s])) . s) = {x} by A3, PBOOLE:def 5;

      end;

      let s9 be set such that

       A4: s9 <> s or not x in (X . s);

      set y = the Element of ((X variables_in ( root-tree [x, s])) . s9);

      assume

       A5: ((X variables_in ( root-tree [x, s])) . s9) <> {} ;

      ( dom (X variables_in t)) = the carrier of S by PARTFUN1:def 2;

      then s9 in the carrier of S by A5, FUNCT_1:def 2;

      then

       A6: ((X variables_in t) . s9) = ((X . s9) /\ { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s9 }) by Th9;

      then y in { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s9 } by A5, XBOOLE_0:def 4;

      then

      consider a be Element of ( rng t) such that

       A7: y = (a `1 ) & (a `2 ) = s9;

      t = { [ {} , [x, s]]} by TREES_4: 6;

      then ( rng t) = { [x, s]} by RELAT_1: 9;

      then a = [x, s] by TARSKI:def 1;

      hence thesis by A4, A5, A6, A7, XBOOLE_0:def 4;

    end;

    theorem :: MSAFREE3:13

    

     Th13: for S be ManySortedSign holds for X be ManySortedSet of the carrier of S holds for s be set st s in the carrier of S holds for p be DTree-yielding FinSequence holds x in ((X variables_in ( [z, the carrier of S] -tree p)) . s) iff ex t be DecoratedTree st t in ( rng p) & x in ((X variables_in t) . s)

    proof

      let S be ManySortedSign, X be ManySortedSet of the carrier of S;

      let s be set such that

       A1: s in the carrier of S;

      let p be DTree-yielding FinSequence;

      reconsider q = ( [z, the carrier of S] -tree p) as DecoratedTree;

      ((X variables_in q) . s) = ((X . s) /\ ((S variables_in q) . s)) by A1, PBOOLE:def 5;

      then

       A2: x in ((X variables_in ( [z, the carrier of S] -tree p)) . s) iff x in (X . s) & x in ((S variables_in ( [z, the carrier of S] -tree p)) . s) by XBOOLE_0:def 4;

      then

       A3: x in ((X variables_in ( [z, the carrier of S] -tree p)) . s) iff x in (X . s) & ex t be DecoratedTree st t in ( rng p) & x in ((S variables_in t) . s) by A1, Th11;

      hereby

        assume x in ((X variables_in ( [z, the carrier of S] -tree p)) . s);

        then

        consider t be DecoratedTree such that

         A4: t in ( rng p) and

         A5: x in (X . s) & x in ((S variables_in t) . s) by A3;

        take t;

        thus t in ( rng p) by A4;

        x in ((X . s) /\ ((S variables_in t) . s)) by A5, XBOOLE_0:def 4;

        hence x in ((X variables_in t) . s) by A1, PBOOLE:def 5;

      end;

      given t be DecoratedTree such that

       A6: t in ( rng p) and

       A7: x in ((X variables_in t) . s);

      

       A8: ((X variables_in t) . s) = ((X . s) /\ ((S variables_in t) . s)) by A1, PBOOLE:def 5;

      then x in ((S variables_in t) . s) by A7, XBOOLE_0:def 4;

      hence thesis by A1, A2, A6, A7, A8, Th11, XBOOLE_0:def 4;

    end;

    theorem :: MSAFREE3:14

    

     Th14: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for t be Term of S, X holds (S variables_in t) c= X

    proof

      let S be non void Signature;

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

      defpred P[ DecoratedTree] means (S variables_in $1) c= X;

      

       A1: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) st for t be Term of S, X st t in ( rng p) holds P[t] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) such that

         A2: for t be Term of S, X st t in ( rng p) holds (S variables_in t) c= X;

        set q = ( [o, the carrier of S] -tree p);

        thus (S variables_in q) c= X

        proof

          let s9 be object;

          assume s9 in the carrier of S;

          then

          reconsider z = s9 as SortSymbol of S;

          let x be object;

          assume x in ((S variables_in q) . s9);

          then

          consider t be DecoratedTree such that

           A3: t in ( rng p) and

           A4: x in ((S variables_in t) . z) by Th11;

          consider i be object such that

           A5: i in ( dom p) and

           A6: t = (p . i) by A3, FUNCT_1:def 3;

          reconsider i as Nat by A5;

          reconsider t = (p . i) as Term of S, X by A5, MSATERM: 22;

          (S variables_in t) c= X by A2, A3, A6;

          then ((S variables_in t) . z) c= (X . z);

          hence thesis by A4, A6;

        end;

      end;

      

       A7: for s be SortSymbol of S, v be Element of (X . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S, v be Element of (X . s);

        thus (S variables_in ( root-tree [v, s])) c= X

        proof

          let s9 be object;

          assume s9 in the carrier of S;

          then

          reconsider z = s9 as SortSymbol of S;

          let x be object;

          assume

           A8: x in ((S variables_in ( root-tree [v, s])) . s9);

          then

           A9: s <> z implies x in {} by Th10;

          s = z implies x in {v} by A8, Th10;

          hence thesis by A9;

        end;

      end;

      for t be Term of S, X holds P[t] from MSATERM:sch 1( A7, A1);

      hence thesis;

    end;

    definition

      let S be non void Signature;

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

      let t be Term of S, X;

      :: MSAFREE3:def4

      func variables_in t -> ManySortedSubset of X equals (S variables_in t);

      correctness

      proof

        (S variables_in t) c= X by Th14;

        then (S variables_in t) = (X variables_in t) by PBOOLE: 23;

        hence thesis;

      end;

    end

    theorem :: MSAFREE3:15

    

     Th15: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for t be Term of S, X holds ( variables_in t) = (X variables_in t) by Th14, PBOOLE: 23;

    definition

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      :: MSAFREE3:def5

      func S -Terms (X,Y) -> MSSubset of ( FreeMSA Y) means

      : Def5: for s be SortSymbol of S holds (it . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X };

      existence

      proof

        deffunc F( SortSymbol of S) = { t where t be Term of S, Y : ( the_sort_of t) = $1 & ( variables_in t) c= X };

        consider T be ManySortedSet of the carrier of S such that

         A1: for s be SortSymbol of S holds (T . s) = F(s) from PBOOLE:sch 5;

        T c= the Sorts of ( FreeMSA Y)

        proof

          let s be object;

          assume s in the carrier of S;

          then

          reconsider s9 = s as SortSymbol of S;

          let x be object;

          assume

           A2: x in (T . s);

          (T . s9) = { t where t be Term of S, Y : ( the_sort_of t) = s9 & ( variables_in t) c= X } by A1;

          then ex t be Term of S, Y st x = t & ( the_sort_of t) = s9 & ( variables_in t) c= X by A2;

          hence thesis by Th7;

        end;

        then

        reconsider T as MSSubset of ( FreeMSA Y) by PBOOLE:def 18;

        take T;

        thus thesis by A1;

      end;

      correctness

      proof

        let T1,T2 be MSSubset of ( FreeMSA Y) such that

         A3: for s be SortSymbol of S holds (T1 . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } and

         A4: for s be SortSymbol of S holds (T2 . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X };

        now

          let s be object;

          assume

           A5: s in the carrier of S;

          

          hence (T1 . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } by A3

          .= (T2 . s) by A4, A5;

        end;

        hence thesis;

      end;

    end

    theorem :: MSAFREE3:16

    

     Th16: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds for s be SortSymbol of S st x in ((S -Terms (X,Y)) . s) holds x is Term of S, Y

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let s be SortSymbol of S;

      assume x in ((S -Terms (X,Y)) . s);

      then x in { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } by Def5;

      then ex t be Term of S, Y st x = t & ( the_sort_of t) = s & ( variables_in t) c= X;

      hence thesis;

    end;

    theorem :: MSAFREE3:17

    

     Th17: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds for t be Term of S, Y holds for s be SortSymbol of S st t in ((S -Terms (X,Y)) . s) holds ( the_sort_of t) = s & ( variables_in t) c= X

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let q be Term of S, Y, s be SortSymbol of S such that

       A1: q in ((S -Terms (X,Y)) . s);

      ((S -Terms (X,Y)) . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } by Def5;

      then ex t be Term of S, Y st q = t & ( the_sort_of t) = s & ( variables_in t) c= X by A1;

      hence thesis;

    end;

    theorem :: MSAFREE3:18

    

     Th18: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds for s be SortSymbol of S holds ( root-tree [x, s]) in ((S -Terms (X,Y)) . s) iff x in (X . s) & x in (Y . s)

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let s be SortSymbol of S;

      

       A1: ((S -Terms (X,Y)) . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } by Def5;

      hereby

        assume ( root-tree [x, s]) in ((S -Terms (X,Y)) . s);

        then

        consider t be Term of S, Y such that

         A2: ( root-tree [x, s]) = t and ( the_sort_of t) = s and

         A3: ( variables_in t) c= X by A1;

        

         A4: (t . {} ) = [x, s] by A2, TREES_4: 3;

        s in the carrier of S;

        then s <> the carrier of S;

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

        then not (t . {} ) in [:the carrier' of S, {the carrier of S}:] by A4, ZFMISC_1: 87;

        then

        consider s9 be SortSymbol of S, v be Element of (Y . s9) such that

         A5: (t . {} ) = [v, s9] by MSATERM: 2;

        

         A6: s = s9 & x = v by A4, A5, XTUPLE_0: 1;

        ((S variables_in t) . s) = {x} & (( variables_in t) . s) c= (X . s) by A2, A3, Th10;

        hence x in (X . s) & x in (Y . s) by A6, ZFMISC_1: 31;

      end;

      assume that

       A7: x in (X . s) and

       A8: x in (Y . s);

      reconsider t = ( root-tree [x, s]) as Term of S, Y by A8, MSATERM: 4;

      

       A9: ( variables_in t) c= X

      proof

        let i be object;

        assume i in the carrier of S;

        

         A10: ((S variables_in t) . s) = {x} by Th10;

        i <> s implies ((S variables_in t) . i) = {} by Th10;

        hence thesis by A7, A10, ZFMISC_1: 31;

      end;

      ( the_sort_of t) = s by A8, MSATERM: 14;

      hence thesis by A1, A9;

    end;

    theorem :: MSAFREE3:19

    

     Th19: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds for o be OperSymbol of S holds for p be ArgumentSeq of ( Sym (o,Y)) holds (( Sym (o,Y)) -tree p) in ((S -Terms (X,Y)) . ( the_result_sort_of o)) iff ( rng p) c= ( Union (S -Terms (X,Y)))

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let o be OperSymbol of S;

      let p be ArgumentSeq of ( Sym (o,Y));

      set s = ( the_result_sort_of o);

      

       A1: ( dom (S -Terms (X,Y))) = the carrier of S by PARTFUN1:def 2;

      

       A2: ( Sym (o,Y)) = [o, the carrier of S] by MSAFREE:def 9;

      

       A3: ((S -Terms (X,Y)) . s) = { t where t be Term of S, Y : ( the_sort_of t) = s & ( variables_in t) c= X } by Def5;

      hereby

        assume (( Sym (o,Y)) -tree p) in ((S -Terms (X,Y)) . s);

        then

        consider t be Term of S, Y such that

         A4: ( [o, the carrier of S] -tree p) = t and ( the_sort_of t) = s and

         A5: ( variables_in t) c= X by A3, A2;

        thus ( rng p) c= ( Union (S -Terms (X,Y)))

        proof

          let y be object;

          assume

           A6: y in ( rng p);

          then

          consider x be object such that

           A7: x in ( dom p) and

           A8: y = (p . x) by FUNCT_1:def 3;

          reconsider x as Nat by A7;

          reconsider q = (p . x) as Term of S, Y by A7, MSATERM: 22;

          

           A9: ( variables_in q) c= X

          proof

            let z be object;

            assume

             A10: z in the carrier of S;

            let a be object;

            assume a in (( variables_in q) . z);

            then

             A11: a in (( variables_in t) . z) by A4, A6, A8, A10, Th11;

            (( variables_in t) . z) c= (X . z) by A5, A10;

            hence thesis by A11;

          end;

          set sq = ( the_sort_of q);

          ((S -Terms (X,Y)) . sq) = { t9 where t9 be Term of S, Y : ( the_sort_of t9) = sq & ( variables_in t9) c= X } by Def5;

          then q in ((S -Terms (X,Y)) . sq) by A9;

          hence thesis by A1, A8, CARD_5: 2;

        end;

      end;

      set t = (( Sym (o,Y)) -tree p);

      assume

       A12: ( rng p) c= ( Union (S -Terms (X,Y)));

      

       A13: ( variables_in t) c= X

      proof

        let z be object;

        assume

         A14: z in the carrier of S;

        let x be object;

        assume x in (( variables_in t) . z);

        then

        consider q be DecoratedTree such that

         A15: q in ( rng p) and

         A16: x in ((S variables_in q) . z) by A2, A14, Th11;

        consider y be object such that

         A17: y in the carrier of S and

         A18: q in ((S -Terms (X,Y)) . y) by A1, A12, A15, CARD_5: 2;

        ((S -Terms (X,Y)) . y) = { t9 where t9 be Term of S, Y : ( the_sort_of t9) = y & ( variables_in t9) c= X } by A17, Def5;

        then

        consider t9 be Term of S, Y such that

         A19: q = t9 and ( the_sort_of t9) = y and

         A20: ( variables_in t9) c= X by A18;

        (( variables_in t9) . z) c= (X . z) by A14, A20;

        hence thesis by A16, A19;

      end;

      ( the_sort_of t) = s by MSATERM: 20;

      hence thesis by A3, A13;

    end;

    theorem :: MSAFREE3:20

    

     Th20: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for A be MSSubset of ( FreeMSA X) holds A is opers_closed iff for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) st ( rng p) c= ( Union A) holds (( Sym (o,X)) -tree p) in (A . ( the_result_sort_of o))

    proof

      let S be non void Signature;

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

      set A = ( FreeMSA X);

      let T be MSSubset of ( FreeMSA X);

      hereby

        assume

         A1: T is opers_closed;

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X));

        T is_closed_on o by A1;

        then

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

        

         A3: p is Element of ( Args (o,A)) by INSTALG1: 1;

        

         A4: ( dom p) = ( dom ( the_arity_of o)) by MSATERM: 22;

        

         A5: ( dom T) = the carrier of S by PARTFUN1:def 2;

        assume

         A6: ( rng p) c= ( Union T);

         A7:

        now

          let x be object;

          assume

           A8: x in ( dom ( the_arity_of o));

          then

          reconsider i = x as Nat;

          reconsider t = (p . i) as Term of S, X by A4, A8, MSATERM: 22;

          

           A9: ( the_sort_of t) = (( the_arity_of o) . x) & ((T * ( the_arity_of o)) . x) = (T . (( the_arity_of o) . x)) by A4, A8, FUNCT_1: 13, MSATERM: 23;

          (p . x) in ( rng p) by A4, A8, FUNCT_1:def 3;

          then

          consider y be object such that

           A10: y in ( dom T) and

           A11: (p . x) in (T . y) by A6, CARD_5: 2;

          T c= the Sorts of A by PBOOLE:def 18;

          then (T . y) c= (the Sorts of A . y) by A10;

          hence (p . x) in ((T * ( the_arity_of o)) . x) by A10, A11, A9, Th7;

        end;

        ( rng ( the_arity_of o)) c= ( dom T) by A5;

        then ( dom (T * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

        then

         A12: p in ( product (T * ( the_arity_of o))) by A4, A7, CARD_3: 9;

        

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

        .= ((T # ) . ( the_arity_of o)) by MSUALG_1:def 1

        .= ( product (T * ( the_arity_of o))) by FINSEQ_2:def 5;

        then

         A14: ((( Den (o,A)) | (((T # ) * the Arity of S) . o)) . p) = (( Den (o,A)) . p) by A12, FUNCT_1: 49;

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

        then p in ( dom (( Den (o,A)) | (((T # ) * the Arity of S) . o))) by A13, A3, A12, RELAT_1: 57;

        then

         A15: (( Den (o,A)) . p) in ( rng (( Den (o,A)) | (((T # ) * the Arity of S) . o))) by A14, FUNCT_1:def 3;

        ((T * the ResultSort of S) . o) = (T . (the ResultSort of S . o)) by FUNCT_2: 15

        .= (T . ( the_result_sort_of o)) by MSUALG_1:def 2;

        then [o, the carrier of S] = ( Sym (o,X)) & (( Den (o,A)) . p) in (T . ( the_result_sort_of o)) by A2, A15, MSAFREE:def 9;

        hence (( Sym (o,X)) -tree p) in (T . ( the_result_sort_of o)) by A3, INSTALG1: 3;

      end;

      assume

       A16: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) st ( rng p) c= ( Union T) holds (( Sym (o,X)) -tree p) in (T . ( the_result_sort_of o));

      let o be OperSymbol of S;

      let x be object;

      

       A17: ((T * the ResultSort of S) . o) = (T . (the ResultSort of S . o)) by FUNCT_2: 15

      .= (T . ( the_result_sort_of o)) by MSUALG_1:def 2;

      assume x in ( rng (( Den (o,A)) | (((T # ) * the Arity of S) . o)));

      then

      consider y be object such that

       A18: y in ( dom (( Den (o,A)) | (((T # ) * the Arity of S) . o))) and

       A19: x = ((( Den (o,A)) | (((T # ) * the Arity of S) . o)) . y) by FUNCT_1:def 3;

      y in ( dom ( Den (o,A))) by A18, RELAT_1: 57;

      then

      reconsider y as Element of ( Args (o,A));

      reconsider p = y as ArgumentSeq of ( Sym (o,X)) by INSTALG1: 1;

      

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

      .= ((T # ) . ( the_arity_of o)) by MSUALG_1:def 1

      .= ( product (T * ( the_arity_of o))) by FINSEQ_2:def 5;

      

       A21: ( rng p) c= ( Union T)

      proof

        let z be object;

        

         A22: ( dom T) = the carrier of S by PARTFUN1:def 2;

        assume z in ( rng p);

        then

        consider a be object such that

         A23: a in ( dom p) and

         A24: z = (p . a) by FUNCT_1:def 3;

        

         A25: ( dom p) = ( dom (T * ( the_arity_of o))) by A18, A20, CARD_3: 9;

        then

         A26: z in ((T * ( the_arity_of o)) . a) & ((T * ( the_arity_of o)) . a) = (T . (( the_arity_of o) . a)) by A18, A20, A23, A24, CARD_3: 9, FUNCT_1: 12;

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

        then ( dom (T * ( the_arity_of o))) = ( dom ( the_arity_of o)) by A22, RELAT_1: 27;

        then (( the_arity_of o) . a) in ( rng ( the_arity_of o)) by A23, A25, FUNCT_1:def 3;

        hence thesis by A22, A26, CARD_5: 2;

      end;

      x = (( Den (o,A)) . y) by A18, A19, FUNCT_1: 47

      .= ( [o, the carrier of S] -tree y) by INSTALG1: 3

      .= (( Sym (o,X)) -tree p) by MSAFREE:def 9;

      hence thesis by A16, A17, A21;

    end;

    theorem :: MSAFREE3:21

    

     Th21: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds (S -Terms (X,Y)) is opers_closed

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      for o be OperSymbol of S holds for p be ArgumentSeq of ( Sym (o,Y)) st ( rng p) c= ( Union (S -Terms (X,Y))) holds (( Sym (o,Y)) -tree p) in ((S -Terms (X,Y)) . ( the_result_sort_of o)) by Th19;

      hence thesis by Th20;

    end;

    theorem :: MSAFREE3:22

    

     Th22: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for X be ManySortedSet of the carrier of S holds (( Reverse Y) "" X) c= (S -Terms (X,Y))

    proof

      let S be non void Signature;

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

      let X be ManySortedSet of the carrier of S;

      let s be object;

      assume s in the carrier of S;

      then

      reconsider s9 = s as SortSymbol of S;

      let x be object;

      assume x in ((( Reverse Y) "" X) . s);

      then

       A1: x in ((( Reverse Y) . s9) " (X . s9)) by EQUATION:def 1;

      then

       A2: x in ( dom (( Reverse Y) . s)) by FUNCT_1:def 7;

      

       A3: ((( Reverse Y) . s) . x) in (X . s) by A1, FUNCT_1:def 7;

      

       A4: (( Reverse Y) . s) = ( Reverse (s9,Y)) by MSAFREE:def 18;

      then

       A5: ( dom (( Reverse Y) . s)) = ( FreeGen (s9,Y)) by FUNCT_2:def 1;

      then

      consider b be set such that

       A6: b in (Y . s9) and

       A7: x = ( root-tree [b, s9]) by A2, MSAFREE:def 15;

      ( FreeGen (s9,Y)) = { ( root-tree t) where t be Symbol of ( DTConMSA Y) : t in ( Terminals ( DTConMSA Y)) & (t `2 ) = s } by MSAFREE: 13;

      then

      consider a be Symbol of ( DTConMSA Y) such that

       A8: x = ( root-tree a) and a in ( Terminals ( DTConMSA Y)) and (a `2 ) = s by A2, A5;

      (( Reverse (s9,Y)) . x) = (a `1 ) by A2, A5, A8, MSAFREE:def 17

      .= ( [b, s] `1 ) by A8, A7, TREES_4: 4

      .= b;

      hence thesis by A3, A4, A6, A7, Th18;

    end;

    theorem :: MSAFREE3:23

    

     Th23: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds for t be Term of S, (X (\/) (the carrier of S --> { 0 })) holds for s be SortSymbol of S st t in ((S -Terms (X,(X (\/) (the carrier of S --> { 0 })))) . s) holds t in (the Sorts of ( Free (S,X)) . s)

    proof

      let S be non void non empty ManySortedSign;

      let X be ManySortedSet of the carrier of S;

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

      set T = the Sorts of ( Free (S,X));

      defpred P[ set] means for s be SortSymbol of S st $1 in ((S -Terms (X,Y)) . s) holds $1 in (T . s);

      

       A1: ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1;

      then

      reconsider TT = T as MSSubset of ( FreeMSA Y) by MSUALG_2:def 9;

       A2:

      now

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,Y)) such that

         A3: for t be Term of S, Y st t in ( rng p) holds P[t];

        thus P[( [o, the carrier of S] -tree p)]

        proof

          let s be SortSymbol of S;

          assume

           A4: ( [o, the carrier of S] -tree p) in ((S -Terms (X,Y)) . s);

          

           A5: ( Sym (o,Y)) = [o, the carrier of S] by MSAFREE:def 9;

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

          then

           A6: s = ( the_result_sort_of o) by A4, A5, Th17;

          then

           A7: ( rng p) c= ( Union (S -Terms (X,Y))) by A4, A5, Th19;

          

           A8: ( rng p) c= ( Union TT)

          proof

            let x be object;

            assume

             A9: x in ( rng p);

            then

            consider y be object such that

             A10: y in ( dom (S -Terms (X,Y))) and

             A11: x in ((S -Terms (X,Y)) . y) by A7, CARD_5: 2;

            reconsider y as SortSymbol of S by A10;

            ((S -Terms (X,Y)) . y) = ((S -Terms (X,Y)) . y);

            then

            reconsider x as Term of S, Y by A11, Th16;

            ( dom T) = the carrier of S & x in (T . y) by A3, A9, A11, PARTFUN1:def 2;

            hence thesis by CARD_5: 2;

          end;

          TT is opers_closed by A1, MSUALG_2:def 9;

          hence thesis by A5, A6, A8, Th20;

        end;

      end;

      

       A12: (S -Terms (X,Y)) c= the Sorts of ( FreeMSA Y) by PBOOLE:def 18;

       A13:

      now

        let s1 be SortSymbol of S, v be Element of (Y . s1);

        thus P[( root-tree [v, s1])]

        proof

          reconsider t = ( root-tree [v, s1]) as Term of S, Y by MSATERM: 4;

          let s be SortSymbol of S;

          assume

           A14: ( root-tree [v, s1]) in ((S -Terms (X,Y)) . s);

          ((S -Terms (X,Y)) . s) c= (the Sorts of ( FreeMSA Y) . s) by A12;

          then

           A15: ( the_sort_of t) = s by A14, Th7;

          

           A16: ( the_sort_of t) = s1 by MSATERM: 14;

          then v in (X . s) by A14, A15, Th18;

          hence thesis by A15, A16, Th4;

        end;

      end;

      thus for t be Term of S, Y holds P[t] from MSATERM:sch 1( A13, A2);

    end;

    theorem :: MSAFREE3:24

    

     Th24: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds the Sorts of ( Free (S,X)) = (S -Terms (X,(X (\/) (the carrier of S --> { 0 }))))

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

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

      set B = MSAlgebra (# (S -Terms (X,Y)), ( Opers (( FreeMSA Y),(S -Terms (X,Y)))) #);

      for Z be MSSubset of ( FreeMSA Y) st Z = the Sorts of B holds Z is opers_closed & the Charact of B = ( Opers (( FreeMSA Y),Z)) by Th21;

      then

      reconsider B as MSSubAlgebra of ( FreeMSA Y) by MSUALG_2:def 9;

      

       A1: ( FreeMSA Y) = MSAlgebra (# ( FreeSort Y), ( FreeOper Y) #) & ( dom ( FreeSort Y)) = the carrier of S by MSAFREE:def 14, PARTFUN1:def 2;

      (( Reverse Y) "" X) c= (S -Terms (X,Y)) by Th22;

      then

       A2: (( Reverse Y) "" X) is MSSubset of B by PBOOLE:def 18;

      let s be Element of S;

      ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1;

      then ( Free (S,X)) is MSSubAlgebra of B by A2, MSUALG_2:def 17;

      then the Sorts of ( Free (S,X)) is MSSubset of B by MSUALG_2:def 9;

      then the Sorts of ( Free (S,X)) c= (S -Terms (X,Y)) by PBOOLE:def 18;

      hence (the Sorts of ( Free (S,X)) . s) c= ((S -Terms (X,Y)) . s);

      let x be object;

      assume

       A3: x in ((S -Terms (X,Y)) . s);

      (S -Terms (X,Y)) c= the Sorts of ( FreeMSA Y) by PBOOLE:def 18;

      then ((S -Terms (X,Y)) . s) c= (the Sorts of ( FreeMSA Y) . s);

      then x in ( Union ( FreeSort Y)) by A3, A1, CARD_5: 2;

      then x is Term of S, Y by MSATERM: 13;

      hence thesis by A3, Th23;

    end;

    theorem :: MSAFREE3:25

    for S be non void Signature holds for X be ManySortedSet of the carrier of S holds (( FreeMSA (X (\/) (the carrier of S --> { 0 }))) | (S -Terms (X,(X (\/) (the carrier of S --> { 0 }))))) = ( Free (S,X))

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

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

      (( FreeMSA Y) | (S -Terms (X,Y))) = MSAlgebra (# (S -Terms (X,Y)), ( Opers (( FreeMSA Y),(S -Terms (X,Y)))) #) & ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1, Th21, MSUALG_2:def 15;

      hence thesis by Th24, MSUALG_2: 9;

    end;

    theorem :: MSAFREE3:26

    

     Th26: for S be non void Signature holds for X,Y be non-empty ManySortedSet of the carrier of S holds for A be MSSubAlgebra of ( FreeMSA X) holds for B be MSSubAlgebra of ( FreeMSA Y) st the Sorts of A = the Sorts of B holds the MSAlgebra of A = the MSAlgebra of B

    proof

      let S be non void Signature;

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

      let A be MSSubAlgebra of ( FreeMSA X);

      let B be MSSubAlgebra of ( FreeMSA Y) such that

       A1: the Sorts of A = the Sorts of B;

      reconsider SB = the Sorts of B as MSSubset of ( FreeMSA Y) by MSUALG_2:def 9;

      reconsider SA = the Sorts of A as MSSubset of ( FreeMSA X) by MSUALG_2:def 9;

      

       A2: SA is opers_closed by MSUALG_2:def 9;

      

       A3: SB is opers_closed by MSUALG_2:def 9;

      now

        let x be object;

        

         A4: SA c= the Sorts of ( FreeMSA X) & the Sorts of ( FreeMSA X) is MSSubset of ( FreeMSA X) by PBOOLE:def 18;

        assume x in the carrier' of S;

        then

        reconsider o = x as OperSymbol of S;

        

         A5: SA is_closed_on o by A2;

        

         A6: (the Charact of A . o) = (( Opers (( FreeMSA X),SA)) . o) by MSUALG_2:def 9

        .= (o /. SA) by MSUALG_2:def 8

        .= (( Den (o,( FreeMSA X))) | (((SA # ) * the Arity of S) . o)) by A5, MSUALG_2:def 7;

        ( Args (o,( FreeMSA X))) = (((the Sorts of ( FreeMSA X) # ) * the Arity of S) . o) by MSUALG_1:def 4;

        then ( dom ( Den (o,( FreeMSA X)))) = (((the Sorts of ( FreeMSA X) # ) * the Arity of S) . o) by FUNCT_2:def 1;

        then

         A7: ( dom (the Charact of A . o)) = (((SA # ) * the Arity of S) . o) by A6, A4, MSUALG_2: 2, RELAT_1: 62;

        

         A8: SB c= the Sorts of ( FreeMSA Y) & the Sorts of ( FreeMSA Y) is MSSubset of ( FreeMSA Y) by PBOOLE:def 18;

        then

         A9: (((SB # ) * the Arity of S) . o) c= (((the Sorts of ( FreeMSA Y) # ) * the Arity of S) . o) by MSUALG_2: 2;

        

         A10: SB is_closed_on o by A3;

        

         A11: (the Charact of B . o) = (( Opers (( FreeMSA Y),SB)) . o) by MSUALG_2:def 9

        .= (o /. SB) by MSUALG_2:def 8

        .= (( Den (o,( FreeMSA Y))) | (((SB # ) * the Arity of S) . o)) by A10, MSUALG_2:def 7;

        ( Args (o,( FreeMSA Y))) = (((the Sorts of ( FreeMSA Y) # ) * the Arity of S) . o) by MSUALG_1:def 4;

        then ( dom ( Den (o,( FreeMSA Y)))) = (((the Sorts of ( FreeMSA Y) # ) * the Arity of S) . o) by FUNCT_2:def 1;

        then

         A12: ( dom (the Charact of B . o)) = (((SB # ) * the Arity of S) . o) by A11, A8, MSUALG_2: 2, RELAT_1: 62;

        

         A13: (((SA # ) * the Arity of S) . o) c= (((the Sorts of ( FreeMSA X) # ) * the Arity of S) . o) by A4, MSUALG_2: 2;

        now

          let x be object;

          assume

           A14: x in (((SA # ) * the Arity of S) . o);

          then

          reconsider p1 = x as Element of ( Args (o,( FreeMSA X))) by A13, MSUALG_1:def 4;

          reconsider p2 = x as Element of ( Args (o,( FreeMSA Y))) by A1, A9, A14, MSUALG_1:def 4;

          

          thus ((the Charact of A . o) . x) = (( Den (o,( FreeMSA X))) . p1) by A6, A7, A14, FUNCT_1: 47

          .= ( [o, the carrier of S] -tree p1) by INSTALG1: 3

          .= (( Den (o,( FreeMSA Y))) . p2) by INSTALG1: 3

          .= ((the Charact of B . o) . x) by A1, A11, A12, A14, FUNCT_1: 47;

        end;

        hence (the Charact of A . x) = (the Charact of B . x) by A1, A7, A12, FUNCT_1: 2;

      end;

      hence thesis by A1, PBOOLE: 3;

    end;

    theorem :: MSAFREE3:27

    

     Th27: for S be non void Signature holds for X be non empty-yielding ManySortedSet of the carrier of S holds for Y be ManySortedSet of the carrier of S holds for t be Element of ( Free (S,X)) holds (S variables_in t) c= X

    proof

      let S be non void Signature;

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

      let Y be ManySortedSet of the carrier of S;

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

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

      reconsider t as Term of S, Z by Th8;

      t in ( Union the Sorts of ( Free (S,X)));

      then

       A1: t in ( Union (S -Terms (X,Z))) by Th24;

      ( dom (S -Terms (X,Z))) = the carrier of S by PARTFUN1:def 2;

      then ex s be object st s in the carrier of S & t in ((S -Terms (X,Z)) . s) by A1, CARD_5: 2;

      then ( variables_in t) c= X by Th17;

      hence thesis;

    end;

    theorem :: MSAFREE3:28

    

     Th28: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for t be Term of S, X holds ( variables_in t) c= X

    proof

      let S be non void Signature;

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

      defpred P[ DecoratedTree] means (S variables_in $1) c= X;

      let t be Term of S, X;

      

       A1: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) st for t be Term of S, X st t in ( rng p) holds P[t] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,X)) such that

         A2: for t be Term of S, X st t in ( rng p) holds (S variables_in t) c= X;

        thus (S variables_in ( [o, the carrier of S] -tree p)) c= X

        proof

          let s be object;

          assume

           A3: s in the carrier of S;

          let x be object;

          assume x in ((S variables_in ( [o, the carrier of S] -tree p)) . s);

          then

          consider t be DecoratedTree such that

           A4: t in ( rng p) and

           A5: x in ((S variables_in t) . s) by A3, Th11;

          consider i be object such that

           A6: i in ( dom p) and

           A7: t = (p . i) by A4, FUNCT_1:def 3;

          reconsider i as Nat by A6;

          reconsider t = (p . i) as Term of S, X by A6, MSATERM: 22;

          (S variables_in t) c= X by A2, A4, A7;

          then ((S variables_in t) . s) c= (X . s) by A3;

          hence thesis by A5, A7;

        end;

      end;

      

       A8: for s be SortSymbol of S, v be Element of (X . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S, x be Element of (X . s);

        thus (S variables_in ( root-tree [x, s])) c= X

        proof

          let y be object;

          assume y in the carrier of S;

          

           A9: y <> s implies ((S variables_in ( root-tree [x, s])) . y) = {} by Th10;

          ((S variables_in ( root-tree [x, s])) . s) = {x} by Th10;

          hence thesis by A9;

        end;

      end;

      for t be Term of S, X holds P[t] from MSATERM:sch 1( A8, A1);

      hence thesis;

    end;

    theorem :: MSAFREE3:29

    

     Th29: for S be non void Signature holds for X,Y be non-empty ManySortedSet of the carrier of S holds for t1 be Term of S, X, t2 be Term of S, Y st t1 = t2 holds ( the_sort_of t1) = ( the_sort_of t2)

    proof

      let S be non void Signature;

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

      let t1 be Term of S, X, t2 be Term of S, Y such that

       A1: t1 = t2;

      per cases by MSATERM: 2;

        suppose ex s be SortSymbol of S, v be Element of (X . s) st (t1 . {} ) = [v, s];

        then

        consider s be SortSymbol of S, x be Element of (X . s) such that

         A2: (t1 . {} ) = [x, s];

        s in the carrier of S;

        then s <> the carrier of S;

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

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

        then

        consider s9 be SortSymbol of S, y be Element of (Y . s9) such that

         A3: (t2 . {} ) = [y, s9] by A1, A2, MSATERM: 2;

        t1 = ( root-tree [x, s]) by A2, MSATERM: 5;

        then

         A4: ( the_sort_of t1) = s by MSATERM: 14;

        t2 = ( root-tree [y, s9]) by A3, MSATERM: 5;

        then ( the_sort_of t2) = s9 by MSATERM: 14;

        hence thesis by A1, A2, A3, A4, XTUPLE_0: 1;

      end;

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

        then

        consider o,z be object such that

         A5: o in the carrier' of S and

         A6: z in {the carrier of S} and

         A7: (t1 . {} ) = [o, z] by ZFMISC_1:def 2;

        reconsider o as OperSymbol of S by A5;

        

         A8: z = the carrier of S by A6, TARSKI:def 1;

        then ( the_sort_of t1) = ( the_result_sort_of o) by A7, MSATERM: 17;

        hence thesis by A1, A7, A8, MSATERM: 17;

      end;

    end;

    theorem :: MSAFREE3:30

    

     Th30: for S be non void Signature holds for X,Y be non-empty ManySortedSet of the carrier of S holds for t be Term of S, Y st ( variables_in t) c= X holds t is Term of S, X

    proof

      let S be non void Signature;

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

      defpred P[ DecoratedTree] means (Y variables_in $1) c= X implies $1 is Term of S, X;

      let t be Term of S, Y;

      

       A1: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,Y)) st for t be Term of S, Y st t in ( rng p) holds P[t] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,Y)) such that

         A2: for t be Term of S, Y st t in ( rng p) & (Y variables_in t) c= X holds t is Term of S, X and

         A3: (Y variables_in ( [o, the carrier of S] -tree p)) c= X;

         A4:

        now

          let i be Nat;

          assume

           A5: i in ( dom p);

          then

          reconsider t = (p . i) as Term of S, Y by MSATERM: 22;

          

           A6: t in ( rng p) by A5, FUNCT_1:def 3;

          (Y variables_in t) c= X

          proof

            let y be object;

            assume y in the carrier of S;

            then

            reconsider s = y as SortSymbol of S;

            let x be object;

            assume x in ((Y variables_in t) . y);

            then

             A7: x in ((Y variables_in ( [o, the carrier of S] -tree p)) . s) by A6, Th13;

            ((Y variables_in ( [o, the carrier of S] -tree p)) . s) c= (X . s) by A3;

            hence thesis by A7;

          end;

          then

          reconsider t9 = t as Term of S, X by A2, A6;

          take t9;

          thus t9 = (p . i);

          ( the_sort_of t) = (( the_arity_of o) . i) by A5, MSATERM: 23;

          hence ( the_sort_of t9) = (( the_arity_of o) . i) by Th29;

        end;

        ( len p) = ( len ( the_arity_of o)) by MSATERM: 22;

        then

        reconsider p as ArgumentSeq of ( Sym (o,X)) by A4, MSATERM: 24;

        (( Sym (o,X)) -tree p) is Term of S, X;

        hence thesis by MSAFREE:def 9;

      end;

      assume ( variables_in t) c= X;

      then

       A8: (Y variables_in t) c= X by Th15;

      

       A9: for s be SortSymbol of S, x be Element of (Y . s) holds P[( root-tree [x, s])]

      proof

        let s be SortSymbol of S, x be Element of (Y . s);

        assume (Y variables_in ( root-tree [x, s])) c= X;

        then

         A10: ((Y variables_in ( root-tree [x, s])) . s) c= (X . s);

        ((Y variables_in ( root-tree [x, s])) . s) = {x} by Th12;

        then x in (X . s) by A10, ZFMISC_1: 31;

        hence thesis by MSATERM: 4;

      end;

      for t be Term of S, Y holds P[t] from MSATERM:sch 1( A9, A1);

      hence thesis by A8;

    end;

    theorem :: MSAFREE3:31

    for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds ( Free (S,X)) = ( FreeMSA X)

    proof

      let S be non void Signature;

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

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

      

       A1: the Sorts of ( Free (S,X)) = (S -Terms (X,Y)) by Th24;

      

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

      

       A3: the Sorts of ( Free (S,X)) = the Sorts of ( FreeMSA X)

      proof

        let s be Element of S;

        reconsider s9 = s as SortSymbol of S;

        thus (the Sorts of ( Free (S,X)) . s) c= (the Sorts of ( FreeMSA X) . s)

        proof

          let x be object;

          assume

           A4: x in (the Sorts of ( Free (S,X)) . s);

          then

          reconsider t = x as Term of S, Y by A1, Th16;

          ( variables_in t) c= X by A1, A4, Th17;

          then

          reconsider t9 = t as Term of S, X by Th30;

          ( the_sort_of t) = s by A1, A4, Th17;

          then ( the_sort_of t9) = s by Th29;

          then x in ( FreeSort (X,s9)) by MSATERM:def 5;

          hence thesis by A2, MSAFREE:def 11;

        end;

        reconsider s9 = s as SortSymbol of S;

        let x be object;

        assume x in (the Sorts of ( FreeMSA X) . s);

        then

         A5: x in ( FreeSort (X,s9)) by A2, MSAFREE:def 11;

        ( FreeSort (X,s9)) c= (S -Terms X) by MSATERM: 12;

        then

        reconsider t = x as Term of S, X by A5;

        X c= Y by PBOOLE: 14;

        then

        reconsider t9 = t as Term of S, Y by MSATERM: 26;

        ( variables_in t) = (S variables_in t);

        then

         A6: ( variables_in t9) c= X by Th28;

        ( the_sort_of t) = s by A5, MSATERM:def 5;

        then ( the_sort_of t9) = s by Th29;

        then t in { q where q be Term of S, Y : ( the_sort_of q) = s9 & ( variables_in q) c= X } by A6;

        hence thesis by A1, Def5;

      end;

      ( FreeMSA X) is MSSubAlgebra of ( FreeMSA X) & ex A be MSSubset of ( FreeMSA Y) st ( Free (S,X)) = ( GenMSAlg A) & A = (( Reverse Y) "" X) by Def1, MSUALG_2: 5;

      hence thesis by A3, Th26;

    end;

    theorem :: MSAFREE3:32

    

     Th32: for S be non void Signature holds for Y be non-empty ManySortedSet of the carrier of S holds for t be Term of S, Y holds for p be Element of ( dom t) holds ( variables_in (t | p)) c= ( variables_in t)

    proof

      let S be non void Signature;

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

      let t be Term of S, Y;

      let p be Element of ( dom t);

      reconsider q = (t | p) as Term of S, Y;

      let s be object;

      assume

       A1: s in the carrier of S;

      let x be object;

      assume x in (( variables_in (t | p)) . s);

      then x in { (a `1 ) where a be Element of ( rng q) : (a `2 ) = s } by A1, Def2;

      then

      consider a be Element of ( rng (t | p)) such that

       A2: x = (a `1 ) & (a `2 ) = s;

      ( rng (t | p)) c= ( rng t) & a in ( rng (t | p)) by TREES_2: 32;

      then x in { (b `1 ) where b be Element of ( rng t) : (b `2 ) = s } by A2;

      hence thesis by A1, Def2;

    end;

    theorem :: MSAFREE3:33

    

     Th33: for S be non void Signature holds for X be non empty-yielding ManySortedSet of the carrier of S holds for t be Element of ( Free (S,X)) holds for p be Element of ( dom t) holds (t | p) is Element of ( Free (S,X))

    proof

      let S be non void Signature;

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

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

      let p be Element of ( dom t);

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

      reconsider t as Term of S, Y by Th8;

      reconsider p as Element of ( dom t);

      

       A1: ( variables_in (t | p)) c= ( variables_in t) by Th32;

      

       A2: the Sorts of ( Free (S,X)) = (S -Terms (X,Y)) & ( dom (S -Terms (X,Y))) = the carrier of S by Th24, PARTFUN1:def 2;

      then ex x be object st x in the carrier of S & t in ((S -Terms (X,Y)) . x) by CARD_5: 2;

      then ( variables_in t) c= X by Th17;

      then ( variables_in (t | p)) c= X by A1, PBOOLE: 13;

      then (t | p) in { q where q be Term of S, Y : ( the_sort_of q) = ( the_sort_of (t | p)) & ( variables_in q) c= X };

      then (t | p) in ((S -Terms (X,Y)) . ( the_sort_of (t | p))) by Def5;

      hence thesis by A2, CARD_5: 2;

    end;

    theorem :: MSAFREE3:34

    

     Th34: for S be non void Signature holds for X be non-empty ManySortedSet of the carrier of S holds for t be Term of S, X holds for a be Element of ( rng t) holds a = [(a `1 ), (a `2 )]

    proof

      let S be non void Signature;

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

      let t be Term of S, X;

      let a be Element of ( rng t);

      consider x be object such that

       A1: x in ( dom t) and

       A2: a = (t . x) by FUNCT_1:def 3;

      reconsider x as Element of ( dom t) by A1;

      a = ((t | x) . {} ) by A2, TREES_9: 35;

      then (ex s be SortSymbol of S, v be Element of (X . s) st a = [v, s]) or a in [:the carrier' of S, {the carrier of S}:] by MSATERM: 2;

      hence thesis by MCART_1: 21;

    end;

    theorem :: MSAFREE3:35

    for S be non void Signature holds for X be non empty-yielding ManySortedSet of the carrier of S holds for t be Element of ( Free (S,X)) holds for s be SortSymbol of S holds (x in ((S variables_in t) . s) implies [x, s] in ( rng t)) & ( [x, s] in ( rng t) implies x in ((S variables_in t) . s) & x in (X . s))

    proof

      let S be non void Signature;

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

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

      let s be SortSymbol of S;

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

      hereby

        assume x in ((S variables_in t) . s);

        then x in { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } by Def2;

        then

        consider a be Element of ( rng t) such that

         A1: x = (a `1 ) & (a `2 ) = s;

        t is Term of S, Y & a in ( rng t) by Th8;

        hence [x, s] in ( rng t) by A1, Th34;

      end;

      assume

       A2: [x, s] in ( rng t);

      then

      consider z be object such that

       A3: z in ( dom t) and

       A4: [x, s] = (t . z) by FUNCT_1:def 3;

      reconsider z as Element of ( dom t) by A3;

      reconsider q = (t | z) as Element of ( Free (S,X)) by Th33;

      

       A5: [x, s] = (q . {} ) by A4, TREES_9: 35;

      ( [x, s] `1 ) = x & ( [x, s] `2 ) = s;

      then

       A6: x in { (a `1 ) where a be Element of ( rng t) : (a `2 ) = s } by A2;

      

       A7: q is Term of S, Y by Th8;

      s in the carrier of S;

      then s <> the carrier of S;

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

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

      then

      consider s9 be SortSymbol of S, v be Element of (Y . s9) such that

       A8: [x, s] = [v, s9] by A5, A7, MSATERM: 2;

      (S variables_in q) c= X by Th27;

      then

       A9: ((S variables_in q) . s9) c= (X . s9);

      q = ( root-tree [v, s9]) by A5, A7, A8, MSATERM: 5;

      then ((S variables_in q) . s9) = {v} by Th10;

      then

       A10: v in (X . s9) by A9, ZFMISC_1: 31;

      x = v by A8, XTUPLE_0: 1;

      hence thesis by A8, A10, A6, Def2, XTUPLE_0: 1;

    end;

    theorem :: MSAFREE3:36

    for S be non void Signature holds for X be ManySortedSet of the carrier of S st for s be SortSymbol of S st (X . s) = {} holds ex o be OperSymbol of S st ( the_result_sort_of o) = s & ( the_arity_of o) = {} holds ( Free (S,X)) is non-empty

    proof

      let C be non void Signature;

      let X be ManySortedSet of the carrier of C such that

       A1: for s be SortSymbol of C st (X . s) = {} holds ex o be OperSymbol of C st ( the_result_sort_of o) = s & ( the_arity_of o) = {} ;

      now

        assume {} in ( rng the Sorts of ( Free (C,X)));

        then

        consider s be object such that

         A2: s in ( dom the Sorts of ( Free (C,X))) and

         A3: {} = (the Sorts of ( Free (C,X)) . s) by FUNCT_1:def 3;

        reconsider s as SortSymbol of C by A2;

        set x = the Element of (X . s);

        per cases ;

          suppose (X . s) = {} ;

          then ex m be OperSymbol of C st ( the_result_sort_of m) = s & ( the_arity_of m) = {} by A1;

          hence contradiction by A3, Th5;

        end;

          suppose (X . s) <> {} ;

          then ( root-tree [x, s]) in (the Sorts of ( Free (C,X)) . s) by Th4;

          hence contradiction by A3;

        end;

      end;

      then the Sorts of ( Free (C,X)) is non-empty by RELAT_1:def 9;

      hence thesis by MSUALG_1:def 3;

    end;

    theorem :: MSAFREE3:37

    

     Th37: for S be non void non empty ManySortedSign holds for A be MSAlgebra over S holds for B be MSSubAlgebra of A holds for o be OperSymbol of S holds ( Args (o,B)) c= ( Args (o,A))

    proof

      let S be non void non empty ManySortedSign;

      let A be MSAlgebra over S;

      let B be MSSubAlgebra of A;

      reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;

      let o be OperSymbol of S;

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

      

       A1: ( Args (o,B)) = (((SB # ) * the Arity of S) . o) by MSUALG_1:def 4;

      SB c= SA & ( Args (o,A)) = (((SA # ) * the Arity of S) . o) by MSUALG_1:def 4, PBOOLE:def 18;

      hence thesis by A1, MSUALG_2: 2;

    end;

    theorem :: MSAFREE3:38

    

     Th38: for S be non void Signature holds for A be feasible MSAlgebra over S holds for B be MSSubAlgebra of A holds B is feasible

    proof

      let S be non void Signature;

      let A be feasible MSAlgebra over S;

      let B be MSSubAlgebra of A;

      reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;

      let o be OperSymbol of S;

      set a = the Element of ( Args (o,B));

      assume ( Args (o,B)) <> {} ;

      then

       A1: a in ( Args (o,B));

      

       A2: ( Args (o,B)) c= ( Args (o,A)) by Th37;

      then ( Result (o,A)) <> {} by A1, MSUALG_6:def 1;

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

      then a in ( dom (( Den (o,A)) | ( Args (o,B)))) by A1, A2, RELAT_1: 57;

      then

       A3: ( Result (o,B)) = ((SB * the ResultSort of S) . o) & ((( Den (o,A)) | ( Args (o,B))) . a) in ( rng (( Den (o,A)) | ( Args (o,B)))) by FUNCT_1:def 3, MSUALG_1:def 5;

      SB is opers_closed by MSUALG_2:def 9;

      then SB is_closed_on o;

      then ( rng (( Den (o,A)) | (((SB # ) * the Arity of S) . o))) c= ((SB * the ResultSort of S) . o);

      hence thesis by A3, MSUALG_1:def 4;

    end;

    registration

      let S be non void Signature, A be feasible MSAlgebra over S;

      cluster -> feasible for MSSubAlgebra of A;

      coherence by Th38;

    end

    theorem :: MSAFREE3:39

    

     Th39: for S be non void Signature holds for X be ManySortedSet of the carrier of S holds ( Free (S,X)) is feasible free

    proof

      let S be non void Signature;

      let X be ManySortedSet of the carrier of S;

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

      consider A be MSSubset of ( FreeMSA Y) such that

       A1: ( Free (S,X)) = ( GenMSAlg A) and

       A2: A = (( Reverse Y) "" X) by Def1;

      thus ( Free (S,X)) is feasible by A1;

      A is ManySortedSubset of ( FreeGen Y) by A2, EQUATION: 8;

      then A c= ( FreeGen Y) by PBOOLE:def 18;

      hence thesis by A1, EQUATION: 28;

    end;

    registration

      let S be non void Signature, X be ManySortedSet of the carrier of S;

      cluster ( Free (S,X)) -> feasible free;

      coherence by Th39;

    end