:: On Defining Functions on Trees
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 12, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, CARD_1, XBOOLE_0, FINSEQ_1, TREES_3, SUBSET_1, RELAT_1,
      FUNCT_1, TARSKI, TREES_2, TREES_4, ZFMISC_1, MCART_1, LANG1, STRUCT_0,
      TDGROUP, CARD_3, ARYTM_3, NAT_1, XXREAL_0, FINSET_1, TREES_1, TREES_A,
      FUNCT_6, PRE_POLY, ORDINAL4, FINSEQ_2, DTCONSTR;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, RELSET_1,
      RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSET_1,
      XTUPLE_0, MCART_1, CARD_3, DOMAIN_1, LANG1, TREES_1, TREES_2, FINSEQ_4,
      TREES_3, TREES_4, FINSEQOP, XXREAL_0, ORDINAL1, NAT_1, PRE_POLY;
 constructors PARTFUN1, BINOP_1, DOMAIN_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1,
      CARD_3, FINSEQOP, FINSEQ_4, FINSOP_1, TREES_4, LANG1, SEQ_1, RELSET_1,
      PRE_POLY, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0,
      XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, TREES_3, STRUCT_0, LANG1,
      FINSET_1, CARD_1, FINSEQ_2, TREES_4, VALUED_0, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FINSEQ_1, XBOOLE_0, XTUPLE_0;
 theorems TARSKI, NAT_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_6, MCART_1,
      LANG1, FINSEQ_1, FINSEQ_2, CARD_5, TREES_1, TREES_3, TREES_4, CARD_3,
      RELSET_1, XBOOLE_0, XBOOLE_1, MEASURE2, XXREAL_0, ORDINAL1, PRE_POLY,
      CARD_1;
 schemes NAT_1, CQC_SIM1, FINSEQ_1, RELSET_1, FRAENKEL, FUNCT_2, FUNCT_1;

begin :: Preliminaries

deffunc T(set) = 0;
deffunc A(set,set,set) = 0;

theorem Th1: :: This really belongs elsewhere
  for D being non empty set, p being FinSequence of FinTrees D holds
  p is FinSequence of Trees D
proof
  let D be non empty set;
  FinTrees D is non empty Subset of Trees D by TREES_3:21;
  hence thesis by FINSEQ_2:24;
end;

theorem Th2:
  for x,y being set, p being FinSequence of x st y in dom p holds p.y in x
proof
  let x,y be set;
  let p be FinSequence of x;
  assume y in dom p;
  then
A1: p.y in rng p by FUNCT_1:def 3;
  rng p c= x by FINSEQ_1:def 4;
  hence thesis by A1;
end;

registration
  let D be non empty set, T be DTree-set of D;
  cluster -> DTree-yielding for FinSequence of T;
  coherence;
end;

definition
  let D be non empty set;
  let F be non empty DTree-set of D;
  let Tset be non empty Subset of F;
  redefine mode Element of Tset -> Element of F;
  coherence
  proof
    let x be Element of Tset;
    thus thesis;
  end;
end;

definition
  let D be non empty set, T be DTree-set of D;
  let p be FinSequence of T;
  redefine func roots p -> FinSequence of D;
  coherence
  proof
    let x be set;
    assume x in rng roots p;
    then consider k being set such that
A1: k in dom roots p and
A2: x = (roots p).k by FUNCT_1:def 3;
    reconsider k as Element of NAT by A1;
A3: dom roots p = dom p by TREES_3:def 18;
    then consider t being DecoratedTree such that
A4: t = p.k and
A5: (roots p).k = t.{} by A1,TREES_3:def 18;
    reconsider t as DecoratedTree of D by A1,A3,A4,Th2,TREES_3:def 6;
    reconsider r = {} as Node of t by TREES_1:22;
    t.r in D;
    hence thesis by A2,A5;
  end;
end;

Lm1: dom roots {} = dom {} by TREES_3:def 18
  .= {};

theorem Th3:
  roots {} = {} by Lm1;

theorem Th4:
  for T being DecoratedTree holds roots <*T*> = <*T.{}*>
proof
  let T be DecoratedTree;
A1: dom <*T*> = Seg 1 by FINSEQ_1:def 8;
A2: dom <*T.{}*> = Seg 1 by FINSEQ_1:def 8;
A3: <*T*>.1 = T by FINSEQ_1:def 8;
A4: <*T.{}*>.1 = T.{} by FINSEQ_1:def 8;
  now
    let i be Element of NAT;
    assume
A5: i in dom <*T*>;
    take t = T;
    thus t = <*T*>.i & <*T.{}*>.i = t.{} by A1,A3,A4,A5,FINSEQ_1:2,TARSKI:def 1
;
  end;
  hence thesis by A1,A2,TREES_3:def 18;
end;

theorem Th5:
  for D being non empty set, F being (Subset of FinTrees D),
  p being FinSequence of F st len roots p = 1
  ex x being Element of FinTrees D st p = <*x*> & x in F
proof
  let D be non empty set, F be (Subset of FinTrees D), p be FinSequence of F;
  assume len roots p = 1;
  then
A1: dom roots p = Seg 1 by FINSEQ_1:def 3;
A2: dom p = dom roots p by TREES_3:def 18;
  then
A3: 1 in dom p by A1;
  then reconsider x = p.1 as Element of FinTrees D by Th2;
  take x;
  thus thesis by A1,A2,A3,Th2,FINSEQ_1:def 8;
end;

theorem
  for T1, T2 being DecoratedTree holds roots <*T1, T2*> = <*T1.{}, T2.{}*>
proof
  let T1, T2 be DecoratedTree;
A1: len <*T1, T2*> = 2 by FINSEQ_1:44;
A2: len <*T1.{}, T2.{}*> = 2 by FINSEQ_1:44;
A3: <*T1, T2*>.1 = T1 by FINSEQ_1:44;
A4: <*T1.{}, T2.{}*>.1 = T1.{} by FINSEQ_1:44;
A5: <*T1, T2*>.2 = T2 by FINSEQ_1:44;
A6: <*T1.{}, T2.{}*>.2 = T2.{} by FINSEQ_1:44;
A7: dom <*T1, T2*> = Seg 2 by A1,FINSEQ_1:def 3;
A8: dom <*T1.{}, T2.{}*> = Seg 2 by A2,FINSEQ_1:def 3;
  now
    let i be Element of NAT;
    assume i in dom <*T1, T2*>;
    then i in Seg 2 by A1,FINSEQ_1:def 3;
    then i = 1 or i = 2 by FINSEQ_1:2,TARSKI:def 2;
    hence ex t being DecoratedTree st
    t = <*T1, T2*>.i & <*T1.{}, T2.{}*>.i = t.{} by A3,A4,A5,A6;
  end;
  hence thesis by A7,A8,TREES_3:def 18;
end;

definition
  let X, Y be set, f be FinSequence of [:X, Y:];
  redefine func pr1 f -> FinSequence of X;
  coherence
  proof
A1: dom pr1 f = dom f by MCART_1:def 12;
    dom f = Seg len f by FINSEQ_1:def 3;
    then reconsider p = pr1 f as FinSequence by A1,FINSEQ_1:def 2;
    rng p c= X
    proof
      let x be set;
      assume x in rng p;
      then consider i being set such that
A2:   i in dom p and
A3:   x = p.i by FUNCT_1:def 3;
A4:   f.i in [:X, Y:] by A1,A2,Th2;
      x = (f.i)`1 by A1,A2,A3,MCART_1:def 12;
      hence thesis by A4,MCART_1:10;
    end;
    hence thesis by FINSEQ_1:def 4;
  end;
  redefine func pr2 f -> FinSequence of Y;
  coherence
  proof
A5: dom pr2 f = dom f by MCART_1:def 13;
    dom f = Seg len f by FINSEQ_1:def 3;
    then reconsider p = pr2 f as FinSequence by A5,FINSEQ_1:def 2;
    rng p c= Y
    proof
      let x be set;
      assume x in rng p;
      then consider i being set such that
A6:   i in dom p and
A7:   x = p.i by FUNCT_1:def 3;
A8:   f.i in [:X, Y:] by A5,A6,Th2;
      x = (f.i)`2 by A5,A6,A7,MCART_1:def 13;
      hence thesis by A8,MCART_1:10;
    end;
    hence thesis by FINSEQ_1:def 4;
  end;
end;

theorem Th7:
  pr1 {} = {} & pr2 {} = {}
proof
  set r = <*>[:{}, {}:];
  dom pr1 r = dom {}
    .= {};
  hence pr1 {} = {};
  dom pr2 r = dom {}
    .= {};
  hence thesis;
end;

begin

registration
  let A be non empty set, R be Relation of A,A*;
  cluster DTConstrStr(#A,R#) -> non empty;
  coherence;
end;

scheme DTConstrStrEx { S() -> non empty set, P[set, set] }:
  ex G be strict non empty DTConstrStr st the carrier of G = S() &
  for x being Symbol of G, p being FinSequence of the carrier of G
  holds x ==> p iff P[x, p]
proof
  consider PR being Relation of S(), S()* such that
A1: for x, y being set
  holds [x,y] in PR iff x in S() & y in S()* & P[x, y] from RELSET_1:sch 1;
  take DT = DTConstrStr (# S(), PR #);
  thus the carrier of DT = S();
  let x be Symbol of DT, p be FinSequence of the carrier of DT;
  hereby
    assume x ==> p;
    then [x, p] in the Rules of DT by LANG1:def 1;
    hence P[x, p] by A1;
  end;
  assume
A2: P[x, p];
  p in (the carrier of DT)* by FINSEQ_1:def 11;
  then [x, p] in PR by A1,A2;
  hence thesis by LANG1:def 1;
end;

scheme DTConstrStrUniq { S() -> non empty set, P[set, set] }:
  for G1, G2 being strict non empty DTConstrStr st (the carrier of G1 = S() &
  for x being Symbol of G1, p being FinSequence of the carrier of G1
  holds x ==> p iff P[x, p]) & (the carrier of G2 = S() &
  for x being Symbol of G2, p being FinSequence of the carrier of G2
  holds x ==> p iff P[x, p]) holds G1 = G2
proof
  let G1, G2 be strict non empty DTConstrStr such that
A1: the carrier of G1 = S() and
A2: for x being Symbol of G1, p being FinSequence of the carrier of G1
  holds x ==> p iff P[x, p] and
A3: the carrier of G2 = S() and
A4: for x being Symbol of G2, p being FinSequence of the carrier of G2
  holds x ==> p iff P[x, p];
  now
    let x, y be set;
    hereby
      assume
A5:   [x, y] in the Rules of G1;
      then
A6:   y in (the carrier of G1)* by ZFMISC_1:87;
      reconsider x1 = x as Symbol of G1 by A5,ZFMISC_1:87;
reconsider y1 = y as FinSequence of the carrier of G1 by A6,FINSEQ_2:def 3;
A7:   x1 ==> y1 iff P[x1, y1] by A2;
      reconsider x2 = x as Symbol of G2 by A1,A3,A5,ZFMISC_1:87;
      reconsider y2 = y as FinSequence of the carrier of G2 by A1,A3,A6,
FINSEQ_2:def 3;
      x2 ==> y2 by A4,A5,A7,LANG1:def 1;
      hence [x, y] in the Rules of G2 by LANG1:def 1;
    end;
    assume
A8: [x, y] in the Rules of G2;
    then
A9: y in (the carrier of G2)* by ZFMISC_1:87;
    reconsider x2 = x as Symbol of G2 by A8,ZFMISC_1:87;
    reconsider y2 = y as FinSequence of the carrier of G2 by A9,FINSEQ_2:def 3;
A10: x2 ==> y2 iff P[x2, y2] by A4;
    reconsider x1 = x as Symbol of G1 by A1,A3,A8,ZFMISC_1:87;
    reconsider y1 = y as FinSequence of the carrier of G1 by A1,A3,A9,
FINSEQ_2:def 3;
    x1 ==> y1 by A2,A8,A10,LANG1:def 1;
    hence [x, y] in the Rules of G1 by LANG1:def 1;
  end;
  hence thesis by A1,A3,RELAT_1:def 2;
end;

theorem
  for G being non empty DTConstrStr holds Terminals G misses NonTerminals G
proof
  let G be non empty DTConstrStr;
A1: Terminals G = { t where t is Symbol of G :
  not ex tnt being FinSequence st t ==> tnt } by LANG1:def 2;
A2: NonTerminals G = { t where t is Symbol of G :
  ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
  assume not thesis;
  then consider x being set such that
A3: x in Terminals G and
A4: x in NonTerminals G by XBOOLE_0:3;
A5: ex t being Symbol of G st x = t & not ex tnt being FinSequence st t ==>
  tnt by A1,A3;
  ex t being Symbol of G st x = t & ex tnt being FinSequence st t ==> tnt
  by A2,A4;
  hence contradiction by A5;
end;

scheme DTCMin { f() -> Function,
  G() -> non empty DTConstrStr, D() -> non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
  ex X being Subset of FinTrees [:the carrier of G(), D():] st X = Union f() &
  (for d being Symbol of G() st d in Terminals G()
  holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G(),
  p being FinSequence of X st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
  for F being Subset of FinTrees [:the carrier of G(), D():] st
  (for d being Symbol of G() st d in Terminals G()
  holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G(),
  p being FinSequence of F st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F) holds X c= F
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Element of NAT holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
  set f = f();
  set G = G();
  set D = D();
  deffunc
  NTV(Symbol of G, FinSequence) = NTermVal($1, pr1 roots $2, pr2 roots $2);
  Union f c= FinTrees [:the carrier of G, D:]
  proof
    let u be set;
    assume u in Union f;
    then
A4: ex k being set st ( k in NAT)&( u in f.k) by A1,CARD_5:2;
    defpred P[Element of NAT] means for u being set st u in f.$1 holds
    u in FinTrees [:the carrier of G, D:];
A5: P[0]
    proof
      let u be set;
      assume u in f.0;
      then ex t being Symbol of G, d being Element of D st u = root-tree [t,d]
      & (t in Terminals G() & d = TermVal(t) or
      t ==> {} & d = NTermVal(t, {}, {})) by A2;
      hence thesis;
    end;
A6: now
      let n be Element of NAT such that
A7:   P[n];
      thus P[n+1]
      proof
        let u be set;
        assume u in f.(n+1);
        then u in f.n \/ { [o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)*:
        ex q being FinSequence of FinTrees[:the carrier of G, D:] st
        p = q & o ==> pr1 roots q } by A3;
        then
A8:     u in f.n or u in { [o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)*:
        ex q being FinSequence of FinTrees[:the carrier of G, D:] st
        p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
        assume
A9:     not u in FinTrees [:the carrier of G, D:];
        then consider o being Symbol of G, p being Element of (f.n)* such that
A10:    u = [o, NTV(o, p)]-tree p and
A11:    ex q being FinSequence of FinTrees [:the carrier of G, D:] st p = q
        & o ==> pr1 roots q
        by A7,A8;
        reconsider p as FinSequence of FinTrees [:the carrier of G, D:] by A11;
        u = [o, NTV(o, p)]-tree p by A10;
        hence contradiction by A9;
      end;
    end;
    for n being Element of NAT holds P[n] from NAT_1:sch 1(A5,A6);
    hence thesis by A4;
  end;
  then reconsider X = Union f as Subset of FinTrees [:the carrier of G, D:];
  take X;
  thus X = Union f;
  hereby
    let d be Symbol of G;
    assume d in Terminals G;
    then root-tree [d, TermVal(d)] in f.0 by A2;
    hence root-tree [d, TermVal(d)] in X by A1,CARD_5:2;
  end;
  hereby
    let o be Symbol of G, p be FinSequence of X such that
A12: o ==> pr1 roots p;
    set s = pr1 roots p, v = pr2 roots p;
A13: dom p = Seg len p by FINSEQ_1:def 3;
    defpred P[set,set] means p.$1 in f.($2);
A14: for x being Nat st x in Seg len p ex n being Element of NAT st P[x,n]
    proof
      let x be Nat;
      assume x in Seg len p;
      then
A15:  p.x in rng p by A13,FUNCT_1:def 3;
      rng p c= X by FINSEQ_1:def 4;
      then ex n being set st n in NAT & p.x in f.n by A1,A15,CARD_5:2;
      hence thesis;
    end;
    consider pn being FinSequence of NAT such that
A16: dom pn = Seg len p & for k being Nat st k in Seg len p holds P[k,pn.k]
    from FINSEQ_1:sch 5(A14);
A17: now
      defpred P[Element of NAT,Element of NAT] means $1 >= $2;
      assume rng pn <> {};
      then
A18:  rng pn is finite & rng pn <> {} & rng pn c= NAT by FINSEQ_1:def 4;
A19:  for x, y being Element of NAT holds P[x,y] or P[y,x];
A20:  for x, y, z being Element of NAT st P[x,y] & P[y,z] holds P[x,z]
      by XXREAL_0:2;
      consider n being Element of NAT such that
A21:  n in rng pn & for y being Element of NAT st y in rng pn holds P[n,y]
      from CQC_SIM1:sch 4 ( A18, A19, A20 );
      take n;
      thus rng p c= f.n
      proof
        let t be set;
        assume t in rng p;
        then consider k being set such that
A22:    k in dom p and
A23:    t = p.k by FUNCT_1:def 3;
        reconsider k as Element of NAT by A22;
A24:    pn.k in rng pn by A13,A16,A22,FUNCT_1:def 3;
        then reconsider pnk = pn.k as Element of NAT by A18;
        consider s being Nat such that
A25:    n = pnk + s by A21,A24,NAT_1:10;
        deffunc H(set,set) =
        { [o1, NTermVal(o1, pr1 roots p1, pr2 roots p1)]-tree p1
        where o1 is Symbol of G(), p1 is Element of (f.$1)* :
        ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
        p1 = q & o1 ==> pr1 roots q };
        for n being Element of NAT holds f.n c= f.(n+1)
        proof
          let n be Element of NAT;
          f.(n+1) = f.n \/ H(n, f.n) by A3;
          hence thesis by XBOOLE_1:7;
        end;
        then
A26:    f.pnk c= f.n by A25,MEASURE2:18,NAT_1:11;
        t in f.(pn.k) by A13,A16,A22,A23;
        hence thesis by A26;
      end;
    end;
    now
      assume rng pn = {};
      then pn = {};
      then p = {} by A16;
      then rng p = {};
      hence rng p c= f.0 by XBOOLE_1:2;
    end;
    then consider n being Element of NAT such that
A27: rng p c= f.n by A17;
A28: X = union rng f by CARD_3:def 4;
    f.n in rng f by A1,FUNCT_1:def 3;
    then f.n c= X by A28,ZFMISC_1:74;
    then reconsider fn = f.n as Subset of FinTrees [:the carrier of G, D:] by
XBOOLE_1:1;
    reconsider q = p as FinSequence of fn by A27,FINSEQ_1:def 4;
    reconsider q9 = q as Element of (fn)* by FINSEQ_1:def 11;
    [o, NTermVal(o, s, v)]-tree q9 in { [oo, NTV(oo, pp)]-tree pp
    where oo is Symbol of G, pp is Element of (fn)* :
    ex q being FinSequence of FinTrees [:the carrier of G, D:] st
    pp = q & oo ==> pr1 roots q } by A12;
    then [o, NTermVal(o, s, v)]-tree q9 in f.n \/ { [oo, NTV(oo, pp)]-tree pp
    where oo is Symbol of G, pp is Element of (fn)* :
    ex q being FinSequence of FinTrees [:the carrier of G, D:] st
    pp = q & oo ==> pr1 roots q } by XBOOLE_0:def 3;
    then [o, NTermVal(o, s, v)]-tree q9 in f.(n+1) by A3;
    hence [o, NTermVal(o, s, v)]-tree p in X by A1,CARD_5:2;
  end;
  let F be Subset of FinTrees [:the carrier of G, D:] such that
A29: for d being Symbol of G st d in Terminals G holds root-tree [d,
  TermVal(d)] in F and
A30: for o being Symbol of G, p being FinSequence of F st o ==> pr1
  roots p holds [o, NTV(o, p)]-tree p in F;
  defpred P[Element of NAT] means f.$1 c= F;
A31: P[0]
  proof
    let x be set;
    reconsider p = <*>F as FinSequence of F;
    assume x in f.0;
    then consider t being Symbol of G, d being Element of D such that
A32: x = root-tree [t, d] and
A33: t in Terminals G() & d = TermVal(t) or t ==> pr1 roots p & d = NTV (t, p)
    by A2,Th3,Th7;
    [t, d]-tree p = root-tree [t, d] by TREES_4:20;
    hence thesis by A29,A30,A32,A33;
  end;
A34: now
    let n be Element of NAT such that
A35: P[n];
    thus P[n+1]
    proof
      let x be set;
      assume that
A36:  x in f.(n+1) and
A37:  not x in F;
      x in f.n \/ {[oo, NTV(oo, pp)]-tree pp
      where oo is Symbol of G, pp is Element of (f.n)* :
      ex q being FinSequence of FinTrees [:the carrier of G, D:] st
      pp = q & oo ==> pr1 roots q } by A3,A36;
      then x in f.n or x in {[oo, NTV(oo, pp)]-tree pp
      where oo is Symbol of G, pp is Element of (f.n)* :
      ex q being FinSequence of FinTrees [:the carrier of G, D:] st
      pp = q & oo ==> pr1 roots q } by XBOOLE_0:def 3;
      then consider o being Symbol of G, p being Element of (f.n)* such that
A38:  x = [o, NTV(o, p)]-tree p and
A39:  ex q being FinSequence of FinTrees [:the carrier of G, D:] st p = q
      & o ==> pr1 roots q
      by A35,A37;
      rng p c= f.n by FINSEQ_1:def 4;
      then rng p c= F by A35,XBOOLE_1:1;
      then reconsider p as FinSequence of F by FINSEQ_1:def 4;
      o ==> pr1 roots p by A39;
      hence contradiction by A30,A37,A38;
    end;
  end;
A40: for n being Element of NAT holds P[n] from NAT_1:sch 1 (A31, A34);
  thus X c= F
  proof
    let x be set;
    assume x in X;
    then consider n being set such that
A41: n in NAT and
A42: x in f.n by A1,CARD_5:2;
    f.n c= F by A40,A41;
    hence thesis by A42;
  end;
end;

scheme DTCSymbols { f() -> Function,
  G() -> non empty DTConstrStr, D() -> non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
  ex X1 being Subset of FinTrees(the carrier of G()) st
  X1 = { t`1 where t is Element of FinTrees [:(the carrier of G()), D():] :
  t in Union f() } &
  (for d being Symbol of G() st d in Terminals G() holds root-tree d in X1) &
  (for o being Symbol of G(), p being FinSequence of X1 st o ==> roots p
  holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G() st
  (for d being Symbol of G() st d in Terminals G() holds root-tree d in F) &
  (for o being Symbol of G(), p being FinSequence of F st o ==> roots p
  holds o-tree p in F) holds X1 c= F
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Element of NAT holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
  set f = f();
  set G = G();
  set D = D();
  set S = the carrier of G;
  set SxD = [:S, D:];
  deffunc
  NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
  A4: f
().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
  t in Terminals G() & d = TermVal(t) or
  t ==> {} & d = NTermVal(t, {}, {}) } by A2;
A5: for n being Element of NAT holds f().(n+1) =
  f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G(), p is Element of (f().n)* :
  ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
  p = q & o ==> pr1 roots q } by A3;
  consider X being Subset of FinTrees [:the carrier of G, D:] such that
A6: X = Union f & (for d being Symbol of G st d in Terminals G
  holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G,
  p being FinSequence of X st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
  for F being Subset of FinTrees [:the carrier of G, D:] st
  (for d being Symbol of G st d in Terminals G
  holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G,
  p being FinSequence of F st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
  holds X c= F from DTCMin (A1, A4, A5);
  set X9 = { t`1 where t is Element of FinTrees [:the carrier of G,D:]:
  t in Union f };
  X9 c= FinTrees(the carrier of G)
  proof
    let x be set;
    assume x in X9;
    then consider tt being Element of FinTrees [:the carrier of G,D:] such that
A7: x = tt`1 and tt in Union f;
A8: tt`1 = pr1(the carrier of G, D) * tt by TREES_3:def 12;
A9: rng tt c= [:the carrier of G, D:] by RELAT_1:def 19;
    dom pr1(the carrier of G, D) = [:the carrier of G, D:] by FUNCT_2:def 1;
    then dom tt`1 = dom tt by A8,A9,RELAT_1:27;
    hence thesis by A7,TREES_3:def 8;
  end;
  then reconsider X9 as Subset of FinTrees(the carrier of G());
  take X1= X9;
  thus X1 = { t`1 where t is Element of FinTrees [:the carrier of G,D:]:
  t in Union f };
  hereby
    let t be Symbol of G();
    assume
A10: t in Terminals G();
A11: (root-tree [t, TermVal(t)])`1 = root-tree t by TREES_4:25;
    root-tree [t, TermVal(t)] in Union f by A6,A10;
    hence root-tree t in X1 by A11;
  end;
  hereby
    let nt be Symbol of G(), ts be FinSequence of X1;
    assume
A12: nt ==> roots ts;
A13: dom ts = Seg len ts by FINSEQ_1:def 3;
    defpred P[set,set] means
    ex dt being DecoratedTree of [:the carrier of G(), D():] st
    dt = $2 & dt`1 = ts.$1 & dt in Union f;
A14: for k being Nat st k in Seg len ts
    ex x being Element of FinTrees [:the carrier of G, D:] st P[k,x]
    proof
      let k be Nat;
      assume k in Seg len ts;
      then
A15:  ts.k in rng ts by A13,FUNCT_1:def 3;
      rng ts c= X1 by FINSEQ_1:def 4;
      then ts.k in X1 by A15;
      then ex x being Element of FinTrees [:the carrier of G, D:] st
      ts.k = x`1 & x in Union f;
      hence thesis;
    end;
    consider dts being FinSequence of FinTrees [:the carrier of G, D:]
    such that
A16: dom dts = Seg len ts and
A17: for k being Nat st k in Seg len ts holds P[k,dts.k]
    from FINSEQ_1:sch 5(A14);
    rng dts c= Union f
    proof
      let x be set;
      assume x in rng dts;
      then consider k being set such that
A18:  k in dom ts and
A19:  x = dts.k by A13,A16,FUNCT_1:def 3;
      reconsider k as Element of NAT by A18;
      ex dt being DecoratedTree of [:the carrier of G(), D():]
      st dt = x & dt`1 = ts.k & dt in Union f by A13,A17,A18,A19;
      hence thesis;
    end;
    then reconsider dts as FinSequence of X by A6,FINSEQ_1:def 4;
A20: dom roots ts = dom ts by TREES_3:def 18;
A21: dom pr1 roots dts = dom roots dts by MCART_1:def 12;
    then
A22: dom pr1 roots dts = dom ts by A13,A16,TREES_3:def 18;
    now
      let k be Nat;
      assume
A23:  k in dom ts;
      then consider dt being DecoratedTree of [:the carrier of G(), D():]
      such that
A24:  dt = dts.k and
A25:  dt`1 = ts.k and dt in Union f by A13,A17;
      reconsider r = {} as Node of dt by TREES_1:22;
      ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{}
      by A23,TREES_3:def 18;
      then
A26:  (roots ts).k = (dt.r)`1 by A25,TREES_3:39;
      ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{}
      by A13,A16,A23,TREES_3:def 18;
      hence (roots ts).k = (pr1 roots dts).k
      by A21,A22,A23,A24,A26,MCART_1:def 12;
    end;
    then roots ts = pr1 roots dts by A20,A22,FINSEQ_1:13;
    then
A27: [nt, NTV(nt, dts)]-tree dts in X by A6,A12;
A28: rng dts c= FinTrees [:the carrier of G(), D():] by FINSEQ_1:def 4;
    FinTrees [:the carrier of G(),D():] c= Trees [:the carrier of G(), D() :]
    by TREES_3:21;
    then rng dts c= Trees [:the carrier of G(), D():] by A28,XBOOLE_1:1;
    then reconsider dts9 = dts as FinSequence of Trees [:the carrier of G(),D()
    :] by FINSEQ_1:def 4;
A29: rng ts c= FinTrees the carrier of G() by FINSEQ_1:def 4;
    FinTrees the carrier of G() c= Trees the carrier of G() by TREES_3:21;
    then rng ts c= Trees the carrier of G() by A29,XBOOLE_1:1;
    then reconsider ts9 = ts as FinSequence of Trees the carrier of G()
    by FINSEQ_1:def 4;
    now
      let i be Element of NAT;
      assume i in dom dts;
      then
A30:  ex dt being DecoratedTree of [:the carrier of G, D:] st ( dt
      = dts.i)&( dt`1 = ts.i)&( dt in Union f) by A16,A17;
      let T be DecoratedTree of [:the carrier of G(), D():];
      assume T = dts.i;
      hence ts.i = T`1 by A30;
    end;
    then ([nt, NTV(nt, dts)]-tree dts9)`1 = nt-tree ts9 by A13,A16,TREES_4:27;
    hence nt-tree ts in X1 by A6,A27;
  end;
  let F be Subset of FinTrees the carrier of G;
  assume that
A31: for d being Symbol of G st d in Terminals G holds root-tree d in F and
A32: for o being Symbol of G, p being FinSequence of F st o ==> roots p
  holds o-tree p in F;
  thus X1 c= F
  proof
    let x be set;
    assume x in X1;
then consider tt being Element of FinTrees [:the carrier of G, D:] such that
A33: x = tt`1 and
A34: tt in Union f;
    set FF = { dt where dt is Element of FinTrees SxD : dt`1 in F };
    FF c= FinTrees SxD
    proof
      let x be set;
      assume x in FF;
      then ex dt being Element of FinTrees SxD st x = dt & dt`1 in F;
      hence thesis;
    end;
    then reconsider FF as Subset of FinTrees SxD;
A35: now
      let d be Symbol of G;
      assume d in Terminals G;
      then
A36:  root-tree d in F by A31;
      (root-tree [d, TermVal(d)])`1 = root-tree d by TREES_4:25;
      hence root-tree [d, TermVal(d)] in FF by A36;
    end;
    now
      let o be Symbol of G, p be FinSequence of FF;
      assume
A37:  o ==> pr1 roots p;
      consider p1 being FinSequence of FinTrees S such that
A38:  dom p1 = dom p and
A39:  for i being Element of NAT st i in dom p
      ex T being Element of FinTrees SxD st T = p.i & p1.i = T`1 and
A40:  ([o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p)`1 = o-tree p1
      by TREES_4:31;
      rng p1 c= F
      proof
        let x be set;
        assume x in rng p1;
        then consider k being set such that
A41:    k in dom p1 and
A42:    x = p1.k by FUNCT_1:def 3;
        reconsider k as Element of NAT by A41;
A43:    p.k in rng p by A38,A41,FUNCT_1:def 3;
A44:    ex dt being Element of FinTrees SxD st ( dt = p.k)&( x = dt
        `1) by A38,A39,A41,A42;
        rng p c= FF by FINSEQ_1:def 4;
        then p.k in FF by A43;
        then ex dt being Element of FinTrees SxD st p.k = dt & dt`1 in F;
        hence thesis by A44;
      end;
      then reconsider p1 as FinSequence of F by FINSEQ_1:def 4;
A45:  dom roots p1 = dom p1 by TREES_3:def 18;
A46:  dom pr1 roots p = dom roots p by MCART_1:def 12;
      then
A47:  dom pr1 roots p = dom p1 by A38,TREES_3:def 18;
      now
        let k be Nat;
        assume
A48:    k in dom p1;
        then
A49:    p.k in rng p by A38,FUNCT_1:def 3;
A50:    ex dt being Element of FinTrees SxD st ( dt = p.k)&( p1.k =
        dt`1) by A38,A39,A48;
        rng p c= FF by FINSEQ_1:def 4;
        then p.k in FF by A49;
        then consider dt being Element of FinTrees SxD such that
A51:    p.k = dt and dt`1 in F;
        reconsider r = {} as Node of dt by TREES_1:22;
        ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{}
        by A48,TREES_3:def 18;
        then
A52:    (roots p1).k = (dt.r)`1 by A50,A51,TREES_3:39;
        ex T being DecoratedTree st T = p.k & (roots p).k = T.{}
        by A38,A48,TREES_3:def 18;
        hence (roots p1).k = (pr1 roots p).k
        by A46,A47,A48,A51,A52,MCART_1:def 12;
      end;
      then pr1 roots p = roots p1 by A45,A47,FINSEQ_1:13;
      then ([o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p)`1 in F
      by A32,A37,A40;
      hence [o, NTV(o, p)]-tree p in FF;
    end;
    then X c= FF by A6,A35;
    then tt in FF by A6,A34;
    then ex dt being Element of FinTrees SxD st tt = dt & dt`1 in F;
    hence thesis by A33;
  end;
end;

scheme DTCHeight { f() -> Function,
  G() -> non empty DTConstrStr, D() -> non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
  for n being Element of NAT,
  dt being Element of FinTrees [:the carrier of G(), D():]
  st dt in Union f() holds dt in f().n iff height dom dt <= n
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Element of NAT holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
  set f = f();
  set G = G();
  set D = D();
  set SxD = [:the carrier of G, D:];
  deffunc
  NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
  defpred R[Element of NAT] means
  for dt being Element of FinTrees SxD st dt in Union f
  holds dt in f.$1 iff height dom dt <= $1;
A4: R[0]
  proof
    let dt be Element of FinTrees SxD;
    assume
A5: dt in Union f;
    hereby
      assume dt in f.0;
      then ex t being Symbol of G, d being Element of D st dt= root-tree [t,d]
      & (t in Terminals G() & d = TermVal(t) or
      t ==> {} & d = NTermVal(t, {}, {})) by A2;
      hence height dom dt <= 0 by TREES_1:42,TREES_4:3;
    end;
    assume height dom dt <= 0;
    then
A6: height dom dt = 0;
    defpred P[Element of NAT] means not dt in f.$1;
    assume
A7: P[0];
A8: now
      let n be Element of NAT;
      assume
A9:   P[n];
      thus P[n+1]
      proof
        assume dt in f.(n+1);
        then dt in f.n \/ { [o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st p=q & o ==> pr1 roots q}
        by A3;
        then dt in f.n or dt in {[o,NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st p=q & o ==> pr1 roots q}
        by XBOOLE_0:def 3;
        then consider o being Symbol of G, p being Element of (f.n)* such that
A10:    dt = [o, NTV(o, p)]-tree p and
A11:    ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
        by A9;
A12:    dt = root-tree (dt.{}) by A6,TREES_1:43,TREES_4:5;
        then
A13:    p = {} by A10,A11,TREES_4:17;
        then dt = root-tree [o, NTermVal(o,{},{})]
        by A10,A12,Th3,Th7,TREES_4:def 4;
        hence contradiction by A2,A7,A11,A13,Th3,Th7;
      end;
    end;
A14: for n being Element of NAT holds P[n] from NAT_1:sch 1 (A7, A8);
    ex n being set st n in NAT & dt in f.n by A1,A5,CARD_5:2;
    hence contradiction by A14;
  end;
A15: now
    let n be Element of NAT;
    assume
A16: R[n];
    thus R[n+1]
    proof
      let dt be Element of FinTrees SxD;
      assume
A17:  dt in Union f;
      hereby
        assume dt in f.(n+1);
        then dt in f.n \/ {[o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        p = q & o ==> pr1 roots q } by A3;
        then
A18:    dt in f.n or dt in {[o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
        per cases;
        suppose dt in f.n;
          then
A19:      height dom dt <= n by A16,A17;
          n <= n+1 by NAT_1:11;
          hence height dom dt <= n+1 by A19,XXREAL_0:2;
        end;
        suppose not dt in f.n;
then consider o being Symbol of G, p being Element of (f.n)* such that
A20:      dt = [o, NTV(o, p)]-tree p and
A21:      ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
          by A18;
          reconsider p as FinSequence of FinTrees SxD by A21;
A22:      dom dt = tree(doms p) by A20,TREES_4:10;
          now
            let t be finite Tree;
            assume t in rng doms p;
            then consider k being set such that
A23:        k in dom doms p and
A24:        t = (doms p).k by FUNCT_1:def 3;
A25:        k in dom p by A23,TREES_3:37;
            then
A26:        p.k in rng p by FUNCT_1:def 3;
            rng p c=FinTrees SxD by FINSEQ_1:def 4;
            then reconsider pk = p.k as Element of FinTrees SxD by A26;
A27:        rng p c= f.n by FINSEQ_1:def 4;
A28:        t = dom pk by A24,A25,FUNCT_6:22;
            pk in Union f by A1,A26,A27,CARD_5:2;
            hence height t <= n by A16,A26,A27,A28;
          end;
          hence height dom dt <= n+1 by A22,TREES_3:77;
        end;
      end;
      assume
A29:  height dom dt <= n+1;
      defpred P[Nat] means dt in f.$1;
      ex k being set st ( k in NAT)&( dt in f.k) by A1,A17,CARD_5:2;
      then
A30:  ex k being Nat st P[k];
      consider mk being Nat such that
A31:  P[mk] & for kk being Nat st P[kk] holds mk <= kk from NAT_1:sch 5(A30);
      deffunc F(set,set) = { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
      where o is Symbol of G(), p is Element of (f.$1)* :
      ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
      p = q & o ==> pr1 roots q };
A32:  for n being Element of NAT holds f.n c= f.(n+1)
      proof
        let n be Element of NAT;
        f.(n+1) = f.n \/ F(n, f.n) by A3;
        hence thesis by XBOOLE_1:7;
      end;
      per cases by NAT_1:6;
      suppose mk = 0;
        then f.mk c= f.(0+(n+1)) by A32,MEASURE2:18;
        hence thesis by A31;
      end;
      suppose ex k being Nat st mk = k+1;
        then consider k being Nat such that
A33:    mk = k+1;
        reconsider k as Element of NAT by ORDINAL1:def 12;
A34:    k < k+1 by NAT_1:13;
        f.mk = f.k \/ {[o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.k)* :
        ex q being FinSequence of FinTrees SxD st
        p = q & o ==> pr1 roots q } by A3,A33;
        then dt in f.k or dt in {[o, NTV(o, p)]-tree p
        where o is Symbol of G, p is Element of (f.k)* :
        ex q being FinSequence of FinTrees SxD st p = q & o ==>
        pr1 roots q } by A31,XBOOLE_0:def 3;
        then consider o being Symbol of G, p being Element of (f.k)* such that
A35:    dt = [o, NTV(o, p)]-tree p and
A36:    ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
        by A31,A33,A34;
        reconsider p as FinSequence of FinTrees SxD by A36;
A37:    dom dt = tree(doms p) by A35,TREES_4:10;
        rng p c= f.n
        proof
          let x be set;
          assume x in rng p;
          then consider k9 being set such that
A38:      k9 in dom p and
A39:      x = p.k9 by FUNCT_1:def 3;
A40:      x in rng p by A38,A39,FUNCT_1:def 3;
          rng p c= FinTrees SxD by FINSEQ_1:def 4;
          then reconsider t = x as Element of FinTrees SxD by A40;
A41:      k9 in dom doms p by A38,A39,FUNCT_6:22;
          dom t = (doms p).k9 by A38,A39,FUNCT_6:22;
          then dom t in rng doms p by A41,FUNCT_1:def 3;
          then height dom t < n+1 by A29,A37,TREES_3:78,XXREAL_0:2;
          then
A42:      height dom t <= n by NAT_1:13;
A43:      rng p c= f.k by FINSEQ_1:def 4;
          t in rng p by A38,A39,FUNCT_1:def 3;
          then t in Union f by A1,A43,CARD_5:2;
          hence thesis by A16,A42;
        end;
        then p is FinSequence of f.n by FINSEQ_1:def 4;
        then reconsider p as Element of (f.n)* by FINSEQ_1:def 11;
        [o, NTV(o, p)]-tree p in {[oo, NTV(oo, pp)]-tree pp
        where oo is Symbol of G, pp is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        pp = q & oo ==> pr1 roots q } by A36;
        then dt in f.n \/ {[oo, NTV(oo, pp)]-tree pp
        where oo is Symbol of G, pp is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        pp = q & oo ==> pr1 roots q } by A35,XBOOLE_0:def 3;
        hence thesis by A3;
      end;
    end;
  end;
  thus for n being Element of NAT holds R[n] from NAT_1:sch 1 (A4, A15
  );
end;

scheme DTCUniq { f() -> Function,
  G() -> non empty DTConstrStr, D() -> non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
  for dt1, dt2 being DecoratedTree of [:(the carrier of G()), D():]
  st dt1 in Union f() & dt2 in Union f() & dt1`1 = dt2`1 holds dt1 = dt2
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Element of NAT holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
  set f = f();
  set G = G();
  set D = D();
  set S = the carrier of G;
  set SxD = [:S, D:];
  deffunc
  NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
  A4: f
().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
  t in Terminals G() & d = TermVal(t) or
  t ==> {} & d = NTermVal(t, {}, {}) } by A2;
A5: for n being Element of NAT holds f().(n+1) =
  f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G(), p is Element of (f().n)* :
  ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
  p = q & o ==> pr1 roots q } by A3;
  defpred R[Element of NAT] means for dt1, dt2 being DecoratedTree of SxD
  st dt1 in f.$1 & dt2 in f.$1 & dt1`1 = dt2`1 holds dt1 = dt2;
A6: R[0]
  proof
    let dt1,dt2 be DecoratedTree of SxD;
    assume that
A7: dt1 in f.0 and
A8: dt2 in f.0 and
A9: dt1`1 = dt2`1;
    consider t1 being Symbol of G, d1 being Element of D such that
A10: dt1= root-tree [t1, d1] and
A11: t1 in Terminals G & d1 = TermVal(t1) or t1 ==> {} & d1 = NTermVal(
    t1, {}, {})
    by A2,A7;
    consider t2 being Symbol of G, d2 being Element of D such that
A12: dt2= root-tree [t2, d2] and
A13: t2 in Terminals G & d2 = TermVal(t2) or t2 ==> {} & d2 = NTermVal(
    t2, {}, {})
    by A2,A8;
A14: root-tree t1 = dt1`1 by A10,TREES_4:25;
    root-tree t2 = dt2`1 by A12,TREES_4:25;
    then
A15: t1 = t2 by A9,A14,TREES_4:4;
    now
      let t be Symbol of G;
      assume t ==> {};
      then not ex t9 being Symbol of G st t=t9 &
      not ex tnt being FinSequence st t9 ==> tnt;
      then not t in {t9 where t9 is Symbol of G:
      not ex tnt being FinSequence st t9 ==> tnt };
      hence not t in Terminals G by LANG1:def 2;
    end;
    hence thesis by A10,A11,A12,A13,A15;
  end;
A16: now
    let n be Element of NAT such that
A17: R[n];
    thus R[n+1]
    proof
      let dt1, dt2 be DecoratedTree of SxD;
      assume that
A18:  dt1 in f.(n+1) and
A19:  dt2 in f.(n+1) and
A20:  dt1`1 = dt2`1;
A21:  dom dt1 = dom dt1`1 by TREES_4:24;
A22:  dom dt2 = dom dt1`1 by A20,TREES_4:24;
A23:  dt1 in Union f by A1,A18,CARD_5:2;
A24:  dt2 in Union f by A1,A19,CARD_5:2;
      ex X being Subset of FinTrees [:the carrier of G(), D():]
      st X = Union f() & (for d being Symbol of G() st d in Terminals G()
      holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G(),
      p being FinSequence of X st o ==> pr1 roots p
      holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
      for F being Subset of FinTrees [:the carrier of G(), D():] st
      (for d being Symbol of G() st d in Terminals G()
      holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G(),
      p being FinSequence of F st o ==> pr1 roots p
      holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
      holds X c= F from DTCMin(A1, A4, A5);
      then reconsider dt19 = dt1, dt29 = dt2 as Element of FinTrees SxD
      by A23,A24;
A25:  for n being Element of NAT,
      dt being Element of FinTrees [:the carrier of G(), D():]
      st dt in Union f() holds dt in f().n iff height dom dt <= n
      from DTCHeight (A1, A4, A5);
      per cases;
      suppose
A26:    dt1 in f.n;
        then height dom dt19 <= n by A23,A25;
        then dt29 in f.n by A21,A22,A24,A25;
        hence thesis by A17,A20,A26;
      end;
      suppose
A27:    not dt1 in f.n;
A28:    f.(n+1) = f.n \/ {[o1, NTV(o1, p1)]-tree p1
        where o1 is Symbol of G, p1 is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        p1 = q & o1 ==> pr1 roots q } by A3;
        then dt1 in f.n or dt1 in {[o1, NTV(o1, p1)]-tree p1
        where o1 is Symbol of G, p1 is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st p1 = q & o1 ==>
        pr1 roots q } by A18,XBOOLE_0:def 3;
then consider o1 being Symbol of G, p1 being Element of (f.n)* such that
A29:    dt1 = [o1, NTV(o1, p1)]-tree p1 and
A30:    ex q being FinSequence of FinTrees SxD st p1 = q & o1 ==> pr1 roots q
        by A27;
        height dom dt19 > n by A23,A25,A27;
        then
A31:    not dt29 in f.n by A21,A22,A24,A25;
        dt2 in f.n or dt2 in {[o2, NTV(o2, p2)]-tree p2
        where o2 is Symbol of G, p2 is Element of (f.n)* :
        ex q being FinSequence of FinTrees SxD st
        p2 = q & o2 ==> pr1 roots q } by A19,A28,XBOOLE_0:def 3;
then consider o2 being Symbol of G, p2 being Element of (f.n)* such that
A32:    dt2 = [o2, NTV(o2, p2)]-tree p2 and
A33:    ex q being FinSequence of FinTrees SxD st p2 = q & o2 ==> pr1 roots q
        by A31;
        reconsider p1 as FinSequence of FinTrees SxD by A30;
        consider p11 being FinSequence of FinTrees S such that
A34:    dom p11 = dom p1 and
A35:    for i being Element of NAT st i in dom p1 holds ex T being Element
        of FinTrees SxD st T = p1.i & p11.i = T`1 and
A36:    ([o1, NTV(o1,p1)]-tree p1)`1 = o1-tree p11 by TREES_4:31;
        reconsider p2 as FinSequence of FinTrees SxD by A33;
        consider p21 being FinSequence of FinTrees S such that
A37:    dom p21 = dom p2 and
A38:    for i being Element of NAT st i in dom p2 holds ex T being Element
        of FinTrees SxD st T = p2.i & p21.i = T`1 and
A39:    ([o2, NTV(o2,p2)]-tree p2)`1 = o2-tree p21 by TREES_4:31;
A40:    o1 = o2 by A20,A29,A32,A36,A39,TREES_4:15;
A41:    p11 = p21 by A20,A29,A32,A36,A39,TREES_4:15;
        now
          let k be Nat;
          assume
A42:      k in dom p11;
          then consider p1k being Element of FinTrees SxD such that
A43:      p1k = p1.k and
A44:      p11.k = p1k`1 by A34,A35;
          consider p2k being Element of FinTrees SxD such that
A45:      p2k = p2.k and
A46:      p21.k = p2k`1 by A37,A38,A41,A42;
A47:      p1k in f.n by A34,A42,A43,Th2;
          p2k in f.n by A37,A41,A42,A45,Th2;
          hence p1.k = p2.k by A17,A41,A43,A44,A45,A46,A47;
        end;
        then p1 = p2 by A34,A37,A41,FINSEQ_1:13;
        hence thesis by A29,A32,A40;
      end;
    end;
  end;
A48: for n be Element of NAT holds R[n] from NAT_1:sch 1 (A6, A16);
  let dt1, dt2 be DecoratedTree of SxD;
  assume that
A49: dt1 in Union f and
A50: dt2 in Union f and
A51: dt1`1 = dt2`1;
  consider n1 being set such that
A52: n1 in NAT and
A53: dt1 in f.n1 by A1,A49,CARD_5:2;
  consider n2 being set such that
A54: n2 in NAT and
A55: dt2 in f.n2 by A1,A50,CARD_5:2;
  reconsider n1, n2 as Element of NAT by A52,A54;
  deffunc F(set,set) = { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G(), p is Element of (f.$1)* :
  ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
  p = q & o ==> pr1 roots q };
A56: for n being Element of NAT holds f.n c= f.(n+1)
  proof
    let n be Element of NAT;
    f.(n+1) = f.n \/ F(n, f.n) by A3;
    hence thesis by XBOOLE_1:7;
  end;
A57: for k, s being Nat holds f.k c= f.(k+s)
  proof
    let k, s be Nat;
    reconsider k, s as Element of NAT by ORDINAL1:def 12;
    k <= k+s by NAT_1:11;
    hence thesis by A56,MEASURE2:18;
  end;
  n1 <= n2 or n1 >= n2;
  then (ex s being Nat st n2 = n1 + s) or
  ex s being Nat st n1 = n2 + s by NAT_1:10;
  then f.n1 c= f.n2 or f.n2 c= f.n1 by A57;
  hence thesis by A48,A51,A53,A55;
end;

definition
  let G be non empty DTConstrStr;

  func TS(G) -> Subset of FinTrees(the carrier of G) means
  :Def1:
  (for d being Symbol of G st d in Terminals G holds root-tree d in it) &
  (for o being Symbol of G, p being FinSequence of it st o ==> roots p
  holds o-tree p in it) & for F being Subset of FinTrees the carrier of G st
  (for d being Symbol of G st d in Terminals G holds root-tree d in F) &
  (for o being Symbol of G, p being FinSequence of F st o ==> roots p
  holds o-tree p in F) holds it c= F;
  existence
  proof
    deffunc F(set,set) = $2 \/ { [o, A(o,pr1 roots p,pr2 roots p)]-tree p
    where o is Symbol of G, p is Element of $2* :
    ex q being FinSequence of FinTrees [:the carrier of G, NAT:] st
    p = q & o ==> pr1 roots q };
    consider f being Function such that
A1: dom f = NAT and
A2: f.0 = { root-tree [t, d] where t is Symbol of G, d is Element of NAT :
    t in Terminals G & d = T(t) or t ==> {} & d = A(t,{},{}) } and
A3: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A4: for n being Element of NAT holds f.(n+1) =
    f.n \/ { [o, A(o, pr1 roots p, pr2 roots p)]-tree p
    where o is Symbol of G, p is Element of (f.n)* :
    ex q being FinSequence of FinTrees [:the carrier of G, NAT:] st
    p = q & o ==> pr1 roots q } by A3;
    ex X1 being Subset of FinTrees(the carrier of G) st
    X1 = { t`1 where t is Element of FinTrees [:(the carrier of G), NAT:] :
    t in Union f }
    & (for d being Symbol of G st d in Terminals G holds root-tree d in X1)
    & (for o being Symbol of G, p being FinSequence of X1 st o ==> roots p
    holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G st
    (for d being Symbol of G st d in Terminals G holds root-tree d in F)
    & (for o being Symbol of G, p being FinSequence of F st o ==> roots p
    holds o-tree p in F) holds X1 c= F from DTCSymbols (A1, A2, A4);
    hence thesis;
  end;
  uniqueness
  proof
    let TSG1, TSG2 be Subset of FinTrees(the carrier of G);
    assume
A5: not thesis;
    then
A6: TSG1 c= TSG2;
    TSG2 c= TSG1 by A5;
    hence contradiction by A5,A6,XBOOLE_0:def 10;
  end;
end;

scheme DTConstrInd{ G()->non empty DTConstrStr, P[set] }:
  for t being DecoratedTree of the carrier of G() st t in TS(G()) holds P[t]
provided
A1: for s being Symbol of G() st s in Terminals G() holds P[root-tree s] and
A2: for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts &
for t being DecoratedTree of the carrier of G() st t in rng ts holds P[t]
holds P[nt-tree ts]
proof
  deffunc F(set,set) =
  $2 \/ { [o, 0]-tree p where o is Symbol of G(), p is Element of $2* :
  ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
  p = q & o ==> pr1 roots q };
  consider f being Function such that
A3: dom f = NAT and
A4: f.0 = { root-tree [t, d] where t is Symbol of G(), d is Element of NAT :
  t in Terminals G() & d = T(t) or t ==> {} & d = A(t,{},{}) } and
A5: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A6: for n being Element of NAT holds f.(n+1) =
  f.n \/ { [o, A(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G(), p is Element of (f.n)* :
  ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
  p = q & o ==> pr1 roots q } by A5;
  A7: ex
 X being Subset of FinTrees [:the carrier of G(), NAT:] st X = Union f &
  (for d being Symbol of G() st d in Terminals G()
  holds root-tree [d, T(d)] in X) & (for o being Symbol of G(),
  p being FinSequence of X st o ==> pr1 roots p
  holds [o, A(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
  for F being Subset of FinTrees [:the carrier of G(), NAT:] st
  (for d being Symbol of G() st d in Terminals G()
  holds root-tree [d, T(d)] in F ) & (for o being Symbol of G(),
  p being FinSequence of F st o ==> pr1 roots p
  holds [o, A(o, pr1 roots p, pr2 roots p)]-tree p in F)
  holds X c= F from DTCMin (A3,A4,A6);
  consider TSG being Subset of FinTrees(the carrier of G()) such that
A8: TSG = { t`1 where t is Element of FinTrees [:(the carrier of G()), NAT:]
  : t in Union f } and
A9: for d being Symbol of G() st d in Terminals G()
  holds root-tree d in TSG and
A10: for o being Symbol of G(), p being FinSequence of TSG st o ==> roots p
  holds o-tree p in TSG and
A11: for F being Subset of FinTrees the carrier of G() st
  (for d being Symbol of G() st d in Terminals G() holds root-tree d in F)
  & (for o being Symbol of G(), p being FinSequence of F st o ==> roots p
  holds o-tree p in F) holds TSG c= F from DTCSymbols (A3, A4, A6);
A12: TSG = TS(G()) by A9,A10,A11,Def1;
  defpred R[Element of NAT] means
  for t being DecoratedTree of [:the carrier of G(), NAT:]
  st t in f.$1 holds P[t`1];
A13: R[0]
  proof
    let tt be DecoratedTree of [:the carrier of G(),NAT:];
    set p = <*>TS G();
    assume tt in f.0;
    then consider t being Symbol of G(), d being Element of NAT such that
A14: tt = root-tree [t, d] and
A15: t in Terminals G() & d = 0 or t ==> roots p & d = 0 by A4,Th3;
A16: tt`1 = root-tree t by A14,TREES_4:25;
A17: t-tree p = root-tree t by TREES_4:20;
    for T being DecoratedTree of the carrier of G() st T in rng p holds P[T];
    hence thesis by A1,A2,A15,A16,A17;
  end;
A18: now
    let n be Element of NAT;
    assume
A19: R[n];
    thus R[n+1]
    proof
      let x be DecoratedTree of [:the carrier of G(), NAT:];
      assume that
A20:  x in f.(n+1) and
A21:  not P[x`1];
      x in f.n \/ {[o, 0]-tree p where o is Symbol of G(),
      p is Element of (f.n)* :
      ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
      p = q & o ==> pr1 roots q } by A5,A20;
      then x in f.n or x in {[o, 0]-tree p where o is Symbol of G(),
      p is Element of (f.n)* :
      ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
      p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
      then consider o being Symbol of G(), p being Element of (f.n)* such that
A22:  x = [o, 0]-tree p and
A23:  ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st p
      = q & o ==> pr1 roots q
      by A19,A21;
A24:  Union f=union rng f by CARD_3:def 4;
A25:  f.n in rng f by A3,FUNCT_1:def 3;
A26:  rng p c= f.n by FINSEQ_1:def 4;
A27:  f.n c= Union f by A24,A25,ZFMISC_1:74;
A28:  dom p = Seg len p by FINSEQ_1:def 3;
      defpred P[set,set] means
      ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
      dt = p.$1 & dt`1 = $2 & dt in Union f;
A29:  for k being Nat st k in Seg len p
      ex x being Element of FinTrees the carrier of G() st P[k,x]
      proof
        let k be Nat;
        assume k in Seg len p;
        then
A30:    p.k in rng p by A28,FUNCT_1:def 3;
A31:    rng p c= Union f by A26,A27,XBOOLE_1:1;
        then p.k in Union f by A30;
        then reconsider dt = p.k as
        Element of FinTrees [:(the carrier of G()), NAT:] by A7;
A32:    dt`1 = pr1(the carrier of G(), NAT) * dt by TREES_3:def 12;
A33:    rng dt c= [:the carrier of G(), NAT:] by RELAT_1:def 19;
        dom pr1(the carrier of G(), NAT) = [:the carrier of G(), NAT:] by
FUNCT_2:def 1;
        then dom dt`1 = dom dt by A32,A33,RELAT_1:27;
        then reconsider x = dt`1 as Element of FinTrees the carrier of G()
        by TREES_3:def 8;
        take x, dt;
        thus thesis by A30,A31;
      end;
      consider p1 being FinSequence of FinTrees the carrier of G() such that
A34:  dom p1 = Seg len p and
A35:  for k being Nat st k in Seg len p holds P[k,p1.k]
      from FINSEQ_1:sch 5(A29);
      reconsider p as FinSequence of Trees [:the carrier of G(), NAT:]
      by A23,Th1;
A36:  dom roots p1 = dom p1 by TREES_3:def 18;
A37:  dom pr1 roots p = dom roots p by MCART_1:def 12;
      then
A38:  dom pr1 roots p = dom p1 by A28,A34,TREES_3:def 18;
      now
        let k be Nat;
        assume
A39:    k in dom p1;
        then consider dt being Element of FinTrees [:the carrier of G(), NAT:]
        such that
A40:    dt = p.k and
A41:    dt`1 = p1.k and dt in Union f by A34,A35;
        reconsider r = {} as Node of dt by TREES_1:22;
        ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{}
        by A39,TREES_3:def 18;
        then
A42:    (roots p1).k = (dt.r)`1 by A41,TREES_3:39;
        ex T being DecoratedTree st T = p.k & (roots p).k = T.{}
        by A28,A34,A39,TREES_3:def 18;
        hence (roots p1).k = (pr1 roots p).k
        by A37,A38,A39,A40,A42,MCART_1:def 12;
      end;
      then
A43:  roots p1 = pr1 roots p by A36,A38,FINSEQ_1:13;
      rng p1 c= TS(G())
      proof
        let x be set;
        assume x in rng p1;
        then consider k being set such that
A44:    k in dom p1 and
A45:    x = p1.k by FUNCT_1:def 3;
        reconsider k as Element of NAT by A44;
        ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
        dt = p.k & dt`1 = p1.k & dt in Union f by A34,A35,A44;
        hence thesis by A8,A12,A45;
      end;
      then reconsider p1 as FinSequence of TS(G()) by FINSEQ_1:def 4;
      now
        let t be DecoratedTree of the carrier of G();
        assume t in rng p1;
        then consider k being set such that
A46:    k in dom p1 and
A47:    t = p1.k by FUNCT_1:def 3;
        reconsider k as Element of NAT by A46;
A48:    ex dt being Element of FinTrees [:the carrier of G(), NAT:]
        st ( dt = p.k)&( dt`1 = p1.k)&( dt in Union f) by A34,A35,A46;
        p.k in rng p by A28,A34,A46,FUNCT_1:def 3;
        hence P[t] by A19,A26,A47,A48;
      end;
      then
A49:  P[o-tree p1] by A2,A23,A43;
      reconsider p1 as FinSequence of Trees the carrier of G() by Th1;
      now
        let k be Element of NAT;
        assume k in dom p;
        then ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
        dt = p.k & dt`1 = p1.k & dt in Union f by A28,A35;
        hence for T being DecoratedTree of [:the carrier of G(), NAT:] st
        T = p.k holds p1.k = T`1;
      end;
      hence contradiction by A21,A22,A28,A34,A49,TREES_4:27;
    end;
  end;
A50: for n being Element of NAT holds R[n] from NAT_1:sch 1 (A13, A18);
  let t be DecoratedTree of the carrier of G();
  assume t in TS(G());
  then consider tt being Element of FinTrees[:the carrier of G(), NAT:] such
  that
A51: t = tt`1 and
A52: tt in Union f by A8,A12;
  ex n being set st n in NAT & tt in f.n by A3,A52,CARD_5:2;
  hence thesis by A50,A51;
end;

scheme DTConstrIndDef{G()->non empty DTConstrStr, D()->non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D() }:
  ex f being Function of TS(G()), D() st
  (for t being Symbol of G() st t in Terminals G()
  holds f.(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
  ts being FinSequence of TS(G()) st nt ==> roots ts
  holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts)
proof
  set G = G();
  deffunc
  NTV(Symbol of G, FinSequence) = NTermVal($1, pr1 roots $2, pr2 roots $2);
deffunc F(set,set) = $2 \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G, p is Element of $2* :
  ex q being FinSequence of FinTrees [:the carrier of G, D():] st
  p = q & o ==> pr1 roots q };
  consider f being Function such that
A1: dom f = NAT and
A2: f.0 = { root-tree [t, d] where t is Symbol of G, d is Element of D() :
  t in Terminals G & d = TermVal(t) or
  t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A4: for n being Element of NAT holds f.(n+1) =
  f.n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
  where o is Symbol of G, p is Element of (f.n)* :
  ex q being FinSequence of FinTrees [:the carrier of G, D():] st
  p = q & o ==> pr1 roots q } by A3;
  ex X1 being Subset of FinTrees(the carrier of G) st
  X1 = { t`1 where t is Element of FinTrees [:(the carrier of G), D():] :
  t in Union f }
  & (for d being Symbol of G st d in Terminals G holds root-tree d in X1)
  & (for o being Symbol of G, p being FinSequence of X1 st o ==> roots p
  holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G st
  (for d being Symbol of G st d in Terminals G holds root-tree d in F)
  & (for o being Symbol of G, p being FinSequence of F st o ==> roots p
  holds o-tree p in F) holds X1 c= F from DTCSymbols (A1, A2, A4);
  then
A5: TS(G) = { t`1 where t is Element of FinTrees [:(the carrier of G), D
  ():] : t in Union f } by Def1;
  defpred P[set,set] means
  for dt being DecoratedTree of [:(the carrier of G), D():]
  st dt in Union f & $1 = dt`1 holds $2 = (dt`2).{};
A6: for e being set st e in TS(G) ex u being set st u in D() & P[e,u]
  proof
    let e be set;
    assume e in TS(G);
    then consider DT being Element of FinTrees [:(the carrier of G), D():]
    such that
A7: e = DT`1 and
A8: DT in Union f by A5;
    reconsider r = {} as Node of DT`2 by TREES_1:22;
    take u = (DT`2).r;
    thus u in D();
A9: for dt1, dt2 being DecoratedTree of [:(the carrier of G), D():]
    st dt1 in Union f & dt2 in Union f & dt1`1 = dt2`1 holds dt1 = dt2
    from DTCUniq (A1, A2, A4);
    let dt be DecoratedTree of [:(the carrier of G), D():];
    assume that
A10: dt in Union f and
A11: e = dt`1;
    thus thesis by A7,A8,A9,A10,A11;
  end;
  consider ff being Function such that
A12: dom ff = TS(G) & rng ff c= D() and
A13: for e being set st e in TS(G) holds P[e,ff.e] from FUNCT_1:sch 5(A6);
  reconsider ff as Function of TS(G), D() by A12,FUNCT_2:def 1,RELSET_1:4;
  take ff;
  consider X be Subset of FinTrees [:the carrier of G, D():] such that
A14: X = Union f and
A15: for d being Symbol of G st d in Terminals G
  holds root-tree [d, TermVal(d)] in X and
A16: for o being Symbol of G, p being FinSequence of X st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X and
  for F being Subset of FinTrees [:the carrier of G, D():] st
  (for d being Symbol of G st d in Terminals G
  holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G,
  p being FinSequence of F st o ==> pr1 roots p
  holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
  holds X c= F from DTCMin (A1, A2, A4);
  hereby
    let t be Symbol of G;
    assume
A17: t in Terminals G;
A18: (root-tree [t, TermVal(t)])`1 = root-tree t by TREES_4:25;
A19: (root-tree [t, TermVal(t)])`2 = root-tree TermVal(t) by TREES_4:25;
    root-tree [t, TermVal(t)] in Union f by A14,A15,A17;
    then root-tree t in TS(G) by A5,A18;
    hence ff.(root-tree t) = (root-tree TermVal(t)).{} by A13,A14,A15,A17,A18
,A19
      .= TermVal(t) by TREES_4:3;
  end;
  let nt be Symbol of G, ts be FinSequence of TS(G);
  set rts = roots ts;
  assume
A20: nt ==> rts;
  set x = ff * ts;
A21: dom ts = Seg len ts by FINSEQ_1:def 3;
  defpred P[set,set] means
  ex dt being DecoratedTree of [:the carrier of G, D():] st
  dt = $2 & dt`1 = ts.$1 & dt in Union f;
A22: for k being Nat st k in Seg len ts
  ex x being Element of FinTrees [:(the carrier of G), D():] st P[k,x]
  proof
    let k be Nat;
    assume k in Seg len ts;
    then
A23: ts.k in rng ts by A21,FUNCT_1:def 3;
    rng ts c= TS(G) by FINSEQ_1:def 4;
    then ts.k in TS(G) by A23;
    then ex x being Element of FinTrees [:(the carrier of G), D():] st
    ts.k = x`1 & x in Union f by A5;
    hence thesis;
  end;
  consider dts being FinSequence of FinTrees [:(the carrier of G), D():]
  such that
A24: dom dts = Seg len ts and
A25: for k being Nat st k in Seg len ts holds P[k,dts.k]
  from FINSEQ_1:sch 5(A22);
  rng dts c= X
  proof
    let x be set;
    assume x in rng dts;
    then consider k being set such that
A26: k in dom ts and
A27: x = dts.k by A21,A24,FUNCT_1:def 3;
    reconsider k as Element of NAT by A26;
    ex dt being DecoratedTree of [:the carrier of G, D():]
    st dt = x & dt`1 = ts.k & dt in Union f by A21,A25,A26,A27;
    hence thesis by A14;
  end;
  then reconsider dts as FinSequence of X by FINSEQ_1:def 4;
A28: dom roots ts = dom ts by TREES_3:def 18;
A29: dom pr1 roots dts = dom roots dts by MCART_1:def 12;
A30: dom pr2 roots dts = dom roots dts by MCART_1:def 13;
A31: dom pr1 roots dts = dom ts by A21,A24,A29,TREES_3:def 18;
A32: dom pr2 roots dts = dom ts by A21,A24,A30,TREES_3:def 18;
  now
    let k be Nat;
    assume
A33: k in dom ts;
    then consider dt being DecoratedTree of [:the carrier of G, D():]
    such that
A34: dt = dts.k and
A35: dt`1 = ts.k and dt in Union f by A21,A25;
    reconsider r = {} as Node of dt by TREES_1:22;
    ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{}
    by A33,TREES_3:def 18;
    then
A36: (roots ts).k = (dt.r)`1 by A35,TREES_3:39;
    ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{}
    by A21,A24,A33,TREES_3:def 18;
    hence (roots ts).k = (pr1 roots dts).k
    by A29,A31,A33,A34,A36,MCART_1:def 12;
  end;
  then
A37: roots ts = pr1 roots dts by A28,A31,FINSEQ_1:13;
  then
A38: [nt, NTV(nt, dts)]-tree dts in X by A16,A20;
A39: rng dts c= FinTrees [:the carrier of G, D():] by FINSEQ_1:def 4;
  FinTrees [:the carrier of G,D():] c= Trees [:the carrier of G, D():]
  by TREES_3:21;
  then rng dts c= Trees [:the carrier of G, D():] by A39,XBOOLE_1:1;
  then reconsider dts9 = dts as FinSequence of Trees [:the carrier of G,D():]
  by FINSEQ_1:def 4;
A40: rng ts c= FinTrees the carrier of G by FINSEQ_1:def 4;
  FinTrees the carrier of G c= Trees the carrier of G by TREES_3:21;
  then rng ts c= Trees the carrier of G by A40,XBOOLE_1:1;
  then reconsider ts9 = ts as FinSequence of Trees the carrier of G
  by FINSEQ_1:def 4;
  now
    let i be Element of NAT;
    assume i in dom dts;
    then
A41: ex dt being DecoratedTree of [:the carrier of G, D():] st (
    dt = dts.i)&( dt`1 = ts.i)&( dt in Union f) by A24,A25;
    let T be DecoratedTree of [:the carrier of G, D():];
    assume T = dts.i;
    hence ts.i = T`1 by A41;
  end;
  then
A42: ([nt, NTV(nt, dts)]-tree dts9)`1 = nt-tree ts9 by A21,A24,TREES_4:27;
A43: rng ts c= dom ff by A12,FINSEQ_1:def 4;
  then
A44: dom (ff * ts) = dom ts by RELAT_1:27;
  now
    let k be Nat;
    assume
A45: k in dom ts;
    then consider dt being DecoratedTree of [:the carrier of G, D():] such
    that
A46: dt = dts.k and
A47: dt`1 = ts.k and
A48: dt in Union f by A21,A25;
    reconsider r = {} as Node of dt by TREES_1:22;
A49: ts.k in rng ts by A45,FUNCT_1:def 3;
A50: x.k = ff.(dt`1) by A44,A45,A47,FUNCT_1:12
      .= dt`2.{} by A12,A13,A43,A47,A48,A49
      .= (dt.r)`2 by TREES_3:39;
    ex T being DecoratedTree st T = dts.k & (roots dts).k = T.r
    by A21,A24,A45,TREES_3:def 18;
    hence x.k = (pr2 roots dts).k by A29,A31,A45,A46,A50,MCART_1:def 13;
  end;
  then
A51: x = pr2 roots dts by A32,A44,FINSEQ_1:13;
  reconsider r = {} as Node of [nt, NTermVal(nt, rts, x)]-tree dts
  by TREES_1:22;
  nt-tree ts in TS(G) by A5,A14,A38,A42;
  then ff.(nt-tree ts) = (([nt, NTermVal(nt, rts, x)]-tree dts)`2).r
  by A13,A14,A16,A20,A37,A42,A51
    .= (([nt, NTermVal(nt, rts, x)]-tree dts).r)`2 by TREES_3:39
    .= [nt, NTermVal(nt, rts, x)]`2 by TREES_4:def 4;
  hence thesis;
end;

scheme DTConstrUniqDef{G()->non empty DTConstrStr, D()->non empty set,
  TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D(),
  f1, f2() -> Function of TS(G()), D() }: f1() = f2()
provided
A1: (for t being Symbol of G() st t in Terminals G()
holds f1().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f1().(nt-tree ts) = NTermVal(nt, roots ts, f1() * ts) and
A2: (for t being Symbol of G() st t in Terminals G()
holds f2().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f2().(nt-tree ts) = NTermVal(nt, roots ts, f2() * ts)
proof
  set G = G();
  defpred P[set] means f1().$1 = f2().$1;
A3: now
    let s be Symbol of G;
    assume
A4: s in Terminals G;
    then f1().(root-tree s) = TermVal(s) by A1
      .= f2().(root-tree s) by A2,A4;
    hence P[root-tree s];
  end;
A5: now
    let nt be Symbol of G, ts be FinSequence of TS(G);
    assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of G st t in rng ts holds P [t];
A8: rng ts c= TS(G) by FINSEQ_1:def 4;
    then rng ts c= dom f1() by FUNCT_2:def 1;
    then
A9: dom (f1() * ts) = dom ts by RELAT_1:27;
    reconsider ntv1 = f1() * ts as FinSequence;
    reconsider ntv1 as FinSequence of D();
    rng ts c= dom f2() by A8,FUNCT_2:def 1;
    then
A10: dom (f2() * ts) = dom ts by RELAT_1:27;
    now
      let x be set;
      assume
A11:  x in dom ts;
      then reconsider t =ts.x as Element of FinTrees the carrier of G by Th2;
      t in rng ts by A11,FUNCT_1:def 3;
      then
A12:  f1().t = f2().t by A7;
      thus (f1() * ts).x = f1().t by A9,A11,FUNCT_1:12
        .= (f2() * ts).x by A10,A11,A12,FUNCT_1:12;
    end;
    then
A13: f1() * ts = f2() * ts by A9,A10,FUNCT_1:2;
    f1().(nt-tree ts) = NTermVal (nt, roots ts, ntv1) by A1,A6
      .= f2().(nt-tree ts) by A2,A6,A13;
    hence P[nt-tree ts];
  end;
 for t being DecoratedTree of the carrier of G st t in TS(G)
  holds P[t] from DTConstrInd (A3,A5);
   then for x being set st x in TS(G) holds f1().x = f2().x;
  hence thesis by FUNCT_2:12;
end;

begin

:: Peano naturals: an example of a decorated tree construction

defpred P[set,set] means $1=1 & ($2=<*0*> or $2=<*1*>);

definition
  func PeanoNat -> strict non empty DTConstrStr means
  :Def2:
  the carrier of it = {0, 1} &
  for x being Symbol of it, y being FinSequence of the carrier of it
  holds x ==> y iff x=1 & (y=<*0*> or y=<*1*>);
  existence
  proof
    thus
    ex G be strict non empty DTConstrStr st the carrier of G = {0,1} &
    for x being Symbol of G, p being FinSequence of the carrier of G
    holds x ==> p iff P[x, p] from DTConstrStrEx;
  end;
  uniqueness
  proof
    thus for G1, G2 being strict non empty DTConstrStr
    st (the carrier of G1 = {0,1} &
    for x being Symbol of G1, p being FinSequence of the carrier of G1
    holds x ==> p iff P[x, p]) & (the carrier of G2 = {0,1} &
    for x being Symbol of G2, p being FinSequence of the carrier of G2
    holds x ==> p iff P[x, p]) holds G1 = G2 from DTConstrStrUniq;
  end;
end;

set PN = PeanoNat;

Lm2: the carrier of PN = {0, 1} by Def2;

then reconsider O = 0 , S = 1 as Symbol of PN by TARSKI:def 2;

Lm3: S ==> <*O*> by Def2;

Lm4: S ==> <*S*> by Def2;

Lm5: S ==> <*O*> by Def2;

Lm6: S ==> <*S*> by Def2;

Lm7: Terminals PN = {x where x is Symbol of PN :
not ex tnt being FinSequence st x ==> tnt } by LANG1:def 2;

Lm8: now
  given x being FinSequence such that
A1: O ==> x;
  [O, x] in the Rules of PN by A1,LANG1:def 1;
  then x in (the carrier of PN)* by ZFMISC_1:87;
  then x is FinSequence of the carrier of PN by FINSEQ_2:def 3;
  hence contradiction by A1,Def2;
end;
then

Lm9: O in Terminals PN by Lm7;

Lm10: Terminals PN c= {O}
proof
  let x be set;
  assume x in Terminals PN;
  then consider y being Symbol of PN such that
A1: x = y and
A2: not ex tnt being FinSequence st y ==> tnt by Lm7;
  y = O or y = S & {O, S} <> {} by Lm2,TARSKI:def 2;
  hence thesis by A1,A2,Lm5,TARSKI:def 1;
end;

Lm11: NonTerminals PN = {x where x is Symbol of PN :
ex tnt being FinSequence st x ==> tnt } by LANG1:def 3;
then

Lm12: S in NonTerminals PN by Lm5;
then

Lm13: {S} c= NonTerminals PN by ZFMISC_1:31;

Lm14: NonTerminals PN c= {S}
proof
  let x be set;
  assume x in NonTerminals PN;
  then consider y being Symbol of PN such that
A1: x = y and
A2: ex tnt being FinSequence st y ==> tnt by Lm11;
  y = O or y = S by Lm2,TARSKI:def 2;
  hence thesis by A1,A2,Lm8,TARSKI:def 1;
end;
then

Lm15: NonTerminals PN = { S } by Lm13,XBOOLE_0:def 10;

reconsider TSPN = TS(PN) as non empty Subset of FinTrees the carrier of PN by
Def1,Lm9;

begin

:: Some properties of decorated tree constructions

definition
  let G be non empty DTConstrStr;
  attr G is with_terminals means
  :Def3:
  Terminals G <> {};
  attr G is with_nonterminals means
  :Def4:
  NonTerminals G <> {};
  attr G is with_useful_nonterminals means
  :Def5:
  for nt being Symbol of G st nt in NonTerminals G
  ex p being FinSequence of TS(G) st nt ==> roots p;
end;

Lm16: PN is with_terminals with_nonterminals with_useful_nonterminals
proof
  thus Terminals PN <> {} by Lm9;
  thus NonTerminals PN <> {} by Lm12;
  reconsider rO = root-tree O as Element of TSPN by Def1,Lm9;
  reconsider p = <*rO qua Element of TSPN qua non empty set*>
  as FinSequence of TSPN;
  reconsider p as FinSequence of TS(PN);
  let nt be Symbol of PN;
  assume nt in NonTerminals PN;
  then
A1: nt = S by Lm14,TARSKI:def 1;
  take p;
A2: dom <*rO*> = Seg 1 by FINSEQ_1:38;
A3: dom <*O*> = Seg 1 by FINSEQ_1:38;
  now
    let i be Element of NAT;
    assume
A4: i in dom p;
    reconsider rO as DecoratedTree;
    take rO;
A5: i = 1 by A2,A4,FINSEQ_1:2,TARSKI:def 1;
    <*O*>.1 = O by FINSEQ_1:40;
    hence rO = p.i & <*O*>.i = rO.{} by A5,FINSEQ_1:40,TREES_4:3;
  end;
  hence thesis by A1,A2,A3,Lm5,TREES_3:def 18;
end;

registration
  cluster with_terminals with_nonterminals with_useful_nonterminals strict
    for non empty DTConstrStr;
  existence by Lm16;
end;

definition
  let G be with_terminals non empty DTConstrStr;
  redefine func Terminals G -> non empty Subset of G;
  coherence
  proof
    defpred P[Element of G] means not ex tnt being FinSequence st $1 ==> tnt;
    { t where t is Element of G : P[t] } c= the carrier of G
    from FRAENKEL:sch 10;
    hence thesis by Def3,LANG1:def 2;
  end;
end;

registration
  let G be with_terminals non empty DTConstrStr;
  cluster TS G -> non empty;
  coherence
  proof
    ex t being set st ( t in Terminals G) by XBOOLE_0:def 1;
    hence thesis by Def1;
  end;
end;

registration
  let G be with_useful_nonterminals non empty DTConstrStr;
  cluster TS G -> non empty;
  coherence
  proof
    set s = the Symbol of G;
    per cases;
    suppose not ex tnt being FinSequence st s ==> tnt;
      then s in {t where t is Symbol of G:
      not ex tnt being FinSequence st t ==> tnt };
      then s in Terminals G by LANG1:def 2;
      hence thesis by Def1;
    end;
    suppose ex tnt being FinSequence st s ==> tnt;
      then s in {t where t is Symbol of G:
      ex tnt being FinSequence st t ==> tnt };
      then s in NonTerminals G by LANG1:def 3;
      then ex p being FinSequence of TS G st ( s ==> roots p) by Def5;
      hence thesis by Def1;
    end;
  end;
end;

definition
  let G be with_nonterminals non empty DTConstrStr;
  redefine func NonTerminals G -> non empty Subset of G;
  coherence
  proof
    defpred P[Element of G] means ex tnt being FinSequence st $1 ==> tnt;
    { t where t is Element of G : P[t]} c= the carrier of G
    from FRAENKEL:sch 10;
    hence thesis by Def4,LANG1:def 3;
  end;
end;

definition
  let G be with_terminals non empty DTConstrStr;
  mode Terminal of G is Element of Terminals G;
end;

definition
  let G be with_nonterminals non empty DTConstrStr;
  mode NonTerminal of G is Element of NonTerminals G;
end;

definition
  let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
  let nt be NonTerminal of G;
  mode SubtreeSeq of nt -> FinSequence of TS(G) means
    :Def6:
    nt ==> roots it;
  existence by Def5;
end;

definition
  let G be with_terminals non empty DTConstrStr;
  let t be Terminal of G;
  redefine func root-tree t -> Element of TS(G);
  coherence by Def1;
end;

definition
  let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
  let nt be NonTerminal of G;
  let p be SubtreeSeq of nt;
  redefine func nt-tree p -> Element of TS(G);
  coherence
  proof
    nt ==> roots p by Def6;
    hence thesis by Def1;
  end;
end;

theorem Th9:
  for G being with_terminals non empty DTConstrStr,
  tsg being Element of TS G, s being Terminal of G
  st tsg.{} = s holds tsg = root-tree s
proof
  let G be with_terminals non empty DTConstrStr, tsg be Element of TS G,
  s be Terminal of G;
  assume
A1: tsg.{} = s;
  defpred P[DecoratedTree of the carrier of G] means
  for s being Terminal of G st $1.{} = s holds $1 = root-tree s;
A2: for s being Symbol of G st s in Terminals G holds P[root-tree s]
  by TREES_4:3;
A3: now
    let nt be Symbol of G, ts be FinSequence of TS G;
    assume that
A4: nt ==> roots ts
    and for t being DecoratedTree of the carrier of G st t in rng ts holds P
    [t];
    thus P[nt-tree ts]
    proof
      let s be Terminal of G;
      assume
A5:   (nt-tree ts).{} = s;
A6:   (nt-tree ts).{} = nt by TREES_4:def 4;
A7:   s in Terminals G;
      Terminals G = { t where t is Symbol of G : not ex tnt being FinSequence
      st t ==> tnt } by LANG1:def 2;
      then ex t being Symbol of G st s = t &
      not ex tnt being FinSequence st t ==> tnt by A7;
      hence thesis by A4,A5,A6;
    end;
  end;
  for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
  from DTConstrInd (A2,A3);
  hence thesis by A1;
end;

theorem Th10:
  for G being with_terminals with_nonterminals non empty DTConstrStr,
  tsg being Element of TS G, nt being NonTerminal of G st tsg.{} = nt
  ex ts being FinSequence of TS G st tsg = nt-tree ts & nt ==> roots ts
proof
  let G be with_terminals with_nonterminals non empty DTConstrStr;
  defpred P[DecoratedTree of the carrier of G] means
  for nt being NonTerminal of G st $1.{} = nt ex ts being FinSequence of TS G
  st $1 = nt-tree ts & nt ==> roots ts;
A1: now
    let s be Symbol of G;
    assume
A2: s in Terminals G;
    thus P[root-tree s]
    proof
      let nt be NonTerminal of G;
      assume (root-tree s).{} = nt;
      then
A3:   s = nt by TREES_4:3;
      Terminals G = { t where t is Symbol of G :
      not ex tnt being FinSequence st t ==> tnt } by LANG1:def 2;
      then
A4:   ex t being Symbol of G st s = t &
      not ex tnt being FinSequence st t ==> tnt by A2;
A5:   nt in NonTerminals G;
      NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence
      st t ==> tnt } by LANG1:def 3;
      then ex t being Symbol of G st nt = t &
      ex tnt being FinSequence st t ==> tnt by A5;
      hence thesis by A3,A4;
    end;
  end;
A6: now
    let nnt be Symbol of G, tts be FinSequence of TS G;
    assume that
A7: nnt ==> roots tts
    and for t being DecoratedTree of the carrier of G st t in rng tts holds
    P[t];
    thus P[nnt-tree tts]
    proof
      let nt be NonTerminal of G;
      assume
A8:   (nnt-tree tts).{} = nt;
      take ts = tts;
      thus thesis by A7,A8,TREES_4:def 4;
    end;
  end;
A9: for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
  from DTConstrInd (A1,A6);
  let tsg be Element of TS G, nt be NonTerminal of G;
  assume tsg.{} = nt;
  hence thesis by A9;
end;

begin

:: Peano naturals continued

registration
  cluster PeanoNat ->
    with_terminals with_nonterminals with_useful_nonterminals;
  coherence by Lm16;
end;

set PN = PeanoNat;
reconsider O as Terminal of PN by Lm9;
reconsider S as NonTerminal of PN by Lm12;

definition
  let nt be NonTerminal of PeanoNat, t be Element of TS PeanoNat;
  redefine func nt-tree t -> Element of TS PeanoNat;
  coherence
  proof
    reconsider r = {} as Node of t by TREES_1:22;
    t.r = 0 or t.r = 1 by Lm2,TARSKI:def 2;
    then
A1: roots <*t*> = <*0*> or roots <*t*> = <*1*> by Th4;
    nt = S by Lm15,TARSKI:def 1;
    then nt-tree <*t*> in TS PN by A1,Def1,Lm5,Lm6;
    hence thesis by TREES_4:def 5;
  end;
end;

definition
  let x be FinSequence of NAT;
  func plus-one x -> Element of NAT equals
  (x.1) + 1;
  coherence;
end;

deffunc N(set,set,FinSequence of NAT) = plus-one($3);

definition
  func PN-to-NAT -> Function of TS(PeanoNat), NAT means
  :Def8:
  (for t being Symbol of PeanoNat st t in Terminals PeanoNat
  holds it.(root-tree t) = 0) & for nt being Symbol of PeanoNat,
  ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
  holds it.(nt-tree ts) = plus-one(it * ts);
  existence
  proof
    thus ex f being Function of TS(PeanoNat), NAT st
    (for t being Symbol of PeanoNat st t in Terminals PeanoNat
    holds f.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
    ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
    holds f.(nt-tree ts) = N(nt, roots ts, f * ts qua FinSequence of NAT)
    from DTConstrIndDef;
  end;
  uniqueness
  proof
    let it1, it2 be Function of TS(PeanoNat), NAT such that
A1: (for t being Symbol of PeanoNat st t in Terminals PeanoNat
    holds it1.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
    ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
    holds it1.(nt-tree ts) =
    N(nt,roots ts,it1 * ts qua FinSequence of NAT) and
A2: (for t being Symbol of PeanoNat st t in Terminals PeanoNat
    holds it2.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
    ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
    holds it2.(nt-tree ts) = N(nt,roots ts,it2 * ts qua FinSequence of NAT);
    thus it1 = it2 from DTConstrUniqDef (A1,A2);
  end;
end;

definition
  let x be Element of TS(PeanoNat);
  func PNsucc x -> Element of TS(PeanoNat) equals
  1-tree <*x*>;
  coherence
  proof
    reconsider r = {} as Node of x by TREES_1:22;
A1: roots <*x*> = <*x.r*> by Th4;
    x.r = O or x.r = S by Lm2,TARSKI:def 2;
    hence thesis by A1,Def1,Lm5,Lm6;
  end;
end;

deffunc F(set,Element of TS(PeanoNat)) = PNsucc $2;

definition
  func NAT-to-PN -> Function of NAT, TS(PeanoNat) means
  :Def10:
  it.0 = root-tree 0 & for n being Nat holds it.(n+1) = PNsucc it.n;
  existence
  proof
    ex f being Function of NAT, TS(PeanoNat) st f.0 = root-tree O &
    for n being Nat
    holds f.(n+1) = F(n,f.n qua Element of TS(PeanoNat)) from NAT_1:sch 12;
    hence thesis;
  end;
  uniqueness
  proof
    let it1, it2 be Function of NAT, TS(PeanoNat);
    assume
A1: not thesis;
    then
A2: it1.0 = root-tree O;
A3: for n being Nat
    holds it1.(n+1) = F(n,it1.n qua Element of TS(PeanoNat)) by A1;
A4: it2.0 = root-tree O by A1;
A5: for n being Nat
    holds it2.(n+1) = F(n,it2.n qua Element of TS(PeanoNat)) by A1;
    it1 = it2 from NAT_1:sch 16(A2,A3, A4,A5);
    hence thesis by A1;
  end;
end;

theorem
  for pn being Element of TS(PeanoNat) holds pn = NAT-to-PN.(PN-to-NAT.pn)
proof
  defpred P[DecoratedTree of the carrier of PN] means
  $1 = NAT-to-PN.(PN-to-NAT.$1);
A1: now
    let s be Symbol of PN;
    assume
A2: s in Terminals PN;
    then NAT-to-PN.(PN-to-NAT.(root-tree s)) = NAT-to-PN.0 by Def8
      .= root-tree O by Def10;
    hence P[root-tree s] by A2,Lm10,TARSKI:def 1;
  end;
A3: now
    let nt be Symbol of PN, ts be FinSequence of TS(PN);
    assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
A6: nt <> O by A4,Lm8;
    roots ts = <*O*> or roots ts = <*S*> by A4,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider dt being Element of FinTrees the carrier of PN such that
A7: ts = <*dt*> and
A8: dt in TS(PN) by Th5;
    reconsider dt as Element of TS(PN) by A8;
    rng ts = {dt} by A7,FINSEQ_1:38;
    then dt in rng ts by TARSKI:def 1;
    then
A9: dt = NAT-to-PN.(PN-to-NAT.dt) by A5;
A10: PN-to-NAT * ts = <*PN-to-NAT.dt*> by A7,FINSEQ_2:35;
    set N = PN-to-NAT.dt;
A11: plus-one(<*N*>) = N+1 by FINSEQ_1:40;
    NAT-to-PN.(N+1) = PNsucc dt by A9,Def10
      .= nt-tree ts by A6,A7,Lm2,TARSKI:def 2;
    hence P[nt-tree ts] by A4,A10,A11,Def8;
  end;
  for t being DecoratedTree of the carrier of PN
  st t in TS(PN) holds P[t] from DTConstrInd (A1,A3);
  hence thesis;
end;

Lm17: 0 = PN-to-NAT.(root-tree O) by Def8
  .= PN-to-NAT.(NAT-to-PN.0) by Def10;

Lm18: now
  let n be Element of NAT;
  assume
A1: n = PN-to-NAT.(NAT-to-PN.n);
  reconsider dt = NAT-to-PN.n as Element of TS(PN);
  reconsider r = {} as Node of dt by TREES_1:22;
A2: dt.r = O or dt.r = S by Lm2,TARSKI:def 2;
A3: NAT-to-PN.(n+1) = PNsucc (NAT-to-PN.n) by Def10
    .= S-tree <*NAT-to-PN.n*>;
A4: S ==> roots <*NAT-to-PN.n*> by A2,Lm3,Lm4,Th4;
  <*PN-to-NAT.(NAT-to-PN.n)*> = PN-to-NAT * <*NAT-to-PN.n*> by FINSEQ_2:35;
  then PN-to-NAT.(S-tree <*NAT-to-PN.n*>) = plus-one <*n*> by A1,A4,Def8
    .= n+1 by FINSEQ_1:40;
  hence n+1 = PN-to-NAT.(NAT-to-PN.(n+1)) by A3;
end;

theorem
  for n being Element of NAT holds n = PN-to-NAT.(NAT-to-PN.n)
proof
  defpred P[Element of NAT] means $1 = PN-to-NAT.(NAT-to-PN.$1);
A1: P[0] by Lm17;
A2: for n being Element of NAT st P[n] holds P[n+1] by Lm18;
  thus for n being Element of NAT holds P[n] from NAT_1:sch 1 (A1,A2);
end;

begin

:: Tree traversals and terminal language

definition
  let G be non empty DTConstrStr, tsg be DecoratedTree of the carrier of G;

  assume
A1: tsg in TS G;
  defpred C[set] means $1 in Terminals G;
  deffunc F(set) = <*$1*>;
  deffunc G(set) = {};
A2: now
    let x be set;
    assume x in the carrier of G;
    hereby
      assume
A3:   C[x];
      then reconsider T = Terminals G as non empty set;
      reconsider x9 = x as Element of T by A3;
      <*x9*> is FinSequence of T;
      hence F(x) in (Terminals G)*;
    end;
    assume not C[x];
    <*>Terminals G = {};
    hence G(x) in (Terminals G)*;
  end;
  consider s2t being Function of the carrier of G, (Terminals G)* such that
A4: for s being set st s in the carrier of G holds
  (C[s] implies s2t.s = F(s)) &
  (not C[s] implies s2t.s = G(s)) from FUNCT_2:sch 5(A2);
  deffunc T(Symbol of G) = s2t.$1;
  deffunc N(set,set,FinSequence of (Terminals G)*) = FlattenSeq($3);
  deffunc F(set) = <*$1*>;
  func TerminalString tsg -> FinSequence of Terminals G means
  :Def11:
  ex f being Function of (TS G), (Terminals G)* st it = f.tsg &
  (for t being Symbol of G st t in Terminals G
  holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
  ts being FinSequence of TS(G) st nt ==> roots ts
  holds f.(nt-tree ts) = FlattenSeq(f * ts);
  existence
  proof
    consider f being Function of TS(G), (Terminals G)* such that
A5: (for t being Symbol of G st t in Terminals G
    holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
    ts being FinSequence of TS(G) st nt ==> roots ts
    holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
    f.tsg is Element of (Terminals G)* by A1,FUNCT_2:5;
    then reconsider IT = f.tsg as FinSequence of Terminals G;
    take IT, f;
    thus IT = f.tsg;
    hereby
      let t be Symbol of G;
      assume
A6:   t in Terminals G;
      then f.(root-tree t) = s2t.t by A5;
      hence f.(root-tree t) = <*t*> by A4,A6;
    end;
    thus thesis by A5;
  end;
  uniqueness
  proof
    let it1, it2 be FinSequence of Terminals G;
    given f1 being Function of (TS G), (Terminals G)* such that
A7: it1 = f1.tsg and
A8: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
    = <*t*> and
A9: for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==>
    roots ts holds f1.(nt-tree ts) = FlattenSeq(f1 * ts);
    given f2 being Function of (TS G), (Terminals G)* such that
A10: it2 = f2.tsg and
A11: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
    = <*t*> and
A12: for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==>
    roots ts holds f2.(nt-tree ts) = FlattenSeq(f2 * ts);
A13: now
      hereby
        let t be Symbol of G;
        assume
A14:    t in Terminals G;
        hence f1.(root-tree t) = <*t*> by A8
          .= T(t) by A4,A14;
      end;
      thus for nt being Symbol of G,
      ts being FinSequence of TS(G) st nt ==> roots ts
      holds f1.(nt-tree ts) = N(nt,roots ts,f1 * ts) by A9;
    end;
A15: now
      hereby
        let t be Symbol of G;
        assume
A16:    t in Terminals G;
        hence f2.(root-tree t) = <*t*> by A11
          .= T(t) by A4,A16;
      end;
      thus for nt being Symbol of G,
      ts being FinSequence of TS(G) st nt ==> roots ts
      holds f2.(nt-tree ts) = N(nt,roots ts,f2 * ts) by A12;
    end;
    f1 = f2 from DTConstrUniqDef (A13, A15);
    hence thesis by A7,A10;
  end;
A17: now
    let x be set;
    assume x in the carrier of G;
    then reconsider x9 = x as Element of G;
    <*x9*> is FinSequence of the carrier of G;
    hence F(x) in (the carrier of G)*;
  end;
  consider s2s being Function of the carrier of G, (the carrier of G)*
  such that
A18: for s being set st s in the carrier of G holds s2s.s = F(s)
  from FUNCT_2:sch 2(A17);
  deffunc T(Symbol of G) = s2s.$1;
  deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
  s2s.$1^FlattenSeq($3);
  func PreTraversal tsg -> FinSequence of the carrier of G means
  :Def12:
  ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
  (for t being Symbol of G st t in Terminals G
  holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
  ts being FinSequence of TS(G),
  rts being FinSequence st rts = roots ts & nt ==> rts
  for x being FinSequence of (the carrier of G)* st x = f * ts
  holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x);
  existence
  proof
    deffunc T(Symbol of G) = s2s.$1;
    deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
    s2s.$1^FlattenSeq($3);
    consider f being Function of TS(G), (the carrier of G)* such that
A19: (for t being Symbol of G st t in Terminals G
    holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
    ts being FinSequence of TS(G) st nt ==> roots ts
    holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
    f.tsg is Element of (the carrier of G)* by A1,FUNCT_2:5;
    then reconsider IT=f.tsg as FinSequence of the carrier of G;
    take IT, f;
    thus IT = f.tsg;
    hereby
      let t be Symbol of G;
      assume t in Terminals G;
      then f.(root-tree t) = s2s.t by A19;
      hence f.(root-tree t) = <*t*> by A18;
    end;
    let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence;
    assume that
A20: rts = roots ts and
A21: nt ==> rts;
    let x be FinSequence of (the carrier of G)*;
    assume x = f * ts;
    hence f.(nt-tree ts) = s2s.nt^FlattenSeq(x) by A19,A20,A21
      .= <*nt*>^FlattenSeq(x) by A18;
  end;
  uniqueness
  proof
    let it1, it2 be FinSequence of the carrier of G;
    given f1 being Function of (TS G), (the carrier of G)* such that
A22: it1 = f1.tsg and
A23: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
    = <*t*> and
A24: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
    FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
    carrier of G)* st x = f1 * ts holds f1.(nt-tree ts) = <*nt*>^FlattenSeq(x);
    given f2 being Function of (TS G), (the carrier of G)* such that
A25: it2 = f2.tsg and
A26: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
    = <*t*> and
A27: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
    FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
    carrier of G)* st x = f2 * ts holds f2.(nt-tree ts) = <*nt*>^FlattenSeq(x);
A28: now
      hereby
        let t be Symbol of G;
        assume t in Terminals G;
        hence f1.(root-tree t) = <*t*> by A23
          .= T(t) by A18;
      end;
      let nt be Symbol of G, ts be FinSequence of TS(G);
      assume nt ==> roots ts;
      hence f1.(nt-tree ts) = <*nt*>^FlattenSeq(f1 * ts) by A24
        .= N(nt,roots ts,f1 * ts) by A18;
    end;
A29: now
      hereby
        let t be Symbol of G;
        assume t in Terminals G;
        hence f2.(root-tree t) = <*t*> by A26
          .= T(t) by A18;
      end;
      let nt be Symbol of G, ts be FinSequence of TS(G);
      assume nt ==> roots ts;
      hence f2.(nt-tree ts) = <*nt*>^FlattenSeq(f2 * ts) by A27
        .= N(nt,roots ts,f2 * ts) by A18;
    end;
    f1 = f2 from DTConstrUniqDef (A28, A29);
    hence thesis by A22,A25;
  end;
  deffunc T(Symbol of G) = s2s.$1;
  deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
  FlattenSeq($3)^s2s.$1;
  func PostTraversal tsg -> FinSequence of the carrier of G means
  :Def13:
  ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
  (for t being Symbol of G st t in Terminals G
  holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
  ts being FinSequence of TS(G),
  rts being FinSequence st rts = roots ts & nt ==> rts
  for x being FinSequence of (the carrier of G)* st x = f * ts
  holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
  existence
  proof
    consider f being Function of TS(G), (the carrier of G)* such that
A30: (for t being Symbol of G st t in Terminals G
    holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
    ts being FinSequence of TS(G) st nt ==> roots ts
    holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
    f.tsg is Element of (the carrier of G)* by A1,FUNCT_2:5;
    then reconsider IT=f.tsg as FinSequence of the carrier of G;
    take IT, f;
    thus IT = f.tsg;
    hereby
      let t be Symbol of G;
      assume t in Terminals G;
      then f.(root-tree t) = s2s.t by A30;
      hence f.(root-tree t) = <*t*> by A18;
    end;
    let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence;
    assume that
A31: rts = roots ts and
A32: nt ==> rts;
    let x be FinSequence of (the carrier of G)*;
    assume x = f * ts;
    hence f.(nt-tree ts) = FlattenSeq(x)^s2s.nt by A30,A31,A32
      .= FlattenSeq(x)^<*nt*> by A18;
  end;
  uniqueness
  proof
    let it1, it2 be FinSequence of the carrier of G;
    given f1 being Function of (TS G), (the carrier of G)* such that
A33: it1 = f1.tsg and
A34: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
    = <*t*> and
A35: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
    FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
    carrier of G)* st x = f1 * ts holds f1.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
    given f2 being Function of (TS G), (the carrier of G)* such that
A36: it2 = f2.tsg and
A37: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
    = <*t*> and
A38: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
    FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
    carrier of G)* st x = f2 * ts holds f2.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
A39: now
      hereby
        let t be Symbol of G;
        assume t in Terminals G;
        hence f1.(root-tree t) = <*t*> by A34
          .= T(t) by A18;
      end;
      let nt be Symbol of G, ts be FinSequence of TS(G);
      assume nt ==> roots ts;
      hence f1.(nt-tree ts) = FlattenSeq(f1 * ts)^<*nt*> by A35
        .= N(nt,roots ts,f1 * ts) by A18;
    end;
A40: now
      hereby
        let t be Symbol of G;
        assume t in Terminals G;
        hence f2.(root-tree t) = <*t*> by A37
          .= T(t) by A18;
      end;
      let nt be Symbol of G, ts be FinSequence of TS(G);
      assume nt ==> roots ts;
      hence f2.(nt-tree ts) = FlattenSeq(f2 * ts)^<*nt*> by A38
        .= N(nt,roots ts,f2 * ts) by A18;
    end;
    f1 = f2 from DTConstrUniqDef (A39, A40);
    hence thesis by A33,A36;
  end;
end;

definition
  let G be with_nonterminals non empty non empty DTConstrStr,
  nt be Symbol of G;
  func TerminalLanguage nt -> Subset of (Terminals G)* equals
  { TerminalString tsg where tsg is Element of FinTrees the carrier of G :
  tsg in TS G & tsg.{} = nt };
  coherence
  proof
    set TL = { TerminalString tsg
    where tsg is Element of FinTrees the carrier of G :
    tsg in TS G & tsg.{} = nt };
    TL c= (Terminals G)*
    proof
      let x be set;
      assume x in TL;
      then ex tsg being Element of FinTrees the carrier of G st ( x =
      TerminalString tsg)&( tsg in TS G)&( tsg.{} = nt);
      hence thesis by FINSEQ_1:def 11;
    end;
    hence thesis;
  end;
  func PreTraversalLanguage nt -> Subset of (the carrier of G)* equals
  { PreTraversal tsg where tsg is Element of FinTrees the carrier of G :
  tsg in TS G & tsg.{} = nt };
  coherence
  proof
    set TL = { PreTraversal tsg
    where tsg is Element of FinTrees the carrier of G :
    tsg in TS G & tsg.{} = nt };
    TL c= (the carrier of G)*
    proof
      let x be set;
      assume x in TL;
      then ex tsg being Element of FinTrees the carrier of G st ( x =
      PreTraversal tsg)&( tsg in TS G)&( tsg.{} = nt);
      hence thesis by FINSEQ_1:def 11;
    end;
    hence thesis;
  end;
  func PostTraversalLanguage nt -> Subset of (the carrier of G)* equals
  { PostTraversal tsg where tsg is Element of FinTrees the carrier of G :
  tsg in TS G & tsg.{} = nt };
  coherence
  proof
    set TL = { PostTraversal tsg
    where tsg is Element of FinTrees the carrier of G :
    tsg in TS G & tsg.{} = nt };
    TL c= (the carrier of G)*
    proof
      let x be set;
      assume x in TL;
      then ex tsg being Element of FinTrees the carrier of G st ( x =
      PostTraversal tsg)&( tsg in TS G)&( tsg.{} = nt);
      hence thesis by FINSEQ_1:def 11;
    end;
    hence thesis;
  end;
end;

theorem Th13:
  for t being DecoratedTree of the carrier of PeanoNat
  st t in TS PeanoNat holds TerminalString t = <*0*>
proof
  consider f being Function of (TS PN), (Terminals PN)* such that
A1: TerminalString root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
  = <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN) st nt ==>
  roots ts holds f.(nt-tree ts) = FlattenSeq(f * ts)
  by Def11;
  defpred P[DecoratedTree of the carrier of PN] means
  TerminalString $1 = <*0*>;
A4: now
    let s be Symbol of PN;
    assume s in Terminals PN;
    then s = O by Lm10,TARSKI:def 1;
    hence P[root-tree s] by A1,A2;
  end;
A5: now
    let nt be Symbol of PN, ts be FinSequence of TS PN;
    assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
A8: nt-tree ts in TS PN by A6,Def1;
    roots ts = <*O*> or roots ts = <*1*> by A6,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider x being Element of FinTrees the carrier of PN such that
A9: ts = <*x*> and
A10: x in TS PN by Th5;
    reconsider x9 = x as Element of TS PN by A10;
    rng ts = {x} by A9,FINSEQ_1:39;
    then
A11: x in rng ts by TARSKI:def 1;
    f.x9 is Element of (Terminals PN)*;
    then
A12: f.x9 = TerminalString x by A2,A3,Def11
      .= <*O*> by A7,A11;
    f * ts = <*f.x*> by A9,FINSEQ_2:35;
    then f.(nt-tree ts) = FlattenSeq(<*f.x9*>) by A3,A6
      .= <*O*> by A12,PRE_POLY:1;
    hence P[nt-tree ts] by A2,A3,A8,Def11;
  end;
  thus for t being DecoratedTree of the carrier of PN
  st t in TS PN holds P[t] from DTConstrInd(A4,A5);
end;

theorem
  for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}
proof
  let nt be Symbol of PeanoNat;
A1: nt = S or nt = O by Lm2,TARSKI:def 2;
  hereby
    let x be set;
    assume x in TerminalLanguage nt;
    then ex tsg being Element of FinTrees the carrier of PN st
    x = TerminalString tsg & tsg in TS PN & tsg.{} = nt;
    then x = <*O*> by Th13;
    hence x in {<*0*>} by TARSKI:def 1;
  end;
  let x be set;
  assume x in {<*0*>};
  then
A2: x = <*O*> by TARSKI:def 1;
  reconsider prtO = root-tree O as Element of (TS PN) qua non empty set;
  reconsider rtO = root-tree O as Element of TS PN;
  reconsider srtO = <*prtO*> as FinSequence of TS PN;
A3: rtO.{} = O by TREES_4:3;
  then S ==> roots <*rtO*> by Lm5,Th4;
  then
A4: S-tree <*prtO*> in TS PN by Def1;
  then
A5: TerminalString (S-tree srtO) = x by A2,Th13;
A6: (S-tree <*rtO*>).{} = S by TREES_4:def 4;
  TerminalString rtO = x by A2,Th13;
  hence thesis by A1,A3,A4,A5,A6;
end;

theorem Th15:
  for t being Element of TS PeanoNat
  holds PreTraversal t = ((height dom t) |-> 1)^<*0*>
proof
  consider f being Function of (TS PN), (the carrier of PN)* such that
A1: PreTraversal root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
  = <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN), rts
  being FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (
  the carrier of PN)* st x = f * ts holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x)
  by Def12;
  reconsider rtO = root-tree O as Element of TS PN;
  defpred P[DecoratedTree of the carrier of PN] means
  ex t being Element of TS PN st $1 = t &
  PreTraversal t = ((height dom t) |-> 1)^<*0*>;
A4: now
    let s be Symbol of PN;
    assume
A5: s in Terminals PN;
    thus P[root-tree s]
    proof
      take t = rtO;
      thus root-tree s = t by A5,Lm10,TARSKI:def 1;
      thus PreTraversal t = <*O*> by A1,A2
        .= {}^<*O*> by FINSEQ_1:34
        .= (0 |-> 1)^<*0*>
        .= ((height dom t) |-> 1)^<*0*> by TREES_1:42,TREES_4:3;
    end;
  end;
A6: now
    let nt be Symbol of PN, ts be FinSequence of TS PN;
    assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
    reconsider t9 = nt-tree ts as Element of TS PN by A7,Def1;
A9: nt = S by A7,Def2;
    roots ts = <*O*> or roots ts = <*1*> by A7,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider x being Element of FinTrees the carrier of PN such that
A10: ts = <*x*> and
A11: x in TS PN by Th5;
    reconsider x9 = x as Element of TS PN by A11;
    rng ts = {x} by A10,FINSEQ_1:39;
    then x in rng ts by TARSKI:def 1;
    then
A12: ex t9 being Element of TS PN st
    x = t9 & PreTraversal t9 = ((height dom t9) |-> 1)^<*0*> by A8;
    f.x9 is Element of (the carrier of PN)*;
    then
A13: f.x9 = ((height dom x9) |-> 1)^<*0*> by A2,A3,A12,Def12;
    f * ts = <*f.x*> by A10,FINSEQ_2:35;
    then
A14: f.(nt-tree ts) = <*nt*>^FlattenSeq(<*f.x9*>) by A3,A7
      .= <*nt*>^(((height dom x9) |-> 1)^<*0*>) by A13,PRE_POLY:1
      .= <*nt*>^((height dom x9) |-> 1)^<*0*> by FINSEQ_1:32
      .= (1|->1)^((height dom x9) |-> 1)^<*0*> by A9,FINSEQ_2:59
      .= (((height dom x9)+1) |-> 1)^<*0*> by FINSEQ_2:123
      .= ((height ^dom x9) |-> 1)^<*0*> by TREES_3:80;
A15: dom (nt-tree x9) = ^dom x9 by TREES_4:13;
A16: t9 = nt-tree x9 by A10,TREES_4:def 5;
    f.t9 is Element of (the carrier of PN)*;
    then PreTraversal(nt-tree ts) = f.(nt-tree ts) by A2,A3,Def12;
    hence P[nt-tree ts] by A14,A15,A16;
  end;
A17: for t being DecoratedTree of the carrier of PN
  st t in TS PN holds P[t] from DTConstrInd(A4,A6);
  let t be Element of TS PeanoNat;
  P[t] by A17;
  hence thesis;
end;

theorem
  for nt being Symbol of PeanoNat holds
  (nt = 0 implies PreTraversalLanguage nt = {<*0*>}) &
  (nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*>
  where n is Element of NAT : n <> 0 })
proof
  let nt be Symbol of PeanoNat;
  reconsider rtO = root-tree O as Element of TS PN;
  height dom root-tree 0 = 0 by TREES_1:42,TREES_4:3;
  then PreTraversal rtO = (0 |-> 1)^<*O*> by Th15;
  then
A1: PreTraversal rtO = {}^<*O*> .= <*O*> by FINSEQ_1:34;
  thus nt = 0 implies PreTraversalLanguage nt = {<*0*>}
  proof
    assume
A2: nt = 0;
    hereby
      let x be set;
      assume x in PreTraversalLanguage nt;
      then consider tsg being Element of FinTrees the carrier of PN such that
A3:   x = PreTraversal tsg and
A4:   tsg in TS PN and
A5:   tsg.{} = O by A2;
      tsg = root-tree O by A4,A5,Th9;
      hence x in {<*0*>} by A1,A3,TARSKI:def 1;
    end;
    let x be set;
    assume x in {<*0*>};
    then
A6: x = <*O*> by TARSKI:def 1;
    rtO.{} = O by TREES_4:3;
    hence thesis by A1,A2,A6;
  end;
  assume
A7: nt = 1;
  hereby
    let x be set;
    assume x in PreTraversalLanguage nt;
    then consider tsg being Element of FinTrees the carrier of PN such that
A8: x = PreTraversal tsg and
A9: tsg in TS PN and
A10: tsg.{} = S by A7;
    consider ts being FinSequence of TS PN such that
A11: tsg = S-tree ts and
A12: S ==> roots ts by A9,A10,Th10;
    roots ts = <*0*> or roots ts = <*1*> by A12,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider t being Element of FinTrees the carrier of PN such that
A13: ts = <*t*> and t in TS PN by Th5;
    tsg = S-tree t by A11,A13,TREES_4:def 5;
    then dom tsg = ^dom t by TREES_4:13;
    then
A14: height dom tsg = (height dom t) + 1 by TREES_3:80;
    x=((height dom tsg)|->1)^<*0*> by A8,A9,Th15;
    hence x in { (n|->1)^<*0*> where n is Element of NAT : n <> 0 } by A14;
  end;
  let x be set;
  assume x in { (n|->1)^<*0*> where n is Element of NAT : n <> 0 };
  then consider n being Element of NAT such that
A15: x = (n |-> 1)^<*0*> and
A16: n <> 0;
  defpred P[Element of NAT] means
  $1 <> 0 implies ex tsg being Element of TS PN st
  tsg.{} = S & PreTraversal tsg = ($1|->1)^<*0*>;
A17: P[0];
A18: now
    let n be Element of NAT;
    assume
A19: P[n];
    thus P[n+1]
    proof
      assume n+1 <> 0;
      per cases;
      suppose n <> 0;
        then consider tsg being Element of TS PN such that
        tsg.{} = S and
A20:    PreTraversal tsg = (n|->1)^<*0*> by A19;
        PreTraversal tsg = ((height dom tsg) |-> 1)^<*0*> by Th15;
        then
A21:    n |-> 1 = (height dom tsg) |-> 1 by A20,FINSEQ_1:33;
        len(n |-> 1) = n by CARD_1:def 7;
        then
A22:    height dom tsg = n by A21,CARD_1:def 7;
        take tsg9 = S-tree tsg;
A23:    tsg9 = S-tree <*tsg*> by TREES_4:def 5;
        height dom tsg9 = height ^dom tsg by TREES_4:13
          .= n+1 by A22,TREES_3:80;
        hence thesis by A23,Th15,TREES_4:def 4;
      end;
      suppose
A24:    n = 0;
        take tsg9 = S-tree rtO;
A25:    tsg9 = S-tree <*rtO*> by TREES_4:def 5;
        height dom tsg9 = height ^dom rtO by TREES_4:13
          .= (height dom rtO)+1 by TREES_3:80
          .= n+1 by A24,TREES_1:42,TREES_4:3;
        hence thesis by A25,Th15,TREES_4:def 4;
      end;
    end;
  end;
  for n being Element of NAT holds P[n] from NAT_1:sch 1 (A17, A18);
  then ex tsg being Element of TS PN st
  tsg.{} = S & PreTraversal tsg = (n|->1)^<*0*> by A16;
  hence thesis by A7,A15;
end;

theorem Th17:
  for t being Element of TS PeanoNat
  holds PostTraversal t = <*0*>^((height dom t) |-> 1)
proof
  consider f being Function of (TS PN), (the carrier of PN)* such that
A1: PostTraversal root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
  = <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN), rts
  being FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (
  the carrier of PN)* st x = f * ts holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>
  by Def13;
  reconsider rtO = root-tree O as Element of TS PN;
  defpred P[DecoratedTree of the carrier of PN] means
  ex t being Element of TS PN st $1 = t &
  PostTraversal t = <*0*>^((height dom t) |-> 1);
A4: now
    let s be Symbol of PN;
    assume
A5: s in Terminals PN;
    thus P[root-tree s]
    proof
      take t = rtO;
      thus root-tree s = t by A5,Lm10,TARSKI:def 1;
      thus PostTraversal t = <*O*> by A1,A2
        .= <*O*>^{} by FINSEQ_1:34
        .= <*0*>^(0 |-> 1)
        .= <*0*>^((height dom t) |-> 1) by TREES_1:42,TREES_4:3;
    end;
  end;
A6: now
    let nt be Symbol of PN, ts be FinSequence of TS PN;
    assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
    reconsider t9 = nt-tree ts as Element of TS PN by A7,Def1;
A9: nt = S by A7,Def2;
    roots ts = <*O*> or roots ts = <*1*> by A7,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider x being Element of FinTrees the carrier of PN such that
A10: ts = <*x*> and
A11: x in TS PN by Th5;
    reconsider x9 = x as Element of TS PN by A11;
    rng ts = {x} by A10,FINSEQ_1:39;
    then x in rng ts by TARSKI:def 1;
    then
A12: ex t9 being Element of TS PN st
    x=t9 & PostTraversal t9 = <*O*>^((height dom t9) |-> 1) by A8;
    f.x9 is Element of (the carrier of PN)*;
    then
A13: f.x9 = <*O*>^((height dom x9) |-> 1) by A2,A3,A12,Def13;
    f * ts = <*f.x*> by A10,FINSEQ_2:35;
    then
A14: f.(nt-tree ts) = FlattenSeq(<*f.x9*>)^<*nt*> by A3,A7
      .= <*O*>^((height dom x9) |-> 1)^<*nt*> by A13,PRE_POLY:1
      .= <*O*>^(((height dom x9) |-> 1)^<*nt*>) by FINSEQ_1:32
      .= <*O*>^(((height dom x9)|->1)^(1|->1)) by A9,FINSEQ_2:59
      .= <*O*>^(((height dom x9)+1) |-> 1) by FINSEQ_2:123
      .= <*O*>^((height ^dom x9) |-> 1) by TREES_3:80;
A15: dom (nt-tree x9) = ^dom x9 by TREES_4:13;
A16: t9 = nt-tree x9 by A10,TREES_4:def 5;
    f.t9 is Element of (the carrier of PN)*;
    then PostTraversal(nt-tree ts) = f.(nt-tree ts) by A2,A3,Def13;
    hence P[nt-tree ts] by A14,A15,A16;
  end;
A17: for t being DecoratedTree of the carrier of PN
  st t in TS PN holds P[t] from DTConstrInd(A4,A6);
  let t be Element of TS PeanoNat;
  P[t] by A17;
  hence thesis;
end;

theorem
  for nt being Symbol of PeanoNat holds
  (nt = 0 implies PostTraversalLanguage nt = {<*0*>}) &
  (nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1)
  where n is Element of NAT : n <> 0 })
proof
  let nt be Symbol of PeanoNat;
  reconsider rtO = root-tree O as Element of TS PN;
  height dom root-tree 0 = 0 by TREES_1:42,TREES_4:3;
  then PostTraversal rtO = <*0*>^(0 |-> 1) by Th17;
  then
A1: PostTraversal rtO = <*O*>^{} .= <*O*> by FINSEQ_1:34;
  thus nt = 0 implies PostTraversalLanguage nt = {<*0*>}
  proof
    assume
A2: nt = 0;
    hereby
      let x be set;
      assume x in PostTraversalLanguage nt;
      then consider tsg being Element of FinTrees the carrier of PN such that
A3:   x = PostTraversal tsg and
A4:   tsg in TS PN and
A5:   tsg.{} = O by A2;
      tsg = root-tree O by A4,A5,Th9;
      hence x in {<*0*>} by A1,A3,TARSKI:def 1;
    end;
    let x be set;
    assume x in {<*0*>};
    then
A6: x = <*O*> by TARSKI:def 1;
    rtO.{} = O by TREES_4:3;
    hence thesis by A1,A2,A6;
  end;
  assume
A7: nt = 1;
  hereby
    let x be set;
    assume x in PostTraversalLanguage nt;
    then consider tsg being Element of FinTrees the carrier of PN such that
A8: x = PostTraversal tsg and
A9: tsg in TS PN and
A10: tsg.{} = S by A7;
    consider ts being FinSequence of TS PN such that
A11: tsg = S-tree ts and
A12: S ==> roots ts by A9,A10,Th10;
    roots ts = <*0*> or roots ts = <*1*> by A12,Def2;
    then len roots ts = 1 by FINSEQ_1:40;
    then consider t being Element of FinTrees the carrier of PN such that
A13: ts = <*t*> and t in TS PN by Th5;
    tsg = S-tree t by A11,A13,TREES_4:def 5;
    then dom tsg = ^dom t by TREES_4:13;
    then
A14: height dom tsg = (height dom t) + 1 by TREES_3:80;
    x=<*0*>^((height dom tsg)|->1) by A8,A9,Th17;
    hence x in { <*0*>^(n|->1) where n is Element of NAT : n <> 0 } by A14;
  end;
  let x be set;
  assume x in { <*0*>^(n|->1) where n is Element of NAT : n <> 0 };
  then consider n being Element of NAT such that
A15: x = <*0*>^(n |-> 1) and
A16: n <> 0;
  defpred P[Element of NAT] means
  $1 <> 0 implies ex tsg being Element of TS PN st
  tsg.{} = S & PostTraversal tsg = <*0*>^($1|->1);
A17: P[0];
A18: now
    let n be Element of NAT;
    assume
A19: P[n];
    thus P[n+1]
    proof
      assume n+1 <> 0;
      per cases;
      suppose n <> 0;
        then consider tsg being Element of TS PN such that
        tsg.{} = S and
A20:    PostTraversal tsg = <*0*>^(n|->1) by A19;
        PostTraversal tsg = <*0*>^((height dom tsg) |-> 1) by Th17;
        then
A21:    n |-> 1 = (height dom tsg) |-> 1 by A20,FINSEQ_1:33;
        len(n |-> 1) = n by CARD_1:def 7;
        then
A22:    height dom tsg = n by A21,CARD_1:def 7;
        take tsg9 = S-tree tsg;
A23:    tsg9 = S-tree <*tsg*> by TREES_4:def 5;
        height dom tsg9 = height ^dom tsg by TREES_4:13
          .= n+1 by A22,TREES_3:80;
        hence thesis by A23,Th17,TREES_4:def 4;
      end;
      suppose
A24:    n = 0;
        take tsg9 = S-tree rtO;
A25:    tsg9 = S-tree <*rtO*> by TREES_4:def 5;
        height dom tsg9 = height ^dom rtO by TREES_4:13
          .= (height dom rtO)+1 by TREES_3:80
          .= n+1 by A24,TREES_1:42,TREES_4:3;
        hence thesis by A25,Th17,TREES_4:def 4;
      end;
    end;
  end;
  for n being Element of NAT holds P[n] from NAT_1:sch 1 (A17, A18);
  then ex tsg being Element of TS PN st
  tsg.{} = S & PostTraversal tsg = <*0*>^(n|->1) by A16;
  hence thesis by A7,A15;
end;
 
:: What remains to be done, but in another article:
::
:: - partial trees (grown from the root towards the leaves)
:: - phrases