### The Mizar article:

### On Defining Functions on Trees

**by****Grzegorz Bancerek, and****Piotr Rudnicki**

- Received October 12, 1993
Copyright (c) 1993 Association of Mizar Users

- MML identifier: DTCONSTR
- [ MML identifier index ]

environ vocabulary FINSEQ_1, TREES_3, RELAT_1, FUNCT_1, FINSET_1, TREES_2, BOOLE, TREES_4, FUNCT_3, MCART_1, LANG1, TDGROUP, PROB_1, TARSKI, TREES_1, FUNCT_6, BINOP_1, FINSOP_1, FINSEQ_2, DTCONSTR; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSET_1, MCART_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, FINSEQOP; constructors NAT_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_4, MEMBERED, PARTFUN1, XBOOLE_0, FINSEQOP; clusters SUBSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, FUNCT_1, RELSET_1, FINSEQ_1, STRUCT_0, XREAL_0, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, FINSEQ_1, XBOOLE_0; theorems TARSKI, AXIOMS, NAT_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_6, MCART_1, FINSOP_1, BINOP_1, LANG1, FINSEQ_1, FINSEQ_2, FINSEQ_3, CARD_5, TREES_1, TREES_2, TREES_3, TREES_4, STRUCT_0, PROB_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1, RECDEF_1, CQC_SIM1, FINSEQ_1, BINOP_1, MATRIX_2, RELSET_1, FRAENKEL, FUNCT_1, FUNCT_2, COMPTS_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:22; hence thesis by FINSEQ_2:27; 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 p.y in rng p & rng p c= x by FINSEQ_1:def 4,FUNCT_1:def 5; hence p.y in x; end; :: This definition really belongs elsewhere definition let X be set; cluster -> Relation-like Function-like Element of X*; coherence; :: for x being Element of X* holds x is Function-like end; definition let X be set; cluster -> FinSequence-like Element of X*; coherence; end; definition let D be non empty set, t be Element of FinTrees D; cluster dom t -> finite; coherence by TREES_3:def 8; end; definition let D be non empty set, T be DTree-set of D; cluster -> DTree-yielding FinSequence of T; coherence proof let ts be FinSequence of T; now let x be set; assume x in dom ts; then ts.x in T by Th2; hence ts.x is DecoratedTree by TREES_3:def 5; end; hence thesis by TREES_3:26; end; 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; x in Tset & Tset c= F; hence x is Element of F; end; end; definition let p be FinSequence such that A1: p is DTree-yielding; defpred P[Nat, set] means ex T being DecoratedTree st T = p.$1 & $2 = T.{}; func roots p -> FinSequence means :Def1: dom it = dom p & for i being Nat st i in dom p ex T being DecoratedTree st T = p.i & it.i = T.{}; existence proof A2: Seg len p = dom p by FINSEQ_1:def 3; A3: for k being Nat, y1, y2 being set st k in Seg len p & P[k,y1] & P[k,y2] holds y1=y2; A4: for k being Nat st k in Seg len p ex x being set st P[k,x] proof let k be Nat; assume k in Seg len p; then p.k in rng p & rng p is constituted-DTrees by A1,A2,FUNCT_1:def 5, TREES_3:def 11; then reconsider T = p.k as DecoratedTree by TREES_3:def 5; take T.{}, T; thus thesis; end; consider q being FinSequence such that A5: dom q = Seg len p & for k being Nat st k in Seg len p holds P[k,q.k] from SeqEx(A3, A4); take q; thus dom q = dom p by A5,FINSEQ_1:def 3; thus thesis by A2,A5; end; uniqueness proof let x1, x2 be FinSequence such that A6: (dom x1 = dom p & for i being Nat st i in dom p holds P[i,x1.i]) & (dom x2 = dom p & for i being Nat st i in dom p holds P[i,x2.i]); now let k be Nat; assume k in dom p; then P[k,x1.k] & P[k,x2.k] by A6; hence x1.k = x2.k; end; hence x1 = x2 by A6,FINSEQ_1:17; 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 & x = (roots p).k by FUNCT_1:def 5; reconsider k as Nat by A1,FINSEQ_3:25; A2: dom roots p = dom p by Def1; then consider t being DecoratedTree such that A3: t = p.k & (roots p).k = t.{} by A1,Def1; t in T by A1,A2,A3,Th2; then reconsider t as DecoratedTree of D by TREES_3:def 6; reconsider r = {} as Node of t by TREES_1:47; t.r in D; hence x in D by A1,A3; end; end; Lm1: dom roots {} = dom {} by Def1,TREES_3:23 .= {} by FINSEQ_1:26; theorem Th3: roots {} = {} by Lm1,FINSEQ_1:26; theorem Th4: for T being DecoratedTree holds roots <*T*> = <*T.{}*> proof let T be DecoratedTree; A1: dom <*T*> = Seg 1 & dom <*T.{}*> = Seg 1 & <*T*> is DTree-yielding & <*T*>.1 = T & <*T.{}*>.1 = T.{} by FINSEQ_1:def 8; now let i be Nat; assume A2: i in dom <*T*>; take t = T; thus t = <*T*>.i & <*T.{}*>.i = t.{} by A1,A2,FINSEQ_1:4,TARSKI:def 1; end; hence thesis by A1,Def1; 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 & dom p = dom roots p by Def1,FINSEQ_1:def 3; then A2: 1 in dom p by FINSEQ_1:4,TARSKI:def 1; then reconsider x = p.1 as Element of FinTrees D by Th2; take x; thus thesis by A1,A2,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 & len <*T1.{}, T2.{}*> = 2 & <*T1, T2*>.1 = T1 & <*T1.{}, T2.{}*>.1 = T1.{} & <*T1, T2*>.2 = T2 & <*T1.{}, T2.{}*>.2 = T2.{} by FINSEQ_1:61; then A2: dom <*T1, T2*> = Seg 2 & dom <*T1.{}, T2.{}*> = Seg 2 by FINSEQ_1:def 3; now let i be 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:4,TARSKI:def 2; hence ex t being DecoratedTree st t = <*T1, T2*>.i & <*T1.{}, T2.{}*>.i = t.{} by A1; end; hence thesis by A2,Def1; end; definition let f be Function; func pr1 f -> Function means :Def2: dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`1; existence proof deffunc F(set) = (f.$1)`1; ex g being Function st dom g = dom f & for x being set st x in dom f holds g.x = F(x) from Lambda; hence thesis; end; uniqueness proof let p1, p2 be Function such that A1: dom p1 = dom f & for x being set st x in dom f holds p1.x = (f.x)`1 and A2: dom p2 = dom f & for x being set st x in dom f holds p2.x = (f.x)`1; now let x be set; assume x in dom f; then p1.x = (f.x)`1 & p2.x = (f.x)`1 by A1,A2; hence p1.x = p2.x; end; hence thesis by A1,A2,FUNCT_1:9; end; func pr2 f -> Function means :Def3: dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`2; existence proof deffunc F(set) = (f.$1)`2; ex g being Function st dom g = dom f & for x being set st x in dom f holds g.x = F(x) from Lambda; hence thesis; end; uniqueness proof let p1, p2 be Function such that A3: dom p1 = dom f & for x being set st x in dom f holds p1.x = (f.x)`2 and A4: dom p2 = dom f & for x being set st x in dom f holds p2.x = (f.x)`2; now let x be set; assume x in dom f; then p1.x = (f.x)`2 & p2.x = (f.x)`2 by A3,A4; hence p1.x = p2.x; end; hence thesis by A3,A4,FUNCT_1:9; end; 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 & dom f = Seg len f by Def2,FINSEQ_1:def 3; then reconsider p = pr1 f as FinSequence by 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 & x = p.i by FUNCT_1:def 5; f.i in [:X, Y:] & x = (f.i)`1 by A1,A2,Def2,Th2; hence thesis by MCART_1:10; end; hence thesis by FINSEQ_1:def 4; end; func pr2 f -> FinSequence of Y; coherence proof A3: dom pr2 f = dom f & dom f = Seg len f by Def3,FINSEQ_1:def 3; then reconsider p = pr2 f as FinSequence by 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 A4: i in dom p & x = p.i by FUNCT_1:def 5; f.i in [:X, Y:] & x = (f.i)`2 by A3,A4,Def3,Th2; hence thesis by MCART_1:10; end; hence thesis by FINSEQ_1:def 4; end; end; theorem Th7: pr1 {} = {} & pr2 {} = {} proof reconsider r = {} as FinSequence of [:{}, {}:] by FINSEQ_1:29; dom pr1 r = dom {} by Def2 .= {} by FINSEQ_1:26; hence pr1 {} = {} by FINSEQ_1:26; dom pr2 r = dom {} by Def3 .= {} by FINSEQ_1:26; hence pr2 {} = {} by FINSEQ_1:26; end; scheme MonoSetSeq { f() -> Function, A() -> set, H(set, set) -> set}: for k, s being Nat holds f().k c= f().(k+s) provided A1: for n being Nat holds f().(n+1) = f().n \/ H(n, f().n) proof let k be Nat; set f = f(); defpred P[Nat] means f.k c= f.(k+$1); A2: P[0]; A3: now let s be Nat; assume A4: P[s]; f.(k+(s+1)) = f.((k+s)+1) by XCMPLX_1:1 .= f.(k+s) \/ H(k+s, f.(k+s)) by A1; then f.(k+s) c= f.(k+(s+1)) by XBOOLE_1:7; hence P[s+1] by A4,XBOOLE_1:1; end; thus for s being Nat holds P[s] from Ind(A2,A3); end; begin definition let A be non empty set, R be Relation of A,A*; cluster DTConstrStr(#A,R#) -> non empty; coherence by STRUCT_0:def 1; 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 defpred R[set,set] means P[$1,$2]; 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()* & R[x, y] from Rel_On_Set_Ex; 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 x ==> p 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() & for x being Symbol of G1, p being FinSequence of the carrier of G1 holds x ==> p iff P[x, p]) and A2: (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]); now let x, y be set; hereby assume A3: [x, y] in the Rules of G1; then A4: x in the carrier of G1 & y in (the carrier of G1)* by ZFMISC_1:106; reconsider x1 = x as Symbol of G1 by A3,ZFMISC_1:106; reconsider y1 = y as FinSequence of the carrier of G1 by A4,FINSEQ_2:def 3; A5: x1 ==> y1 iff P[x1, y1] by A1; reconsider x2 = x as Symbol of G2 by A1,A2,A3,ZFMISC_1:106; reconsider y2 = y as FinSequence of the carrier of G2 by A1,A2,A4,FINSEQ_2: def 3; x2 ==> y2 by A2,A3,A5,LANG1:def 1; hence [x, y] in the Rules of G2 by LANG1:def 1; end; assume A6: [x, y] in the Rules of G2; then A7: x in the carrier of G2 & y in (the carrier of G2)* by ZFMISC_1:106; reconsider x2 = x as Symbol of G2 by A6,ZFMISC_1:106; reconsider y2 = y as FinSequence of the carrier of G2 by A7,FINSEQ_2:def 3; A8: x2 ==> y2 iff P[x2, y2] by A2; reconsider x1 = x as Symbol of G1 by A1,A2,A6,ZFMISC_1:106; reconsider y1 = y as FinSequence of the carrier of G1 by A1,A2,A7,FINSEQ_2: def 3; x1 ==> y1 by A1,A6,A8,LANG1:def 1; hence [x, y] in the Rules of G1 by LANG1:def 1; end; hence G1 = G2 by A1,A2,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 & x in NonTerminals G by XBOOLE_0:3; (ex t being Symbol of G st x = t & not ex tnt being FinSequence st t ==> tnt) & (ex t being Symbol of G st x = t & ex tnt being FinSequence st t ==> tnt ) by A1,A2,A3; hence contradiction; 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 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 consider k being set such that A4: k in NAT & u in f.k by A1,CARD_5:10; defpred P[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 u in FinTrees [:the carrier of G, D:]; end; A6: now let n be 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 2; 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 & 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 A10; u = [o, NTV(o, p)]-tree p by A10; hence contradiction by A9; end; end; for n being Nat holds P[n] from Ind(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:10; end; hereby let o be Symbol of G, p be FinSequence of X such that A11: 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 Nat st P[x,n] proof let x be Nat; assume x in Seg len p; then p.x in rng p & rng p c= X by A13,FINSEQ_1:def 4,FUNCT_1:def 5; then ex n being set st n in NAT & p.x in f.n by A1,CARD_5:10; hence thesis; end; consider pn being FinSequence of NAT such that A15: dom pn = Seg len p & for k being Nat st k in Seg len p holds P[k,pn.k] from SeqDEx (A14); A16: now defpred P[Nat,Nat] means $1 >= $2; assume rng pn <> {}; then A17: rng pn is finite & rng pn <> {} & rng pn c= NAT by FINSEQ_1:def 4; A18: for x, y being Nat holds P[x,y] or P[y,x]; A19: for x, y, z being Nat st P[x,y] & P[y,z] holds P[x,z] by AXIOMS:22; consider n being Nat such that A20: n in rng pn & for y being Nat st y in rng pn holds P[n,y] from MaxFinDomElem ( A17, A18, A19 ); 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 A21: k in dom p & t = p.k by FUNCT_1:def 5; reconsider k as Nat by A21,FINSEQ_3:25; A22: pn.k in rng pn by A13,A15,A21,FUNCT_1:def 5; then reconsider pnk = pn.k as Nat by A17; n >= pnk by A20,A22; then consider s being Nat such that A23: n = pnk + s by NAT_1:28; 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 }; A24: for n being Nat holds f.(n+1) = f.n \/ H(n, f.n) by A3 ; for k, s being Nat holds f.k c= f.(k+s) from MonoSetSeq (A24); then A25: f.pnk c= f.n by A23; t in f.(pn.k) by A13,A15,A21; hence thesis by A25; end; end; now assume rng pn = {}; then pn = {} by FINSEQ_1:27; then dom pn = {} by FINSEQ_1:26; then p = {} by A13,A15,FINSEQ_1:26; then A26: rng p = {} by FINSEQ_1:27; consider n being Nat; take n; thus rng p c= f.n by A26,XBOOLE_1:2; end; then consider n being Nat such that A27: rng p c= f.n by A16; X = union rng f & f.n in rng f by A1,FUNCT_1:def 5,PROB_1:def 3; then f.n c= X by ZFMISC_1:92; 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 q' = q as Element of (fn)* by FINSEQ_1:def 11; [o, NTermVal(o, s, v)]-tree q' 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 A11; then [o, NTermVal(o, s, v)]-tree q' 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 2; then [o, NTermVal(o, s, v)]-tree q' in f.(n+1) by A3; hence [o, NTermVal(o, s, v)]-tree p in X by A1,CARD_5:10; end; let F be Subset of FinTrees [:the carrier of G, D:] such that A28: (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, NTV(o, p)]-tree p in F); defpred P[Nat] means f.$1 c= F; A29:P[0] proof let x be set; reconsider p = {} as FinSequence of F by FINSEQ_1:29; assume x in f.0; then consider t being Symbol of G, d being Element of D such that A30: x = root-tree [t, d] & (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 x in F by A28,A30; end; A31: now let n be Nat such that A32: P[n]; thus P[n+1] proof let x be set; assume A33: x in f.(n+1) & not x in F; then 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; 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 2; then consider o being Symbol of G, p being Element of (f.n)* such that A34: x = [o, NTV(o, p)]-tree p & ex q being FinSequence of FinTrees [:the carrier of G, D:] st p = q & o ==> pr1 roots q by A32,A33; rng p c= f.n by FINSEQ_1:def 4; then rng p c= F by A32,XBOOLE_1:1; then reconsider p as FinSequence of F by FINSEQ_1:def 4; o ==> pr1 roots p by A34; hence contradiction by A28,A33,A34; end; end; A35: for n being Nat holds P[n] from Ind (A29, A31); thus X c= F proof let x be set; assume x in X; then consider n being set such that A36: n in NAT & x in f.n by A1,CARD_5:10; f.n c= F by A35,A36; hence x in F by A36; 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 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); deffunc F(set) = TermVal($1); deffunc G(set,set,set) = NTermVal($1,$2,$3); A4: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() : t in Terminals G() & d = F(t) or t ==> {} & d = G(t, {}, {}) } by A2; A5: for n being Nat holds f().(n+1) = f().n \/ { [o, G(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, F(d)] in X) & (for o being Symbol of G, p being FinSequence of X st o ==> pr1 roots p holds [o, G(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, F(d)] in F ) & (for o being Symbol of G, p being FinSequence of F st o ==> pr1 roots p holds [o, G(o, pr1 roots p, pr2 roots p)]-tree p in F) holds X c= F ) from DTCMin (A1, A4, A5); set X' = { t`1 where t is Element of FinTrees [:the carrier of G,D:]: t in Union f }; X' c= FinTrees(the carrier of G) proof let x be set; assume x in X'; then consider tt being Element of FinTrees [:the carrier of G,D:] such that A7: x = tt`1 & tt in Union f; tt`1 = pr1(the carrier of G, D) * tt & rng tt c= [:the carrier of G, D:] & dom pr1(the carrier of G, D) = [:the carrier of G, D:] by FUNCT_2:def 1,TREES_2:def 9,TREES_3:def 12; then dom tt`1 = dom tt & dom tt is finite by RELAT_1:46; hence x in FinTrees the carrier of G by A7,TREES_3:def 8; end; then reconsider X' as Subset of FinTrees(the carrier of G()); take X1= X'; 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 A8: t in Terminals G(); A9: (root-tree [t, TermVal(t)])`1 = root-tree t by TREES_4:25; root-tree [t, TermVal(t)] in Union f by A6,A8; hence root-tree t in X1 by A9; end; hereby let nt be Symbol of G(), ts be FinSequence of X1; assume A10: nt ==> roots ts; A11: 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; A12: 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 ts.k in rng ts & rng ts c= X1 by A11,FINSEQ_1:def 4,FUNCT_1:def 5; then ts.k in X1; 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 A13: dom dts = Seg len ts and A14: for k being Nat st k in Seg len ts holds P[k,dts.k] from SeqDEx (A12); rng dts c= Union f proof let x be set; assume x in rng dts; then consider k being set such that A15: k in dom ts & x = dts.k by A11,A13,FUNCT_1:def 5; reconsider k as Nat by A15,FINSEQ_3:25; ex dt being DecoratedTree of [:the carrier of G(), D():] st dt = x & dt`1 = ts.k & dt in Union f by A11,A14,A15; hence thesis; end; then reconsider dts as FinSequence of X by A6,FINSEQ_1:def 4; A16: dom roots ts = dom ts by Def1; A17: dom pr1 roots dts = dom roots dts & dom pr2 roots dts = dom roots dts by Def2,Def3; then A18: dom pr1 roots dts = dom ts & dom pr2 roots dts = dom ts by A11,A13,Def1; now let k be Nat; assume A19: k in dom ts; then consider dt being DecoratedTree of [:the carrier of G(), D():] such that A20: dt = dts.k & dt`1 = ts.k & dt in Union f by A11,A14; reconsider r = {} as Node of dt by TREES_1:47; ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{} by A19,Def1; then A21: (roots ts).k = (dt.r)`1 by A20,TREES_3:41; ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{} by A11,A13,A19,Def1; hence (roots ts).k = (pr1 roots dts).k by A17,A18,A19,A20,A21,Def2; end; then roots ts = pr1 roots dts by A16,A18,FINSEQ_1:17; then A22: [nt, NTV(nt, dts)]-tree dts in X by A6,A10; A23: 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:22; then rng dts c= Trees [:the carrier of G(), D():] by A23,XBOOLE_1:1; then reconsider dts' = dts as FinSequence of Trees [:the carrier of G(),D() :] by FINSEQ_1:def 4; A24: 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:22; then rng ts c= Trees the carrier of G() by A24,XBOOLE_1:1; then reconsider ts' = ts as FinSequence of Trees the carrier of G() by FINSEQ_1:def 4; now let i be Nat; assume i in dom dts; then consider dt being DecoratedTree of [:the carrier of G, D:] such that A25: dt = dts.i & dt`1 = ts.i & dt in Union f by A13,A14; let T be DecoratedTree of [:the carrier of G(), D():]; assume T = dts.i; hence ts.i = T`1 by A25; end; then ([nt, NTV(nt, dts)]-tree dts')`1 = nt-tree ts' by A11,A13,TREES_4:27; hence nt-tree ts in X1 by A6,A22; end; let F be Subset of FinTrees the carrier of G; assume that A26: for d being Symbol of G st d in Terminals G holds root-tree d in F and A27: 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 A28: x = tt`1 & 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; A29: now let d be Symbol of G; assume d in Terminals G; then A30: root-tree d in F by A26; (root-tree [d, TermVal(d)])`1 = root-tree d by TREES_4:25; hence root-tree [d, TermVal(d)] in FF by A30; end; now let o be Symbol of G, p be FinSequence of FF; assume A31: o ==> pr1 roots p; consider p1 being FinSequence of FinTrees S such that A32: dom p1 = dom p and A33: for i being Nat st i in dom p ex T being Element of FinTrees SxD st T = p.i & p1.i = T`1 and A34: ([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 A35: k in dom p1 & x = p1.k by FUNCT_1:def 5; reconsider k as Nat by A35,FINSEQ_3:25; A36: p.k in rng p by A32,A35,FUNCT_1:def 5; consider dt being Element of FinTrees SxD such that A37: dt = p.k & x = dt`1 by A32,A33,A35; rng p c= FF by FINSEQ_1:def 4; then p.k in FF by A36; then ex dt being Element of FinTrees SxD st p.k = dt & dt`1 in F; hence thesis by A37; end; then reconsider p1 as FinSequence of F by FINSEQ_1:def 4; A38: dom roots p1 = dom p1 by Def1; A39: dom pr1 roots p = dom roots p by Def2; then A40: dom pr1 roots p = dom p1 by A32,Def1; now let k be Nat; assume A41: k in dom p1; then A42: p.k in rng p by A32,FUNCT_1:def 5; consider dt being Element of FinTrees SxD such that A43: dt = p.k & p1.k = dt`1 by A32,A33,A41; rng p c= FF by FINSEQ_1:def 4; then p.k in FF by A42; then consider dt being Element of FinTrees SxD such that A44: p.k = dt & dt`1 in F; reconsider r = {} as Node of dt by TREES_1:47; ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{} by A41,Def1; then A45: (roots p1).k = (dt.r)`1 by A43,A44,TREES_3:41; ex T being DecoratedTree st T = p.k & (roots p).k = T.{} by A32,A41,Def1; hence (roots p1).k = (pr1 roots p).k by A39,A40,A41,A44,A45,Def2; end; then pr1 roots p = roots p1 by A38,A40,FINSEQ_1:17; then ([o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p)`1 in F by A27,A31,A34; hence [o, NTV(o, p)]-tree p in FF; end; then X c= FF by A6,A29; then tt in FF by A6,A28; then ex dt being Element of FinTrees SxD st tt = dt & dt`1 in F; hence x in F by A28; 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 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 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[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:79,TREES_4:3; end; assume height dom dt <= 0; then height dom dt = 0 by NAT_1:18; then A6: dom dt = elementary_tree 0 by TREES_1:80; defpred P[Nat] means not dt in f.$1; assume A7: P[0]; A8: now let n be 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 2; then consider o being Symbol of G, p being Element of (f.n)* such that A10: dt = [o, NTV(o, p)]-tree p & ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q by A9; A11: dt = root-tree (dt.{}) by A6,TREES_4:5; then A12: p = {} by A10,TREES_4:17; then dt = root-tree [o, NTermVal(o,{},{})] by A10,A11,Th3,Th7,TREES_4:def 4; hence contradiction by A2,A7,A10,A12,Th3,Th7; end; end; A13: for n being Nat holds P[n] from Ind (A7, A8); ex n being set st n in NAT & dt in f.n by A1,A5,CARD_5:10; hence contradiction by A13; end; A14: now let n be Nat; assume A15: R[n]; thus R[n+1] proof let dt be Element of FinTrees SxD; assume A16: 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 A17: 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 2; per cases; suppose dt in f.n; then height dom dt <= n & n <= n+1 by A15,A16,NAT_1:29; hence height dom dt <= n+1 by AXIOMS:22; suppose not dt in f.n; then consider o being Symbol of G, p being Element of (f.n)* such that A18: dt = [o, NTV(o, p)]-tree p & ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q by A17; reconsider p as FinSequence of FinTrees SxD by A18; A19: dom dt = tree(doms p) by A18,TREES_4:10; now let t be finite Tree; assume t in rng doms p; then consider k being set such that A20: k in dom doms p & t = (doms p).k by FUNCT_1:def 5; A21: k in dom p by A20,TREES_3:39; then A22: p.k in rng p & rng p c=FinTrees SxD by FINSEQ_1:def 4,FUNCT_1: def 5; then reconsider pk = p.k as Element of FinTrees SxD; A23: rng p c= f.n by FINSEQ_1:def 4; then A24: t = dom pk & pk in f.n by A20,A21,A22,FUNCT_6:31; pk in Union f by A1,A22,A23,CARD_5:10; hence height t <= n by A15,A24; end; hence height dom dt <= n+1 by A19,TREES_3:80; end; assume A25: 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,A16,CARD_5:10; then A26: ex k being Nat st P[k]; consider mk being Nat such that A27: P[mk] & for kk being Nat st P[kk] holds mk <= kk from Min (A26); 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 }; A28: for n being Nat holds f.(n+1) = f.n \/ F(n, f.n) by A3 ; A29: for k, s being Nat holds f.k c= f.(k+s) from MonoSetSeq (A28); per cases by NAT_1:22; suppose mk = 0; then f.mk c= f.(0+(n+1)) & 0+(n+1) = n+1 by A29; hence dt in f.(n+1) by A27; suppose ex k being Nat st mk = k+1; then consider k being Nat such that A30: mk = k+1; A31: k < k+1 by NAT_1:38; 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,A30; 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 A27,XBOOLE_0:def 2; then consider o being Symbol of G, p being Element of (f.k)* such that A32: dt = [o, NTV(o, p)]-tree p & ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q by A27,A30,A31; reconsider p as FinSequence of FinTrees SxD by A32; A33: dom dt = tree(doms p) by A32,TREES_4:10; rng p c= f.n proof let x be set; assume x in rng p; then consider k' being set such that A34: k' in dom p & x = p.k' by FUNCT_1:def 5; x in rng p & rng p c= FinTrees SxD by A34,FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider t = x as Element of FinTrees SxD; t = x; then k' in dom doms p & dom t = (doms p).k' by A34,FUNCT_6:31; then dom t in rng doms p by FUNCT_1:def 5; then height dom t < height dom dt by A33,TREES_3:81; then height dom t < n+1 by A25,AXIOMS:22; then A35: height dom t <= n by NAT_1:38; rng p c= f.k & t in rng p by A34,FINSEQ_1:def 4,FUNCT_1:def 5; then t in Union f by A1,CARD_5:10; hence thesis by A15,A35; 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 A32; 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 A32,XBOOLE_0:def 2; hence dt in f.(n+1) by A3; end; end; thus for n being Nat holds R[n] from Ind (A4, A14); 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 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); deffunc F(set) = TermVal($1); deffunc G(set,set,set) = NTermVal($1,$2,$3); A4: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() : t in Terminals G() & d = F(t) or t ==> {} & d = G(t, {}, {}) } by A2; A5: for n being Nat holds f().(n+1) = f().n \/ { [o, G(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[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 A7: dt1 in f.0 & dt2 in f.0 & dt1`1 = dt2`1; then consider t1 being Symbol of G, d1 being Element of D such that A8: dt1= root-tree [t1, d1] & (t1 in Terminals G & d1 = TermVal(t1) or t1 ==> {} & d1 = NTermVal(t1, {}, {})) by A2; consider t2 being Symbol of G, d2 being Element of D such that A9: dt2= root-tree [t2, d2] & (t2 in Terminals G & d2 = TermVal(t2) or t2 ==> {} & d2 = NTermVal(t2, {}, {})) by A2,A7; root-tree t1 = dt1`1 & root-tree t2 = dt2`1 by A8,A9,TREES_4:25; then A10: t1 = t2 by A7,TREES_4:4; now let t be Symbol of G; assume t ==> {}; then not ex t' being Symbol of G st t=t' & not ex tnt being FinSequence st t' ==> tnt; then not t in {t' where t' is Symbol of G: not ex tnt being FinSequence st t' ==> tnt }; hence not t in Terminals G by LANG1:def 2; end; hence dt1 = dt2 by A8,A9,A10; end; A11: now let n be Nat such that A12: R[n]; thus R[n+1] proof let dt1, dt2 be DecoratedTree of SxD; assume A13: dt1 in f.(n+1) & dt2 in f.(n+1) & dt1`1 = dt2`1; then A14: dom dt1 = dom dt1`1 & dom dt2 = dom dt1`1 by TREES_4:24; A15: dt1 in Union f & dt2 in Union f by A1,A13,CARD_5:10; 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, F(d)] in X) & (for o being Symbol of G(), p being FinSequence of X st o ==> pr1 roots p holds [o, G(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, F(d)] in F ) & (for o being Symbol of G(), p being FinSequence of F st o ==> pr1 roots p holds [o, G(o, pr1 roots p, pr2 roots p)]-tree p in F) holds X c= F ) from DTCMin(A1, A4, A5); then reconsider dt1' = dt1, dt2' = dt2 as Element of FinTrees SxD by A15; A16: for n being 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 A17: dt1 in f.n; then height dom dt1' <= n by A15,A16; then dt2' in f.n by A14,A15,A16; hence dt1 = dt2 by A12,A13,A17; suppose A18: not dt1 in f.n; A19: 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 A13,XBOOLE_0:def 2; then consider o1 being Symbol of G, p1 being Element of (f.n)* such that A20: dt1 = [o1, NTV(o1, p1)]-tree p1 & ex q being FinSequence of FinTrees SxD st p1 = q & o1 ==> pr1 roots q by A18; height dom dt1' > n by A15,A16,A18; then A21: not dt2' in f.n by A14,A15,A16; 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 A13,A19,XBOOLE_0:def 2; then consider o2 being Symbol of G, p2 being Element of (f.n)* such that A22: dt2 = [o2, NTV(o2, p2)]-tree p2 & ex q being FinSequence of FinTrees SxD st p2 = q & o2 ==> pr1 roots q by A21; reconsider p1 as FinSequence of FinTrees SxD by A20; consider p11 being FinSequence of FinTrees S such that A23: dom p11 = dom p1 & (for i being Nat st i in dom p1 holds ex T being Element of FinTrees SxD st T = p1.i & p11.i = T`1) & ([o1, NTV(o1,p1)]-tree p1)`1 = o1-tree p11 by TREES_4:31; reconsider p2 as FinSequence of FinTrees SxD by A22; consider p21 being FinSequence of FinTrees S such that A24: dom p21 = dom p2 & (for i being Nat st i in dom p2 holds ex T being Element of FinTrees SxD st T = p2.i & p21.i = T`1) & ([o2, NTV(o2,p2)]-tree p2)`1 = o2-tree p21 by TREES_4:31; A25: o1 = o2 & p11 = p21 by A13,A20,A22,A23,A24,TREES_4:15; now let k be Nat; assume A26: k in dom p11; then consider p1k being Element of FinTrees SxD such that A27: p1k = p1.k & p11.k = p1k`1 by A23; consider p2k being Element of FinTrees SxD such that A28: p2k = p2.k & p21.k = p2k`1 by A24,A25,A26; p1k in f.n & p2k in f.n by A23,A24,A25,A26,A27,A28,Th2; hence p1.k = p2.k by A12,A25,A27,A28; end; then p1 = p2 by A23,A24,A25,FINSEQ_1:17; hence dt1 = dt2 by A20,A22,A25; end; end; A29: for n be Nat holds R[n] from Ind (A6, A11); let dt1, dt2 be DecoratedTree of SxD; assume A30: dt1 in Union f & dt2 in Union f & dt1`1 = dt2`1; then consider n1 being set such that A31: n1 in NAT & dt1 in f.n1 by A1,CARD_5:10; consider n2 being set such that A32: n2 in NAT & dt2 in f.n2 by A1,A30,CARD_5:10; reconsider n1, n2 as Nat by A31,A32; 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 }; A33: for n being Nat holds f.(n+1) = f.n \/ F(n, f.n) by A3 ; A34: for k, s being Nat holds f.k c= f.(k+s) from MonoSetSeq (A33); 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:28; then f.n1 c= f.n2 or f.n2 c= f.n1 by A34; hence dt1 = dt2 by A29,A30,A31, A32; end; definition let G be non empty DTConstrStr; func TS(G) -> Subset of FinTrees(the carrier of G) means :Def4: (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 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 LambdaRecEx; A4: for n being 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 TSG1 c= TSG2 & TSG2 c= TSG1; hence contradiction by A5,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 :: 0 and NAT used for D() from FThn A3: dom f = NAT and A4: f.0 = { root-tree [t, d] where t is Symbol of G(), d is 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 LambdaRecEx; A6: for n being 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,Def4; defpred R[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:]; reconsider p = {} as FinSequence of TS(G()) by FINSEQ_1:29; assume tt in f.0; then consider t being Symbol of G(), d being Nat such that A14: tt = root-tree [t, d] & (t in Terminals G() & d = 0 or t ==> roots p & d = 0) by A4,Th3; A15: tt`1 = root-tree t & t-tree p = root-tree t by A14,TREES_4:20,25; for T being DecoratedTree of the carrier of G() st T in rng p holds P[T] by FINSEQ_1:27; hence P[tt`1] by A1,A2,A14,A15; end; A16: now let n be Nat; assume A17: R[n]; thus R[n+1] proof let x be DecoratedTree of [:the carrier of G(), NAT:]; assume A18: x in f.(n+1) & not P[x`1]; then 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; 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 2; then consider o being Symbol of G(), p being Element of (f.n)* such that A19: x = [o, 0]-tree p & ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st p = q & o ==> pr1 roots q by A17,A18; Union f=union rng f & f.n in rng f by A3,FUNCT_1:def 5,PROB_1:def 3; then A20: rng p c= f.n & f.n c= Union f by FINSEQ_1:def 4,ZFMISC_1:92; A21: 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; A22: 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 A23: p.k in rng p & rng p c= Union f by A20,A21,FUNCT_1:def 5,XBOOLE_1:1; then p.k in Union f; then reconsider dt = p.k as Element of FinTrees [:(the carrier of G()), NAT:] by A7; dt`1 = pr1(the carrier of G(), NAT) * dt & rng dt c= [:the carrier of G(), NAT:] & dom pr1(the carrier of G(), NAT) = [:the carrier of G(), NAT:] by FUNCT_2:def 1,TREES_2:def 9,TREES_3:def 12; then dom dt`1 = dom dt & dom dt is finite by RELAT_1:46; then reconsider x = dt`1 as Element of FinTrees the carrier of G() by TREES_3:def 8; take x, dt; thus thesis by A23; end; consider p1 being FinSequence of FinTrees the carrier of G() such that A24: dom p1 = Seg len p and A25: for k being Nat st k in Seg len p holds P[k,p1.k] from SeqDEx (A22); reconsider p as FinSequence of Trees [:the carrier of G(), NAT:] by A19,Th1; A26: dom roots p1 = dom p1 by Def1; A27: dom pr1 roots p = dom roots p by Def2; then A28: dom pr1 roots p = dom p1 by A21,A24,Def1; now let k be Nat; assume A29: k in dom p1; then consider dt being Element of FinTrees [:the carrier of G(), NAT:] such that A30: dt = p.k & dt`1 = p1.k & dt in Union f by A24,A25; reconsider r = {} as Node of dt by TREES_1:47; ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{} by A29,Def1; then A31: (roots p1).k = (dt.r)`1 by A30,TREES_3:41; ex T being DecoratedTree st T = p.k & (roots p).k = T.{} by A21,A24,A29,Def1; hence (roots p1).k = (pr1 roots p).k by A27,A28,A29,A30,A31,Def2; end; then A32: roots p1 = pr1 roots p by A26,A28,FINSEQ_1:17; rng p1 c= TS(G()) proof let x be set; assume x in rng p1; then consider k being set such that A33: k in dom p1 & x = p1.k by FUNCT_1:def 5; reconsider k as Nat by A33,FINSEQ_3:25; ex dt being Element of FinTrees [:the carrier of G(), NAT:] st dt = p.k & dt`1 = p1.k & dt in Union f by A24,A25,A33; hence thesis by A8,A12,A33; 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 A34: k in dom p1 & t = p1.k by FUNCT_1:def 5; reconsider k as Nat by A34,FINSEQ_3:25; consider dt being Element of FinTrees [:the carrier of G(), NAT:] such that A35: dt = p.k & dt`1 = p1.k & dt in Union f by A24,A25,A34; p.k in rng p by A21,A24,A34,FUNCT_1:def 5; hence P[t] by A17,A20,A34,A35; end; then A36: P[o-tree p1] by A2,A19,A32; reconsider p1 as FinSequence of Trees the carrier of G() by Th1; now let k be 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 A21,A25; hence for T being DecoratedTree of [:the carrier of G(), NAT:] st T = p.k holds p1.k = T`1; end; hence contradiction by A18,A19,A21,A24,A36,TREES_4:27; end; end; A37: for n being Nat holds R[n] from Ind (A13, A16); 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 A38: t = tt`1 & tt in Union f by A8,A12; ex n being set st n in NAT & tt in f.n by A3,A38,CARD_5:10; hence P[t] by A37,A38; 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 TT(set) = TermVal($1); deffunc NN(set,set,set) = NTermVal($1,$2,$3); deffunc NTV(Symbol of G, FinSequence) = NN($1, pr1 roots $2, pr2 roots $2); deffunc F(set,set) = $2 \/ { [o, NN(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 = TT(t) or t ==> {} & d = NN(t, {}, {}) } and A3: for n being Nat holds f.(n+1) = F(n,f.n) from LambdaRecEx; A4: for n being Nat holds f.(n+1) = f.n \/ { [o, NN(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 Def4; 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 & DT in Union f by A5; reconsider r = {} as Node of DT`2 by TREES_1:47; take u = (DT`2).r; thus u in D(); A8: 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 dt in Union f & e = dt`1; hence u = (dt`2).{} by A7,A8; end; consider ff being Function such that A9: dom ff = TS(G) & rng ff c= D() and A10: for e being set st e in TS(G) holds P[e,ff.e] from NonUniqBoundFuncEx (A6); reconsider ff as Function of TS(G), D() by A9,FUNCT_2:def 1,RELSET_1:11; take ff; consider X be Subset of FinTrees [:the carrier of G, D():] such that A11: X = Union f and A12: for d being Symbol of G st d in Terminals G holds root-tree [d, TT(d)] in X and A13: for o being Symbol of G, p being FinSequence of X st o ==> pr1 roots p holds [o, NN(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, TT(d)] in F ) & (for o being Symbol of G, p being FinSequence of F st o ==> pr1 roots p holds [o, NN(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 A14: t in Terminals G; A15: (root-tree [t, TermVal(t)])`1 = root-tree t & (root-tree [t, TermVal(t)])`2 = root-tree TermVal(t) by TREES_4:25; A16: root-tree [t, TermVal(t)] in Union f by A11,A12,A14; then root-tree t in TS(G) by A5,A15; hence ff.(root-tree t) = (root-tree TermVal(t)).{} by A10,A15,A16 .= TermVal(t) by TREES_4:3; end; let nt be Symbol of G, ts be FinSequence of TS(G); set rts = roots ts; assume A17: nt ==> rts; set x = ff * ts; A19: 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; A20: 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 ts.k in rng ts & rng ts c= TS(G) by A19,FINSEQ_1:def 4,FUNCT_1:def 5; then ts.k in TS(G); 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 A21: dom dts = Seg len ts and A22: for k being Nat st k in Seg len ts holds P[k,dts.k] from SeqDEx (A20); rng dts c= X proof let x be set; assume x in rng dts; then consider k being set such that A23: k in dom ts & x = dts.k by A19,A21,FUNCT_1:def 5; reconsider k as Nat by A23,FINSEQ_3:25; ex dt being DecoratedTree of [:the carrier of G, D():] st dt = x & dt`1 = ts.k & dt in Union f by A19,A22,A23; hence thesis by A11; end; then reconsider dts as FinSequence of X by FINSEQ_1:def 4; A24: dom roots ts = dom ts by Def1; A25: dom pr1 roots dts = dom roots dts & dom pr2 roots dts = dom roots dts by Def2,Def3; then A26: dom pr1 roots dts = dom ts & dom pr2 roots dts = dom ts by A19,A21,Def1; now let k be Nat; assume A27: k in dom ts; then consider dt being DecoratedTree of [:the carrier of G, D():] such that A28: dt = dts.k & dt`1 = ts.k & dt in Union f by A19,A22; reconsider r = {} as Node of dt by TREES_1:47; ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{} by A27,Def1; then A29: (roots ts).k = (dt.r)`1 by A28,TREES_3:41; ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{} by A19,A21,A27,Def1; hence (roots ts).k = (pr1 roots dts).k by A25,A26,A27,A28,A29,Def2; end; then A30: roots ts = pr1 roots dts by A24,A26,FINSEQ_1:17; then A31: [nt, NTV(nt, dts)]-tree dts in X by A13,A17; A32: 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:22; then rng dts c= Trees [:the carrier of G, D():] by A32,XBOOLE_1:1; then reconsider dts' = dts as FinSequence of Trees [:the carrier of G,D():] by FINSEQ_1:def 4; A33: 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:22; then rng ts c= Trees the carrier of G by A33,XBOOLE_1:1; then reconsider ts' = ts as FinSequence of Trees the carrier of G by FINSEQ_1:def 4; now let i be Nat; assume i in dom dts; then consider dt being DecoratedTree of [:the carrier of G, D():] such that A34: dt = dts.i & dt`1 = ts.i & dt in Union f by A21,A22; let T be DecoratedTree of [:the carrier of G, D():]; assume T = dts.i; hence ts.i = T`1 by A34; end; then A35: ([nt, NTV(nt, dts)]-tree dts')`1 = nt-tree ts' by A19,A21,TREES_4:27; A36: rng ts c= dom ff by A9,FINSEQ_1:def 4; then A37: dom (ff * ts) = dom ts by RELAT_1:46; now let k be Nat; assume A38: k in dom ts; then consider dt being DecoratedTree of [:the carrier of G, D():] such that A39: dt = dts.k & dt`1 = ts.k & dt in Union f by A19,A22; reconsider r = {} as Node of dt by TREES_1:47; A40: ts.k in rng ts by A38,FUNCT_1:def 5; A41: x.k = ff.(dt`1) by A37,A38,A39,FUNCT_1:22 .= dt`2.{} by A9,A10,A36,A39,A40 .= (dt.r)`2 by TREES_3:41; ex T being DecoratedTree st T = dts.k & (roots dts).k = T.r by A19,A21,A38,Def1; hence x.k = (pr2 roots dts).k by A25,A26,A38,A39,A41,Def3; end; then A42: x = pr2 roots dts by A26,A37,FINSEQ_1:17; reconsider r = {} as Node of [nt, NTermVal(nt, rts, x)]-tree dts by TREES_1:47; nt-tree ts in TS(G) by A5,A11,A31,A35; then ff.(nt-tree ts) = (([nt, NTermVal(nt, rts, x)]-tree dts)`2).r by A10,A11,A30,A31,A35,A42 .= (([nt, NTermVal(nt, rts, x)]-tree dts).r)`2 by TREES_3:41 .= [nt, NTermVal(nt, rts, x)]`2 by TREES_4:def 4; hence ff.(nt-tree ts) = NTermVal(nt, rts, ff * ts) by MCART_1:7; 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 A6: nt ==> roots ts & for t being DecoratedTree of the carrier of G st t in rng ts holds P[t]; A7: rng ts c= TS(G) by FINSEQ_1:def 4; then rng ts c= dom f1() by FUNCT_2:def 1; then A8: dom (f1() * ts) = dom ts & dom ts = Seg len ts by FINSEQ_1:def 3,RELAT_1:46; reconsider ntv1 = f1() * ts as FinSequence; reconsider ntv1 as FinSequence of D(); rng ts c= dom f2() by A7,FUNCT_2:def 1; then A9: dom (f2() * ts) = dom ts by RELAT_1:46; now let x be set; assume A10: x in dom ts; then reconsider t =ts.x as Element of FinTrees the carrier of G by Th2; t in rng ts by A10,FUNCT_1:def 5; then A11: f1().t = f2().t by A6; thus (f1() * ts).x = f1().t by A8,A10,FUNCT_1:22 .= (f2() * ts).x by A9,A10,A11,FUNCT_1:22; end; then A12: f1() * ts = f2() * ts by A8,A9,FUNCT_1:9; f1().(nt-tree ts) = NTermVal (nt, roots ts, ntv1) by A1,A6 .= f2().(nt-tree ts) by A2,A6,A12; hence P[nt-tree ts]; end; A13: for t being DecoratedTree of the carrier of G st t in TS(G) holds P[t] from DTConstrInd (A3,A5); now let x be set; assume A14: x in TS(G); then reconsider x' = x as Element of FinTrees the carrier of G; x' = x; hence f1().x = f2().x by A13,A14; end; hence thesis by FUNCT_2:18; 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 :Def5: 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 Def5; then reconsider O = 0 , S = 1 as Symbol of PN by TARSKI:def 2; Lm3: S ==> <*O*> & S ==> <*S*> by Def5; Lm4: S ==> <*O*> by Def5; Lm5: S ==> <*S*> by Def5; Lm6: Terminals PN = {x where x is Symbol of PN : not ex tnt being FinSequence st x ==> tnt } by LANG1:def 2; Lm7: 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:106; then x is FinSequence of the carrier of PN by FINSEQ_2:def 3; hence contradiction by A1,Def5; end; then Lm8: O in Terminals PN by Lm6; Lm9: 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 & not ex tnt being FinSequence st y ==> tnt by Lm6; y = O or y = S & {O, S} <> {} by Lm2,TARSKI:def 2; hence x in {O} by A1,Lm4,TARSKI:def 1; end; Lm10: NonTerminals PN = {x where x is Symbol of PN : ex tnt being FinSequence st x ==> tnt } by LANG1:def 3; then Lm11: S in NonTerminals PN by Lm4; then Lm12: {S} c= NonTerminals PN by ZFMISC_1:37; Lm13: 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 & ex tnt being FinSequence st y ==> tnt by Lm10; y = O or y = S by Lm2,TARSKI:def 2; hence x in {S} by A1,Lm7,TARSKI:def 1; end; then Lm14: NonTerminals PN = { S } by Lm12,XBOOLE_0:def 10; reconsider TSPN = TS(PN) as non empty Subset of FinTrees the carrier of PN by Def4,Lm8; begin :: Some properties of decorated tree constructions ::::::::::::::::::::::::: definition let G be non empty DTConstrStr; attr G is with_terminals means :Def6: Terminals G <> {}; attr G is with_nonterminals means :Def7: NonTerminals G <> {}; attr G is with_useful_nonterminals means :Def8: for nt being Symbol of G st nt in NonTerminals G ex p being FinSequence of TS(G) st nt ==> roots p; end; Lm15: PN is with_terminals with_nonterminals with_useful_nonterminals proof thus Terminals PN <> {} by Lm8; thus NonTerminals PN <> {} by Lm11; reconsider rO = root-tree O as Element of TSPN by Def4,Lm8; 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 Lm13,TARSKI:def 1; take p; A2: dom <*rO*> = Seg 1 & dom <*O*> = Seg 1 by FINSEQ_1:55; now let i be Nat; assume A3: i in dom p; reconsider rO as DecoratedTree; take rO; i = 1 & <*O*>.1 = O by A2,A3,FINSEQ_1:4,57,TARSKI:def 1; hence rO = p.i & <*O*>.i = rO.{} by FINSEQ_1:57,TREES_4:3; end; hence nt ==> roots p by A1,A2,Def1,Lm4; end; definition cluster with_terminals with_nonterminals with_useful_nonterminals strict (non empty DTConstrStr); existence by Lm15; 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 Fr_Set0; hence thesis by Def6,LANG1:def 2; end; cluster TS G -> non empty; coherence proof Terminals G is non empty by Def6; then consider t being set such that A1: t in Terminals G by XBOOLE_0:def 1; t in {s where s is Symbol of G: not ex tnt being FinSequence st s==>tnt} by A1,LANG1:def 2; then consider s being Symbol of G such that A2: t = s & not ex tnt being FinSequence st s ==> tnt; thus thesis by A1,A2,Def4; end; end; definition let G be with_useful_nonterminals (non empty DTConstrStr); cluster TS G -> non empty; coherence proof consider s being 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 Def4; 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 consider p being FinSequence of TS G such that A1: s ==> roots p by Def8; thus thesis by A1,Def4; 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 Fr_Set0; hence thesis by Def7,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 :Def9: nt ==> roots it; existence by Def8; 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 Def4; 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 Def9; hence thesis by Def4; 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 A4: nt ==> roots ts & 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; 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; hence nt-tree ts = root-tree s 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 tsg = root-tree s 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; 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; hence ex ts being FinSequence of TS G st (root-tree s) = nt-tree ts & nt ==> roots ts by A3,A4; end; end; A5: now let nnt be Symbol of G, tts be FinSequence of TS G; assume A6: nnt ==> roots tts & 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 A7: (nnt-tree tts).{} = nt; take ts = tts; thus (nnt-tree tts) = nt-tree ts & nt ==> roots ts by A6,A7,TREES_4:def 4; end; end; A8: for t being DecoratedTree of the carrier of G st t in TS G holds P[t] from DTConstrInd (A1,A5); let tsg be Element of TS G, nt be NonTerminal of G; assume tsg.{} = nt; hence ex ts being FinSequence of TS G st tsg=nt-tree ts & nt==> roots ts by A8; end; begin :: Peano naturals continued :::::::::::::::::::::::::::::::::::::::::::::::: definition cluster PeanoNat -> with_terminals with_nonterminals with_useful_nonterminals; coherence by Lm15; end; set PN = PeanoNat; reconsider O as Terminal of PN by Lm8; reconsider S as NonTerminal of PN by Lm11; 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:47; t.r = 0 or t.r = 1 by Lm2,TARSKI:def 2; then (roots <*t*> = <*0*> or roots <*t*> = <*1*>) & nt = S by Lm14,Th4,TARSKI:def 1 ; then nt-tree <*t*> in TS PN by Def4,Lm4,Lm5; hence thesis by TREES_4:def 5; end; end; definition let x be FinSequence of NAT such that A1: x <> {}; func plus-one x -> Nat means :Def10: ex n being Nat st it = n+1 & x.1 = n; existence proof len x <> 0 by A1,FINSEQ_1:25; then len x > 0 by NAT_1:19; then len x >= 0+1 by NAT_1:38; then 1 in dom x by FINSEQ_3:27; then x.1 in rng x & rng x c= NAT by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider n = x.1 as Nat; take n+1, n; thus thesis; end; correctness; end; deffunc N(set,set,FinSequence of NAT) = plus-one($3); definition func PN-to-NAT -> Function of TS(PeanoNat), NAT means :Def11: (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)) 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)) 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)); 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 :Def12: 1-tree <*x*>; coherence proof reconsider r = {} as Node of x by TREES_1:47; roots <*x*> = <*x.r*> & (x.r = O or x.r = S) by Lm2,Th4,TARSKI:def 2 ; hence thesis by Def4,Lm4,Lm5; end; end; deffunc F(set,Element of TS(PeanoNat)) = PNsucc $2; definition func NAT-to-PN -> Function of NAT, TS(PeanoNat) means :Def13: 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) from LambdaRecExD; 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 & for n being Nat holds it1.(n+1) = F(n,it1.n); A3: it2.0 = root-tree O & for n being Nat holds it2.(n+1) = F(n,it2.n) by A1; it1 = it2 from LambdaRecUnD (A2, A3); 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 Def11 .= root-tree O by Def13; hence P[root-tree s] by A2,Lm9,TARSKI:def 1; end; A3: now let nt be Symbol of PN, ts be FinSequence of TS(PN); assume A4: nt ==> roots ts & for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t]; then nt <> O by Lm7; then A5: nt = S by Lm2,TARSKI:def 2; roots ts = <*O*> or roots ts = <*S*> by A4,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider dt being Element of FinTrees the carrier of PN such that A6: ts = <*dt*> & dt in TS(PN) by Th5; reconsider dt as Element of TS(PN) by A6; rng ts = {dt} by A6,FINSEQ_1:55; then dt in rng ts by TARSKI:def 1; then A7: dt = NAT-to-PN.(PN-to-NAT.dt) by A4; A8: PN-to-NAT * ts = <*PN-to-NAT.dt*> by A6,FINSEQ_2:39; reconsider N = PN-to-NAT.dt as Nat; reconsider x = <*N*> as FinSequence of NAT; {} <> <*N*> by TREES_1:4; then consider n being Nat such that A9: plus-one(x) = n+1 & <*N*>.1 = n by Def10; N = n by A9,FINSEQ_1:57; then NAT-to-PN.(n+1) = PNsucc dt by A7,Def13 .= nt-tree ts by A5,A6,Def12; hence P[nt-tree ts] by A4,A8,A9,Def11; 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; Lm16: 0 = PN-to-NAT.(root-tree O) by Def11 .= PN-to-NAT.(NAT-to-PN.0) by Def13; Lm17: now let n be 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:47; 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 Def13 .= S-tree <*NAT-to-PN.n*> by Def12; A4: S ==> roots <*NAT-to-PN.n*> by A2,Lm3,Th4; {} <> <*n*> by TREES_1:4; then consider k being Nat such that A5: plus-one <*n*> = k+1 & <*n*>.1 = k by Def10; <*PN-to-NAT.(NAT-to-PN.n)*> = PN-to-NAT * <*NAT-to-PN.n*> by FINSEQ_2:39; then PN-to-NAT.(S-tree <*NAT-to-PN.n*>) = plus-one <*n*> by A1,A4,Def11 .= n+1 by A5,FINSEQ_1:57; hence n+1 = PN-to-NAT.(NAT-to-PN.(n+1)) by A3; end; theorem for n being Nat holds n = PN-to-NAT.(NAT-to-PN.n) proof defpred P[Nat] means $1 = PN-to-NAT.(NAT-to-PN.$1); A1: P[0] by Lm16; A2: for n being Nat st P[n] holds P[n+1] by Lm17; thus for n being Nat holds P[n] from Ind (A1,A2); end; begin :: Tree traversals and terminal language ::::::::::::::::::::::::::::::::::: definition let D be set, F be FinSequence of D*; func FlattenSeq F -> Element of D* means :Def14: ex g being BinOp of D* st (for p, q being Element of D* holds g.(p,q) = p^q) & it = g "**" F; existence proof deffunc F(Element of D*,Element of D*) = $1^$2; consider g being BinOp of D* such that A1: for a, b being Element of D* holds g.(a,b) = F(a,b) from BinOpLambda; take g "**" F, g; thus thesis by A1; end; uniqueness proof let it1, it2 be Element of D*; given g1 being BinOp of D* such that A2: (for p, q being Element of D* holds g1.(p,q) = p^q) & it1 = g1 "**" F; given g2 being BinOp of D* such that A3: (for p, q being Element of D* holds g2.(p,q) = p^q) & it2 = g2 "**" F; now let a, b be Element of D*; thus g1.(a,b) = a^b by A2 .= g2.(a,b) by A3; end; hence it1 = it2 by A2,A3,BINOP_1:2; end; end; theorem Th13: for D being set, d be Element of D* holds FlattenSeq <*d*> = d proof let D be set, d be Element of D*; ex g being BinOp of D* st (for p, q being Element of D* holds g.(p,q) = p^q) & FlattenSeq <*d*> = g "**" <* d *> by Def14; hence FlattenSeq <*d*> = d by FINSOP_1:12; end; 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 x' = x as Element of T by A3; <*x'*> is FinSequence of T; hence F(x) in (Terminals G)*; end; assume not C[x]; {} is FinSequence of Terminals G by FINSEQ_1:29; hence G(x) in (Terminals G)* by FINSEQ_1:def 11; 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 Lambda1C(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 :Def15: 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:7; 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 for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==> roots ts holds f.(nt-tree ts) = FlattenSeq(f * ts) 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 & (for t being Symbol of G st t in Terminals G holds f1.(root-tree t) = <*t*>) & (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 A8: it2 = f2.tsg & (for t being Symbol of G st t in Terminals G holds f2.(root-tree t) = <*t*>) & (for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==> roots ts holds f2.(nt-tree ts) = FlattenSeq(f2 * ts)); A9: now hereby let t be Symbol of G; assume A10: t in Terminals G; hence f1.(root-tree t) = <*t*> by A7 .= T(t) by A4,A10; 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 A7; end; A11: now hereby let t be Symbol of G; assume A12: t in Terminals G; hence f2.(root-tree t) = <*t*> by A8 .= T(t) by A4,A12; 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 A8; end; f1 = f2 from DTConstrUniqDef (A9, A11); hence it1 = it2 by A7,A8; end; A13: now let x be set; assume x in the carrier of G; then reconsider x' = x as Element of G; <*x'*> 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 A14: for s being set st s in the carrier of G holds s2s.s = F(s) from Lambda1( A13 ); 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 :Def16: 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 A15: (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:7; 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 A15; hence f.(root-tree t) = <*t*> by A14; end; let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence; assume A16: rts = roots ts & 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 A15,A16 .= <*nt*>^FlattenSeq(x) by A14; 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 A17: it1 = f1.tsg & (for t being Symbol of G st t in Terminals G holds f1.(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 = f1 * ts holds f1.(nt-tree ts) = <*nt*>^FlattenSeq(x)); given f2 being Function of (TS G), (the carrier of G)* such that A18: it2 = f2.tsg & (for t being Symbol of G st t in Terminals G holds f2.(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 = f2 * ts holds f2.(nt-tree ts) = <*nt*>^FlattenSeq(x)); A19: now hereby let t be Symbol of G; assume t in Terminals G; hence f1.(root-tree t) = <*t*> by A17 .= T(t) by A14; 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 A17 .= N(nt,roots ts,f1 * ts) by A14; end; A21: now hereby let t be Symbol of G; assume t in Terminals G; hence f2.(root-tree t) = <*t*> by A18 .= T(t) by A14; 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 A18 .= N(nt,roots ts,f2 * ts) by A14; end; f1 = f2 from DTConstrUniqDef (A19, A21); hence it1 = it2 by A17,A18; 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 :Def17: 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 A23: (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:7; 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 A23; hence f.(root-tree t) = <*t*> by A14; end; let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence; assume A24: rts = roots ts & 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 A23,A24 .= FlattenSeq(x)^<*nt*> by A14; 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 A25: it1 = f1.tsg & (for t being Symbol of G st t in Terminals G holds f1.(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 = f1 * ts holds f1.(nt-tree ts) = FlattenSeq(x)^<*nt*>); given f2 being Function of (TS G), (the carrier of G)* such that A26: it2 = f2.tsg & (for t being Symbol of G st t in Terminals G holds f2.(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 = f2 * ts holds f2.(nt-tree ts) = FlattenSeq(x)^<*nt*>); A27: now hereby let t be Symbol of G; assume t in Terminals G; hence f1.(root-tree t) = <*t*> by A25 .= T(t) by A14; 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 A25 .= N(nt,roots ts,f1 * ts) by A14; 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 A14; 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 A26 .= N(nt,roots ts,f2 * ts) by A14; end; f1 = f2 from DTConstrUniqDef (A27, A29); hence it1 = it2 by A25,A26; 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 :Def18: { 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 consider tsg being Element of FinTrees the carrier of G such that A1: x = TerminalString tsg & tsg in TS G & tsg.{} = nt; thus thesis by A1,FINSEQ_1:def 11; end; hence thesis; end; func PreTraversalLanguage nt -> Subset of (the carrier of G)* equals :Def19: { 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 consider tsg being Element of FinTrees the carrier of G such that A2: x = PreTraversal tsg & tsg in TS G & tsg.{} = nt; thus thesis by A2,FINSEQ_1:def 11; end; hence thesis; end; func PostTraversalLanguage nt -> Subset of (the carrier of G)* equals :Def20: { 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 consider tsg being Element of FinTrees the carrier of G such that A3: x = PostTraversal tsg & tsg in TS G & tsg.{} = nt; thus thesis by A3,FINSEQ_1:def 11; end; hence thesis; end; end; theorem Th14: 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) & (for t being Symbol of PN st t in Terminals PN holds f.(root-tree t) = <*t*>) & (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 Def15; defpred P[DecoratedTree of the carrier of PN] means TerminalString $1 = <*0*>; A2: now let s be Symbol of PN; assume s in Terminals PN; then s = O by Lm9,TARSKI:def 1; hence P[root-tree s] by A1; end; A3: now let nt be Symbol of PN, ts be FinSequence of TS PN; assume A4: nt ==> roots ts & for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t]; then A5: nt-tree ts in TS PN by Def4; nt = S & (roots ts = <*O*> or roots ts = <*1*>) by A4,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider x being Element of FinTrees the carrier of PN such that A6: ts = <*x*> & x in TS PN by Th5; reconsider x' = x as Element of TS PN by A6; rng ts = {x} by A6,FINSEQ_1:56; then A7: x in rng ts by TARSKI:def 1; f.x' is Element of (Terminals PN)*; then A8: f.x' = TerminalString x by A1,Def15 .= <*O*> by A4,A7; f * ts = <*f.x*> by A6,FINSEQ_2:39; then f.(nt-tree ts) = FlattenSeq(<*f.x'*>) by A1,A4 .= <*O*> by A8,Th13; hence P[nt-tree ts] by A1,A5,Def15; end; thus for t being DecoratedTree of the carrier of PN st t in TS PN holds P[t] from DTConstrInd(A2,A3); 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; A2: TerminalLanguage nt = { TerminalString tsg where tsg is Element of FinTrees the carrier of PN : tsg in TS PN & tsg.{} = nt } by Def18; 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 by A2; then x = <*O*> by Th14; hence x in {<*0*>} by TARSKI:def 1; end; let x be set; assume x in {<*0*>}; then A3: 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; A4: rtO.{} = O by TREES_4:3; then S ==> roots <*rtO*> by Lm4,Th4; then A5: S-tree <*prtO*> in TS PN by Def4; then TerminalString (S-tree srtO) = x & (S-tree <*rtO*>).{} = S & TerminalString rtO = x by A3,Th14,TREES_4:def 4; hence x in TerminalLanguage nt by A1,A2,A4,A5; end; theorem Th16: 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) & (for t being Symbol of PN st t in Terminals PN holds f.(root-tree t) = <*t*>) & (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 Def16; 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*>; A2: now let s be Symbol of PN; assume A3: s in Terminals PN; thus P[root-tree s] proof take t = rtO; thus root-tree s = t by A3,Lm9,TARSKI:def 1; thus PreTraversal t = <*O*> by A1 .= {}^<*O*> by FINSEQ_1:47 .= (0 |-> 1)^<*0*> by FINSEQ_2:72 .= ((height dom t) |-> 1)^<*0*> by TREES_1:79,TREES_4:3; end; end; A4: now let nt be Symbol of PN, ts be FinSequence of TS PN; assume A5: nt ==> roots ts & for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t]; then reconsider t' = nt-tree ts as Element of TS PN by Def4; A6: nt = S & (roots ts = <*O*> or roots ts = <*1*>) by A5,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider x being Element of FinTrees the carrier of PN such that A7: ts = <*x*> & x in TS PN by Th5; reconsider x' = x as Element of TS PN by A7; rng ts = {x} by A7,FINSEQ_1:56; then x in rng ts by TARSKI:def 1; then A8: ex t' being Element of TS PN st x = t' & PreTraversal t' = ((height dom t') |-> 1)^<*0*> by A5; f.x' is Element of (the carrier of PN)*; then A9: f.x' = ((height dom x') |-> 1)^<*0*> by A1,A8,Def16; f * ts = <*f.x*> by A7,FINSEQ_2:39; then A10: f.(nt-tree ts) = <*nt*>^FlattenSeq(<*f.x'*>) by A1,A5 .= <*nt*>^(((height dom x') |-> 1)^<*0*>) by A9,Th13 .= <*nt*>^((height dom x') |-> 1)^<*0*> by FINSEQ_1:45 .= (1|->1)^((height dom x') |-> 1)^<*0*> by A6,FINSEQ_2:73 .= (((height dom x')+1) |-> 1)^<*0*> by FINSEQ_2:143 .= ((height ^dom x') |-> 1)^<*0*> by TREES_3:83; A11: dom (nt-tree x') = ^dom x' & t' = nt-tree x' by A7,TREES_4:13,def 5; f.t' is Element of (the carrier of PN)*; then PreTraversal(nt-tree ts) = f.(nt-tree ts) by A1,Def16; hence P[nt-tree ts] by A10,A11; end; A12: for t being DecoratedTree of the carrier of PN st t in TS PN holds P[t] from DTConstrInd(A2,A4); let t be Element of TS PeanoNat; P[t] by A12; 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 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:79,TREES_4:3; then PreTraversal rtO = (0 |-> 1)^<*O*> by Th16; then A1: PreTraversal rtO = {}^<*O*> by FINSEQ_2:72 .= <*O*> by FINSEQ_1:47; thus (nt = 0 implies PreTraversalLanguage nt = {<*0*>}) proof assume A2: nt = 0; A3: PreTraversalLanguage O = { PreTraversal tsg where tsg is Element of FinTrees the carrier of PN : tsg in TS PN & tsg.{} = O } by Def19; hereby let x be set; assume x in PreTraversalLanguage nt; then consider tsg being Element of FinTrees the carrier of PN such that A4: x = PreTraversal tsg & tsg in TS PN & tsg.{} = O by A2,A3; tsg = root-tree O by A4,Th9; hence x in {<*0*>} by A1,A4,TARSKI:def 1; end; let x be set; assume x in {<*0*>}; then A5: x = <*O*> by TARSKI:def 1; rtO.{} = O by TREES_4:3; hence x in PreTraversalLanguage nt by A1,A2,A3,A5; end; assume A6: nt = 1; A7: PreTraversalLanguage S = { PreTraversal tsg where tsg is Element of FinTrees the carrier of PN : tsg in TS PN & tsg.{} = S } by Def19; 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 & tsg in TS PN & tsg.{} = S by A6,A7; consider ts being FinSequence of TS PN such that A9: tsg = S-tree ts & S ==> roots ts by A8,Th10; roots ts = <*0*> or roots ts = <*1*> by A9,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider t being Element of FinTrees the carrier of PN such that A10: ts = <*t*> & t in TS PN by Th5; tsg = S-tree t by A9,A10,TREES_4:def 5; then dom tsg = ^dom t by TREES_4:13; then height dom tsg = (height dom t) + 1 by TREES_3:83; then height dom tsg<>0 & x=((height dom tsg)|->1)^<*0*> by A8,Th16; hence x in { (n|->1)^<*0*> where n is Nat : n <> 0 }; end; let x be set; assume x in { (n|->1)^<*0*> where n is Nat : n <> 0 }; then consider n being Nat such that A11: x = (n |-> 1)^<*0*> & n <> 0; defpred P[Nat] means $1 <> 0 implies ex tsg being Element of TS PN st tsg.{} = S & PreTraversal tsg = ($1|->1)^<*0*>; A12: P[0]; A13: now let n be Nat; assume A14: 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 A15: tsg.{} = S & PreTraversal tsg = (n|->1)^<*0*> by A14; PreTraversal tsg = ((height dom tsg) |-> 1)^<*0*> by Th16; then n |-> 1 = (height dom tsg) |-> 1 & len(n |-> 1) = n by A15,FINSEQ_1:46,FINSEQ_2:69; then A16: height dom tsg = n by FINSEQ_2:69; take tsg' = S-tree tsg; A17: tsg' = S-tree <*tsg*> by TREES_4:def 5; height dom tsg' = height ^dom tsg by TREES_4:13 .= n+1 by A16,TREES_3:83; hence tsg'.{} = S & PreTraversal tsg' = ((n+1)|->1)^<*0*> by A17,Th16,TREES_4:def 4; suppose A18: n = 0; take tsg' = S-tree rtO; A19: tsg' = S-tree <*rtO*> by TREES_4:def 5; height dom tsg' = height ^dom rtO by TREES_4:13 .= (height dom rtO)+1 by TREES_3:83 .= n+1 by A18,TREES_1:79,TREES_4:3; hence tsg'.{} = S & PreTraversal tsg' = ((n+1)|->1)^<*0*> by A19,Th16,TREES_4:def 4; end; end; for n being Nat holds P[n] from Ind (A12, A13); then ex tsg being Element of TS PN st tsg.{} = S & PreTraversal tsg = (n|->1)^<*0*> by A11; hence x in PreTraversalLanguage nt by A6,A7,A11; end; theorem Th18: 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) & (for t being Symbol of PN st t in Terminals PN holds f.(root-tree t) = <*t*>) & (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 Def17; 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); A2: now let s be Symbol of PN; assume A3: s in Terminals PN; thus P[root-tree s] proof take t = rtO; thus root-tree s = t by A3,Lm9,TARSKI:def 1; thus PostTraversal t = <*O*> by A1 .= <*O*>^{} by FINSEQ_1:47 .= <*0*>^(0 |-> 1) by FINSEQ_2:72 .= <*0*>^((height dom t) |-> 1) by TREES_1:79,TREES_4:3; end; end; A4: now let nt be Symbol of PN, ts be FinSequence of TS PN; assume A5: nt ==> roots ts & for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t]; then reconsider t' = nt-tree ts as Element of TS PN by Def4; A6: nt = S & (roots ts = <*O*> or roots ts = <*1*>) by A5,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider x being Element of FinTrees the carrier of PN such that A7: ts = <*x*> & x in TS PN by Th5; reconsider x' = x as Element of TS PN by A7; rng ts = {x} by A7,FINSEQ_1:56; then x in rng ts by TARSKI:def 1; then A8: ex t' being Element of TS PN st x=t' & PostTraversal t' = <*O*>^((height dom t') |-> 1) by A5; f.x' is Element of (the carrier of PN)*; then A9: f.x' = <*O*>^((height dom x') |-> 1) by A1,A8,Def17; f * ts = <*f.x*> by A7,FINSEQ_2:39; then A10: f.(nt-tree ts) = FlattenSeq(<*f.x'*>)^<*nt*> by A1,A5 .= <*O*>^((height dom x') |-> 1)^<*nt*> by A9,Th13 .= <*O*>^(((height dom x') |-> 1)^<*nt*>) by FINSEQ_1:45 .= <*O*>^(((height dom x')|->1)^(1|->1)) by A6,FINSEQ_2:73 .= <*O*>^(((height dom x')+1) |-> 1) by FINSEQ_2:143 .= <*O*>^((height ^dom x') |-> 1) by TREES_3:83; A11: dom (nt-tree x') = ^dom x' & t' = nt-tree x' by A7,TREES_4:13,def 5; f.t' is Element of (the carrier of PN)*; then PostTraversal(nt-tree ts) = f.(nt-tree ts) by A1,Def17; hence P[nt-tree ts] by A10,A11; end; A12: for t being DecoratedTree of the carrier of PN st t in TS PN holds P[t] from DTConstrInd(A2,A4); let t be Element of TS PeanoNat; P[t] by A12; 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 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:79,TREES_4:3; then PostTraversal rtO = <*0*>^(0 |-> 1) by Th18; then A1: PostTraversal rtO = <*O*>^{} by FINSEQ_2:72 .= <*O*> by FINSEQ_1:47; thus (nt = 0 implies PostTraversalLanguage nt = {<*0*>}) proof assume A2: nt = 0; A3: PostTraversalLanguage O = { PostTraversal tsg where tsg is Element of FinTrees the carrier of PN : tsg in TS PN & tsg.{} = O } by Def20; hereby let x be set; assume x in PostTraversalLanguage nt; then consider tsg being Element of FinTrees the carrier of PN such that A4: x = PostTraversal tsg & tsg in TS PN & tsg.{} = O by A2,A3; tsg = root-tree O by A4,Th9; hence x in {<*0*>} by A1,A4,TARSKI:def 1; end; let x be set; assume x in {<*0*>}; then A5: x = <*O*> by TARSKI:def 1; rtO.{} = O by TREES_4:3; hence x in PostTraversalLanguage nt by A1,A2,A3,A5; end; assume A6: nt = 1; A7: PostTraversalLanguage S = { PostTraversal tsg where tsg is Element of FinTrees the carrier of PN : tsg in TS PN & tsg.{} = S } by Def20; 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 & tsg in TS PN & tsg.{} = S by A6,A7; consider ts being FinSequence of TS PN such that A9: tsg = S-tree ts & S ==> roots ts by A8,Th10; roots ts = <*0*> or roots ts = <*1*> by A9,Def5; then len roots ts = 1 by FINSEQ_1:57; then consider t being Element of FinTrees the carrier of PN such that A10: ts = <*t*> & t in TS PN by Th5; tsg = S-tree t by A9,A10,TREES_4:def 5; then dom tsg = ^dom t by TREES_4:13; then height dom tsg = (height dom t) + 1 by TREES_3:83; then height dom tsg<>0 & x=<*0*>^((height dom tsg)|->1) by A8,Th18; hence x in { <*0*>^(n|->1) where n is Nat : n <> 0 }; end; let x be set; assume x in { <*0*>^(n|->1) where n is Nat : n <> 0 }; then consider n being Nat such that A11: x = <*0*>^(n |-> 1) & n <> 0; defpred P[Nat] means $1 <> 0 implies ex tsg being Element of TS PN st tsg.{} = S & PostTraversal tsg = <*0*>^($1|->1); A12: P[0]; A13: now let n be Nat; assume A14: 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 A15: tsg.{} = S & PostTraversal tsg = <*0*>^(n|->1) by A14; PostTraversal tsg = <*0*>^((height dom tsg) |-> 1) by Th18; then n |-> 1 = (height dom tsg) |-> 1 & len(n |-> 1) = n by A15,FINSEQ_1:46,FINSEQ_2:69; then A16: height dom tsg = n by FINSEQ_2:69; take tsg' = S-tree tsg; A17: tsg' = S-tree <*tsg*> by TREES_4:def 5; height dom tsg' = height ^dom tsg by TREES_4:13 .= n+1 by A16,TREES_3:83; hence tsg'.{} = S & PostTraversal tsg' = <*0*>^((n+1)|->1) by A17,Th18,TREES_4:def 4; suppose A18: n = 0; take tsg' = S-tree rtO; A19: tsg' = S-tree <*rtO*> by TREES_4:def 5; height dom tsg' = height ^dom rtO by TREES_4:13 .= (height dom rtO)+1 by TREES_3:83 .= n+1 by A18,TREES_1:79,TREES_4:3; hence tsg'.{} = S & PostTraversal tsg' = <*0*>^((n+1)|->1) by A19,Th18,TREES_4:def 4; end; end; for n being Nat holds P[n] from Ind (A12, A13); then ex tsg being Element of TS PN st tsg.{} = S & PostTraversal tsg = <*0*>^(n|->1) by A11; hence x in PostTraversalLanguage nt by A6,A7,A11; end; :: What remains to be done, but in another article: :: :: - partial trees (grown from the root towards the leaves) :: - phrases

Back to top