msaterm.miz



    begin

    

     Lm1: for n be set, p be FinSequence st n in ( dom p) holds ex k be Element of NAT st n = (k + 1) & k < ( len p)

    proof

      let n be set, p be FinSequence;

      assume

       A1: n in ( dom p);

      then

      reconsider n as Element of NAT ;

      n >= 1 by A1, FINSEQ_3: 25;

      then

      consider k be Nat such that

       A2: n = (1 + k) by NAT_1: 10;

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

      take k;

      n <= ( len p) by A1, FINSEQ_3: 25;

      hence thesis by A2, NAT_1: 13;

    end;

     Lm2:

    now

      let n be Element of NAT , x be set;

      let p be FinSequence of x;

      n >= 0 by NAT_1: 2;

      then

       A1: (n + 1) >= ( 0 + 1) by XREAL_1: 7;

      assume n < ( len p);

      then (n + 1) <= ( len p) by NAT_1: 13;

      then (n + 1) in ( dom p) by A1, FINSEQ_3: 25;

      then

       A2: (p . (n + 1)) in ( rng p) by FUNCT_1:def 3;

      ( rng p) c= x by FINSEQ_1:def 4;

      hence (p . (n + 1)) in x by A2;

    end;

    reserve S for non void non empty ManySortedSign,

V for non-empty ManySortedSet of the carrier of S;

    definition

      let S;

      let V be ManySortedSet of the carrier of S;

      :: MSATERM:def1

      func S -Terms V -> Subset of ( FinTrees the carrier of ( DTConMSA V)) equals

      : Def1: ( TS ( DTConMSA V));

      correctness ;

    end

    registration

      let S, V;

      cluster (S -Terms V) -> non empty;

      correctness ;

    end

    definition

      let S, V;

      mode Term of S,V is Element of (S -Terms V);

    end

    reserve A for MSAlgebra over S,

t for Term of S, V;

    definition

      let S, V;

      let o be OperSymbol of S;

      :: original: Sym

      redefine

      func Sym (o,V) -> NonTerminal of ( DTConMSA V) ;

      coherence

      proof

        

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

        

         A2: ( NonTerminals ( DTConMSA V)) = [:the carrier' of S, {the carrier of S}:] by MSAFREE: 6;

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

        hence thesis by A2, A1, ZFMISC_1: 87;

      end;

    end

    definition

      let S, V;

      let sy be NonTerminal of ( DTConMSA V);

      :: MSATERM:def2

      mode ArgumentSeq of sy -> FinSequence of (S -Terms V) means

      : Def2: it is SubtreeSeq of sy;

      existence

      proof

        set q = the SubtreeSeq of sy;

        q is FinSequence of (S -Terms V);

        hence thesis;

      end;

    end

    theorem :: MSATERM:1

    

     Th1: for o be OperSymbol of S, a be FinSequence holds ( [o, the carrier of S] -tree a) in (S -Terms V) & a is DTree-yielding iff a is ArgumentSeq of ( Sym (o,V))

    proof

      let o be OperSymbol of S, a be FinSequence;

      

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

      

       A2: (S -Terms V) = ( TS ( DTConMSA V));

      hereby

        assume ( [o, the carrier of S] -tree a) in (S -Terms V);

        then

        reconsider t = ( [o, the carrier of S] -tree a) as Element of ( TS ( DTConMSA V));

        assume

         A3: a is DTree-yielding;

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

        then

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

         A4: t = (( Sym (o,V)) -tree p) and

         A5: ( Sym (o,V)) ==> ( roots p) by A1, DTCONSTR: 10;

        a = p by A3, A4, TREES_4: 15;

        then a is SubtreeSeq of ( Sym (o,V)) by A5, DTCONSTR:def 6;

        hence a is ArgumentSeq of ( Sym (o,V)) by A2, Def2;

      end;

      assume a is ArgumentSeq of ( Sym (o,V));

      then

      reconsider a as ArgumentSeq of ( Sym (o,V));

      reconsider p = a as FinSequence of ( TS ( DTConMSA V)) by Def1;

      p is SubtreeSeq of ( Sym (o,V)) by Def2;

      then ( Sym (o,V)) ==> ( roots p) by DTCONSTR:def 6;

      hence thesis by A1, DTCONSTR:def 1;

    end;

     Lm3:

    now

      let S, V;

      let x be set;

      set X = V, G = ( DTConMSA X);

      

       A1: ( Terminals G) = ( Union ( coprod X)) by MSAFREE: 6;

      hereby

        assume x in ( Terminals G);

        then

        consider s be object such that

         A2: s in ( dom ( coprod X)) and

         A3: x in (( coprod X) . s) by A1, CARD_5: 2;

        reconsider s as SortSymbol of S by A2, PARTFUN1:def 2;

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

        then ex a be set st a in (X . s) & x = [a, s] by A3, MSAFREE:def 2;

        hence ex s be SortSymbol of S, v be Element of (V . s) st x = [v, s];

      end;

      let s be SortSymbol of S;

      let a be Element of (V . s);

      assume x = [a, s];

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

      then

       A4: x in (( coprod X) . s) by MSAFREE:def 3;

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

      hence x in ( Terminals G) by A1, A4, CARD_5: 2;

    end;

     Lm4:

    now

      let S, A, V;

      let x be set;

      set X = (the Sorts of A (\/) V), G = ( DTConMSA X);

      

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

      

       A2: ( Terminals G) = ( Union ( coprod X)) by MSAFREE: 6;

      hereby

        assume x in ( Terminals G);

        then

        consider s be object such that

         A3: s in ( dom ( coprod X)) and

         A4: x in (( coprod X) . s) by A2, CARD_5: 2;

        reconsider s as SortSymbol of S by A3, PARTFUN1:def 2;

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

        then

        consider a be set such that

         A5: a in (X . s) and

         A6: x = [a, s] by A4, MSAFREE:def 2;

        (X . s) = ((the Sorts of A . s) \/ (V . s)) by PBOOLE:def 4;

        then a in (the Sorts of A . s) or a in (V . s) by A5, XBOOLE_0:def 3;

        hence (ex s be SortSymbol of S, a be set st a in (the Sorts of A . s) & x = [a, s]) or ex s be SortSymbol of S, v be Element of (V . s) st x = [v, s] by A6;

      end;

      let s be SortSymbol of S;

      

       A7: (X . s) = ((the Sorts of A . s) \/ (V . s)) by PBOOLE:def 4;

      hereby

        let a be set;

        assume a in (the Sorts of A . s);

        then

         A8: a in (X . s) by A7, XBOOLE_0:def 3;

        assume x = [a, s];

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

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

        hence x in ( Terminals G) by A2, A1, CARD_5: 2;

      end;

      let a be Element of (V . s);

      assume

       A9: x = [a, s];

      a in (X . s) by A7, XBOOLE_0:def 3;

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

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

      hence x in ( Terminals G) by A2, A1, CARD_5: 2;

    end;

     Lm5:

    now

      let S, V;

      set G = ( DTConMSA V);

      let x be set;

      ( NonTerminals G) = [:the carrier' of S, {the carrier of S}:] by MSAFREE: 6;

      hence x is NonTerminal of G iff x in [:the carrier' of S, {the carrier of S}:];

    end;

    scheme :: MSATERM:sch1

    TermInd { S() -> non void non empty ManySortedSign , V() -> non-empty ManySortedSet of the carrier of S() , P[ set] } :

for t be Term of S(), V() holds P[t]

      provided

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

       and

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

      set X = V(), G = ( DTConMSA X);

      

       A3: for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) & for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t] holds P[(nt -tree ts)]

      proof

        let nt be Symbol of G, ts be FinSequence of ( TS G) such that

         A4: nt ==> ( roots ts) and

         A5: for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t];

        nt in { s where s be Symbol of G : ex n be FinSequence st s ==> n } by A4;

        then

        reconsider sy = nt as NonTerminal of G by LANG1:def 3;

        reconsider p = ts as FinSequence of (S() -Terms X);

        sy in [:the carrier' of S(), {the carrier of S()}:] by Lm5;

        then

        consider o be OperSymbol of S(), x2 be Element of {the carrier of S()} such that

         A6: sy = [o, x2] by DOMAIN_1: 1;

        

         A7: x2 = the carrier of S() by TARSKI:def 1;

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

        then ts is SubtreeSeq of ( Sym (o,X)) by A4, A6, A7, DTCONSTR:def 6;

        then

        reconsider p as ArgumentSeq of ( Sym (o,V())) by Def2;

        for t be Term of S(), V() st t in ( rng p) holds P[t] by A5;

        hence thesis by A2, A6, A7;

      end;

      

       A8: for s be Symbol of G st s in ( Terminals G) holds P[( root-tree s)]

      proof

        let x be Symbol of G;

        assume x in ( Terminals G);

        then ex s be SortSymbol of S(), v be Element of (V() . s) st x = [v, s] by Lm3;

        hence thesis by A1;

      end;

      for t be DecoratedTree of the carrier of G st t in ( TS G) holds P[t] from DTCONSTR:sch 7( A8, A3);

      hence thesis;

    end;

    definition

      let S, A, V;

      mode c-Term of A,V is Term of S, (the Sorts of A (\/) V);

    end

    definition

      let S, A, V;

      let o be OperSymbol of S;

      mode ArgumentSeq of o,A,V is ArgumentSeq of ( Sym (o,(the Sorts of A (\/) V)));

    end

    scheme :: MSATERM:sch2

    CTermInd { S() -> non void non empty ManySortedSign , A() -> non-empty MSAlgebra over S() , V() -> non-empty ManySortedSet of the carrier of S() , P[ set] } :

for t be c-Term of A(), V() holds P[t]

      provided

       A1: for s be SortSymbol of S(), x be Element of (the Sorts of A() . s) holds P[( root-tree [x, s])]

       and

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

       and

       A3: for o be OperSymbol of S(), p be ArgumentSeq of o, A(), V() st for t be c-Term of A(), V() st t in ( rng p) holds P[t] holds P[(( Sym (o,(the Sorts of A() (\/) V()))) -tree p)];

      set X = (the Sorts of A() (\/) V()), G = ( DTConMSA X);

      

       A4: for nt be Symbol of G, ts be FinSequence of ( TS G) st nt ==> ( roots ts) & for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t] holds P[(nt -tree ts)]

      proof

        let nt be Symbol of G, ts be FinSequence of ( TS G) such that

         A5: nt ==> ( roots ts) and

         A6: for t be DecoratedTree of the carrier of G st t in ( rng ts) holds P[t];

        nt in { s where s be Symbol of G : ex n be FinSequence st s ==> n } by A5;

        then

        reconsider sy = nt as NonTerminal of G by LANG1:def 3;

        reconsider p = ts as FinSequence of (S() -Terms X);

        sy in [:the carrier' of S(), {the carrier of S()}:] by Lm5;

        then

        consider o be OperSymbol of S(), x2 be Element of {the carrier of S()} such that

         A7: sy = [o, x2] by DOMAIN_1: 1;

        

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

        

         A9: x2 = the carrier of S() by TARSKI:def 1;

        then ts is SubtreeSeq of ( Sym (o,X)) by A5, A7, A8, DTCONSTR:def 6;

        then

        reconsider p as ArgumentSeq of ( Sym (o,(the Sorts of A() (\/) V()))) by Def2;

        for t be c-Term of A(), V() st t in ( rng p) holds P[t] by A6;

        hence thesis by A3, A7, A9, A8;

      end;

      

       A10: for s be Symbol of G st s in ( Terminals G) holds P[( root-tree s)]

      proof

        let x be Symbol of G;

        assume x in ( Terminals G);

        then (ex s be SortSymbol of S(), a be set st a in (the Sorts of A() . s) & x = [a, s]) or ex s be SortSymbol of S(), v be Element of (V() . s) st x = [v, s] by Lm4;

        hence thesis by A1, A2;

      end;

      for t be DecoratedTree of the carrier of G st t in ( TS G) holds P[t] from DTCONSTR:sch 7( A10, A4);

      hence thesis;

    end;

    definition

      let S, V, t;

      let p be Node of t;

      :: original: .

      redefine

      func t . p -> Symbol of ( DTConMSA V) ;

      coherence

      proof

        reconsider t as Element of ( TS ( DTConMSA V));

        reconsider t as DecoratedTree of the carrier of ( DTConMSA V);

        reconsider p as Node of t;

        (t . p) = (t . p);

        hence thesis;

      end;

    end

    registration

      let S, V;

      cluster -> finite for Term of S, V;

      coherence ;

    end

     Lm6:

    now

      let G be with_terminals with_nonterminals non empty DTConstrStr;

      let s be Symbol of G;

      the carrier of G = (( Terminals G) \/ ( NonTerminals G)) by LANG1: 1;

      hence s is Terminal of G or s is NonTerminal of G by XBOOLE_0:def 3;

      ( Terminals G) misses ( NonTerminals G) by DTCONSTR: 8;

      hence not (s is Terminal of G & s is NonTerminal of G) by XBOOLE_0: 3;

    end;

    theorem :: MSATERM:2

    

     Th2: (ex s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s]) or (t . {} ) in [:the carrier' of S, {the carrier of S}:]

    proof

      set G = ( DTConMSA V);

      

       A1: the carrier of G = (( Terminals G) \/ ( NonTerminals G)) by LANG1: 1;

      reconsider e = {} as Node of t by TREES_1: 22;

      ( NonTerminals G) = [:the carrier' of S, {the carrier of S}:] by MSAFREE: 6;

      then (t . e) in ( Terminals G) or (t . e) in [:the carrier' of S, {the carrier of S}:] by A1, XBOOLE_0:def 3;

      hence thesis by Lm3;

    end;

    theorem :: MSATERM:3

    for t be c-Term of A, V holds (ex s be SortSymbol of S, x be set st x in (the Sorts of A . s) & (t . {} ) = [x, s]) or (ex s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s]) or (t . {} ) in [:the carrier' of S, {the carrier of S}:]

    proof

      let t be c-Term of A, V;

      set G = ( DTConMSA (the Sorts of A (\/) V));

      

       A1: the carrier of G = (( Terminals G) \/ ( NonTerminals G)) by LANG1: 1;

      reconsider e = {} as Node of t by TREES_1: 22;

      ( NonTerminals G) = [:the carrier' of S, {the carrier of S}:] by MSAFREE: 6;

      then (t . e) in ( Terminals G) or (t . e) in [:the carrier' of S, {the carrier of S}:] by A1, XBOOLE_0:def 3;

      hence thesis by Lm4;

    end;

    theorem :: MSATERM:4

    

     Th4: for s be SortSymbol of S, v be Element of (V . s) holds ( root-tree [v, s]) is Term of S, V

    proof

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

      reconsider vs = [v, s] as Terminal of ( DTConMSA V) by MSAFREE: 7;

      ( root-tree vs) in ( TS ( DTConMSA V));

      hence thesis;

    end;

    theorem :: MSATERM:5

    

     Th5: for s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s] holds t = ( root-tree [v, s])

    proof

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

      set G = ( DTConMSA V);

      reconsider a = [x, s] as Terminal of G by Lm3;

      reconsider t as Element of ( TS G);

      (t . {} ) = a implies t = ( root-tree a) by DTCONSTR: 9;

      hence thesis;

    end;

    theorem :: MSATERM:6

    

     Th6: for s be SortSymbol of S, x be set st x in (the Sorts of A . s) holds ( root-tree [x, s]) is c-Term of A, V

    proof

      let s be SortSymbol of S, x be set;

      

       A1: ((the Sorts of A (\/) V) . s) = ((the Sorts of A . s) \/ (V . s)) by PBOOLE:def 4;

      assume x in (the Sorts of A . s);

      then x in ((the Sorts of A (\/) V) . s) by A1, XBOOLE_0:def 3;

      then

      reconsider xs = [x, s] as Terminal of ( DTConMSA (the Sorts of A (\/) V)) by MSAFREE: 7;

      ( root-tree xs) in ( TS ( DTConMSA (the Sorts of A (\/) V)));

      hence thesis;

    end;

    theorem :: MSATERM:7

    for t be c-Term of A, V holds for s be SortSymbol of S, x be set st x in (the Sorts of A . s) & (t . {} ) = [x, s] holds t = ( root-tree [x, s])

    proof

      let t be c-Term of A, V;

      let s be SortSymbol of S, x be set;

      set G = ( DTConMSA (the Sorts of A (\/) V));

      reconsider t as Element of ( TS G);

      assume x in (the Sorts of A . s);

      then

      reconsider a = [x, s] as Terminal of G by Lm4;

      (t . {} ) = a implies t = ( root-tree a) by DTCONSTR: 9;

      hence thesis;

    end;

    theorem :: MSATERM:8

    

     Th8: for s be SortSymbol of S, v be Element of (V . s) holds ( root-tree [v, s]) is c-Term of A, V

    proof

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

      ((the Sorts of A (\/) V) . s) = ((the Sorts of A . s) \/ (V . s)) by PBOOLE:def 4;

      then v in ((the Sorts of A (\/) V) . s) by XBOOLE_0:def 3;

      then

      reconsider vs = [v, s] as Terminal of ( DTConMSA (the Sorts of A (\/) V)) by MSAFREE: 7;

      ( root-tree vs) in ( TS ( DTConMSA (the Sorts of A (\/) V)));

      hence thesis;

    end;

    theorem :: MSATERM:9

    for t be c-Term of A, V holds for s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s] holds t = ( root-tree [v, s])

    proof

      let t be c-Term of A, V;

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

      set G = ( DTConMSA (the Sorts of A (\/) V));

      reconsider a = [x, s] as Terminal of G by Lm4;

      reconsider t as Element of ( TS G);

      (t . {} ) = a implies t = ( root-tree a) by DTCONSTR: 9;

      hence thesis;

    end;

    theorem :: MSATERM:10

    

     Th10: for o be OperSymbol of S st (t . {} ) = [o, the carrier of S] holds ex a be ArgumentSeq of ( Sym (o,V)) st t = ( [o, the carrier of S] -tree a)

    proof

      let o be OperSymbol of S such that

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

      set X = V, G = ( DTConMSA X);

      reconsider t as Element of ( TS G);

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

      then

      consider p be FinSequence of ( TS G) such that

       A2: t = (( Sym (o,X)) -tree p) and

       A3: ( Sym (o,X)) ==> ( roots p) by A1, DTCONSTR: 10;

      reconsider a = p as FinSequence of (S -Terms V);

      a is SubtreeSeq of ( Sym (o,X)) by A3, DTCONSTR:def 6;

      then

      reconsider a as ArgumentSeq of ( Sym (o,V)) by Def2;

      take a;

      thus thesis by A2, MSAFREE:def 9;

    end;

    definition

      let S;

      let A be non-empty MSAlgebra over S;

      let V;

      let s be SortSymbol of S;

      let x be Element of (the Sorts of A . s);

      :: MSATERM:def3

      func x -term (A,V) -> c-Term of A, V equals ( root-tree [x, s]);

      correctness by Th6;

    end

    definition

      let S, A, V;

      let s be SortSymbol of S;

      let v be Element of (V . s);

      :: MSATERM:def4

      func v -term A -> c-Term of A, V equals ( root-tree [v, s]);

      correctness by Th8;

    end

    definition

      let S, V;

      let sy be NonTerminal of ( DTConMSA V);

      let p be ArgumentSeq of sy;

      :: original: -tree

      redefine

      func sy -tree p -> Term of S, V ;

      coherence

      proof

        sy in [:the carrier' of S, {the carrier of S}:] by Lm5;

        then

        consider o be OperSymbol of S, x2 be Element of {the carrier of S} such that

         A1: sy = [o, x2] by DOMAIN_1: 1;

        

         A2: x2 = the carrier of S by TARSKI:def 1;

        then sy = ( Sym (o,V)) by A1, MSAFREE:def 9;

        hence thesis by A1, A2, Th1;

      end;

    end

    scheme :: MSATERM:sch3

    TermInd2 { S() -> non void non empty ManySortedSign , A() -> non-empty MSAlgebra over S() , V() -> non-empty ManySortedSet of the carrier of S() , P[ set] } :

for t be c-Term of A(), V() holds P[t]

      provided

       A1: for s be SortSymbol of S(), x be Element of (the Sorts of A() . s) holds P[(x -term (A(),V()))]

       and

       A2: for s be SortSymbol of S(), v be Element of (V() . s) holds P[(v -term A())]

       and

       A3: for o be OperSymbol of S(), p be ArgumentSeq of ( Sym (o,(the Sorts of A() (\/) V()))) st for t be c-Term of A(), V() st t in ( rng p) holds P[t] holds P[(( Sym (o,(the Sorts of A() (\/) V()))) -tree p)];

       A4:

      now

        let s be SortSymbol of S(), x be Element of (the Sorts of A() . s);

        P[(x -term (A(),V()))] by A1;

        hence P[( root-tree [x, s])];

      end;

       A5:

      now

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

        P[(v -term A())] by A2;

        hence P[( root-tree [v, s])];

      end;

      

       A6: for o be OperSymbol of S(), p be ArgumentSeq of ( Sym (o,(the Sorts of A() (\/) V()))) st for t be c-Term of A(), V() st t in ( rng p) holds P[t] holds P[(( Sym (o,(the Sorts of A() (\/) V()))) -tree p)] by A3;

      for t be c-Term of A(), V() holds P[t] from CTermInd( A4, A5, A6);

      hence thesis;

    end;

    begin

    theorem :: MSATERM:11

    

     Th11: for t be Term of S, V holds ex s be SortSymbol of S st t in ( FreeSort (V,s))

    proof

      let t be Term of S, V;

      set X = V;

      set G = ( DTConMSA X);

      reconsider e = {} as Node of t by TREES_1: 22;

      per cases ;

        suppose (t . {} ) is Terminal of G;

        then

        reconsider ts = (t . {} ) as Terminal of G;

        consider s be SortSymbol of S, x be set such that

         A1: x in (X . s) and

         A2: ts = [x, s] by MSAFREE: 7;

        take s;

        t = ( root-tree [x, s]) by A2, DTCONSTR: 9;

        then t in { a where a be Element of ( TS G) : (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 A1;

        hence thesis by MSAFREE:def 10;

      end;

        suppose not (t . {} ) is Terminal of G;

        then

        reconsider nt = (t . e) as NonTerminal of G by Lm6;

        nt in [:the carrier' of S, {the carrier of S}:] by Lm5;

        then

        consider o be OperSymbol of S, x2 be Element of {the carrier of S} such that

         A3: nt = [o, x2] by DOMAIN_1: 1;

        take s = ( the_result_sort_of o);

        x2 = the carrier of S by TARSKI:def 1;

        then t in { a where a be Element of ( TS G) : (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 A3;

        hence thesis by MSAFREE:def 10;

      end;

    end;

    theorem :: MSATERM:12

    for s be SortSymbol of S holds ( FreeSort (V,s)) c= (S -Terms V);

    theorem :: MSATERM:13

    (S -Terms V) = ( Union ( FreeSort V))

    proof

      set T = (S -Terms V), X = V;

      

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

      hereby

        let x be object;

        assume x in T;

        then

        reconsider t = x as Term of S, V;

        consider s be SortSymbol of S such that

         A2: t in ( FreeSort (X,s)) by Th11;

        ( FreeSort (X,s)) = (( FreeSort X) . s) by MSAFREE:def 11;

        hence x in ( Union ( FreeSort X)) by A1, A2, CARD_5: 2;

      end;

      let x be object;

      assume x in ( Union ( FreeSort X));

      then

      consider y be object such that

       A3: y in ( dom ( FreeSort X)) and

       A4: x in (( FreeSort X) . y) by CARD_5: 2;

      reconsider y as SortSymbol of S by A3, PARTFUN1:def 2;

      x in ( FreeSort (X,y)) by A4, MSAFREE:def 11;

      hence thesis;

    end;

    

     Lm7: for x be set holds not x in x;

    definition

      let S, V, t;

      :: MSATERM:def5

      func the_sort_of t -> SortSymbol of S means

      : Def5: t in ( FreeSort (V,it ));

      existence by Th11;

      uniqueness

      proof

        set X = V;

        let s1,s2 be SortSymbol of S such that

         A1: t in ( FreeSort (X,s1)) and

         A2: t in ( FreeSort (X,s2));

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

        then

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

         A3: t = a1 and

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

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

        then

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

         A5: t = a2 and

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

        per cases by A4;

          suppose ex x be set st x in (X . s1) & a1 = ( root-tree [x, s1]);

          then

          consider x1 be set such that x1 in (X . s1) and

           A7: a1 = ( root-tree [x1, s1]);

          now

            let o be OperSymbol of S;

            assume [o, the carrier of S] = [x1, s1];

            then the carrier of S = s1 by XTUPLE_0: 1;

            hence contradiction by Lm7;

          end;

          then

          consider x2 be set such that x2 in (X . s2) and

           A8: a2 = ( root-tree [x2, s2]) by A3, A5, A6, A7, TREES_4: 3;

           [x1, s1] = [x2, s2] by A3, A5, A7, A8, TREES_4: 4;

          hence thesis by XTUPLE_0: 1;

        end;

          suppose ex o be OperSymbol of S st [o, the carrier of S] = (a1 . {} ) & ( the_result_sort_of o) = s1;

          then

          consider o1 be OperSymbol of S such that

           A9: [o1, the carrier of S] = (a1 . {} ) and

           A10: ( the_result_sort_of o1) = s1;

          now

            given x2 be set such that x2 in (X . s2) and

             A11: a2 = ( root-tree [x2, s2]);

             [o1, the carrier of S] = [x2, s2] by A3, A5, A9, A11, TREES_4: 3;

            then the carrier of S = s2 by XTUPLE_0: 1;

            hence contradiction by Lm7;

          end;

          hence thesis by A3, A5, A6, A9, A10, XTUPLE_0: 1;

        end;

      end;

    end

    theorem :: MSATERM:14

    

     Th14: for s be SortSymbol of S, v be Element of (V . s) st t = ( root-tree [v, s]) holds ( the_sort_of t) = s

    proof

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

      set X = V, G = ( DTConMSA X);

      set tst = ( the_sort_of t);

      

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

      t in ( FreeSort (V,( the_sort_of t))) by Def5;

      then

      consider a be Element of ( TS G) such that

       A2: t = a and

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

      

       A4: [x, s] in ( Terminals G) by Lm3;

      assume

       A5: t = ( root-tree [x, s]);

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

      then not (t . {} ) is NonTerminal of G by A4, Lm6;

      then

       A6: not (t . {} ) in [:the carrier' of S, {the carrier of S}:] by Lm5;

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

      then

      consider y be set such that y in (X . tst) and

       A7: a = ( root-tree [y, tst]) by A2, A3, A6, ZFMISC_1: 87;

       [y, tst] = [x, s] by A2, A5, A7, TREES_4: 4;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: MSATERM:15

    

     Th15: for t be c-Term of A, V holds for s be SortSymbol of S, x be set st x in (the Sorts of A . s) & t = ( root-tree [x, s]) holds ( the_sort_of t) = s

    proof

      let t be c-Term of A, V;

      let s be SortSymbol of S, x be set;

      assume x in (the Sorts of A . s);

      then x in ((the Sorts of A . s) \/ (V . s)) by XBOOLE_0:def 3;

      then x in ((the Sorts of A (\/) V) . s) by PBOOLE:def 4;

      hence thesis by Th14;

    end;

    theorem :: MSATERM:16

    for t be c-Term of A, V holds for s be SortSymbol of S, v be Element of (V . s) st t = ( root-tree [v, s]) holds ( the_sort_of t) = s

    proof

      let t be c-Term of A, V;

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

      x in ((the Sorts of A . s) \/ (V . s)) by XBOOLE_0:def 3;

      then x in ((the Sorts of A (\/) V) . s) by PBOOLE:def 4;

      hence thesis by Th14;

    end;

    theorem :: MSATERM:17

    

     Th17: for o be OperSymbol of S st (t . {} ) = [o, the carrier of S] holds ( the_sort_of t) = ( the_result_sort_of o)

    proof

      let o be OperSymbol of S;

      set X = V, G = ( DTConMSA X);

      set tst = ( the_sort_of t);

      

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

      t in ( FreeSort (V,( the_sort_of t))) by Def5;

      then

      consider a be Element of ( TS G) such that

       A2: t = a and

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

      assume

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

      per cases by A3;

        suppose ex x be set st x in (X . tst) & a = ( root-tree [x, tst]);

        then

        consider x be set such that x in (X . tst) and

         A5: a = ( root-tree [x, tst]);

         [o, the carrier of S] = [x, tst] by A2, A4, A5, TREES_4: 3;

        then the carrier of S = tst by XTUPLE_0: 1;

        hence thesis by Lm7;

      end;

        suppose ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = tst;

        hence thesis by A2, A4, XTUPLE_0: 1;

      end;

    end;

    theorem :: MSATERM:18

    for A be non-empty MSAlgebra over S holds for s be SortSymbol of S, x be Element of (the Sorts of A . s) holds ( the_sort_of (x -term (A,V))) = s by Th15;

    theorem :: MSATERM:19

    

     Th19: for s be SortSymbol of S, v be Element of (V . s) holds ( the_sort_of (v -term A)) = s

    proof

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

      ((the Sorts of A (\/) V) . s) = ((the Sorts of A . s) \/ (V . s)) by PBOOLE:def 4;

      then v in ((the Sorts of A (\/) V) . s) by XBOOLE_0:def 3;

      hence thesis by Th14;

    end;

    theorem :: MSATERM:20

    

     Th20: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) holds ( the_sort_of (( Sym (o,V)) -tree p) qua Term of S, V) = ( the_result_sort_of o)

    proof

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

      

       A1: (( [o, the carrier of S] -tree p) . {} ) = [o, the carrier of S] by TREES_4:def 4;

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

      hence thesis by A1, Th17;

    end;

    begin

    theorem :: MSATERM:21

    

     Th21: for o be OperSymbol of S, a be FinSequence of (S -Terms V) holds a is ArgumentSeq of ( Sym (o,V)) iff ( Sym (o,V)) ==> ( roots a)

    proof

      let o be OperSymbol of S, a be FinSequence of (S -Terms V);

      a is SubtreeSeq of ( Sym (o,V)) iff ( Sym (o,V)) ==> ( roots a) by DTCONSTR:def 6;

      hence thesis by Def2;

    end;

    

     Lm8: for o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V)) holds ( len a) = ( len ( the_arity_of o)) & ( dom a) = ( dom ( the_arity_of o)) & for i be Nat st i in ( dom a) holds ex t be Term of S, V st t = (a . i) & t = (a qua FinSequence of (S -Terms V) qua non empty set /. i) & ( the_sort_of t) = (( the_arity_of o) . i) & ( the_sort_of t) = (( the_arity_of o) /. i)

    proof

      let o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V));

      set X = V;

      reconsider p = a as FinSequence of ( TS ( DTConMSA X)) by Def1;

      ( Sym (o,X)) ==> ( roots a) by Th21;

      then

       A1: p in (((( FreeSort X) # ) * the Arity of S) . o) by MSAFREE: 10;

      then

       A2: ( dom p) = ( dom ( the_arity_of o)) by MSAFREE: 9;

      hence ( len a) = ( len ( the_arity_of o)) & ( dom a) = ( dom ( the_arity_of o)) by FINSEQ_3: 29;

      let i be Nat;

      reconsider t = (a qua FinSequence of (S -Terms V) qua non empty set /. i) as Term of S, V;

      assume

       A3: i in ( dom a);

      then

       A4: i <= ( len a) by FINSEQ_3: 25;

      take t;

      1 <= i by A3, FINSEQ_3: 25;

      hence t = (a . i) by A4, FINSEQ_4: 15;

      then t in ( FreeSort (X,(( the_arity_of o) /. i))) by A1, A3, MSAFREE: 9;

      then ( the_sort_of t) = (( the_arity_of o) /. i) by Def5;

      hence thesis by A2, A3, PARTFUN1:def 6;

    end;

    theorem :: MSATERM:22

    

     Th22: for o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V)) holds ( len a) = ( len ( the_arity_of o)) & ( dom a) = ( dom ( the_arity_of o)) & for i be Nat st i in ( dom a) holds (a . i) is Term of S, V

    proof

      let o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V));

      thus ( len a) = ( len ( the_arity_of o)) & ( dom a) = ( dom ( the_arity_of o)) by Lm8;

      let i be Nat;

      assume i in ( dom a);

      then ex t be Term of S, V st t = (a . i) & t = (a qua FinSequence of (S -Terms V) qua non empty set /. i) & ( the_sort_of t) = (( the_arity_of o) . i) & ( the_sort_of t) = (( the_arity_of o) /. i) by Lm8;

      hence thesis;

    end;

    theorem :: MSATERM:23

    for o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V)) holds for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds t = (a qua FinSequence of (S -Terms V) qua non empty set /. i) & ( the_sort_of t) = (( the_arity_of o) . i) & ( the_sort_of t) = (( the_arity_of o) /. i)

    proof

      let o be OperSymbol of S, a be ArgumentSeq of ( Sym (o,V));

      let i be Nat;

      assume i in ( dom a);

      then ex t be Term of S, V st t = (a . i) & t = (a qua FinSequence of (S -Terms V) qua non empty set /. i) & ( the_sort_of t) = (( the_arity_of o) . i) & ( the_sort_of t) = (( the_arity_of o) /. i) by Lm8;

      hence thesis;

    end;

    theorem :: MSATERM:24

    

     Th24: for o be OperSymbol of S, a be FinSequence st (( len a) = ( len ( the_arity_of o)) or ( dom a) = ( dom ( the_arity_of o))) & ((for i be Nat st i in ( dom a) holds ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i)) or for i be Nat st i in ( dom a) holds ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) /. i)) holds a is ArgumentSeq of ( Sym (o,V))

    proof

      set X = V;

      let o be OperSymbol of S, a be FinSequence such that

       A1: ( len a) = ( len ( the_arity_of o)) or ( dom a) = ( dom ( the_arity_of o)) and

       A2: (for i be Nat st i in ( dom a) holds ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i)) or for i be Nat st i in ( dom a) holds ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) /. i);

      ( rng a) c= ( TS ( DTConMSA X))

      proof

        let x be object;

        assume x in ( rng a);

        then

        consider i be object such that

         A3: i in ( dom a) and

         A4: x = (a . i) by FUNCT_1:def 3;

        reconsider i as Nat by A3;

        (ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i)) or ex t be Term of S, V st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) /. i) by A2, A3;

        hence thesis by A4;

      end;

      then

      reconsider p = a as FinSequence of ( TS ( DTConMSA X)) by FINSEQ_1:def 4;

      

       A5: ( dom a) = ( dom ( the_arity_of o)) by A1, FINSEQ_3: 29;

      now

        let n be Nat;

        assume

         A6: n in ( dom p);

        thus (p . n) in ( FreeSort (X,(( the_arity_of o) /. n)))

        proof

          per cases by A2, A6;

            suppose ex t be Term of S, V st t = (a . n) & ( the_sort_of t) = (( the_arity_of o) . n);

            then

            consider t be Term of S, V such that

             A7: t = (a . n) and

             A8: ( the_sort_of t) = (( the_arity_of o) . n);

            ( the_sort_of t) = (( the_arity_of o) /. n) by A5, A6, A8, PARTFUN1:def 6;

            hence thesis by A7, Def5;

          end;

            suppose ex t be Term of S, V st t = (a . n) & ( the_sort_of t) = (( the_arity_of o) /. n);

            hence thesis by Def5;

          end;

        end;

      end;

      then p in (((( FreeSort X) # ) * the Arity of S) . o) by A5, MSAFREE: 9;

      then

       A9: ( Sym (o,X)) ==> ( roots p) by MSAFREE: 10;

      (S -Terms V) = ( TS ( DTConMSA X));

      hence thesis by A9, Th21;

    end;

    theorem :: MSATERM:25

    for o be OperSymbol of S, a be FinSequence of (S -Terms V) st (( len a) = ( len ( the_arity_of o)) or ( dom a) = ( dom ( the_arity_of o))) & ((for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) . i)) or for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) /. i)) holds a is ArgumentSeq of ( Sym (o,V))

    proof

      let o be OperSymbol of S, a be FinSequence of (S -Terms V) such that

       A1: ( len a) = ( len ( the_arity_of o)) or ( dom a) = ( dom ( the_arity_of o)) and

       A2: (for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) . i)) or for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) /. i);

       A3:

      now

        let i be Nat;

        assume i in ( dom a);

        then

         A4: (a . i) in ( rng a) by FUNCT_1:def 3;

        ( rng a) c= (S -Terms V) by FINSEQ_1:def 4;

        hence (a . i) in (S -Terms V) by A4;

      end;

      now

        per cases by A2;

          case

           A5: for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) . i);

          let i be Nat;

          assume

           A6: i in ( dom a);

          then

          reconsider t = (a . i) as Term of S, V by A3;

          take t;

          thus t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i) by A5, A6;

        end;

          case

           A7: for i be Nat st i in ( dom a) holds for t be Term of S, V st t = (a . i) holds ( the_sort_of t) = (( the_arity_of o) /. i);

          let i be Nat;

          assume

           A8: i in ( dom a);

          then

          reconsider t = (a . i) as Term of S, V by A3;

          take t;

          thus t = (a . i) & ( the_sort_of t) = (( the_arity_of o) /. i) by A7, A8;

        end;

      end;

      hence thesis by A1, Th24;

    end;

    theorem :: MSATERM:26

    

     Th26: for S be non void non empty ManySortedSign, V1,V2 be non-empty ManySortedSet of the carrier of S st V1 c= V2 holds for t be Term of S, V1 holds t is Term of S, V2

    proof

      let S be non void non empty ManySortedSign;

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

       A1: for s be object st s in the carrier of S holds (V1 . s) c= (V2 . s);

      defpred P[ set] means $1 is Term of S, V2;

      

       A2: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V1)) st for t be Term of S, V1 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,V1));

        assume

         A3: for t be Term of S, V1 st t in ( rng p) holds t is Term of S, V2;

        ( rng p) c= (S -Terms V2)

        proof

          let x be object;

          assume

           A4: x in ( rng p);

          ( rng p) c= (S -Terms V1) by FINSEQ_1:def 4;

          then

          reconsider x as Term of S, V1 by A4;

          x is Term of S, V2 by A3, A4;

          hence thesis;

        end;

        then

        reconsider q = p as FinSequence of (S -Terms V2) by FINSEQ_1:def 4;

         A5:

        now

          let i be Nat;

          assume

           A6: i in ( dom q);

          then

          consider t be Term of S, V1 such that

           A7: t = (q . i) and t = (p qua FinSequence of (S -Terms V1) qua non empty set /. i) and

           A8: ( the_sort_of t) = (( the_arity_of o) . i) and ( the_sort_of t) = (( the_arity_of o) /. i) by Lm8;

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

          then

          reconsider T = t as Term of S, V2 by A3;

          take T;

          thus T = (q . i) by A7;

          thus ( the_sort_of T) = (( the_arity_of o) . i)

          proof

            per cases by Th2;

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

              then

              consider s be SortSymbol of S, v be Element of (V1 . s) such that

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

              

               A10: t = ( root-tree [v, s]) by A9, Th5;

              (V1 . s) c= (V2 . s) by A1;

              then v in (V2 . s);

              

              hence ( the_sort_of T) = s by A10, Th14

              .= (( the_arity_of o) . i) by A8, A10, Th14;

            end;

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

              then

              consider o9 be OperSymbol of S, x2 be Element of {the carrier of S} such that

               A11: (t . {} ) = [o9, x2] by DOMAIN_1: 1;

              

               A12: x2 = the carrier of S by TARSKI:def 1;

              

              hence ( the_sort_of T) = ( the_result_sort_of o9) by A11, Th17

              .= (( the_arity_of o) . i) by A8, A11, A12, Th17;

            end;

          end;

        end;

        ( len p) = ( len ( the_arity_of o)) by Lm8;

        then q is ArgumentSeq of ( Sym (o,V2)) by A5, Th24;

        hence thesis by Th1;

      end;

      

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

      proof

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

        (V1 . s) c= (V2 . s) by A1;

        then v in (V2 . s);

        hence thesis by Th4;

      end;

      for t be Term of S, V1 holds P[t] from TermInd( A13, A2);

      hence thesis;

    end;

    theorem :: MSATERM:27

    for S be non void non empty ManySortedSign, A be MSAlgebra over S, V be non-empty ManySortedSet of the carrier of S, t be Term of S, V holds t is c-Term of A, V by Th26, PBOOLE: 14;

    begin

    definition

      let S be non void non empty ManySortedSign;

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

      :: MSATERM:def6

      mode CompoundTerm of S,V -> Term of S, V means (it . {} ) in [:the carrier' of S, {the carrier of S}:];

      existence

      proof

        set s = the OperSymbol of S;

        reconsider nt = ( Sym (s,V)) as NonTerminal of ( DTConMSA V);

        set p = the SubtreeSeq of nt;

        reconsider t = (nt -tree p) as Term of S, V;

        take t;

        nt = [s, the carrier of S] by MSAFREE:def 9;

        then

         A1: [s, the carrier of S] = (t . {} ) by TREES_4:def 4;

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

        hence thesis by A1, ZFMISC_1: 87;

      end;

    end

    definition

      let S be non void non empty ManySortedSign;

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

      :: MSATERM:def7

      mode SetWithCompoundTerm of S,V -> non empty Subset of (S -Terms V) means ex t be CompoundTerm of S, V st t in it ;

      existence

      proof

        set t = the CompoundTerm of S, V;

        reconsider X = {t} as non empty Subset of (S -Terms V) by ZFMISC_1: 31;

        take X, t;

        thus thesis by TARSKI:def 1;

      end;

    end

    theorem :: MSATERM:28

     not t is root implies t is CompoundTerm of S, V

    proof

      assume

       A1: not t is root;

      per cases by Th2;

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

        then

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

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

        t = ( root-tree [x, s]) by A2, Th5;

        hence thesis by A1;

      end;

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

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

      end;

    end;

    

     Lm9: for n be Element of NAT , p be FinSequence holds n < ( len p) implies (n + 1) in ( dom p) & (p . (n + 1)) in ( rng p)

    proof

      let n be Element of NAT , p be FinSequence;

      n >= 0 by NAT_1: 2;

      then

       A1: (n + 1) >= ( 0 + 1) by XREAL_1: 7;

      assume n < ( len p);

      then (n + 1) <= ( len p) by NAT_1: 13;

      then (n + 1) in ( dom p) by A1, FINSEQ_3: 25;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: MSATERM:29

    

     Th29: for p be Node of t holds (t | p) is Term of S, V

    proof

      defpred P[ set] means for q be Node of t st q = $1 holds (t | q) is Term of S, V;

      

       A1: for p be Node of t, n be Nat st P[p] & (p ^ <*n*>) in ( dom t) holds P[(p ^ <*n*>)]

      proof

        let p be Node of t, n be Nat;

        assume that

         A2: for q be Node of t st q = p holds (t | q) is Term of S, V and

         A3: (p ^ <*n*>) in ( dom t);

        reconsider u = (t | p) as Term of S, V by A2;

        

         A4: ( dom u) = (( dom t) | p) by TREES_2:def 10;

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

        

         A5: <*nn*> in (( dom t) | p) by A3, TREES_1:def 6;

         A6:

        now

          given s be SortSymbol of S, x be Element of (V . s) such that

           A7: (u . {} ) = [x, s];

          u = ( root-tree [x, s]) by A7, Th5;

          then <*n*> in { {} } by A5, A4, TREES_1: 29, TREES_4: 3;

          hence contradiction by TARSKI:def 1;

        end;

        (ex s be SortSymbol of S, v be Element of (V . s) st (u . {} ) = [v, s]) or (u . {} ) in [:the carrier' of S, {the carrier of S}:] by Th2;

        then

        consider o be OperSymbol of S, x2 be Element of {the carrier of S} such that

         A8: (u . {} ) = [o, x2] by A6, DOMAIN_1: 1;

        x2 = the carrier of S by TARSKI:def 1;

        then

        consider a be ArgumentSeq of ( Sym (o,V)) such that

         A9: u = ( [o, the carrier of S] -tree a) by A8, Th10;

        consider i be Nat, T be DecoratedTree, r be Node of T such that

         A10: i < ( len a) and T = (a . (i + 1)) and

         A11: <*n*> = ( <*i*> ^ r) by A5, A4, A9, TREES_4: 11;

        

         A12: n = ( <*n*> . 1) by FINSEQ_1: 40

        .= i by A11, FINSEQ_1: 41;

        then

         A13: (u | <*nn*>) = (a . (nn + 1)) by A9, A10, TREES_4:def 4;

        let q be Node of t;

        (nn + 1) in ( dom a) by A10, A12, Lm9;

        then ex t be Term of S, V st t = (u | <*nn*>) & t = (a qua FinSequence of (S -Terms V) qua non empty set /. (n + 1)) & ( the_sort_of t) = (( the_arity_of o) . (n + 1)) & ( the_sort_of t) = (( the_arity_of o) /. (n + 1)) by A13, Lm8;

        hence thesis by TREES_9: 3;

      end;

      

       A14: P[ {} ] by TREES_9: 1;

      for p be Node of t holds P[p] from TREES_2:sch 1( A14, A1);

      hence thesis;

    end;

    definition

      let S be non void non empty ManySortedSign;

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

      let t be Term of S, V;

      let p be Node of t;

      :: original: |

      redefine

      func t | p -> Term of S, V ;

      coherence by Th29;

    end

    begin

    definition

      let S be non void non empty ManySortedSign;

      let A be MSAlgebra over S;

      :: MSATERM:def8

      mode Variables of A -> non-empty ManySortedSet of the carrier of S means

      : Def8: it misses the Sorts of A;

      existence

      proof

        deffunc F( object) = {(the Sorts of A . $1)};

        consider V be ManySortedSet of the carrier of S such that

         A1: for s be object st s in the carrier of S holds (V . s) = F(s) from PBOOLE:sch 4;

        V is non-empty

        proof

          let s be object;

          assume s in the carrier of S;

          then (V . s) = {(the Sorts of A . s)} by A1;

          hence thesis;

        end;

        then

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

        take V;

        let s be object;

        assume s in the carrier of S;

        then

         A2: (V . s) = {(the Sorts of A . s)} by A1;

        now

          let x be object;

          assume x in (V . s);

          then

           A: x = (the Sorts of A . s) by A2, TARSKI:def 1;

          then

          reconsider xx = x as set;

           not xx in xx;

          hence not x in (the Sorts of A . s) by A;

        end;

        hence thesis by XBOOLE_0: 3;

      end;

    end

    theorem :: MSATERM:30

    

     Th30: for V be Variables of A holds for s be SortSymbol of S, x be set st x in (the Sorts of A . s) holds for v be Element of (V . s) holds x <> v

    proof

      let V be Variables of A;

      let s be SortSymbol of S, x be set such that

       A1: x in (the Sorts of A . s);

      let v be Element of (V . s);

      V misses the Sorts of A by Def8;

      then (V . s) misses (the Sorts of A . s);

      hence thesis by A1, XBOOLE_0: 3;

    end;

    definition

      let S be non void non empty ManySortedSign;

      let A be non-empty MSAlgebra over S;

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

      let t be c-Term of A, V;

      let f be ManySortedFunction of V, the Sorts of A;

      let vt be finite DecoratedTree;

      :: MSATERM:def9

      pred vt is_an_evaluation_of t,f means ( dom vt) = ( dom t) & for p be Node of vt holds (for s be SortSymbol of S, v be Element of (V . s) st (t . p) = [v, s] holds (vt . p) = ((f . s) . v)) & (for s be SortSymbol of S, x be Element of (the Sorts of A . s) st (t . p) = [x, s] holds (vt . p) = x) & for o be OperSymbol of S st (t . p) = [o, the carrier of S] holds (vt . p) = (( Den (o,A)) . ( succ (vt,p)));

    end

    reserve S for non void non empty ManySortedSign,

A for non-empty MSAlgebra over S,

V for Variables of A,

t for c-Term of A, V,

f for ManySortedFunction of V, the Sorts of A;

    theorem :: MSATERM:31

    

     Th31: for s be SortSymbol of S, x be Element of (the Sorts of A . s) st t = ( root-tree [x, s]) holds ( root-tree x) is_an_evaluation_of (t,f)

    proof

      let s be SortSymbol of S, x be Element of (the Sorts of A . s) such that

       A1: t = ( root-tree [x, s]);

      

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

      set vt = ( root-tree x);

      

       A3: ( dom vt) = ( elementary_tree 0 ) by TREES_4: 3;

      hence ( dom vt) = ( dom t) by A1, TREES_4: 3;

      let p be Node of vt;

      reconsider e = p as empty FinSequence of NAT by A3, TARSKI:def 1, TREES_1: 29;

      hereby

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

        assume (t . p) = [v, s1];

        

        then

         A4: [v, s1] = (t . e)

        .= [x, s] by A1, TREES_4: 3;

        then

         A5: x = v by XTUPLE_0: 1;

        s = s1 by A4, XTUPLE_0: 1;

        hence (vt . p) = ((f . s1) . v) by A5, Th30;

      end;

      

       A6: (vt . {} ) = x by TREES_4: 3;

      hereby

        let s1 be SortSymbol of S, x1 be Element of (the Sorts of A . s1);

        assume (t . p) = [x1, s1];

        then [x1, s1] = (t . e);

        hence (vt . p) = x1 by A2, A6, XTUPLE_0: 1;

      end;

      let o be OperSymbol of S;

      assume (t . p) = [o, the carrier of S];

      

      then the carrier of S = ((t . e) `2 )

      .= s by A2;

      hence (vt . p) = (( Den (o,A)) . ( succ (vt,p))) by Lm7;

    end;

    theorem :: MSATERM:32

    

     Th32: for s be SortSymbol of S, v be Element of (V . s) st t = ( root-tree [v, s]) holds ( root-tree ((f . s) . v)) is_an_evaluation_of (t,f)

    proof

      let s be SortSymbol of S, x be Element of (V . s) such that

       A1: t = ( root-tree [x, s]);

      set vt = ( root-tree ((f . s) . x));

      

       A2: ( dom vt) = ( elementary_tree 0 ) by TREES_4: 3;

      hence ( dom vt) = ( dom t) by A1, TREES_4: 3;

      let p be Node of vt;

      reconsider e = p as empty FinSequence of NAT by A2, TARSKI:def 1, TREES_1: 29;

      

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

      hereby

        let s1 be SortSymbol of S, x1 be Element of (V . s1);

        

         A4: e = p;

        assume (t . p) = [x1, s1];

        then

         A5: [x1, s1] = (t . e);

        then

         A6: s = s1 by A3, XTUPLE_0: 1;

        x = x1 by A3, A5, XTUPLE_0: 1;

        hence (vt . p) = ((f . s1) . x1) by A6, A4, TREES_4: 3;

      end;

      hereby

        let s1 be SortSymbol of S, v be Element of (the Sorts of A . s1);

        assume (t . p) = [v, s1];

        

        then

         A7: [v, s1] = (t . e)

        .= [x, s] by A1, TREES_4: 3;

        then

         A8: x = v by XTUPLE_0: 1;

        s = s1 by A7, XTUPLE_0: 1;

        hence (vt . p) = v by A8, Th30;

      end;

      let o be OperSymbol of S;

      assume (t . p) = [o, the carrier of S];

      

      then the carrier of S = ((t . e) `2 )

      .= s by A3;

      hence (vt . p) = (( Den (o,A)) . ( succ (vt,p))) by Lm7;

    end;

    theorem :: MSATERM:33

    

     Th33: for o be OperSymbol of S, p be ArgumentSeq of o, A, V holds for q be DTree-yielding FinSequence st ( len q) = ( len p) & for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q . i) & vt is_an_evaluation_of (t,f) holds ex vt be finite DecoratedTree st vt = ((( Den (o,A)) . ( roots q)) -tree q) & vt is_an_evaluation_of ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V,f)

    proof

      let o be OperSymbol of S, p be ArgumentSeq of o, A, V;

      

       A1: ( Sym (o,(the Sorts of A (\/) V))) = [o, the carrier of S] by MSAFREE:def 9;

      

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

      

       A3: ( tree ( doms p)) = ( dom ( [o, the carrier of S] -tree p)) by TREES_4: 10;

      

       A4: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      let q be DTree-yielding FinSequence such that

       A5: ( len q) = ( len p) and

       A6: for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q . i) & vt is_an_evaluation_of (t,f);

      

       A7: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

      now

        let x be object;

        

         A8: ( rng p) c= (S -Terms (the Sorts of A (\/) V)) by FINSEQ_1:def 4;

        assume

         A9: x in ( dom ( doms q));

        then

         A10: x in ( dom q) by TREES_3: 37;

        then (p . x) in ( rng p) by A5, A4, A7, FUNCT_1:def 3;

        then

        reconsider t = (p . x) as c-Term of A, V by A8;

        reconsider i = x as Nat by A9;

        consider vt be finite DecoratedTree such that

         A11: vt = (q . i) and vt is_an_evaluation_of (t,f) by A5, A6, A4, A7, A10;

        (( doms q) . x) = ( dom vt) by A10, A11, FUNCT_6: 22;

        hence (( doms q) . x) is finite Tree;

      end;

      then

      reconsider r = ( doms q) as FinTree-yielding FinSequence by TREES_3: 23;

       A12:

      now

        let i be Nat;

        

         A13: ( rng p) c= (S -Terms (the Sorts of A (\/) V)) by FINSEQ_1:def 4;

        assume

         A14: i in ( dom p);

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

        then

        reconsider t = (p . i) as c-Term of A, V by A13;

        consider vt be finite DecoratedTree such that

         A15: vt = (q . i) and

         A16: vt is_an_evaluation_of (t,f) by A6, A14;

        

        thus (r . i) = ( dom vt) by A5, A4, A7, A14, A15, FUNCT_6: 22

        .= ( dom t) by A16

        .= (( doms p) . i) by A14, FUNCT_6: 22;

      end;

      set vt = ((( Den (o,A)) . ( roots q)) -tree q);

      

       A17: ( len ( doms q)) = ( len q) by TREES_3: 38;

      

       A18: ( dom vt) = ( tree r) by TREES_4: 10;

      then

      reconsider vt as finite DecoratedTree by FINSET_1: 10;

      take vt;

      thus vt = ((( Den (o,A)) . ( roots q)) -tree q);

      ( dom ( doms q)) = ( dom q) by TREES_3: 37;

      hence ( dom vt) = ( dom (( Sym (o,(the Sorts of A (\/) V))) -tree p)) by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1: 13;

      let n be Node of vt;

      

       A19: (( [o, the carrier of S] -tree p) . {} ) = [o, the carrier of S] by TREES_4:def 4;

      hereby

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

        assume

         A20: ((( Sym (o,(the Sorts of A (\/) V))) -tree p) . n) = [v, s];

        now

          assume n = {} ;

          then s = the carrier of S by A1, A19, A20, XTUPLE_0: 1;

          hence contradiction by Lm7;

        end;

        then

        consider w be FinSequence of NAT , i be Element of NAT such that

         A21: n = ( <*i*> ^ w) by FINSEQ_2: 130;

        

         A22: w in (( doms q) . (i + 1)) by A18, A21, TREES_3: 48;

        

         A23: i < ( len p) by A5, A18, A17, A21, TREES_3: 48;

        then

        reconsider t = (p . (i + 1)) as c-Term of A, V by Lm2;

        consider e be finite DecoratedTree such that

         A24: e = (q . (i + 1)) and

         A25: e is_an_evaluation_of (t,f) by A6, A23, Lm9;

        (i + 1) in ( dom p) by A23, Lm9;

        then

        reconsider w as Node of e by A5, A4, A7, A22, A24, FUNCT_6: 22;

        ( dom e) = ( dom t) by A25;

        then

         A26: (t . w) = [v, s] by A20, A21, A23, TREES_4: 12;

        

        thus (vt . n) = (e . w) by A5, A21, A23, A24, TREES_4: 12

        .= ((f . s) . v) by A25, A26;

      end;

      hereby

        let s be SortSymbol of S, x be Element of (the Sorts of A . s);

        assume

         A27: ((( Sym (o,(the Sorts of A (\/) V))) -tree p) . n) = [x, s];

        now

          assume n = {} ;

          then s = the carrier of S by A1, A19, A27, XTUPLE_0: 1;

          hence contradiction by Lm7;

        end;

        then

        consider w be FinSequence of NAT , i be Element of NAT such that

         A28: n = ( <*i*> ^ w) by FINSEQ_2: 130;

        

         A29: w in (( doms q) . (i + 1)) by A18, A28, TREES_3: 48;

        

         A30: i < ( len p) by A5, A18, A17, A28, TREES_3: 48;

        then

        reconsider t = (p . (i + 1)) as c-Term of A, V by Lm2;

        consider e be finite DecoratedTree such that

         A31: e = (q . (i + 1)) and

         A32: e is_an_evaluation_of (t,f) by A6, A30, Lm9;

        (i + 1) in ( dom p) by A30, Lm9;

        then

        reconsider w as Node of e by A5, A4, A7, A29, A31, FUNCT_6: 22;

        ( dom e) = ( dom t) by A32;

        then

         A33: (t . w) = [x, s] by A27, A28, A30, TREES_4: 12;

        

        thus (vt . n) = (e . w) by A5, A28, A30, A31, TREES_4: 12

        .= x by A32, A33;

      end;

      let o1 be OperSymbol of S;

      assume

       A34: ((( Sym (o,(the Sorts of A (\/) V))) -tree p) . n) = [o1, the carrier of S];

      per cases ;

        suppose

         A35: n = {} ;

        

        then ((( Sym (o,(the Sorts of A (\/) V))) -tree p) . n) = ( Sym (o,(the Sorts of A (\/) V))) by TREES_4:def 4

        .= [o, the carrier of S] by MSAFREE:def 9;

        then

         A36: o = o1 by A34, XTUPLE_0: 1;

        ( succ (vt,n)) = ( roots q) by A35, TREES_9: 30;

        hence thesis by A35, A36, TREES_4:def 4;

      end;

        suppose n <> {} ;

        then

        consider w be FinSequence of NAT , i be Element of NAT such that

         A37: n = ( <*i*> ^ w) by FINSEQ_2: 130;

        reconsider ii = <*i*> as Node of vt by A37, TREES_1: 21;

        

         A38: w in (( doms q) . (i + 1)) by A18, A37, TREES_3: 48;

        

         A39: i < ( len p) by A5, A18, A17, A37, TREES_3: 48;

        then

        reconsider t = (p . (i + 1)) as c-Term of A, V by Lm2;

        consider e be finite DecoratedTree such that

         A40: e = (q . (i + 1)) and

         A41: e is_an_evaluation_of (t,f) by A6, A39, Lm9;

        

         A42: e = (vt | ii) by A5, A39, A40, TREES_4:def 4;

        (i + 1) in ( dom p) by A39, Lm9;

        then

        reconsider w as Node of e by A5, A4, A7, A38, A40, FUNCT_6: 22;

        ( dom e) = ( dom t) by A41;

        then (t . w) = [o1, the carrier of S] by A34, A37, A39, TREES_4: 12;

        

        then (e . w) = (( Den (o1,A)) . ( succ (e,w))) by A41

        .= (( Den (o1,A)) . ( succ (vt,n))) by A37, A42, TREES_9: 31;

        hence thesis by A5, A37, A39, A40, TREES_4: 12;

      end;

    end;

    theorem :: MSATERM:34

    

     Th34: for t be c-Term of A, V, e be finite DecoratedTree st e is_an_evaluation_of (t,f) holds for p be Node of t, n be Node of e st n = p holds (e | n) is_an_evaluation_of ((t | p),f)

    proof

      let t be c-Term of A, V, e be finite DecoratedTree such that

       A1: ( dom e) = ( dom t) and

       A2: for p be Node of e holds (for s be SortSymbol of S, v be Element of (V . s) st (t . p) = [v, s] holds (e . p) = ((f . s) . v)) & (for s be SortSymbol of S, x be Element of (the Sorts of A . s) st (t . p) = [x, s] holds (e . p) = x) & for o be OperSymbol of S st (t . p) = [o, the carrier of S] holds (e . p) = (( Den (o,A)) . ( succ (e,p)));

      let p be Node of t, n be Node of e;

      set vt = (e | n), tp = (t | p);

      

       A3: ( dom vt) = (( dom e) | n) by TREES_2:def 10;

      assume

       A4: n = p;

      hence ( dom vt) = ( dom tp) by A1, A3, TREES_2:def 10;

      let q be Node of vt;

      reconsider nq = (n ^ q) as Node of e by A3, TREES_1:def 6;

      reconsider pq = (p ^ q) as Node of t by A1, A4, A3, TREES_1:def 6;

      hereby

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

        assume (tp . q) = [v, s];

        then (t . pq) = [v, s] by A1, A4, A3, TREES_2:def 10;

        then (e . nq) = ((f . s) . v) by A2, A4;

        hence (vt . q) = ((f . s) . v) by A3, TREES_2:def 10;

      end;

      hereby

        let s be SortSymbol of S, x be Element of (the Sorts of A . s);

        assume (tp . q) = [x, s];

        then (t . pq) = [x, s] by A1, A4, A3, TREES_2:def 10;

        then (e . nq) = x by A2, A4;

        hence (vt . q) = x by A3, TREES_2:def 10;

      end;

      let o be OperSymbol of S;

      assume (tp . q) = [o, the carrier of S];

      then (t . pq) = [o, the carrier of S] by A1, A4, A3, TREES_2:def 10;

      then (e . nq) = (( Den (o,A)) . ( succ (e,nq))) by A2, A4;

      then (vt . q) = (( Den (o,A)) . ( succ (e,(n ^ q)))) by A3, TREES_2:def 10;

      hence thesis by TREES_9: 31;

    end;

    theorem :: MSATERM:35

    

     Th35: for o be OperSymbol of S, p be ArgumentSeq of o, A, V holds for vt be finite DecoratedTree st vt is_an_evaluation_of ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V,f) holds ex q be DTree-yielding FinSequence st ( len q) = ( len p) & vt = ((( Den (o,A)) . ( roots q)) -tree q) & for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q . i) & vt is_an_evaluation_of (t,f)

    proof

      let o be OperSymbol of S, p be ArgumentSeq of o, A, V;

      let vt be finite DecoratedTree;

      assume

       A1: vt is_an_evaluation_of ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V,f);

      reconsider r = {} as empty Element of ( dom vt) by TREES_1: 22;

      consider x be set, q be DTree-yielding FinSequence such that

       A2: vt = (x -tree q) by TREES_9: 8;

      

       A3: ( dom vt) = ( tree ( doms q)) by A2, TREES_4: 10;

      take q;

      

       A4: ( len ( doms q)) = ( len q) by TREES_3: 38;

      

       A5: ( Sym (o,(the Sorts of A (\/) V))) = [o, the carrier of S] by MSAFREE:def 9;

      then

       A6: ( dom vt) = ( dom ( [o, the carrier of S] -tree p)) by A1;

      then ( dom vt) = ( tree ( doms p)) by TREES_4: 10;

      then

       A7: ( doms q) = ( doms p) by A3, TREES_3: 50;

      hence ( len q) = ( len p) by A4, TREES_3: 38;

      (( [o, the carrier of S] -tree p) . r) = [o, the carrier of S] by TREES_4:def 4;

      

      then (vt . r) = (( Den (o,A)) . ( succ (vt,r))) by A5, A1

      .= (( Den (o,A)) . ( roots q)) by A2, TREES_9: 30;

      hence vt = ((( Den (o,A)) . ( roots q)) -tree q) by A2, TREES_4:def 4;

      let i be Nat, t be c-Term of A, V;

      assume that

       A8: i in ( dom p) and

       A9: t = (p . i);

      reconsider u = {} as Node of t by TREES_1: 22;

      consider k be Element of NAT such that

       A10: i = (k + 1) and

       A11: k < ( len p) by A8, Lm1;

      ( <*k*> ^ u) = <*k*> by FINSEQ_1: 34;

      then

      reconsider r = <*k*> as Node of vt by A6, A9, A10, A11, TREES_4: 11;

      take e = (vt | r);

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

      hence e = (q . i) by A2, A7, A4, A10, A11, TREES_4:def 4;

      reconsider r1 = r as Node of ( [o, the carrier of S] -tree p) by A5, A1;

      t = (( [o, the carrier of S] -tree p) | r1) by A9, A10, A11, TREES_4:def 4;

      hence thesis by A5, A1, Th34;

    end;

    theorem :: MSATERM:36

    

     Th36: ex vt be finite DecoratedTree st vt is_an_evaluation_of (t,f)

    proof

      defpred P[ set] means ex t be c-Term of A, V, vt be finite DecoratedTree st t = $1 & vt is_an_evaluation_of (t,f);

      

       A1: for o be OperSymbol of S, p be ArgumentSeq of o, A, V st for t be c-Term of A, V st t in ( rng p) holds P[t] holds P[(( Sym (o,(the Sorts of A (\/) V))) -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of o, A, V such that

         A2: for t be c-Term of A, V st t in ( rng p) holds ex u be c-Term of A, V, vt be finite DecoratedTree st u = t & vt is_an_evaluation_of (u,f);

        defpred Q[ object, object] means ex t be c-Term of A, V, vt be finite DecoratedTree st $2 = vt & t = (p . $1) & vt is_an_evaluation_of (t,f);

        

         A3: for e be object st e in ( dom p) holds ex u be object st Q[e, u]

        proof

          let x be object;

          assume x in ( dom p);

          then

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

          ( rng p) c= (S -Terms (the Sorts of A (\/) V)) by FINSEQ_1:def 4;

          then

          reconsider t = (p . x) as c-Term of A, V by A4;

          ex u be c-Term of A, V, vt be finite DecoratedTree st u = t & vt is_an_evaluation_of (u,f) by A2, A4;

          hence thesis;

        end;

        consider q be Function such that

         A5: ( dom q) = ( dom p) & for x be object st x in ( dom p) holds Q[x, (q . x)] from CLASSES1:sch 1( A3);

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

        then

        reconsider q as FinSequence by A5, FINSEQ_1:def 2;

        

         A6: ( len p) = ( len q) by A5, FINSEQ_3: 29;

        now

          let x be object;

          assume x in ( dom q);

          then ex t be c-Term of A, V, vt be finite DecoratedTree st (q . x) = vt & t = (p . x) & vt is_an_evaluation_of (t,f) by A5;

          hence (q . x) is DecoratedTree;

        end;

        then

        reconsider q as DTree-yielding FinSequence by TREES_3: 24;

        now

          let i be Nat, t be c-Term of A, V;

          assume i in ( dom p);

          then ex t be c-Term of A, V, vt be finite DecoratedTree st (q . i) = vt & t = (p . i) & vt is_an_evaluation_of (t,f) by A5;

          hence t = (p . i) implies ex vt be finite DecoratedTree st vt = (q . i) & vt is_an_evaluation_of (t,f);

        end;

        then ex vt be finite DecoratedTree st vt = ((( Den (o,A)) . ( roots q)) -tree q) & vt is_an_evaluation_of ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V,f) by A6, Th33;

        hence thesis;

      end;

      

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

      proof

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

        reconsider t = ( root-tree [x, s]) as c-Term of A, V by Th8;

        take t, ( root-tree ((f . s) . x));

        thus t = ( root-tree [x, s]);

        thus thesis by Th32;

      end;

      

       A8: for s be SortSymbol of S, x be Element of (the Sorts of A . s) holds P[( root-tree [x, s])]

      proof

        let s be SortSymbol of S, x be Element of (the Sorts of A . s);

        reconsider t = ( root-tree [x, s]) as c-Term of A, V by Th6;

        take t, ( root-tree x);

        thus t = ( root-tree [x, s]);

        thus thesis by Th31;

      end;

      for t be c-Term of A, V holds P[t] from CTermInd( A8, A7, A1);

      then ex u be c-Term of A, V, vt be finite DecoratedTree st u = t & vt is_an_evaluation_of (u,f);

      hence thesis;

    end;

    theorem :: MSATERM:37

    

     Th37: for e1,e2 be finite DecoratedTree st e1 is_an_evaluation_of (t,f) & e2 is_an_evaluation_of (t,f) holds e1 = e2

    proof

      defpred P[ c-Term of A, V] means for e1,e2 be finite DecoratedTree st e1 is_an_evaluation_of ($1,f) & e2 is_an_evaluation_of ($1,f) holds e1 = e2;

       A1:

      now

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

        thus P[(v -term A)]

        proof

          let e1,e2 be finite DecoratedTree;

          set t = (v -term A);

          assume that

           A2: e1 is_an_evaluation_of (t,f) and

           A3: e2 is_an_evaluation_of (t,f);

          

           A4: ( dom e1) = ( dom t) by A2;

          

           A5: {} is Node of e1 by TREES_1: 22;

          

           A6: (( root-tree [v, s]) . {} ) = [v, s] by TREES_4: 3;

          then (e1 . {} ) = ((f . s) . v) by A2, A5;

          then

           A7: e1 = ( root-tree ((f . s) . v)) by A4, TREES_4: 3, TREES_4: 5;

          

           A8: ( dom e2) = ( dom t) by A3;

          (e2 . {} ) = ((f . s) . v) by A3, A4, A6, A5;

          hence thesis by A8, A7, TREES_4: 3, TREES_4: 5;

        end;

      end;

       A9:

      now

        let o be OperSymbol of S, p be ArgumentSeq of o, A, V;

        assume

         A10: for t be c-Term of A, V st t in ( rng p) holds P[t];

        thus P[(( Sym (o,(the Sorts of A (\/) V))) -tree p)]

        proof

          set t = (( Sym (o,(the Sorts of A (\/) V))) -tree p);

          let e1,e2 be finite DecoratedTree;

          assume that

           A11: e1 is_an_evaluation_of (t qua c-Term of A, V,f) and

           A12: e2 is_an_evaluation_of (t qua c-Term of A, V,f);

          consider q1 be DTree-yielding FinSequence such that

           A13: ( len q1) = ( len p) and

           A14: e1 = ((( Den (o,A)) . ( roots q1)) -tree q1) and

           A15: for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q1 . i) & vt is_an_evaluation_of (t,f) by A11, Th35;

          consider q2 be DTree-yielding FinSequence such that

           A16: ( len q2) = ( len p) and

           A17: e2 = ((( Den (o,A)) . ( roots q2)) -tree q2) and

           A18: for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q2 . i) & vt is_an_evaluation_of (t,f) by A12, Th35;

           A19:

          now

            let i be Element of NAT ;

            assume

             A20: i < ( len p);

            then

            reconsider t = (p . (i + 1)) as c-Term of A, V by Lm2;

            

             A21: ex vt2 be finite DecoratedTree st vt2 = (q2 . (i + 1)) & vt2 is_an_evaluation_of (t,f) by A18, A20, Lm9;

            ex vt1 be finite DecoratedTree st vt1 = (q1 . (i + 1)) & vt1 is_an_evaluation_of (t,f) by A15, A20, Lm9;

            hence (q1 . (i + 1)) = (q2 . (i + 1)) by A10, A20, A21, Lm9;

          end;

           A22:

          now

            let i be Nat;

            assume i in ( dom q1);

            then ex k be Element of NAT st i = (k + 1) & k < ( len q1) by Lm1;

            hence (q1 . i) = (q2 . i) by A13, A19;

          end;

          

           A23: ( dom q2) = ( Seg ( len q2)) by FINSEQ_1:def 3;

          ( dom q1) = ( Seg ( len q1)) by FINSEQ_1:def 3;

          then q1 = q2 by A13, A16, A23, A22, FINSEQ_1: 13;

          hence thesis by A14, A17;

        end;

      end;

       A24:

      now

        let s be SortSymbol of S, x be Element of (the Sorts of A . s);

        thus P[(x -term (A,V))]

        proof

          let e1,e2 be finite DecoratedTree;

          set t = (x -term (A,V));

          assume that

           A25: e1 is_an_evaluation_of (t,f) and

           A26: e2 is_an_evaluation_of (t,f);

          

           A27: ( dom e1) = ( dom t) by A25;

          

           A28: {} is Node of e1 by TREES_1: 22;

          

           A29: (( root-tree [x, s]) . {} ) = [x, s] by TREES_4: 3;

          then (e1 . {} ) = x by A25, A28;

          then

           A30: e1 = ( root-tree x) by A27, TREES_4: 3, TREES_4: 5;

          

           A31: ( dom e2) = ( dom t) by A26;

          (e2 . {} ) = x by A26, A27, A29, A28;

          hence thesis by A31, A30, TREES_4: 3, TREES_4: 5;

        end;

      end;

      for t be c-Term of A, V holds P[t] from TermInd2( A24, A1, A9);

      hence thesis;

    end;

    theorem :: MSATERM:38

    

     Th38: for vt be finite DecoratedTree st vt is_an_evaluation_of (t,f) holds (vt . {} ) in (the Sorts of A . ( the_sort_of t))

    proof

      defpred P[ c-Term of A, V] means for vt be finite DecoratedTree st vt is_an_evaluation_of ($1,f) holds (vt . {} ) in (the Sorts of A . ( the_sort_of $1));

       A1:

      now

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

        thus P[(v -term A)]

        proof

          let vt be finite DecoratedTree;

          set t = (v -term A);

          assume

           A2: vt is_an_evaluation_of (t,f);

          ( root-tree ((f . s) . v)) is_an_evaluation_of (t,f) by Th32;

          then vt = ( root-tree ((f . s) . v)) by A2, Th37;

          then

           A3: (vt . {} ) = ((f . s) . v) by TREES_4: 3;

          s = ( the_sort_of t) by Th19;

          hence thesis by A3;

        end;

      end;

       A4:

      now

        let o be OperSymbol of S, p be ArgumentSeq of o, A, V;

        assume

         A5: for t be c-Term of A, V st t in ( rng p) holds P[t];

        thus P[(( Sym (o,(the Sorts of A (\/) V))) -tree p)]

        proof

          let vt be finite DecoratedTree;

          set t = (( Sym (o,(the Sorts of A (\/) V))) -tree p);

          

           A6: ( dom (the Sorts of A * the ResultSort of S)) = the carrier' of S by PARTFUN1:def 2;

          assume vt is_an_evaluation_of (t qua c-Term of A, V,f);

          then

          consider q be DTree-yielding FinSequence such that

           A7: ( len q) = ( len p) and

           A8: vt = ((( Den (o,A)) . ( roots q)) -tree q) and

           A9: for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (q . i) & vt is_an_evaluation_of (t,f) by Th35;

          

           A10: (vt . {} ) = (( Den (o,A)) . ( roots q)) by A8, TREES_4:def 4;

          now

            

             A11: ( rng ( the_arity_of o)) c= the carrier of S by FINSEQ_1:def 4;

            

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

            

             A13: ( dom ( roots q)) = ( dom q) by TREES_3:def 18;

            

            hence

             A14: ( dom ( roots q)) = ( Seg ( len q)) by FINSEQ_1:def 3

            .= ( Seg ( len ( the_arity_of o))) by A7, Lm8

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

            .= ( dom (the Sorts of A * ( the_arity_of o))) by A12, A11, RELAT_1: 27;

            let x be object;

            assume

             A15: x in ( dom (the Sorts of A * ( the_arity_of o)));

            then

            consider i be Element of NAT such that

             A16: x = (i + 1) and

             A17: i < ( len q) by A13, A14, Lm1;

            

             A18: ex T be DecoratedTree st T = (q . (i + 1)) & (( roots q) . (i + 1)) = (T . {} ) by A13, A14, A15, A16, TREES_3:def 18;

            (i + 1) in ( dom p) by A7, A17, Lm9;

            then

             A19: ex t be c-Term of A, V st t = (p . (i + 1)) & t = (p qua FinSequence of (S -Terms (the Sorts of A (\/) V)) qua non empty set /. (i + 1)) & ( the_sort_of t) = (( the_arity_of o) . (i + 1)) & ( the_sort_of t) = (( the_arity_of o) /. (i + 1)) by Lm8;

            reconsider t = (p . (i + 1)) as c-Term of A, V by A7, A17, Lm2;

            consider vt be finite DecoratedTree such that

             A20: vt = (q . (i + 1)) and

             A21: vt is_an_evaluation_of (t,f) by A7, A9, A17, Lm9;

            (vt . {} ) in (the Sorts of A . ( the_sort_of t)) by A5, A7, A17, A21, Lm9;

            hence (( roots q) . x) in ((the Sorts of A * ( the_arity_of o)) . x) by A15, A16, A18, A20, A19, FUNCT_1: 12;

          end;

          then ( roots q) in ( product (the Sorts of A * ( the_arity_of o))) by CARD_3: 9;

          then ( roots q) in ((the Sorts of A # ) . ( the_arity_of o)) by FINSEQ_2:def 5;

          then

           A22: ( roots q) in ((the Sorts of A # ) . (the Arity of S . o)) by MSUALG_1:def 1;

          ( dom ((the Sorts of A # ) * the Arity of S)) = the carrier' of S by PARTFUN1:def 2;

          then ( roots q) in (((the Sorts of A # ) * the Arity of S) . o) by A22, FUNCT_1: 12;

          then

           A23: ( roots q) in ( Args (o,A)) by MSUALG_1:def 4;

          ( Result (o,A)) = ((the Sorts of A * the ResultSort of S) . o) by MSUALG_1:def 5

          .= (the Sorts of A . (the ResultSort of S . o)) by A6, FUNCT_1: 12

          .= (the Sorts of A . ( the_result_sort_of o)) by MSUALG_1:def 2

          .= (the Sorts of A . ( the_sort_of t qua c-Term of A, V)) by Th20;

          hence thesis by A10, A23, FUNCT_2: 5;

        end;

      end;

       A24:

      now

        let s be SortSymbol of S, x be Element of (the Sorts of A . s);

        thus P[(x -term (A,V))]

        proof

          let vt be finite DecoratedTree;

          set t = (x -term (A,V));

          assume

           A25: vt is_an_evaluation_of (t,f);

          ( root-tree x) is_an_evaluation_of (t,f) by Th31;

          then vt = ( root-tree x) by A25, Th37;

          then

           A26: (vt . {} ) = x by TREES_4: 3;

          s = ( the_sort_of t) by Th15;

          hence thesis by A26;

        end;

      end;

      for t be c-Term of A, V holds P[t] from TermInd2( A24, A1, A4);

      hence thesis;

    end;

    definition

      let S be non void non empty ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let V be Variables of A;

      let t be c-Term of A, V;

      let f be ManySortedFunction of V, the Sorts of A;

      :: MSATERM:def10

      func t @ f -> Element of (the Sorts of A . ( the_sort_of t)) means

      : Def10: ex vt be finite DecoratedTree st vt is_an_evaluation_of (t,f) & it = (vt . {} );

      existence

      proof

        consider vt be finite DecoratedTree such that

         A1: vt is_an_evaluation_of (t,f) by Th36;

        reconsider tf = (vt . {} ) as Element of (the Sorts of A . ( the_sort_of t)) by A1, Th38;

        take tf, vt;

        thus thesis by A1;

      end;

      uniqueness by Th37;

    end

    reserve t for c-Term of A, V;

    theorem :: MSATERM:39

    

     Th39: for vt be finite DecoratedTree st vt is_an_evaluation_of (t,f) holds (t @ f) = (vt . {} )

    proof

      

       A1: ex e be finite DecoratedTree st e is_an_evaluation_of (t,f) & (t @ f) = (e . {} ) by Def10;

      let vt be finite DecoratedTree;

      assume vt is_an_evaluation_of (t,f);

      hence thesis by A1, Th37;

    end;

    theorem :: MSATERM:40

    for vt be finite DecoratedTree st vt is_an_evaluation_of (t,f) holds for p be Node of t holds (vt . p) = ((t | p) @ f)

    proof

      let vt be finite DecoratedTree such that

       A1: vt is_an_evaluation_of (t,f);

      let p be Node of t;

      reconsider n = p as Node of vt by A1;

      

       A2: (n ^ {} ) = n by FINSEQ_1: 34;

      

       A3: {} in (( dom vt) | p) by TREES_1: 22;

      ((t | p) @ f) = ((vt | n) . ( <*> NAT )) by A1, Th34, Th39;

      hence thesis by A2, A3, TREES_2:def 10;

    end;

    theorem :: MSATERM:41

    for s be SortSymbol of S, x be Element of (the Sorts of A . s) holds ((x -term (A,V)) @ f) = x

    proof

      let s be SortSymbol of S, x be Element of (the Sorts of A . s);

      x = (( root-tree x) . {} ) by TREES_4: 3;

      hence thesis by Th31, Th39;

    end;

    theorem :: MSATERM:42

    for s be SortSymbol of S, v be Element of (V . s) holds ((v -term A) @ f) = ((f . s) . v)

    proof

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

      ((f . s) . v) = (( root-tree ((f . s) . v)) . {} ) by TREES_4: 3;

      hence thesis by Th32, Th39;

    end;

    theorem :: MSATERM:43

    for o be OperSymbol of S, p be ArgumentSeq of o, A, V holds for q be FinSequence st ( len q) = ( len p) & for i be Nat st i in ( dom p) holds for t be c-Term of A, V st t = (p . i) holds (q . i) = (t @ f) holds ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V @ f) = (( Den (o,A)) . q)

    proof

      let o be OperSymbol of S, p be ArgumentSeq of o, A, V;

      let q be FinSequence;

      assume that

       A1: ( len q) = ( len p) and

       A2: for i be Nat st i in ( dom p) holds for t be c-Term of A, V st t = (p . i) holds (q . i) = (t @ f);

      consider vt be finite DecoratedTree such that

       A3: vt is_an_evaluation_of ((( Sym (o,(the Sorts of A (\/) V))) -tree p),f) by Th36;

      consider r be DTree-yielding FinSequence such that

       A4: ( len r) = ( len p) and

       A5: vt = ((( Den (o,A)) . ( roots r)) -tree r) and

       A6: for i be Nat, t be c-Term of A, V st i in ( dom p) & t = (p . i) holds ex vt be finite DecoratedTree st vt = (r . i) & vt is_an_evaluation_of (t,f) by A3, Th35;

      now

        thus

         A7: ( dom p) = ( dom p) & ( dom q) = ( dom p) & ( dom r) = ( dom p) by A1, A4, FINSEQ_3: 29;

        let i be Element of NAT ;

        assume

         A8: i in ( dom r);

        then

        reconsider t = (p . i) as c-Term of A, V by A7, Th22;

        consider vt be finite DecoratedTree such that

         A9: vt = (r . i) and

         A10: vt is_an_evaluation_of (t,f) by A6, A7, A8;

        reconsider T = vt as DecoratedTree;

        take T;

        thus T = (r . i) by A9;

        

        thus (q . i) = (t @ f) by A2, A7, A8

        .= (T . {} ) by A10, Th39;

      end;

      then q = ( roots r) by TREES_3:def 18;

      

      hence ((( Sym (o,(the Sorts of A (\/) V))) -tree p) qua c-Term of A, V @ f) = (((( Den (o,A)) . q) -tree r) . {} ) by A3, A5, Th39

      .= (( Den (o,A)) . q) by TREES_4:def 4;

    end;