:: DTCONSTR semantic presentation begin deffunc H1( set ) -> Element of NAT = 0 ; deffunc H2( set , set , set ) -> Element of NAT = 0 ; theorem Th1: :: DTCONSTR:1 for D being non empty set for p being FinSequence of FinTrees D holds p is FinSequence of Trees D proof let D be non empty set ; ::_thesis: for p being FinSequence of FinTrees D holds p is FinSequence of Trees D FinTrees D is non empty Subset of (Trees D) by TREES_3:21; hence for p being FinSequence of FinTrees D holds p is FinSequence of Trees D by FINSEQ_2:24; ::_thesis: verum end; theorem Th2: :: DTCONSTR:2 for x, y being set for p being FinSequence of x st y in dom p holds p . y in x proof let x, y be set ; ::_thesis: for p being FinSequence of x st y in dom p holds p . y in x let p be FinSequence of x; ::_thesis: ( y in dom p implies p . y in x ) assume y in dom p ; ::_thesis: p . y in x then A1: p . y in rng p by FUNCT_1:def_3; rng p c= x by FINSEQ_1:def_4; hence p . y in x by A1; ::_thesis: verum end; registration let D be non empty set ; let T be DTree-set of D; cluster -> DTree-yielding for FinSequence of T; coherence for b1 being FinSequence of T holds b1 is DTree-yielding ; 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; :: original: Element redefine mode Element of Tset -> Element of F; coherence for b1 being Element of Tset holds b1 is Element of F proof let x be Element of Tset; ::_thesis: x is Element of F thus x is Element of F ; ::_thesis: verum end; end; definition let D be non empty set ; let T be DTree-set of D; let p be FinSequence of T; :: original: roots redefine func roots p -> FinSequence of D; coherence roots p is FinSequence of D proof let x be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not x in rng (roots p) or x in D ) assume x in rng (roots p) ; ::_thesis: x in D then consider k being set such that A1: k in dom (roots p) and A2: x = (roots p) . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A1; A3: dom (roots p) = dom p by TREES_3:def_18; then consider t being DecoratedTree such that A4: t = p . k and A5: (roots p) . k = t . {} by A1, TREES_3:def_18; reconsider t = t as DecoratedTree of D by A1, A3, A4, Th2, TREES_3:def_6; reconsider r = {} as Node of t by TREES_1:22; t . r in D ; hence x in D by A2, A5; ::_thesis: verum end; end; Lm1: dom (roots {}) = dom {} by TREES_3:def_18 .= {} ; theorem Th3: :: DTCONSTR:3 roots {} = {} by Lm1; theorem Th4: :: DTCONSTR:4 for T being DecoratedTree holds roots <*T*> = <*(T . {})*> proof let T be DecoratedTree; ::_thesis: roots <*T*> = <*(T . {})*> A1: dom <*T*> = Seg 1 by FINSEQ_1:def_8; A2: dom <*(T . {})*> = Seg 1 by FINSEQ_1:def_8; A3: <*T*> . 1 = T by FINSEQ_1:def_8; A4: <*(T . {})*> . 1 = T . {} by FINSEQ_1:def_8; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_<*T*>_holds_ ex_t_being_DecoratedTree_st_ (_t_=_<*T*>_._i_&_<*(T_._{})*>_._i_=_t_._{}_) let i be Element of NAT ; ::_thesis: ( i in dom <*T*> implies ex t being DecoratedTree st ( t = <*T*> . i & <*(T . {})*> . i = t . {} ) ) assume A5: i in dom <*T*> ; ::_thesis: ex t being DecoratedTree st ( t = <*T*> . i & <*(T . {})*> . i = t . {} ) take t = T; ::_thesis: ( t = <*T*> . i & <*(T . {})*> . i = t . {} ) thus ( t = <*T*> . i & <*(T . {})*> . i = t . {} ) by A1, A3, A4, A5, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; hence roots <*T*> = <*(T . {})*> by A1, A2, TREES_3:def_18; ::_thesis: verum end; theorem Th5: :: DTCONSTR:5 for D being non empty set for F being Subset of (FinTrees D) for p being FinSequence of F st len (roots p) = 1 holds ex x being Element of FinTrees D st ( p = <*x*> & x in F ) proof let D be non empty set ; ::_thesis: for F being Subset of (FinTrees D) for p being FinSequence of F st len (roots p) = 1 holds ex x being Element of FinTrees D st ( p = <*x*> & x in F ) let F be Subset of (FinTrees D); ::_thesis: for p being FinSequence of F st len (roots p) = 1 holds ex x being Element of FinTrees D st ( p = <*x*> & x in F ) let p be FinSequence of F; ::_thesis: ( len (roots p) = 1 implies ex x being Element of FinTrees D st ( p = <*x*> & x in F ) ) assume len (roots p) = 1 ; ::_thesis: ex x being Element of FinTrees D st ( p = <*x*> & x in F ) then A1: dom (roots p) = Seg 1 by FINSEQ_1:def_3; A2: dom p = dom (roots p) by TREES_3:def_18; then A3: 1 in dom p by A1; then reconsider x = p . 1 as Element of FinTrees D by Th2; take x ; ::_thesis: ( p = <*x*> & x in F ) thus ( p = <*x*> & x in F ) by A1, A2, A3, Th2, FINSEQ_1:def_8; ::_thesis: verum end; theorem :: DTCONSTR:6 for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*> proof let T1, T2 be DecoratedTree; ::_thesis: roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*> A1: len <*T1,T2*> = 2 by FINSEQ_1:44; A2: len <*(T1 . {}),(T2 . {})*> = 2 by FINSEQ_1:44; A3: <*T1,T2*> . 1 = T1 by FINSEQ_1:44; A4: <*(T1 . {}),(T2 . {})*> . 1 = T1 . {} by FINSEQ_1:44; A5: <*T1,T2*> . 2 = T2 by FINSEQ_1:44; A6: <*(T1 . {}),(T2 . {})*> . 2 = T2 . {} by FINSEQ_1:44; A7: dom <*T1,T2*> = Seg 2 by A1, FINSEQ_1:def_3; A8: dom <*(T1 . {}),(T2 . {})*> = Seg 2 by A2, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_<*T1,T2*>_holds_ ex_t_being_DecoratedTree_st_ (_t_=_<*T1,T2*>_._i_&_<*(T1_._{}),(T2_._{})*>_._i_=_t_._{}_) let i be Element of NAT ; ::_thesis: ( i in dom <*T1,T2*> implies ex t being DecoratedTree st ( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) ) assume i in dom <*T1,T2*> ; ::_thesis: ex t being DecoratedTree st ( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) then i in Seg 2 by A1, FINSEQ_1:def_3; then ( i = 1 or i = 2 ) by FINSEQ_1:2, TARSKI:def_2; hence ex t being DecoratedTree st ( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) by A3, A4, A5, A6; ::_thesis: verum end; hence roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*> by A7, A8, TREES_3:def_18; ::_thesis: verum end; definition let X, Y be set ; let f be FinSequence of [:X,Y:]; :: original: pr1 redefine func pr1 f -> FinSequence of X; coherence pr1 f is FinSequence of X proof A1: dom (pr1 f) = dom f by MCART_1:def_12; dom f = Seg (len f) by FINSEQ_1:def_3; then reconsider p = pr1 f as FinSequence by A1, FINSEQ_1:def_2; rng p c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in X ) assume x in rng p ; ::_thesis: x in X then consider i being set such that A2: i in dom p and A3: x = p . i by FUNCT_1:def_3; A4: f . i in [:X,Y:] by A1, A2, Th2; x = (f . i) `1 by A1, A2, A3, MCART_1:def_12; hence x in X by A4, MCART_1:10; ::_thesis: verum end; hence pr1 f is FinSequence of X by FINSEQ_1:def_4; ::_thesis: verum end; :: original: pr2 redefine func pr2 f -> FinSequence of Y; coherence pr2 f is FinSequence of Y proof A5: dom (pr2 f) = dom f by MCART_1:def_13; dom f = Seg (len f) by FINSEQ_1:def_3; then reconsider p = pr2 f as FinSequence by A5, FINSEQ_1:def_2; rng p c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Y ) assume x in rng p ; ::_thesis: x in Y then consider i being set such that A6: i in dom p and A7: x = p . i by FUNCT_1:def_3; A8: f . i in [:X,Y:] by A5, A6, Th2; x = (f . i) `2 by A5, A6, A7, MCART_1:def_13; hence x in Y by A8, MCART_1:10; ::_thesis: verum end; hence pr2 f is FinSequence of Y by FINSEQ_1:def_4; ::_thesis: verum end; end; theorem Th7: :: DTCONSTR:7 ( pr1 {} = {} & pr2 {} = {} ) proof set r = <*> [:{},{}:]; dom (pr1 (<*> [:{},{}:])) = dom {} .= {} ; hence pr1 {} = {} ; ::_thesis: pr2 {} = {} dom (pr2 (<*> [:{},{}:])) = dom {} .= {} ; hence pr2 {} = {} ; ::_thesis: verum end; begin registration let A be non empty set ; let R be Relation of A,(A *); cluster DTConstrStr(# A,R #) -> non empty ; coherence not DTConstrStr(# A,R #) is empty ; end; scheme :: DTCONSTR:sch 1 DTConstrStrEx{ F1() -> non empty set , P1[ set , set ] } : ex G being non empty strict DTConstrStr st ( the carrier of G = F1() & ( for x being Symbol of G for p being FinSequence of the carrier of G holds ( x ==> p iff P1[x,p] ) ) ) proof consider PR being Relation of F1(),(F1() *) such that A1: for x, y being set holds ( [x,y] in PR iff ( x in F1() & y in F1() * & P1[x,y] ) ) from RELSET_1:sch_1(); take DT = DTConstrStr(# F1(),PR #); ::_thesis: ( the carrier of DT = F1() & ( for x being Symbol of DT for p being FinSequence of the carrier of DT holds ( x ==> p iff P1[x,p] ) ) ) thus the carrier of DT = F1() ; ::_thesis: for x being Symbol of DT for p being FinSequence of the carrier of DT holds ( x ==> p iff P1[x,p] ) let x be Symbol of DT; ::_thesis: for p being FinSequence of the carrier of DT holds ( x ==> p iff P1[x,p] ) let p be FinSequence of the carrier of DT; ::_thesis: ( x ==> p iff P1[x,p] ) hereby ::_thesis: ( P1[x,p] implies x ==> p ) assume x ==> p ; ::_thesis: P1[x,p] then [x,p] in the Rules of DT by LANG1:def_1; hence P1[x,p] by A1; ::_thesis: verum end; assume A2: P1[x,p] ; ::_thesis: 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; ::_thesis: verum end; scheme :: DTCONSTR:sch 2 DTConstrStrUniq{ F1() -> non empty set , P1[ set , set ] } : for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = F1() & ( for x being Symbol of G1 for p being FinSequence of the carrier of G1 holds ( x ==> p iff P1[x,p] ) ) & the carrier of G2 = F1() & ( for x being Symbol of G2 for p being FinSequence of the carrier of G2 holds ( x ==> p iff P1[x,p] ) ) holds G1 = G2 proof let G1, G2 be non empty strict DTConstrStr ; ::_thesis: ( the carrier of G1 = F1() & ( for x being Symbol of G1 for p being FinSequence of the carrier of G1 holds ( x ==> p iff P1[x,p] ) ) & the carrier of G2 = F1() & ( for x being Symbol of G2 for p being FinSequence of the carrier of G2 holds ( x ==> p iff P1[x,p] ) ) implies G1 = G2 ) assume that A1: the carrier of G1 = F1() and A2: for x being Symbol of G1 for p being FinSequence of the carrier of G1 holds ( x ==> p iff P1[x,p] ) and A3: the carrier of G2 = F1() and A4: for x being Symbol of G2 for p being FinSequence of the carrier of G2 holds ( x ==> p iff P1[x,p] ) ; ::_thesis: G1 = G2 now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_the_Rules_of_G1_implies_[x,y]_in_the_Rules_of_G2_)_&_(_[x,y]_in_the_Rules_of_G2_implies_[x,y]_in_the_Rules_of_G1_)_) let x, y be set ; ::_thesis: ( ( [x,y] in the Rules of G1 implies [x,y] in the Rules of G2 ) & ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 ) ) hereby ::_thesis: ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 ) assume A5: [x,y] in the Rules of G1 ; ::_thesis: [x,y] in the Rules of G2 then A6: y in the carrier of G1 * by ZFMISC_1:87; reconsider x1 = x as Symbol of G1 by A5, ZFMISC_1:87; reconsider y1 = y as FinSequence of the carrier of G1 by A6, FINSEQ_2:def_3; A7: ( x1 ==> y1 iff P1[x1,y1] ) by A2; reconsider x2 = x as Symbol of G2 by A1, A3, A5, ZFMISC_1:87; reconsider y2 = y as FinSequence of the carrier of G2 by A1, A3, A6, FINSEQ_2:def_3; x2 ==> y2 by A4, A5, A7, LANG1:def_1; hence [x,y] in the Rules of G2 by LANG1:def_1; ::_thesis: verum end; assume A8: [x,y] in the Rules of G2 ; ::_thesis: [x,y] in the Rules of G1 then A9: y in the carrier of G2 * by ZFMISC_1:87; reconsider x2 = x as Symbol of G2 by A8, ZFMISC_1:87; reconsider y2 = y as FinSequence of the carrier of G2 by A9, FINSEQ_2:def_3; A10: ( x2 ==> y2 iff P1[x2,y2] ) by A4; reconsider x1 = x as Symbol of G1 by A1, A3, A8, ZFMISC_1:87; reconsider y1 = y as FinSequence of the carrier of G1 by A1, A3, A9, FINSEQ_2:def_3; x1 ==> y1 by A2, A8, A10, LANG1:def_1; hence [x,y] in the Rules of G1 by LANG1:def_1; ::_thesis: verum end; hence G1 = G2 by A1, A3, RELAT_1:def_2; ::_thesis: verum end; theorem :: DTCONSTR:8 for G being non empty DTConstrStr holds Terminals G misses NonTerminals G proof let G be non empty DTConstrStr ; ::_thesis: Terminals G misses NonTerminals G A1: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not 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 Terminals G misses NonTerminals G ; ::_thesis: contradiction then consider x being set such that A3: x in Terminals G and A4: x in NonTerminals G by XBOOLE_0:3; A5: ex t being Symbol of G st ( x = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A1, A3; ex t being Symbol of G st ( x = t & ex tnt being FinSequence st t ==> tnt ) by A2, A4; hence contradiction by A5; ::_thesis: verum end; scheme :: DTCONSTR:sch 3 DTCMin{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } : ex X being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) provided A1: dom F1() = NAT and A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } proof set f = F1(); set G = F2(); set D = F3(); deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2))); Union F1() c= FinTrees [: the carrier of F2(),F3():] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Union F1() or u in FinTrees [: the carrier of F2(),F3():] ) assume u in Union F1() ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():] then A4: ex k being set st ( k in NAT & u in F1() . k ) by A1, CARD_5:2; defpred S1[ Element of NAT ] means for u being set st u in F1() . $1 holds u in FinTrees [: the carrier of F2(),F3():]; A5: S1[ 0 ] proof let u be set ; ::_thesis: ( u in F1() . 0 implies u in FinTrees [: the carrier of F2(),F3():] ) assume u in F1() . 0 ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():] then ex t being Symbol of F2() ex d being Element of F3() st ( u = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2; hence u in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: verum end; A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let u be set ; ::_thesis: ( u in F1() . (n + 1) implies u in FinTrees [: the carrier of F2(),F3():] ) assume u in F1() . (n + 1) ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():] then u in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3; then A8: ( u in F1() . n or u in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3; assume A9: not u in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: contradiction then consider o being Symbol of F2(), p being Element of (F1() . n) * such that A10: u = [o,H3(o,p)] -tree p and A11: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) by A7, A8; reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A11; u = [o,H3(o,p)] -tree p by A10; hence contradiction by A9; ::_thesis: verum end; end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A6); hence u in FinTrees [: the carrier of F2(),F3():] by A4; ::_thesis: verum end; then reconsider X = Union F1() as Subset of (FinTrees [: the carrier of F2(),F3():]) ; take X ; ::_thesis: ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) thus X = Union F1() ; ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) hereby ::_thesis: ( ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) let d be Symbol of F2(); ::_thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in X ) assume d in Terminals F2() ; ::_thesis: root-tree [d,F4(d)] in X then root-tree [d,F4(d)] in F1() . 0 by A2; hence root-tree [d,F4(d)] in X by A1, CARD_5:2; ::_thesis: verum end; hereby ::_thesis: for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F let o be Symbol of F2(); ::_thesis: for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X let p be FinSequence of X; ::_thesis: ( o ==> pr1 (roots p) implies [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) assume A12: o ==> pr1 (roots p) ; ::_thesis: [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X set s = pr1 (roots p); set v = pr2 (roots p); A13: dom p = Seg (len p) by FINSEQ_1:def_3; defpred S1[ set , set ] means p . $1 in F1() . $2; A14: for x being Nat st x in Seg (len p) holds ex n being Element of NAT st S1[x,n] proof let x be Nat; ::_thesis: ( x in Seg (len p) implies ex n being Element of NAT st S1[x,n] ) assume x in Seg (len p) ; ::_thesis: ex n being Element of NAT st S1[x,n] then A15: p . x in rng p by A13, FUNCT_1:def_3; rng p c= X by FINSEQ_1:def_4; then ex n being set st ( n in NAT & p . x in F1() . n ) by A1, A15, CARD_5:2; hence ex n being Element of NAT st S1[x,n] ; ::_thesis: verum end; consider pn being FinSequence of NAT such that A16: ( dom pn = Seg (len p) & ( for k being Nat st k in Seg (len p) holds S1[k,pn . k] ) ) from FINSEQ_1:sch_5(A14); A17: now__::_thesis:_(_rng_pn_<>_{}_implies_ex_n_being_Element_of_NAT_st_rng_p_c=_F1()_._n_) defpred S2[ Element of NAT , Element of NAT ] means $1 >= $2; assume rng pn <> {} ; ::_thesis: ex n being Element of NAT st rng p c= F1() . n then A18: ( rng pn is finite & rng pn <> {} & rng pn c= NAT ) by FINSEQ_1:def_4; A19: for x, y being Element of NAT holds ( S2[x,y] or S2[y,x] ) ; A20: for x, y, z being Element of NAT st S2[x,y] & S2[y,z] holds S2[x,z] by XXREAL_0:2; consider n being Element of NAT such that A21: ( n in rng pn & ( for y being Element of NAT st y in rng pn holds S2[n,y] ) ) from CQC_SIM1:sch_4(A18, A19, A20); take n = n; ::_thesis: rng p c= F1() . n thus rng p c= F1() . n ::_thesis: verum proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng p or t in F1() . n ) assume t in rng p ; ::_thesis: t in F1() . n then consider k being set such that A22: k in dom p and A23: t = p . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A22; A24: pn . k in rng pn by A13, A16, A22, FUNCT_1:def_3; then reconsider pnk = pn . k as Element of NAT by A18; consider s being Nat such that A25: n = pnk + s by A21, A24, NAT_1:10; deffunc H4( set , set ) -> set = { ([o1,F5(o1,(pr1 (roots p1)),(pr2 (roots p1)))] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p1 = q & o1 ==> pr1 (roots q) ) } ; for n being Element of NAT holds F1() . n c= F1() . (n + 1) proof let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1) F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3; hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum end; then A26: F1() . pnk c= F1() . n by A25, MEASURE2:18, NAT_1:11; t in F1() . (pn . k) by A13, A16, A22, A23; hence t in F1() . n by A26; ::_thesis: verum end; end; now__::_thesis:_(_rng_pn_=_{}_implies_rng_p_c=_F1()_._0_) assume rng pn = {} ; ::_thesis: rng p c= F1() . 0 then pn = {} ; then p = {} by A16; then rng p = {} ; hence rng p c= F1() . 0 by XBOOLE_1:2; ::_thesis: verum end; then consider n being Element of NAT such that A27: rng p c= F1() . n by A17; A28: X = union (rng F1()) by CARD_3:def_4; F1() . n in rng F1() by A1, FUNCT_1:def_3; then F1() . n c= X by A28, ZFMISC_1:74; then reconsider fn = F1() . n as Subset of (FinTrees [: the carrier of F2(),F3():]) by XBOOLE_1:1; reconsider q = p as FinSequence of fn by A27, FINSEQ_1:def_4; reconsider q9 = q as Element of fn * by FINSEQ_1:def_11; [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } by A12; then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } by XBOOLE_0:def_3; then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in F1() . (n + 1) by A3; hence [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X by A1, CARD_5:2; ::_thesis: verum end; let F be Subset of (FinTrees [: the carrier of F2(),F3():]); ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) implies X c= F ) assume that A29: for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F and A30: for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,H3(o,p)] -tree p in F ; ::_thesis: X c= F defpred S1[ Element of NAT ] means F1() . $1 c= F; A31: S1[ 0 ] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() . 0 or x in F ) reconsider p = <*> F as FinSequence of F ; assume x in F1() . 0 ; ::_thesis: x in F then consider t being Symbol of F2(), d being Element of F3() such that A32: x = root-tree [t,d] and A33: ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> pr1 (roots p) & d = H3(t,p) ) ) by A2, Th3, Th7; [t,d] -tree p = root-tree [t,d] by TREES_4:20; hence x in F by A29, A30, A32, A33; ::_thesis: verum end; A34: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A35: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() . (n + 1) or x in F ) assume that A36: x in F1() . (n + 1) and A37: not x in F ; ::_thesis: contradiction x in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } by A3, A36; then ( x in F1() . n or x in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3; then consider o being Symbol of F2(), p being Element of (F1() . n) * such that A38: x = [o,H3(o,p)] -tree p and A39: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) by A35, A37; rng p c= F1() . n by FINSEQ_1:def_4; then rng p c= F by A35, XBOOLE_1:1; then reconsider p = p as FinSequence of F by FINSEQ_1:def_4; o ==> pr1 (roots p) by A39; hence contradiction by A30, A37, A38; ::_thesis: verum end; end; A40: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A31, A34); thus X c= F ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in F ) assume x in X ; ::_thesis: x in F then consider n being set such that A41: n in NAT and A42: x in F1() . n by A1, CARD_5:2; F1() . n c= F by A40, A41; hence x in F by A42; ::_thesis: verum end; end; scheme :: DTCONSTR:sch 4 DTCSymbols{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } : ex X1 being Subset of (FinTrees the carrier of F2()) st ( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in X1 ) & ( for o being Symbol of F2() for p being FinSequence of X1 st o ==> roots p holds o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) provided A1: dom F1() = NAT and A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } proof set f = F1(); set G = F2(); set D = F3(); set S = the carrier of F2(); set SxD = [: the carrier of F2(),F3():]; deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2))); A4: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } by A2; A5: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3; consider X being Subset of (FinTrees [: the carrier of F2(),F3():]) such that A6: ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) from DTCONSTR:sch_3(A1, A4, A5); set X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ; { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } c= FinTrees the carrier of F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } or x in FinTrees the carrier of F2() ) assume x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ; ::_thesis: x in FinTrees the carrier of F2() then consider tt being Element of FinTrees [: the carrier of F2(),F3():] such that A7: x = tt `1 and tt in Union F1() ; A8: tt `1 = (pr1 ( the carrier of F2(),F3())) * tt by TREES_3:def_12; A9: rng tt c= [: the carrier of F2(),F3():] by RELAT_1:def_19; dom (pr1 ( the carrier of F2(),F3())) = [: the carrier of F2(),F3():] by FUNCT_2:def_1; then dom (tt `1) = dom tt by A8, A9, RELAT_1:27; hence x in FinTrees the carrier of F2() by A7, TREES_3:def_8; ::_thesis: verum end; then reconsider X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } as Subset of (FinTrees the carrier of F2()) ; take X1 = X9; ::_thesis: ( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in X1 ) & ( for o being Symbol of F2() for p being FinSequence of X1 st o ==> roots p holds o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) thus X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ; ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in X1 ) & ( for o being Symbol of F2() for p being FinSequence of X1 st o ==> roots p holds o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) hereby ::_thesis: ( ( for o being Symbol of F2() for p being FinSequence of X1 st o ==> roots p holds o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) let t be Symbol of F2(); ::_thesis: ( t in Terminals F2() implies root-tree t in X1 ) assume A10: t in Terminals F2() ; ::_thesis: root-tree t in X1 A11: (root-tree [t,F4(t)]) `1 = root-tree t by TREES_4:25; root-tree [t,F4(t)] in Union F1() by A6, A10; hence root-tree t in X1 by A11; ::_thesis: verum end; hereby ::_thesis: for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F let nt be Symbol of F2(); ::_thesis: for ts being FinSequence of X1 st nt ==> roots ts holds nt -tree ts in X1 let ts be FinSequence of X1; ::_thesis: ( nt ==> roots ts implies nt -tree ts in X1 ) assume A12: nt ==> roots ts ; ::_thesis: nt -tree ts in X1 A13: dom ts = Seg (len ts) by FINSEQ_1:def_3; defpred S1[ set , set ] means ex dt being DecoratedTree of [: the carrier of F2(),F3():] st ( dt = $2 & dt `1 = ts . $1 & dt in Union F1() ); A14: for k being Nat st k in Seg (len ts) holds ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] ) assume k in Seg (len ts) ; ::_thesis: ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] then A15: ts . k in rng ts by A13, FUNCT_1:def_3; rng ts c= X1 by FINSEQ_1:def_4; then ts . k in X1 by A15; then ex x being Element of FinTrees [: the carrier of F2(),F3():] st ( ts . k = x `1 & x in Union F1() ) ; hence ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] ; ::_thesis: verum end; consider dts being FinSequence of FinTrees [: the carrier of F2(),F3():] such that A16: dom dts = Seg (len ts) and A17: for k being Nat st k in Seg (len ts) holds S1[k,dts . k] from FINSEQ_1:sch_5(A14); rng dts c= Union F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng dts or x in Union F1() ) assume x in rng dts ; ::_thesis: x in Union F1() then consider k being set such that A18: k in dom ts and A19: x = dts . k by A13, A16, FUNCT_1:def_3; reconsider k = k as Element of NAT by A18; ex dt being DecoratedTree of [: the carrier of F2(),F3():] st ( dt = x & dt `1 = ts . k & dt in Union F1() ) by A13, A17, A18, A19; hence x in Union F1() ; ::_thesis: verum end; then reconsider dts = dts as FinSequence of X by A6, FINSEQ_1:def_4; A20: dom (roots ts) = dom ts by TREES_3:def_18; A21: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def_12; then A22: dom (pr1 (roots dts)) = dom ts by A13, A16, TREES_3:def_18; now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_ (roots_ts)_._k_=_(pr1_(roots_dts))_._k let k be Nat; ::_thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k ) assume A23: k in dom ts ; ::_thesis: (roots ts) . k = (pr1 (roots dts)) . k then consider dt being DecoratedTree of [: the carrier of F2(),F3():] such that A24: dt = dts . k and A25: dt `1 = ts . k and dt in Union F1() by A13, A17; reconsider r = {} as Node of dt by TREES_1:22; ex T being DecoratedTree st ( T = ts . k & (roots ts) . k = T . {} ) by A23, TREES_3:def_18; then A26: (roots ts) . k = (dt . r) `1 by A25, TREES_3:39; ex T being DecoratedTree st ( T = dts . k & (roots dts) . k = T . {} ) by A13, A16, A23, TREES_3:def_18; hence (roots ts) . k = (pr1 (roots dts)) . k by A21, A22, A23, A24, A26, MCART_1:def_12; ::_thesis: verum end; then roots ts = pr1 (roots dts) by A20, A22, FINSEQ_1:13; then A27: [nt,H3(nt,dts)] -tree dts in X by A6, A12; A28: rng dts c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4; FinTrees [: the carrier of F2(),F3():] c= Trees [: the carrier of F2(),F3():] by TREES_3:21; then rng dts c= Trees [: the carrier of F2(),F3():] by A28, XBOOLE_1:1; then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F2(),F3():] by FINSEQ_1:def_4; A29: rng ts c= FinTrees the carrier of F2() by FINSEQ_1:def_4; FinTrees the carrier of F2() c= Trees the carrier of F2() by TREES_3:21; then rng ts c= Trees the carrier of F2() by A29, XBOOLE_1:1; then reconsider ts9 = ts as FinSequence of Trees the carrier of F2() by FINSEQ_1:def_4; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_dts_holds_ for_T_being_DecoratedTree_of_[:_the_carrier_of_F2(),F3():]_st_T_=_dts_._i_holds_ ts_._i_=_T_`1 let i be Element of NAT ; ::_thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds ts . i = T `1 ) assume i in dom dts ; ::_thesis: for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds ts . i = T `1 then A30: ex dt being DecoratedTree of [: the carrier of F2(),F3():] st ( dt = dts . i & dt `1 = ts . i & dt in Union F1() ) by A16, A17; let T be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( T = dts . i implies ts . i = T `1 ) assume T = dts . i ; ::_thesis: ts . i = T `1 hence ts . i = T `1 by A30; ::_thesis: verum end; then ([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A13, A16, TREES_4:27; hence nt -tree ts in X1 by A6, A27; ::_thesis: verum end; let F be Subset of (FinTrees the carrier of F2()); ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) implies X1 c= F ) assume that A31: for d being Symbol of F2() st d in Terminals F2() holds root-tree d in F and A32: for o being Symbol of F2() for p being FinSequence of F st o ==> roots p holds o -tree p in F ; ::_thesis: X1 c= F thus X1 c= F ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in F ) assume x in X1 ; ::_thesis: x in F then consider tt being Element of FinTrees [: the carrier of F2(),F3():] such that A33: x = tt `1 and A34: tt in Union F1() ; set FF = { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ; { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } c= FinTrees [: the carrier of F2(),F3():] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } or x in FinTrees [: the carrier of F2(),F3():] ) assume x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ; ::_thesis: x in FinTrees [: the carrier of F2(),F3():] then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st ( x = dt & dt `1 in F ) ; hence x in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: verum end; then reconsider FF = { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } as Subset of (FinTrees [: the carrier of F2(),F3():]) ; A35: now__::_thesis:_for_d_being_Symbol_of_F2()_st_d_in_Terminals_F2()_holds_ root-tree_[d,F4(d)]_in_FF let d be Symbol of F2(); ::_thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in FF ) assume d in Terminals F2() ; ::_thesis: root-tree [d,F4(d)] in FF then A36: root-tree d in F by A31; (root-tree [d,F4(d)]) `1 = root-tree d by TREES_4:25; hence root-tree [d,F4(d)] in FF by A36; ::_thesis: verum end; now__::_thesis:_for_o_being_Symbol_of_F2() for_p_being_FinSequence_of_FF_st_o_==>_pr1_(roots_p)_holds_ [o,H3(o,p)]_-tree_p_in_FF let o be Symbol of F2(); ::_thesis: for p being FinSequence of FF st o ==> pr1 (roots p) holds [o,H3(o,p)] -tree p in FF let p be FinSequence of FF; ::_thesis: ( o ==> pr1 (roots p) implies [o,H3(o,p)] -tree p in FF ) assume A37: o ==> pr1 (roots p) ; ::_thesis: [o,H3(o,p)] -tree p in FF consider p1 being FinSequence of FinTrees the carrier of F2() such that A38: dom p1 = dom p and A39: for i being Element of NAT st i in dom p holds ex T being Element of FinTrees [: the carrier of F2(),F3():] st ( T = p . i & p1 . i = T `1 ) and A40: ([o,F5(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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p1 or x in F ) assume x in rng p1 ; ::_thesis: x in F then consider k being set such that A41: k in dom p1 and A42: x = p1 . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A41; A43: p . k in rng p by A38, A41, FUNCT_1:def_3; A44: ex dt being Element of FinTrees [: the carrier of F2(),F3():] st ( dt = p . k & x = dt `1 ) by A38, A39, A41, A42; rng p c= FF by FINSEQ_1:def_4; then p . k in FF by A43; then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st ( p . k = dt & dt `1 in F ) ; hence x in F by A44; ::_thesis: verum end; then reconsider p1 = p1 as FinSequence of F by FINSEQ_1:def_4; A45: dom (roots p1) = dom p1 by TREES_3:def_18; A46: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def_12; then A47: dom (pr1 (roots p)) = dom p1 by A38, TREES_3:def_18; now__::_thesis:_for_k_being_Nat_st_k_in_dom_p1_holds_ (roots_p1)_._k_=_(pr1_(roots_p))_._k let k be Nat; ::_thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k ) assume A48: k in dom p1 ; ::_thesis: (roots p1) . k = (pr1 (roots p)) . k then A49: p . k in rng p by A38, FUNCT_1:def_3; A50: ex dt being Element of FinTrees [: the carrier of F2(),F3():] st ( dt = p . k & p1 . k = dt `1 ) by A38, A39, A48; rng p c= FF by FINSEQ_1:def_4; then p . k in FF by A49; then consider dt being Element of FinTrees [: the carrier of F2(),F3():] such that A51: p . k = dt and dt `1 in F ; reconsider r = {} as Node of dt by TREES_1:22; ex T being DecoratedTree st ( T = p1 . k & (roots p1) . k = T . {} ) by A48, TREES_3:def_18; then A52: (roots p1) . k = (dt . r) `1 by A50, A51, TREES_3:39; ex T being DecoratedTree st ( T = p . k & (roots p) . k = T . {} ) by A38, A48, TREES_3:def_18; hence (roots p1) . k = (pr1 (roots p)) . k by A46, A47, A48, A51, A52, MCART_1:def_12; ::_thesis: verum end; then pr1 (roots p) = roots p1 by A45, A47, FINSEQ_1:13; then ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 in F by A32, A37, A40; hence [o,H3(o,p)] -tree p in FF ; ::_thesis: verum end; then X c= FF by A6, A35; then tt in FF by A6, A34; then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st ( tt = dt & dt `1 in F ) ; hence x in F by A33; ::_thesis: verum end; end; scheme :: DTCONSTR:sch 5 DTCHeight{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } : for n being Element of NAT for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds ( dt in F1() . n iff height (dom dt) <= n ) provided A1: dom F1() = NAT and A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } proof set f = F1(); set G = F2(); set D = F3(); set SxD = [: the carrier of F2(),F3():]; deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2))); defpred S1[ Element of NAT ] means for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds ( dt in F1() . $1 iff height (dom dt) <= $1 ); A4: S1[ 0 ] proof let dt be Element of FinTrees [: the carrier of F2(),F3():]; ::_thesis: ( dt in Union F1() implies ( dt in F1() . 0 iff height (dom dt) <= 0 ) ) assume A5: dt in Union F1() ; ::_thesis: ( dt in F1() . 0 iff height (dom dt) <= 0 ) hereby ::_thesis: ( height (dom dt) <= 0 implies dt in F1() . 0 ) assume dt in F1() . 0 ; ::_thesis: height (dom dt) <= 0 then ex t being Symbol of F2() ex d being Element of F3() st ( dt = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2; hence height (dom dt) <= 0 by TREES_1:42, TREES_4:3; ::_thesis: verum end; assume height (dom dt) <= 0 ; ::_thesis: dt in F1() . 0 then A6: height (dom dt) = 0 ; defpred S2[ Element of NAT ] means not dt in F1() . $1; assume A7: S2[ 0 ] ; ::_thesis: contradiction A8: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_ S2[n_+_1] let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A9: S2[n] ; ::_thesis: S2[n + 1] thus S2[n + 1] ::_thesis: verum proof assume dt in F1() . (n + 1) ; ::_thesis: contradiction then dt in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3; then ( dt in F1() . n or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3; then consider o being Symbol of F2(), p being Element of (F1() . n) * such that A10: dt = [o,H3(o,p)] -tree p and A11: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) by A9; A12: dt = root-tree (dt . {}) by A6, TREES_1:43, TREES_4:5; then A13: p = {} by A10, A11, TREES_4:17; then dt = root-tree [o,F5(o,{},{})] by A10, A12, Th3, Th7, TREES_4:def_4; hence contradiction by A2, A7, A11, A13, Th3, Th7; ::_thesis: verum end; end; A14: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A7, A8); ex n being set st ( n in NAT & dt in F1() . n ) by A1, A5, CARD_5:2; hence contradiction by A14; ::_thesis: verum end; A15: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A16: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let dt be Element of FinTrees [: the carrier of F2(),F3():]; ::_thesis: ( dt in Union F1() implies ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 ) ) assume A17: dt in Union F1() ; ::_thesis: ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 ) hereby ::_thesis: ( height (dom dt) <= n + 1 implies dt in F1() . (n + 1) ) assume dt in F1() . (n + 1) ; ::_thesis: height (dom dt) <= n + 1 then dt in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3; then A18: ( dt in F1() . n or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3; percases ( dt in F1() . n or not dt in F1() . n ) ; suppose dt in F1() . n ; ::_thesis: height (dom dt) <= n + 1 then A19: height (dom dt) <= n by A16, A17; n <= n + 1 by NAT_1:11; hence height (dom dt) <= n + 1 by A19, XXREAL_0:2; ::_thesis: verum end; suppose not dt in F1() . n ; ::_thesis: height (dom dt) <= n + 1 then consider o being Symbol of F2(), p being Element of (F1() . n) * such that A20: dt = [o,H3(o,p)] -tree p and A21: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) by A18; reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A21; A22: dom dt = tree (doms p) by A20, TREES_4:10; now__::_thesis:_for_t_being_finite_Tree_st_t_in_rng_(doms_p)_holds_ height_t_<=_n let t be finite Tree; ::_thesis: ( t in rng (doms p) implies height t <= n ) assume t in rng (doms p) ; ::_thesis: height t <= n then consider k being set such that A23: k in dom (doms p) and A24: t = (doms p) . k by FUNCT_1:def_3; A25: k in dom p by A23, TREES_3:37; then A26: p . k in rng p by FUNCT_1:def_3; rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4; then reconsider pk = p . k as Element of FinTrees [: the carrier of F2(),F3():] by A26; A27: rng p c= F1() . n by FINSEQ_1:def_4; A28: t = dom pk by A24, A25, FUNCT_6:22; pk in Union F1() by A1, A26, A27, CARD_5:2; hence height t <= n by A16, A26, A27, A28; ::_thesis: verum end; hence height (dom dt) <= n + 1 by A22, TREES_3:77; ::_thesis: verum end; end; end; assume A29: height (dom dt) <= n + 1 ; ::_thesis: dt in F1() . (n + 1) defpred S2[ Nat] means dt in F1() . $1; ex k being set st ( k in NAT & dt in F1() . k ) by A1, A17, CARD_5:2; then A30: ex k being Nat st S2[k] ; consider mk being Nat such that A31: ( S2[mk] & ( for kk being Nat st S2[kk] holds mk <= kk ) ) from NAT_1:sch_5(A30); deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ; A32: for n being Element of NAT holds F1() . n c= F1() . (n + 1) proof let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1) F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3; hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum end; percases ( mk = 0 or ex k being Nat st mk = k + 1 ) by NAT_1:6; suppose mk = 0 ; ::_thesis: dt in F1() . (n + 1) then F1() . mk c= F1() . (0 + (n + 1)) by A32, MEASURE2:18; hence dt in F1() . (n + 1) by A31; ::_thesis: verum end; suppose ex k being Nat st mk = k + 1 ; ::_thesis: dt in F1() . (n + 1) then consider k being Nat such that A33: mk = k + 1 ; reconsider k = k as Element of NAT by ORDINAL1:def_12; A34: k < k + 1 by NAT_1:13; F1() . mk = (F1() . k) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3, A33; then ( dt in F1() . k or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ) by A31, XBOOLE_0:def_3; then consider o being Symbol of F2(), p being Element of (F1() . k) * such that A35: dt = [o,H3(o,p)] -tree p and A36: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) by A31, A33, A34; reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A36; A37: dom dt = tree (doms p) by A35, TREES_4:10; rng p c= F1() . n proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() . n ) assume x in rng p ; ::_thesis: x in F1() . n then consider k9 being set such that A38: k9 in dom p and A39: x = p . k9 by FUNCT_1:def_3; A40: x in rng p by A38, A39, FUNCT_1:def_3; rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4; then reconsider t = x as Element of FinTrees [: the carrier of F2(),F3():] by A40; A41: k9 in dom (doms p) by A38, A39, FUNCT_6:22; dom t = (doms p) . k9 by A38, A39, FUNCT_6:22; then dom t in rng (doms p) by A41, FUNCT_1:def_3; then height (dom t) < n + 1 by A29, A37, TREES_3:78, XXREAL_0:2; then A42: height (dom t) <= n by NAT_1:13; A43: rng p c= F1() . k by FINSEQ_1:def_4; t in rng p by A38, A39, FUNCT_1:def_3; then t in Union F1() by A1, A43, CARD_5:2; hence x in F1() . n by A16, A42; ::_thesis: verum end; then p is FinSequence of F1() . n by FINSEQ_1:def_4; then reconsider p = p as Element of (F1() . n) * by FINSEQ_1:def_11; [o,H3(o,p)] -tree p in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } by A36; then dt in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( pp = q & oo ==> pr1 (roots q) ) } by A35, XBOOLE_0:def_3; hence dt in F1() . (n + 1) by A3; ::_thesis: verum end; end; end; end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A15); ::_thesis: verum end; scheme :: DTCONSTR:sch 6 DTCUniq{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } : for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 holds dt1 = dt2 provided A1: dom F1() = NAT and A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } proof set f = F1(); set G = F2(); set D = F3(); set S = the carrier of F2(); set SxD = [: the carrier of F2(),F3():]; deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2))); A4: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } by A2; A5: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } by A3; defpred S1[ Element of NAT ] means for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in F1() . $1 & dt2 in F1() . $1 & dt1 `1 = dt2 `1 holds dt1 = dt2; A6: S1[ 0 ] proof let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in F1() . 0 & dt2 in F1() . 0 & dt1 `1 = dt2 `1 implies dt1 = dt2 ) assume that A7: dt1 in F1() . 0 and A8: dt2 in F1() . 0 and A9: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2 consider t1 being Symbol of F2(), d1 being Element of F3() such that A10: dt1 = root-tree [t1,d1] and A11: ( ( t1 in Terminals F2() & d1 = F4(t1) ) or ( t1 ==> {} & d1 = F5(t1,{},{}) ) ) by A2, A7; consider t2 being Symbol of F2(), d2 being Element of F3() such that A12: dt2 = root-tree [t2,d2] and A13: ( ( t2 in Terminals F2() & d2 = F4(t2) ) or ( t2 ==> {} & d2 = F5(t2,{},{}) ) ) by A2, A8; A14: root-tree t1 = dt1 `1 by A10, TREES_4:25; root-tree t2 = dt2 `1 by A12, TREES_4:25; then A15: t1 = t2 by A9, A14, TREES_4:4; now__::_thesis:_for_t_being_Symbol_of_F2()_st_t_==>_{}_holds_ not_t_in_Terminals_F2() let t be Symbol of F2(); ::_thesis: ( t ==> {} implies not t in Terminals F2() ) assume t ==> {} ; ::_thesis: not t in Terminals F2() then for t9 being Symbol of F2() holds ( not t = t9 or ex tnt being FinSequence st t9 ==> tnt ) ; then not t in { t9 where t9 is Symbol of F2() : for tnt being FinSequence holds not t9 ==> tnt } ; hence not t in Terminals F2() by LANG1:def_2; ::_thesis: verum end; hence dt1 = dt2 by A10, A11, A12, A13, A15; ::_thesis: verum end; A16: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A17: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in F1() . (n + 1) & dt2 in F1() . (n + 1) & dt1 `1 = dt2 `1 implies dt1 = dt2 ) assume that A18: dt1 in F1() . (n + 1) and A19: dt2 in F1() . (n + 1) and A20: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2 A21: dom dt1 = dom (dt1 `1) by TREES_4:24; A22: dom dt2 = dom (dt1 `1) by A20, TREES_4:24; A23: dt1 in Union F1() by A1, A18, CARD_5:2; A24: dt2 in Union F1() by A1, A19, CARD_5:2; ex X being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F ) ) from DTCONSTR:sch_3(A1, A4, A5); then reconsider dt19 = dt1, dt29 = dt2 as Element of FinTrees [: the carrier of F2(),F3():] by A23, A24; A25: for n being Element of NAT for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds ( dt in F1() . n iff height (dom dt) <= n ) from DTCONSTR:sch_5(A1, A4, A5); percases ( dt1 in F1() . n or not dt1 in F1() . n ) ; supposeA26: dt1 in F1() . n ; ::_thesis: dt1 = dt2 then height (dom dt19) <= n by A23, A25; then dt29 in F1() . n by A21, A22, A24, A25; hence dt1 = dt2 by A17, A20, A26; ::_thesis: verum end; supposeA27: not dt1 in F1() . n ; ::_thesis: dt1 = dt2 A28: F1() . (n + 1) = (F1() . n) \/ { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p1 = q & o1 ==> pr1 (roots q) ) } by A3; then ( dt1 in F1() . n or dt1 in { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p1 = q & o1 ==> pr1 (roots q) ) } ) by A18, XBOOLE_0:def_3; then consider o1 being Symbol of F2(), p1 being Element of (F1() . n) * such that A29: dt1 = [o1,H3(o1,p1)] -tree p1 and A30: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p1 = q & o1 ==> pr1 (roots q) ) by A27; height (dom dt19) > n by A23, A25, A27; then A31: not dt29 in F1() . n by A21, A22, A24, A25; ( dt2 in F1() . n or dt2 in { ([o2,H3(o2,p2)] -tree p2) where o2 is Symbol of F2(), p2 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p2 = q & o2 ==> pr1 (roots q) ) } ) by A19, A28, XBOOLE_0:def_3; then consider o2 being Symbol of F2(), p2 being Element of (F1() . n) * such that A32: dt2 = [o2,H3(o2,p2)] -tree p2 and A33: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p2 = q & o2 ==> pr1 (roots q) ) by A31; reconsider p1 = p1 as FinSequence of FinTrees [: the carrier of F2(),F3():] by A30; consider p11 being FinSequence of FinTrees the carrier of F2() such that A34: dom p11 = dom p1 and A35: for i being Element of NAT st i in dom p1 holds ex T being Element of FinTrees [: the carrier of F2(),F3():] st ( T = p1 . i & p11 . i = T `1 ) and A36: ([o1,H3(o1,p1)] -tree p1) `1 = o1 -tree p11 by TREES_4:31; reconsider p2 = p2 as FinSequence of FinTrees [: the carrier of F2(),F3():] by A33; consider p21 being FinSequence of FinTrees the carrier of F2() such that A37: dom p21 = dom p2 and A38: for i being Element of NAT st i in dom p2 holds ex T being Element of FinTrees [: the carrier of F2(),F3():] st ( T = p2 . i & p21 . i = T `1 ) and A39: ([o2,H3(o2,p2)] -tree p2) `1 = o2 -tree p21 by TREES_4:31; A40: o1 = o2 by A20, A29, A32, A36, A39, TREES_4:15; A41: p11 = p21 by A20, A29, A32, A36, A39, TREES_4:15; now__::_thesis:_for_k_being_Nat_st_k_in_dom_p11_holds_ p1_._k_=_p2_._k let k be Nat; ::_thesis: ( k in dom p11 implies p1 . k = p2 . k ) assume A42: k in dom p11 ; ::_thesis: p1 . k = p2 . k then consider p1k being Element of FinTrees [: the carrier of F2(),F3():] such that A43: p1k = p1 . k and A44: p11 . k = p1k `1 by A34, A35; consider p2k being Element of FinTrees [: the carrier of F2(),F3():] such that A45: p2k = p2 . k and A46: p21 . k = p2k `1 by A37, A38, A41, A42; A47: p1k in F1() . n by A34, A42, A43, Th2; p2k in F1() . n by A37, A41, A42, A45, Th2; hence p1 . k = p2 . k by A17, A41, A43, A44, A45, A46, A47; ::_thesis: verum end; then p1 = p2 by A34, A37, A41, FINSEQ_1:13; hence dt1 = dt2 by A29, A32, A40; ::_thesis: verum end; end; end; end; A48: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A16); let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 implies dt1 = dt2 ) assume that A49: dt1 in Union F1() and A50: dt2 in Union F1() and A51: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2 consider n1 being set such that A52: n1 in NAT and A53: dt1 in F1() . n1 by A1, A49, CARD_5:2; consider n2 being set such that A54: n2 in NAT and A55: dt2 in F1() . n2 by A1, A50, CARD_5:2; reconsider n1 = n1, n2 = n2 as Element of NAT by A52, A54; deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st ( p = q & o ==> pr1 (roots q) ) } ; A56: for n being Element of NAT holds F1() . n c= F1() . (n + 1) proof let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1) F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3; hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum end; A57: for k, s being Nat holds F1() . k c= F1() . (k + s) proof let k, s be Nat; ::_thesis: F1() . k c= F1() . (k + s) reconsider k = k, s = s as Element of NAT by ORDINAL1:def_12; k <= k + s by NAT_1:11; hence F1() . k c= F1() . (k + s) by A56, MEASURE2:18; ::_thesis: verum end; ( n1 <= n2 or n1 >= n2 ) ; then ( ex s being Nat st n2 = n1 + s or ex s being Nat st n1 = n2 + s ) by NAT_1:10; then ( F1() . n1 c= F1() . n2 or F1() . n2 c= F1() . n1 ) by A57; hence dt1 = dt2 by A48, A51, A53, A55; ::_thesis: verum end; definition let G be non empty DTConstrStr ; func TS G -> Subset of (FinTrees the carrier of G) means :Def1: :: DTCONSTR:def 1 ( ( for d being Symbol of G st d in Terminals G holds root-tree d in it ) & ( for o being Symbol of G for 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds it c= F ) ); existence ex b1 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 b1 ) & ( for o being Symbol of G for p being FinSequence of b1 st o ==> roots p holds o -tree p in b1 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds b1 c= F ) ) proof deffunc H3( set , set ) -> set = $2 \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of G, p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of G,NAT:] st ( p = q & o ==> pr1 (roots q) ) } ; consider f being Function such that A1: dom f = NAT and A2: f . 0 = { (root-tree [t,d]) where t is Symbol of G, d is Element of NAT : ( ( t in Terminals G & d = H1(t) ) or ( t ==> {} & d = H2(t, {} , {} ) ) ) } and A3: for n being Nat holds f . (n + 1) = H3(n,f . n) from NAT_1:sch_11(); A4: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,H2(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 for 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) from DTCONSTR:sch_4(A1, A2, A4); hence ex b1 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 b1 ) & ( for o being Symbol of G for p being FinSequence of b1 st o ==> roots p holds o -tree p in b1 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds b1 c= F ) ) ; ::_thesis: verum end; uniqueness for b1, b2 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 b1 ) & ( for o being Symbol of G for p being FinSequence of b1 st o ==> roots p holds o -tree p in b1 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds b1 c= F ) & ( for d being Symbol of G st d in Terminals G holds root-tree d in b2 ) & ( for o being Symbol of G for p being FinSequence of b2 st o ==> roots p holds o -tree p in b2 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds b2 c= F ) holds b1 = b2 proof let TSG1, TSG2 be Subset of (FinTrees the carrier of G); ::_thesis: ( ( for d being Symbol of G st d in Terminals G holds root-tree d in TSG1 ) & ( for o being Symbol of G for p being FinSequence of TSG1 st o ==> roots p holds o -tree p in TSG1 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds root-tree d in TSG2 ) & ( for o being Symbol of G for p being FinSequence of TSG2 st o ==> roots p holds o -tree p in TSG2 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds TSG2 c= F ) implies TSG1 = TSG2 ) assume A5: ( ( for d being Symbol of G st d in Terminals G holds root-tree d in TSG1 ) & ( for o being Symbol of G for p being FinSequence of TSG1 st o ==> roots p holds o -tree p in TSG1 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds root-tree d in TSG2 ) & ( for o being Symbol of G for p being FinSequence of TSG2 st o ==> roots p holds o -tree p in TSG2 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds TSG2 c= F ) & not TSG1 = TSG2 ) ; ::_thesis: contradiction then A6: TSG1 c= TSG2 ; TSG2 c= TSG1 by A5; hence contradiction by A5, A6, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def1 defines TS DTCONSTR:def_1_:_ for G being non empty DTConstrStr for b2 being Subset of (FinTrees the carrier of G) holds ( b2 = TS G iff ( ( for d being Symbol of G st d in Terminals G holds root-tree d in b2 ) & ( for o being Symbol of G for p being FinSequence of b2 st o ==> roots p holds o -tree p in b2 ) & ( 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 for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds b2 c= F ) ) ); scheme :: DTCONSTR:sch 7 DTConstrInd{ F1() -> non empty DTConstrStr , P1[ set ] } : for t being DecoratedTree of the carrier of F1() st t in TS F1() holds P1[t] provided A1: for s being Symbol of F1() st s in Terminals F1() holds P1[ root-tree s] and A2: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds P1[t] ) holds P1[nt -tree ts] proof deffunc H3( set , set ) -> set = $2 \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st ( p = q & o ==> pr1 (roots q) ) } ; consider f being Function such that A3: dom f = NAT and A4: f . 0 = { (root-tree [t,d]) where t is Symbol of F1(), d is Element of NAT : ( ( t in Terminals F1() & d = H1(t) ) or ( t ==> {} & d = H2(t, {} , {} ) ) ) } and A5: for n being Nat holds f . (n + 1) = H3(n,f . n) from NAT_1:sch_11(); A6: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st ( p = q & o ==> pr1 (roots q) ) } by A5; A7: ex X being Subset of (FinTrees [: the carrier of F1(),NAT:]) st ( X = Union f & ( for d being Symbol of F1() st d in Terminals F1() holds root-tree [d,H1(d)] in X ) & ( for o being Symbol of F1() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F1(),NAT:]) st ( for d being Symbol of F1() st d in Terminals F1() holds root-tree [d,H1(d)] in F ) & ( for o being Symbol of F1() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in F ) holds X c= F ) ) from DTCONSTR:sch_3(A3, A4, A6); consider TSG being Subset of (FinTrees the carrier of F1()) such that A8: TSG = { (t `1) where t is Element of FinTrees [: the carrier of F1(),NAT:] : t in Union f } and A9: for d being Symbol of F1() st d in Terminals F1() holds root-tree d in TSG and A10: for o being Symbol of F1() for 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 F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds root-tree d in F ) & ( for o being Symbol of F1() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds TSG c= F from DTCONSTR:sch_4(A3, A4, A6); A12: TSG = TS F1() by A9, A10, A11, Def1; defpred S1[ Element of NAT ] means for t being DecoratedTree of [: the carrier of F1(),NAT:] st t in f . $1 holds P1[t `1 ]; A13: S1[ 0 ] proof let tt be DecoratedTree of [: the carrier of F1(),NAT:]; ::_thesis: ( tt in f . 0 implies P1[tt `1 ] ) set p = <*> (TS F1()); assume tt in f . 0 ; ::_thesis: P1[tt `1 ] then consider t being Symbol of F1(), d being Element of NAT such that A14: tt = root-tree [t,d] and A15: ( ( t in Terminals F1() & d = 0 ) or ( t ==> roots (<*> (TS F1())) & d = 0 ) ) by A4, Th3; A16: tt `1 = root-tree t by A14, TREES_4:25; A17: t -tree (<*> (TS F1())) = root-tree t by TREES_4:20; for T being DecoratedTree of the carrier of F1() st T in rng (<*> (TS F1())) holds P1[T] ; hence P1[tt `1 ] by A1, A2, A15, A16, A17; ::_thesis: verum end; A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A19: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let x be DecoratedTree of [: the carrier of F1(),NAT:]; ::_thesis: ( x in f . (n + 1) implies P1[x `1 ] ) assume that A20: x in f . (n + 1) and A21: P1[x `1 ] ; ::_thesis: contradiction x in (f . n) \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st ( p = q & o ==> pr1 (roots q) ) } by A5, A20; then ( x in f . n or x in { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st ( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3; then consider o being Symbol of F1(), p being Element of (f . n) * such that A22: x = [o,0] -tree p and A23: ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st ( p = q & o ==> pr1 (roots q) ) by A19, A21; A24: Union f = union (rng f) by CARD_3:def_4; A25: f . n in rng f by A3, FUNCT_1:def_3; A26: rng p c= f . n by FINSEQ_1:def_4; A27: f . n c= Union f by A24, A25, ZFMISC_1:74; A28: dom p = Seg (len p) by FINSEQ_1:def_3; defpred S2[ set , set ] means ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st ( dt = p . $1 & dt `1 = $2 & dt in Union f ); A29: for k being Nat st k in Seg (len p) holds ex x being Element of FinTrees the carrier of F1() st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len p) implies ex x being Element of FinTrees the carrier of F1() st S2[k,x] ) assume k in Seg (len p) ; ::_thesis: ex x being Element of FinTrees the carrier of F1() st S2[k,x] then A30: p . k in rng p by A28, FUNCT_1:def_3; A31: rng p c= Union f by A26, A27, XBOOLE_1:1; then p . k in Union f by A30; then reconsider dt = p . k as Element of FinTrees [: the carrier of F1(),NAT:] by A7; A32: dt `1 = (pr1 ( the carrier of F1(),NAT)) * dt by TREES_3:def_12; A33: rng dt c= [: the carrier of F1(),NAT:] by RELAT_1:def_19; dom (pr1 ( the carrier of F1(),NAT)) = [: the carrier of F1(),NAT:] by FUNCT_2:def_1; then dom (dt `1) = dom dt by A32, A33, RELAT_1:27; then reconsider x = dt `1 as Element of FinTrees the carrier of F1() by TREES_3:def_8; take x ; ::_thesis: S2[k,x] take dt ; ::_thesis: ( dt = p . k & dt `1 = x & dt in Union f ) thus ( dt = p . k & dt `1 = x & dt in Union f ) by A30, A31; ::_thesis: verum end; consider p1 being FinSequence of FinTrees the carrier of F1() such that A34: dom p1 = Seg (len p) and A35: for k being Nat st k in Seg (len p) holds S2[k,p1 . k] from FINSEQ_1:sch_5(A29); reconsider p = p as FinSequence of Trees [: the carrier of F1(),NAT:] by A23, Th1; A36: dom (roots p1) = dom p1 by TREES_3:def_18; A37: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def_12; then A38: dom (pr1 (roots p)) = dom p1 by A28, A34, TREES_3:def_18; now__::_thesis:_for_k_being_Nat_st_k_in_dom_p1_holds_ (roots_p1)_._k_=_(pr1_(roots_p))_._k let k be Nat; ::_thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k ) assume A39: k in dom p1 ; ::_thesis: (roots p1) . k = (pr1 (roots p)) . k then consider dt being Element of FinTrees [: the carrier of F1(),NAT:] such that A40: dt = p . k and A41: dt `1 = p1 . k and dt in Union f by A34, A35; reconsider r = {} as Node of dt by TREES_1:22; ex T being DecoratedTree st ( T = p1 . k & (roots p1) . k = T . {} ) by A39, TREES_3:def_18; then A42: (roots p1) . k = (dt . r) `1 by A41, TREES_3:39; ex T being DecoratedTree st ( T = p . k & (roots p) . k = T . {} ) by A28, A34, A39, TREES_3:def_18; hence (roots p1) . k = (pr1 (roots p)) . k by A37, A38, A39, A40, A42, MCART_1:def_12; ::_thesis: verum end; then A43: roots p1 = pr1 (roots p) by A36, A38, FINSEQ_1:13; rng p1 c= TS F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p1 or x in TS F1() ) assume x in rng p1 ; ::_thesis: x in TS F1() then consider k being set such that A44: k in dom p1 and A45: x = p1 . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A44; ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st ( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A44; hence x in TS F1() by A8, A12, A45; ::_thesis: verum end; then reconsider p1 = p1 as FinSequence of TS F1() by FINSEQ_1:def_4; now__::_thesis:_for_t_being_DecoratedTree_of_the_carrier_of_F1()_st_t_in_rng_p1_holds_ P1[t] let t be DecoratedTree of the carrier of F1(); ::_thesis: ( t in rng p1 implies P1[t] ) assume t in rng p1 ; ::_thesis: P1[t] then consider k being set such that A46: k in dom p1 and A47: t = p1 . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A46; A48: ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st ( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A46; p . k in rng p by A28, A34, A46, FUNCT_1:def_3; hence P1[t] by A19, A26, A47, A48; ::_thesis: verum end; then A49: P1[o -tree p1] by A2, A23, A43; reconsider p1 = p1 as FinSequence of Trees the carrier of F1() by Th1; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_ for_T_being_DecoratedTree_of_[:_the_carrier_of_F1(),NAT:]_st_T_=_p_._k_holds_ p1_._k_=_T_`1 let k be Element of NAT ; ::_thesis: ( k in dom p implies for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds p1 . k = T `1 ) assume k in dom p ; ::_thesis: for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds p1 . k = T `1 then ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st ( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A28, A35; hence for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds p1 . k = T `1 ; ::_thesis: verum end; hence contradiction by A21, A22, A28, A34, A49, TREES_4:27; ::_thesis: verum end; end; A50: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A18); let t be DecoratedTree of the carrier of F1(); ::_thesis: ( t in TS F1() implies P1[t] ) assume t in TS F1() ; ::_thesis: P1[t] then consider tt being Element of FinTrees [: the carrier of F1(),NAT:] such that A51: t = tt `1 and A52: tt in Union f by A8, A12; ex n being set st ( n in NAT & tt in f . n ) by A3, A52, CARD_5:2; hence P1[t] by A50, A51; ::_thesis: verum end; scheme :: DTCONSTR:sch 8 DTConstrIndDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2() } : ex f being Function of (TS F1()),F2() st ( ( for t being Symbol of F1() st t in Terminals F1() holds f . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds f . (nt -tree ts) = F4(nt,(roots ts),(f * ts)) ) ) proof set G = F1(); deffunc H3( Symbol of F1(), FinSequence) -> Element of F2() = F4($1,(pr1 (roots $2)),(pr2 (roots $2))); deffunc H4( set , set ) -> set = $2 \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of F1(),F2():] 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 F1(), d is Element of F2() : ( ( t in Terminals F1() & d = F3(t) ) or ( t ==> {} & d = F4(t,{},{}) ) ) } and A3: for n being Nat holds f . (n + 1) = H4(n,f . n) from NAT_1:sch_11(); A4: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),F2():] st ( p = q & o ==> pr1 (roots q) ) } by A3; ex X1 being Subset of (FinTrees the carrier of F1()) st ( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F1(),F2():] : t in Union f } & ( for d being Symbol of F1() st d in Terminals F1() holds root-tree d in X1 ) & ( for o being Symbol of F1() for p being FinSequence of X1 st o ==> roots p holds o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds root-tree d in F ) & ( for o being Symbol of F1() for p being FinSequence of F st o ==> roots p holds o -tree p in F ) holds X1 c= F ) ) from DTCONSTR:sch_4(A1, A2, A4); then A5: TS F1() = { (t `1) where t is Element of FinTrees [: the carrier of F1(),F2():] : t in Union f } by Def1; defpred S1[ set , set ] means for dt being DecoratedTree of [: the carrier of F1(),F2():] st dt in Union f & $1 = dt `1 holds $2 = (dt `2) . {}; A6: for e being set st e in TS F1() holds ex u being set st ( u in F2() & S1[e,u] ) proof let e be set ; ::_thesis: ( e in TS F1() implies ex u being set st ( u in F2() & S1[e,u] ) ) assume e in TS F1() ; ::_thesis: ex u being set st ( u in F2() & S1[e,u] ) then consider DT being Element of FinTrees [: the carrier of F1(),F2():] such that A7: e = DT `1 and A8: DT in Union f by A5; reconsider r = {} as Node of (DT `2) by TREES_1:22; take u = (DT `2) . r; ::_thesis: ( u in F2() & S1[e,u] ) thus u in F2() ; ::_thesis: S1[e,u] A9: for dt1, dt2 being DecoratedTree of [: the carrier of F1(),F2():] st dt1 in Union f & dt2 in Union f & dt1 `1 = dt2 `1 holds dt1 = dt2 from DTCONSTR:sch_6(A1, A2, A4); let dt be DecoratedTree of [: the carrier of F1(),F2():]; ::_thesis: ( dt in Union f & e = dt `1 implies u = (dt `2) . {} ) assume that A10: dt in Union f and A11: e = dt `1 ; ::_thesis: u = (dt `2) . {} thus u = (dt `2) . {} by A7, A8, A9, A10, A11; ::_thesis: verum end; consider ff being Function such that A12: ( dom ff = TS F1() & rng ff c= F2() ) and A13: for e being set st e in TS F1() holds S1[e,ff . e] from FUNCT_1:sch_5(A6); reconsider ff = ff as Function of (TS F1()),F2() by A12, FUNCT_2:def_1, RELSET_1:4; take ff ; ::_thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds ff . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ) ) consider X being Subset of (FinTrees [: the carrier of F1(),F2():]) such that A14: X = Union f and A15: for d being Symbol of F1() st d in Terminals F1() holds root-tree [d,F3(d)] in X and A16: for o being Symbol of F1() for p being FinSequence of X st o ==> pr1 (roots p) holds [o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X and for F being Subset of (FinTrees [: the carrier of F1(),F2():]) st ( for d being Symbol of F1() st d in Terminals F1() holds root-tree [d,F3(d)] in F ) & ( for o being Symbol of F1() for p being FinSequence of F st o ==> pr1 (roots p) holds [o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds X c= F from DTCONSTR:sch_3(A1, A2, A4); hereby ::_thesis: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) let t be Symbol of F1(); ::_thesis: ( t in Terminals F1() implies ff . (root-tree t) = F3(t) ) assume A17: t in Terminals F1() ; ::_thesis: ff . (root-tree t) = F3(t) A18: (root-tree [t,F3(t)]) `1 = root-tree t by TREES_4:25; A19: (root-tree [t,F3(t)]) `2 = root-tree F3(t) by TREES_4:25; root-tree [t,F3(t)] in Union f by A14, A15, A17; then root-tree t in TS F1() by A5, A18; hence ff . (root-tree t) = (root-tree F3(t)) . {} by A13, A14, A15, A17, A18, A19 .= F3(t) by TREES_4:3 ; ::_thesis: verum end; let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts implies ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ) set rts = roots ts; assume A20: nt ==> roots ts ; ::_thesis: ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) set x = ff * ts; A21: dom ts = Seg (len ts) by FINSEQ_1:def_3; defpred S2[ set , set ] means ex dt being DecoratedTree of [: the carrier of F1(),F2():] st ( dt = $2 & dt `1 = ts . $1 & dt in Union f ); A22: for k being Nat st k in Seg (len ts) holds ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] ) assume k in Seg (len ts) ; ::_thesis: ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] then A23: ts . k in rng ts by A21, FUNCT_1:def_3; rng ts c= TS F1() by FINSEQ_1:def_4; then ts . k in TS F1() by A23; then ex x being Element of FinTrees [: the carrier of F1(),F2():] st ( ts . k = x `1 & x in Union f ) by A5; hence ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] ; ::_thesis: verum end; consider dts being FinSequence of FinTrees [: the carrier of F1(),F2():] such that A24: dom dts = Seg (len ts) and A25: for k being Nat st k in Seg (len ts) holds S2[k,dts . k] from FINSEQ_1:sch_5(A22); rng dts c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng dts or x in X ) assume x in rng dts ; ::_thesis: x in X then consider k being set such that A26: k in dom ts and A27: x = dts . k by A21, A24, FUNCT_1:def_3; reconsider k = k as Element of NAT by A26; ex dt being DecoratedTree of [: the carrier of F1(),F2():] st ( dt = x & dt `1 = ts . k & dt in Union f ) by A21, A25, A26, A27; hence x in X by A14; ::_thesis: verum end; then reconsider dts = dts as FinSequence of X by FINSEQ_1:def_4; A28: dom (roots ts) = dom ts by TREES_3:def_18; A29: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def_12; A30: dom (pr2 (roots dts)) = dom (roots dts) by MCART_1:def_13; A31: dom (pr1 (roots dts)) = dom ts by A21, A24, A29, TREES_3:def_18; A32: dom (pr2 (roots dts)) = dom ts by A21, A24, A30, TREES_3:def_18; now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_ (roots_ts)_._k_=_(pr1_(roots_dts))_._k let k be Nat; ::_thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k ) assume A33: k in dom ts ; ::_thesis: (roots ts) . k = (pr1 (roots dts)) . k then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that A34: dt = dts . k and A35: dt `1 = ts . k and dt in Union f by A21, A25; reconsider r = {} as Node of dt by TREES_1:22; ex T being DecoratedTree st ( T = ts . k & (roots ts) . k = T . {} ) by A33, TREES_3:def_18; then A36: (roots ts) . k = (dt . r) `1 by A35, TREES_3:39; ex T being DecoratedTree st ( T = dts . k & (roots dts) . k = T . {} ) by A21, A24, A33, TREES_3:def_18; hence (roots ts) . k = (pr1 (roots dts)) . k by A29, A31, A33, A34, A36, MCART_1:def_12; ::_thesis: verum end; then A37: roots ts = pr1 (roots dts) by A28, A31, FINSEQ_1:13; then A38: [nt,H3(nt,dts)] -tree dts in X by A16, A20; A39: rng dts c= FinTrees [: the carrier of F1(),F2():] by FINSEQ_1:def_4; FinTrees [: the carrier of F1(),F2():] c= Trees [: the carrier of F1(),F2():] by TREES_3:21; then rng dts c= Trees [: the carrier of F1(),F2():] by A39, XBOOLE_1:1; then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F1(),F2():] by FINSEQ_1:def_4; A40: rng ts c= FinTrees the carrier of F1() by FINSEQ_1:def_4; FinTrees the carrier of F1() c= Trees the carrier of F1() by TREES_3:21; then rng ts c= Trees the carrier of F1() by A40, XBOOLE_1:1; then reconsider ts9 = ts as FinSequence of Trees the carrier of F1() by FINSEQ_1:def_4; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_dts_holds_ for_T_being_DecoratedTree_of_[:_the_carrier_of_F1(),F2():]_st_T_=_dts_._i_holds_ ts_._i_=_T_`1 let i be Element of NAT ; ::_thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds ts . i = T `1 ) assume i in dom dts ; ::_thesis: for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds ts . i = T `1 then A41: ex dt being DecoratedTree of [: the carrier of F1(),F2():] st ( dt = dts . i & dt `1 = ts . i & dt in Union f ) by A24, A25; let T be DecoratedTree of [: the carrier of F1(),F2():]; ::_thesis: ( T = dts . i implies ts . i = T `1 ) assume T = dts . i ; ::_thesis: ts . i = T `1 hence ts . i = T `1 by A41; ::_thesis: verum end; then A42: ([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A21, A24, TREES_4:27; A43: rng ts c= dom ff by A12, FINSEQ_1:def_4; then A44: dom (ff * ts) = dom ts by RELAT_1:27; now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_ (ff_*_ts)_._k_=_(pr2_(roots_dts))_._k let k be Nat; ::_thesis: ( k in dom ts implies (ff * ts) . k = (pr2 (roots dts)) . k ) assume A45: k in dom ts ; ::_thesis: (ff * ts) . k = (pr2 (roots dts)) . k then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that A46: dt = dts . k and A47: dt `1 = ts . k and A48: dt in Union f by A21, A25; reconsider r = {} as Node of dt by TREES_1:22; A49: ts . k in rng ts by A45, FUNCT_1:def_3; A50: (ff * ts) . k = ff . (dt `1) by A44, A45, A47, FUNCT_1:12 .= (dt `2) . {} by A12, A13, A43, A47, A48, A49 .= (dt . r) `2 by TREES_3:39 ; ex T being DecoratedTree st ( T = dts . k & (roots dts) . k = T . r ) by A21, A24, A45, TREES_3:def_18; hence (ff * ts) . k = (pr2 (roots dts)) . k by A29, A31, A45, A46, A50, MCART_1:def_13; ::_thesis: verum end; then A51: ff * ts = pr2 (roots dts) by A32, A44, FINSEQ_1:13; reconsider r = {} as Node of ([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) by TREES_1:22; nt -tree ts in TS F1() by A5, A14, A38, A42; then ff . (nt -tree ts) = (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) `2) . r by A13, A14, A16, A20, A37, A42, A51 .= (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) . r) `2 by TREES_3:39 .= [nt,F4(nt,(roots ts),(ff * ts))] `2 by TREES_4:def_4 ; hence ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ; ::_thesis: verum end; scheme :: DTCONSTR:sch 9 DTConstrUniqDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of (TS F1()),F2(), F6() -> Function of (TS F1()),F2() } : F5() = F6() provided A1: ( ( for t being Symbol of F1() st t in Terminals F1() holds F5() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds F5() . (nt -tree ts) = F4(nt,(roots ts),(F5() * ts)) ) ) and A2: ( ( for t being Symbol of F1() st t in Terminals F1() holds F6() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds F6() . (nt -tree ts) = F4(nt,(roots ts),(F6() * ts)) ) ) proof set G = F1(); defpred S1[ set ] means F5() . $1 = F6() . $1; A3: now__::_thesis:_for_s_being_Symbol_of_F1()_st_s_in_Terminals_F1()_holds_ S1[_root-tree_s] let s be Symbol of F1(); ::_thesis: ( s in Terminals F1() implies S1[ root-tree s] ) assume A4: s in Terminals F1() ; ::_thesis: S1[ root-tree s] then F5() . (root-tree s) = F3(s) by A1 .= F6() . (root-tree s) by A2, A4 ; hence S1[ root-tree s] ; ::_thesis: verum end; A5: now__::_thesis:_for_nt_being_Symbol_of_F1() for_ts_being_FinSequence_of_TS_F1()_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_F1()_st_t_in_rng_ts_holds_ S1[t]_)_holds_ S1[nt_-tree_ts] let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ) holds S1[nt -tree ts] let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ) implies S1[nt -tree ts] ) assume that A6: nt ==> roots ts and A7: for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ; ::_thesis: S1[nt -tree ts] A8: rng ts c= TS F1() by FINSEQ_1:def_4; then rng ts c= dom F5() by FUNCT_2:def_1; then A9: dom (F5() * ts) = dom ts by RELAT_1:27; reconsider ntv1 = F5() * ts as FinSequence ; reconsider ntv1 = ntv1 as FinSequence of F2() ; rng ts c= dom F6() by A8, FUNCT_2:def_1; then A10: dom (F6() * ts) = dom ts by RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_ts_holds_ (F5()_*_ts)_._x_=_(F6()_*_ts)_._x let x be set ; ::_thesis: ( x in dom ts implies (F5() * ts) . x = (F6() * ts) . x ) assume A11: x in dom ts ; ::_thesis: (F5() * ts) . x = (F6() * ts) . x then reconsider t = ts . x as Element of FinTrees the carrier of F1() by Th2; t in rng ts by A11, FUNCT_1:def_3; then A12: F5() . t = F6() . t by A7; thus (F5() * ts) . x = F5() . t by A9, A11, FUNCT_1:12 .= (F6() * ts) . x by A10, A11, A12, FUNCT_1:12 ; ::_thesis: verum end; then A13: F5() * ts = F6() * ts by A9, A10, FUNCT_1:2; F5() . (nt -tree ts) = F4(nt,(roots ts),ntv1) by A1, A6 .= F6() . (nt -tree ts) by A2, A6, A13 ; hence S1[nt -tree ts] ; ::_thesis: verum end; for t being DecoratedTree of the carrier of F1() st t in TS F1() holds S1[t] from DTCONSTR:sch_7(A3, A5); then for x being set st x in TS F1() holds F5() . x = F6() . x ; hence F5() = F6() by FUNCT_2:12; ::_thesis: verum end; begin defpred S1[ set , set ] means ( $1 = 1 & ( $2 = <*0*> or $2 = <*1*> ) ); definition func PeanoNat -> non empty strict DTConstrStr means :Def2: :: DTCONSTR:def 2 ( the carrier of it = {0,1} & ( for x being Symbol of it for y being FinSequence of the carrier of it holds ( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ); existence ex b1 being non empty strict DTConstrStr st ( the carrier of b1 = {0,1} & ( for x being Symbol of b1 for y being FinSequence of the carrier of b1 holds ( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ) proof thus ex G being non empty strict DTConstrStr st ( the carrier of G = {0,1} & ( for x being Symbol of G for p being FinSequence of the carrier of G holds ( x ==> p iff S1[x,p] ) ) ) from DTCONSTR:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being non empty strict DTConstrStr st the carrier of b1 = {0,1} & ( for x being Symbol of b1 for y being FinSequence of the carrier of b1 holds ( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) & the carrier of b2 = {0,1} & ( for x being Symbol of b2 for y being FinSequence of the carrier of b2 holds ( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) holds b1 = b2 proof thus for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = {0,1} & ( for x being Symbol of G1 for p being FinSequence of the carrier of G1 holds ( x ==> p iff S1[x,p] ) ) & the carrier of G2 = {0,1} & ( for x being Symbol of G2 for p being FinSequence of the carrier of G2 holds ( x ==> p iff S1[x,p] ) ) holds G1 = G2 from DTCONSTR:sch_2(); ::_thesis: verum end; end; :: deftheorem Def2 defines PeanoNat DTCONSTR:def_2_:_ for b1 being non empty strict DTConstrStr holds ( b1 = PeanoNat iff ( the carrier of b1 = {0,1} & ( for x being Symbol of b1 for y being FinSequence of the carrier of b1 holds ( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ) ); set PN = PeanoNat ; Lm2: the carrier of PeanoNat = {0,1} by Def2; then reconsider O = 0 , S = 1 as Symbol of PeanoNat by TARSKI:def_2; Lm3: S ==> <*O*> by Def2; Lm4: S ==> <*S*> by Def2; Lm5: S ==> <*O*> by Def2; Lm6: S ==> <*S*> by Def2; Lm7: Terminals PeanoNat = { x where x is Symbol of PeanoNat : for tnt being FinSequence holds not x ==> tnt } by LANG1:def_2; Lm8: now__::_thesis:_for_x_being_FinSequence_holds_not_O_==>_x given x being FinSequence such that A1: O ==> x ; ::_thesis: contradiction [O,x] in the Rules of PeanoNat by A1, LANG1:def_1; then x in the carrier of PeanoNat * by ZFMISC_1:87; then x is FinSequence of the carrier of PeanoNat by FINSEQ_2:def_3; hence contradiction by A1, Def2; ::_thesis: verum end; then Lm9: O in Terminals PeanoNat by Lm7; Lm10: Terminals PeanoNat c= {O} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Terminals PeanoNat or x in {O} ) assume x in Terminals PeanoNat ; ::_thesis: x in {O} then consider y being Symbol of PeanoNat such that A1: x = y and A2: for tnt being FinSequence holds not y ==> tnt by Lm7; ( y = O or ( y = S & {O,S} <> {} ) ) by Lm2, TARSKI:def_2; hence x in {O} by A1, A2, Lm5, TARSKI:def_1; ::_thesis: verum end; Lm11: NonTerminals PeanoNat = { x where x is Symbol of PeanoNat : ex tnt being FinSequence st x ==> tnt } by LANG1:def_3; then Lm12: S in NonTerminals PeanoNat by Lm5; then Lm13: {S} c= NonTerminals PeanoNat by ZFMISC_1:31; Lm14: NonTerminals PeanoNat c= {S} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NonTerminals PeanoNat or x in {S} ) assume x in NonTerminals PeanoNat ; ::_thesis: x in {S} then consider y being Symbol of PeanoNat such that A1: x = y and A2: ex tnt being FinSequence st y ==> tnt by Lm11; ( y = O or y = S ) by Lm2, TARSKI:def_2; hence x in {S} by A1, A2, Lm8, TARSKI:def_1; ::_thesis: verum end; then Lm15: NonTerminals PeanoNat = {S} by Lm13, XBOOLE_0:def_10; reconsider TSPN = TS PeanoNat as non empty Subset of (FinTrees the carrier of PeanoNat) by Def1, Lm9; begin definition let G be non empty DTConstrStr ; attrG is with_terminals means :Def3: :: DTCONSTR:def 3 Terminals G <> {} ; attrG is with_nonterminals means :Def4: :: DTCONSTR:def 4 NonTerminals G <> {} ; attrG is with_useful_nonterminals means :Def5: :: DTCONSTR:def 5 for nt being Symbol of G st nt in NonTerminals G holds ex p being FinSequence of TS G st nt ==> roots p; end; :: deftheorem Def3 defines with_terminals DTCONSTR:def_3_:_ for G being non empty DTConstrStr holds ( G is with_terminals iff Terminals G <> {} ); :: deftheorem Def4 defines with_nonterminals DTCONSTR:def_4_:_ for G being non empty DTConstrStr holds ( G is with_nonterminals iff NonTerminals G <> {} ); :: deftheorem Def5 defines with_useful_nonterminals DTCONSTR:def_5_:_ for G being non empty DTConstrStr holds ( G is with_useful_nonterminals iff for nt being Symbol of G st nt in NonTerminals G holds ex p being FinSequence of TS G st nt ==> roots p ); Lm16: ( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) proof thus Terminals PeanoNat <> {} by Lm9; :: according to DTCONSTR:def_3 ::_thesis: ( PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) thus NonTerminals PeanoNat <> {} by Lm12; :: according to DTCONSTR:def_4 ::_thesis: PeanoNat is with_useful_nonterminals reconsider rO = root-tree O as Element of TSPN by Def1, Lm9; reconsider p = <*rO*> as FinSequence of TSPN ; reconsider p = p as FinSequence of TS PeanoNat ; let nt be Symbol of PeanoNat; :: according to DTCONSTR:def_5 ::_thesis: ( nt in NonTerminals PeanoNat implies ex p being FinSequence of TS PeanoNat st nt ==> roots p ) assume nt in NonTerminals PeanoNat ; ::_thesis: ex p being FinSequence of TS PeanoNat st nt ==> roots p then A1: nt = S by Lm14, TARSKI:def_1; take p ; ::_thesis: nt ==> roots p A2: dom <*rO*> = Seg 1 by FINSEQ_1:38; A3: dom <*O*> = Seg 1 by FINSEQ_1:38; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_ ex_rO_being_DecoratedTree_st_ (_rO_=_p_._i_&_<*O*>_._i_=_rO_._{}_) let i be Element of NAT ; ::_thesis: ( i in dom p implies ex rO being DecoratedTree st ( rO = p . i & <*O*> . i = rO . {} ) ) assume A4: i in dom p ; ::_thesis: ex rO being DecoratedTree st ( rO = p . i & <*O*> . i = rO . {} ) reconsider rO = rO as DecoratedTree ; take rO = rO; ::_thesis: ( rO = p . i & <*O*> . i = rO . {} ) A5: i = 1 by A2, A4, FINSEQ_1:2, TARSKI:def_1; <*O*> . 1 = O by FINSEQ_1:40; hence ( rO = p . i & <*O*> . i = rO . {} ) by A5, FINSEQ_1:40, TREES_4:3; ::_thesis: verum end; hence nt ==> roots p by A1, A2, A3, Lm5, TREES_3:def_18; ::_thesis: verum end; registration cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals for DTConstrStr ; existence ex b1 being non empty DTConstrStr st ( b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict ) by Lm16; end; definition let G be non empty with_terminals DTConstrStr ; :: original: Terminals redefine func Terminals G -> non empty Subset of G; coherence Terminals G is non empty Subset of G proof defpred S2[ Element of G] means for tnt being FinSequence holds not $1 ==> tnt; { t where t is Element of G : S2[t] } c= the carrier of G from FRAENKEL:sch_10(); hence Terminals G is non empty Subset of G by Def3, LANG1:def_2; ::_thesis: verum end; end; registration let G be non empty with_terminals DTConstrStr ; cluster TS G -> non empty ; coherence not TS G is empty proof ex t being set st t in Terminals G by XBOOLE_0:def_1; hence not TS G is empty by Def1; ::_thesis: verum end; end; registration let G be non empty with_useful_nonterminals DTConstrStr ; cluster TS G -> non empty ; coherence not TS G is empty proof set s = the Symbol of G; percases ( for tnt being FinSequence holds not the Symbol of G ==> tnt or ex tnt being FinSequence st the Symbol of G ==> tnt ) ; suppose for tnt being FinSequence holds not the Symbol of G ==> tnt ; ::_thesis: not TS G is empty then the Symbol of G in { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } ; then the Symbol of G in Terminals G by LANG1:def_2; hence not TS G is empty by Def1; ::_thesis: verum end; suppose ex tnt being FinSequence st the Symbol of G ==> tnt ; ::_thesis: not TS G is empty then the Symbol of G in { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } ; then the Symbol of G in NonTerminals G by LANG1:def_3; then ex p being FinSequence of TS G st the Symbol of G ==> roots p by Def5; hence not TS G is empty by Def1; ::_thesis: verum end; end; end; end; definition let G be non empty with_nonterminals DTConstrStr ; :: original: NonTerminals redefine func NonTerminals G -> non empty Subset of G; coherence NonTerminals G is non empty Subset of G proof defpred S2[ Element of G] means ex tnt being FinSequence st $1 ==> tnt; { t where t is Element of G : S2[t] } c= the carrier of G from FRAENKEL:sch_10(); hence NonTerminals G is non empty Subset of G by Def4, LANG1:def_3; ::_thesis: verum end; end; definition let G be non empty with_terminals DTConstrStr ; mode Terminal of G is Element of Terminals G; end; definition let G be non empty with_nonterminals DTConstrStr ; mode NonTerminal of G is Element of NonTerminals G; end; definition let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ; let nt be NonTerminal of G; mode SubtreeSeq of nt -> FinSequence of TS G means :Def6: :: DTCONSTR:def 6 nt ==> roots it; existence ex b1 being FinSequence of TS G st nt ==> roots b1 by Def5; end; :: deftheorem Def6 defines SubtreeSeq DTCONSTR:def_6_:_ for G being non empty with_nonterminals with_useful_nonterminals DTConstrStr for nt being NonTerminal of G for b3 being FinSequence of TS G holds ( b3 is SubtreeSeq of nt iff nt ==> roots b3 ); definition let G be non empty with_terminals DTConstrStr ; let t be Terminal of G; :: original: root-tree redefine func root-tree t -> Element of TS G; coherence root-tree t is Element of TS G by Def1; end; definition let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ; let nt be NonTerminal of G; let p be SubtreeSeq of nt; :: original: -tree redefine funcnt -tree p -> Element of TS G; coherence nt -tree p is Element of TS G proof nt ==> roots p by Def6; hence nt -tree p is Element of TS G by Def1; ::_thesis: verum end; end; theorem Th9: :: DTCONSTR:9 for G being non empty with_terminals DTConstrStr for tsg being Element of TS G for s being Terminal of G st tsg . {} = s holds tsg = root-tree s proof let G be non empty with_terminals DTConstrStr ; ::_thesis: for tsg being Element of TS G for s being Terminal of G st tsg . {} = s holds tsg = root-tree s let tsg be Element of TS G; ::_thesis: for s being Terminal of G st tsg . {} = s holds tsg = root-tree s let s be Terminal of G; ::_thesis: ( tsg . {} = s implies tsg = root-tree s ) assume A1: tsg . {} = s ; ::_thesis: tsg = root-tree s defpred S2[ 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 S2[ root-tree s] by TREES_4:3; A3: now__::_thesis:_for_nt_being_Symbol_of_G for_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_ S2[t]_)_holds_ S2[nt_-tree_ts] let nt be Symbol of G; ::_thesis: for 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 S2[t] ) holds S2[nt -tree ts] let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds S2[t] ) implies S2[nt -tree ts] ) assume that A4: nt ==> roots ts and for t being DecoratedTree of the carrier of G st t in rng ts holds S2[t] ; ::_thesis: S2[nt -tree ts] thus S2[nt -tree ts] ::_thesis: verum proof let s be Terminal of G; ::_thesis: ( (nt -tree ts) . {} = s implies nt -tree ts = root-tree s ) assume A5: (nt -tree ts) . {} = s ; ::_thesis: nt -tree ts = root-tree s A6: (nt -tree ts) . {} = nt by TREES_4:def_4; A7: s in Terminals G ; Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def_2; then ex t being Symbol of G st ( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A7; hence nt -tree ts = root-tree s by A4, A5, A6; ::_thesis: verum end; end; for t being DecoratedTree of the carrier of G st t in TS G holds S2[t] from DTCONSTR:sch_7(A2, A3); hence tsg = root-tree s by A1; ::_thesis: verum end; theorem Th10: :: DTCONSTR:10 for G being non empty with_terminals with_nonterminals DTConstrStr for tsg being Element of TS G for nt being NonTerminal of G st tsg . {} = nt holds ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) proof let G be non empty with_terminals with_nonterminals DTConstrStr ; ::_thesis: for tsg being Element of TS G for nt being NonTerminal of G st tsg . {} = nt holds ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) defpred S2[ DecoratedTree of the carrier of G] means for nt being NonTerminal of G st $1 . {} = nt holds ex ts being FinSequence of TS G st ( $1 = nt -tree ts & nt ==> roots ts ); A1: now__::_thesis:_for_s_being_Symbol_of_G_st_s_in_Terminals_G_holds_ S2[_root-tree_s] let s be Symbol of G; ::_thesis: ( s in Terminals G implies S2[ root-tree s] ) assume A2: s in Terminals G ; ::_thesis: S2[ root-tree s] thus S2[ root-tree s] ::_thesis: verum proof let nt be NonTerminal of G; ::_thesis: ( (root-tree s) . {} = nt implies ex ts being FinSequence of TS G st ( root-tree s = nt -tree ts & nt ==> roots ts ) ) assume (root-tree s) . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st ( root-tree s = nt -tree ts & nt ==> roots ts ) then A3: s = nt by TREES_4:3; Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def_2; then A4: ex t being Symbol of G st ( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A2; A5: nt in NonTerminals G ; NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def_3; then ex t being Symbol of G st ( nt = t & ex tnt being FinSequence st t ==> tnt ) by A5; hence ex ts being FinSequence of TS G st ( root-tree s = nt -tree ts & nt ==> roots ts ) by A3, A4; ::_thesis: verum end; end; A6: now__::_thesis:_for_nnt_being_Symbol_of_G for_tts_being_FinSequence_of_TS_G_st_nnt_==>_roots_tts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_G_st_t_in_rng_tts_holds_ S2[t]_)_holds_ S2[nnt_-tree_tts] let nnt be Symbol of G; ::_thesis: for tts being FinSequence of TS G st nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds S2[t] ) holds S2[nnt -tree tts] let tts be FinSequence of TS G; ::_thesis: ( nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds S2[t] ) implies S2[nnt -tree tts] ) assume that A7: nnt ==> roots tts and for t being DecoratedTree of the carrier of G st t in rng tts holds S2[t] ; ::_thesis: S2[nnt -tree tts] thus S2[nnt -tree tts] ::_thesis: verum proof let nt be NonTerminal of G; ::_thesis: ( (nnt -tree tts) . {} = nt implies ex ts being FinSequence of TS G st ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) ) assume A8: (nnt -tree tts) . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) take ts = tts; ::_thesis: ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) thus ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) by A7, A8, TREES_4:def_4; ::_thesis: verum end; end; A9: for t being DecoratedTree of the carrier of G st t in TS G holds S2[t] from DTCONSTR:sch_7(A1, A6); let tsg be Element of TS G; ::_thesis: for nt being NonTerminal of G st tsg . {} = nt holds ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) let nt be NonTerminal of G; ::_thesis: ( tsg . {} = nt implies ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) ) assume tsg . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) hence ex ts being FinSequence of TS G st ( tsg = nt -tree ts & nt ==> roots ts ) by A9; ::_thesis: verum end; begin registration cluster PeanoNat -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ; coherence ( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) by Lm16; end; set PN = PeanoNat ; reconsider O = O as Terminal of PeanoNat by Lm9; reconsider S = S as NonTerminal of PeanoNat by Lm12; definition let nt be NonTerminal of PeanoNat; let t be Element of TS PeanoNat; :: original: -tree redefine funcnt -tree t -> Element of TS PeanoNat; coherence nt -tree t is Element of TS PeanoNat proof reconsider r = {} as Node of t by TREES_1:22; ( t . r = 0 or t . r = 1 ) by Lm2, TARSKI:def_2; then A1: ( roots <*t*> = <*0*> or roots <*t*> = <*1*> ) by Th4; nt = S by Lm15, TARSKI:def_1; then nt -tree <*t*> in TS PeanoNat by A1, Def1, Lm5, Lm6; hence nt -tree t is Element of TS PeanoNat by TREES_4:def_5; ::_thesis: verum end; end; definition let x be FinSequence of NAT ; func plus-one x -> Element of NAT equals :: DTCONSTR:def 7 (x . 1) + 1; coherence (x . 1) + 1 is Element of NAT ; end; :: deftheorem defines plus-one DTCONSTR:def_7_:_ for x being FinSequence of NAT holds plus-one x = (x . 1) + 1; deffunc H3( set , set , FinSequence of NAT ) -> Element of NAT = plus-one $3; definition func PN-to-NAT -> Function of (TS PeanoNat),NAT means :Def8: :: DTCONSTR:def 8 ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds it . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds it . (nt -tree ts) = plus-one (it * ts) ) ); existence ex b1 being Function of (TS PeanoNat),NAT st ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds b1 . (nt -tree ts) = plus-one (b1 * ts) ) ) 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) = H1(t) ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds f . (nt -tree ts) = H3(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (TS PeanoNat),NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds b1 . (nt -tree ts) = plus-one (b1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds b2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds b2 . (nt -tree ts) = plus-one (b2 * ts) ) holds b1 = b2 proof let it1, it2 be Function of (TS PeanoNat),NAT; ::_thesis: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds it1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds it1 . (nt -tree ts) = plus-one (it1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds it2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds it2 . (nt -tree ts) = plus-one (it2 * ts) ) implies it1 = it2 ) assume that A1: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds it1 . (root-tree t) = H1(t) ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds it1 . (nt -tree ts) = H3(nt, roots ts,it1 * ts) ) ) and A2: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds it2 . (root-tree t) = H1(t) ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds it2 . (nt -tree ts) = H3(nt, roots ts,it2 * ts) ) ) ; ::_thesis: it1 = it2 thus it1 = it2 from DTCONSTR:sch_9(A1, A2); ::_thesis: verum end; end; :: deftheorem Def8 defines PN-to-NAT DTCONSTR:def_8_:_ for b1 being Function of (TS PeanoNat),NAT holds ( b1 = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds b1 . (nt -tree ts) = plus-one (b1 * ts) ) ) ); definition let x be Element of TS PeanoNat; func PNsucc x -> Element of TS PeanoNat equals :: DTCONSTR:def 9 1 -tree <*x*>; coherence 1 -tree <*x*> is Element of TS PeanoNat proof reconsider r = {} as Node of x by TREES_1:22; A1: roots <*x*> = <*(x . r)*> by Th4; ( x . r = O or x . r = S ) by Lm2, TARSKI:def_2; hence 1 -tree <*x*> is Element of TS PeanoNat by A1, Def1, Lm5, Lm6; ::_thesis: verum end; end; :: deftheorem defines PNsucc DTCONSTR:def_9_:_ for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>; deffunc H4( set , Element of TS PeanoNat) -> Element of TS PeanoNat = PNsucc $2; definition func NAT-to-PN -> Function of NAT,(TS PeanoNat) means :Def10: :: DTCONSTR:def 10 ( it . 0 = root-tree 0 & ( for n being Nat holds it . (n + 1) = PNsucc (it . n) ) ); existence ex b1 being Function of NAT,(TS PeanoNat) st ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) proof ex f being Function of NAT,(TS PeanoNat) st ( f . 0 = root-tree O & ( for n being Nat holds f . (n + 1) = H4(n,f . n) ) ) from NAT_1:sch_12(); hence ex b1 being Function of NAT,(TS PeanoNat) st ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(TS PeanoNat) st b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) & b2 . 0 = root-tree 0 & ( for n being Nat holds b2 . (n + 1) = PNsucc (b2 . n) ) holds b1 = b2 proof let it1, it2 be Function of NAT,(TS PeanoNat); ::_thesis: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) implies it1 = it2 ) assume A1: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) & not it1 = it2 ) ; ::_thesis: contradiction then A2: it1 . 0 = root-tree O ; A3: for n being Nat holds it1 . (n + 1) = H4(n,it1 . n) by A1; A4: it2 . 0 = root-tree O by A1; A5: for n being Nat holds it2 . (n + 1) = H4(n,it2 . n) by A1; it1 = it2 from NAT_1:sch_16(A2, A3, A4, A5); hence contradiction by A1; ::_thesis: verum end; end; :: deftheorem Def10 defines NAT-to-PN DTCONSTR:def_10_:_ for b1 being Function of NAT,(TS PeanoNat) holds ( b1 = NAT-to-PN iff ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) ); theorem :: DTCONSTR:11 for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn) proof defpred S2[ DecoratedTree of the carrier of PeanoNat] means $1 = NAT-to-PN . (PN-to-NAT . $1); A1: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_ S2[_root-tree_s] let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] ) assume A2: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s] then NAT-to-PN . (PN-to-NAT . (root-tree s)) = NAT-to-PN . 0 by Def8 .= root-tree O by Def10 ; hence S2[ root-tree s] by A2, Lm10, TARSKI:def_1; ::_thesis: verum end; A3: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_ S2[t]_)_holds_ S2[nt_-tree_ts] let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) holds S2[nt -tree ts] let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) implies S2[nt -tree ts] ) assume that A4: nt ==> roots ts and A5: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ; ::_thesis: S2[nt -tree ts] A6: nt <> O by A4, Lm8; ( roots ts = <*O*> or roots ts = <*S*> ) by A4, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider dt being Element of FinTrees the carrier of PeanoNat such that A7: ts = <*dt*> and A8: dt in TS PeanoNat by Th5; reconsider dt = dt as Element of TS PeanoNat by A8; rng ts = {dt} by A7, FINSEQ_1:38; then dt in rng ts by TARSKI:def_1; then A9: dt = NAT-to-PN . (PN-to-NAT . dt) by A5; A10: PN-to-NAT * ts = <*(PN-to-NAT . dt)*> by A7, FINSEQ_2:35; set N = PN-to-NAT . dt; A11: plus-one <*(PN-to-NAT . dt)*> = (PN-to-NAT . dt) + 1 by FINSEQ_1:40; NAT-to-PN . ((PN-to-NAT . dt) + 1) = PNsucc dt by A9, Def10 .= nt -tree ts by A6, A7, Lm2, TARSKI:def_2 ; hence S2[nt -tree ts] by A4, A10, A11, Def8; ::_thesis: verum end; for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds S2[t] from DTCONSTR:sch_7(A1, A3); hence for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn) ; ::_thesis: verum end; Lm17: 0 = PN-to-NAT . (root-tree O) by Def8 .= PN-to-NAT . (NAT-to-PN . 0) by Def10 ; Lm18: now__::_thesis:_for_n_being_Element_of_NAT_st_n_=_PN-to-NAT_._(NAT-to-PN_._n)_holds_ n_+_1_=_PN-to-NAT_._(NAT-to-PN_._(n_+_1)) let n be Element of NAT ; ::_thesis: ( n = PN-to-NAT . (NAT-to-PN . n) implies n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) ) assume A1: n = PN-to-NAT . (NAT-to-PN . n) ; ::_thesis: n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) reconsider dt = NAT-to-PN . n as Element of TS PeanoNat ; reconsider r = {} as Node of dt by TREES_1:22; A2: ( dt . r = O or dt . r = S ) by Lm2, TARSKI:def_2; A3: NAT-to-PN . (n + 1) = PNsucc (NAT-to-PN . n) by Def10 .= S -tree <*(NAT-to-PN . n)*> ; A4: S ==> roots <*(NAT-to-PN . n)*> by A2, Lm3, Lm4, Th4; <*(PN-to-NAT . (NAT-to-PN . n))*> = PN-to-NAT * <*(NAT-to-PN . n)*> by FINSEQ_2:35; then PN-to-NAT . (S -tree <*(NAT-to-PN . n)*>) = plus-one <*n*> by A1, A4, Def8 .= n + 1 by FINSEQ_1:40 ; hence n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) by A3; ::_thesis: verum end; theorem :: DTCONSTR:12 for n being Element of NAT holds n = PN-to-NAT . (NAT-to-PN . n) proof defpred S2[ Element of NAT ] means $1 = PN-to-NAT . (NAT-to-PN . $1); A1: S2[ 0 ] by Lm17; A2: for n being Element of NAT st S2[n] holds S2[n + 1] by Lm18; thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A1, A2); ::_thesis: verum end; begin definition let G be non empty DTConstrStr ; let tsg be DecoratedTree of the carrier of G; assume A1: tsg in TS G ; defpred S2[ set ] means $1 in Terminals G; deffunc H5( set ) -> set = <*$1*>; deffunc H6( set ) -> set = {} ; A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_ (_(_S2[x]_implies_H5(x)_in_(Terminals_G)_*_)_&_(_not_S2[x]_implies_H6(x)_in_(Terminals_G)_*_)_) let x be set ; ::_thesis: ( x in the carrier of G implies ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) ) ) assume x in the carrier of G ; ::_thesis: ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) ) hereby ::_thesis: ( not S2[x] implies H6(x) in (Terminals G) * ) assume A3: S2[x] ; ::_thesis: H5(x) in (Terminals G) * then reconsider T = Terminals G as non empty set ; reconsider x9 = x as Element of T by A3; <*x9*> is FinSequence of T ; hence H5(x) in (Terminals G) * ; ::_thesis: verum end; assume not S2[x] ; ::_thesis: H6(x) in (Terminals G) * <*> (Terminals G) = {} ; hence H6(x) in (Terminals G) * ; ::_thesis: verum 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 ( ( S2[s] implies s2t . s = H5(s) ) & ( not S2[s] implies s2t . s = H6(s) ) ) from FUNCT_2:sch_5(A2); deffunc H7( Symbol of G) -> Element of (Terminals G) * = s2t . $1; deffunc H8( set , set , FinSequence of (Terminals G) * ) -> Element of (Terminals G) * = FlattenSeq $3; deffunc H9( set ) -> set = <*$1*>; func TerminalString tsg -> FinSequence of Terminals G means :Def11: :: DTCONSTR:def 11 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ); existence ex b1 being FinSequence of Terminals G ex f being Function of (TS G),((Terminals G) *) st ( b1 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) 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) = H7(t) ) & ( for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = H8(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8(); f . tsg is Element of (Terminals G) * by A1, FUNCT_2:5; then reconsider IT = f . tsg as FinSequence of Terminals G ; take IT ; ::_thesis: 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) take f ; ::_thesis: ( 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) thus IT = f . tsg ; ::_thesis: ( ( for t being Symbol of G st t in Terminals G holds f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> ) assume A6: t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*> then f . (root-tree t) = s2t . t by A5; hence f . (root-tree t) = <*t*> by A4, A6; ::_thesis: verum end; thus for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) by A5; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of Terminals G st ex f being Function of (TS G),((Terminals G) *) st ( b1 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) & ex f being Function of (TS G),((Terminals G) *) st ( b2 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) holds b1 = b2 proof let it1, it2 be FinSequence of Terminals G; ::_thesis: ( ex f being Function of (TS G),((Terminals G) *) st ( it1 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) & ex f being Function of (TS G),((Terminals G) *) st ( it2 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) implies it1 = it2 ) given f1 being Function of (TS G),((Terminals G) *) such that A7: it1 = f1 . tsg and A8: for t being Symbol of G st t in Terminals G holds f1 . (root-tree t) = <*t*> and A9: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = FlattenSeq (f1 * ts) ; ::_thesis: ( for f being Function of (TS G),((Terminals G) *) holds ( not it2 = f . tsg or ex t being Symbol of G st ( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G st ( nt ==> roots ts & not f . (nt -tree ts) = FlattenSeq (f * ts) ) ) or it1 = it2 ) given f2 being Function of (TS G),((Terminals G) *) such that A10: it2 = f2 . tsg and A11: for t being Symbol of G st t in Terminals G holds f2 . (root-tree t) = <*t*> and A12: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = FlattenSeq (f2 * ts) ; ::_thesis: it1 = it2 A13: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f1_._(root-tree_t)_=_H7(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f1_._(nt_-tree_ts)_=_H8(nt,_roots_ts,f1_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H8(nt, roots ts,f1 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H7(t) ) assume A14: t in Terminals G ; ::_thesis: f1 . (root-tree t) = H7(t) hence f1 . (root-tree t) = <*t*> by A8 .= H7(t) by A4, A14 ; ::_thesis: verum end; thus for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H8(nt, roots ts,f1 * ts) by A9; ::_thesis: verum end; A15: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f2_._(root-tree_t)_=_H7(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f2_._(nt_-tree_ts)_=_H8(nt,_roots_ts,f2_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H8(nt, roots ts,f2 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H7(t) ) assume A16: t in Terminals G ; ::_thesis: f2 . (root-tree t) = H7(t) hence f2 . (root-tree t) = <*t*> by A11 .= H7(t) by A4, A16 ; ::_thesis: verum end; thus for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H8(nt, roots ts,f2 * ts) by A12; ::_thesis: verum end; f1 = f2 from DTCONSTR:sch_9(A13, A15); hence it1 = it2 by A7, A10; ::_thesis: verum end; A17: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_ H9(x)_in_the_carrier_of_G_* let x be set ; ::_thesis: ( x in the carrier of G implies H9(x) in the carrier of G * ) assume x in the carrier of G ; ::_thesis: H9(x) in the carrier of G * then reconsider x9 = x as Element of G ; <*x9*> is FinSequence of the carrier of G ; hence H9(x) in the carrier of G * ; ::_thesis: verum end; consider s2s being Function of the carrier of G,( the carrier of G *) such that A18: for s being set st s in the carrier of G holds s2s . s = H9(s) from FUNCT_2:sch_2(A17); deffunc H10( Symbol of G) -> Element of the carrier of G * = s2s . $1; deffunc H11( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3); func PreTraversal tsg -> FinSequence of the carrier of G means :Def12: :: DTCONSTR:def 12 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ); existence ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st ( b1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) proof deffunc H12( Symbol of G) -> Element of the carrier of G * = s2s . $1; deffunc H13( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3); consider f being Function of (TS G),( the carrier of G *) such that A19: ( ( for t being Symbol of G st t in Terminals G holds f . (root-tree t) = H12(t) ) & ( for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = H13(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8(); f . tsg is Element of the carrier of G * by A1, FUNCT_2:5; then reconsider IT = f . tsg as FinSequence of the carrier of G ; take IT ; ::_thesis: 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) take f ; ::_thesis: ( 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) thus IT = f . tsg ; ::_thesis: ( ( for t being Symbol of G st t in Terminals G holds f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> ) assume t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*> then f . (root-tree t) = s2s . t by A19; hence f . (root-tree t) = <*t*> by A18; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) let ts be FinSequence of TS G; ::_thesis: for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) let rts be FinSequence; ::_thesis: ( rts = roots ts & nt ==> rts implies for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) assume that A20: rts = roots ts and A21: nt ==> rts ; ::_thesis: for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) let x be FinSequence of the carrier of G * ; ::_thesis: ( x = f * ts implies f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) assume x = f * ts ; ::_thesis: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) hence f . (nt -tree ts) = (s2s . nt) ^ (FlattenSeq x) by A19, A20, A21 .= <*nt*> ^ (FlattenSeq x) by A18 ; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st ( b1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) & ex f being Function of (TS G),( the carrier of G *) st ( b2 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) holds b1 = b2 proof let it1, it2 be FinSequence of the carrier of G; ::_thesis: ( ex f being Function of (TS G),( the carrier of G *) st ( it1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) & ex f being Function of (TS G),( the carrier of G *) st ( it2 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) implies it1 = it2 ) given f1 being Function of (TS G),( the carrier of G *) such that A22: it1 = f1 . tsg and A23: for t being Symbol of G st t in Terminals G holds f1 . (root-tree t) = <*t*> and A24: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f1 * ts holds f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; ::_thesis: ( for f being Function of (TS G),( the carrier of G *) holds ( not it2 = f . tsg or ex t being Symbol of G st ( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G ex rts being FinSequence st ( rts = roots ts & nt ==> rts & ex x being FinSequence of the carrier of G * st ( x = f * ts & not f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) ) or it1 = it2 ) given f2 being Function of (TS G),( the carrier of G *) such that A25: it2 = f2 . tsg and A26: for t being Symbol of G st t in Terminals G holds f2 . (root-tree t) = <*t*> and A27: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f2 * ts holds f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; ::_thesis: it1 = it2 A28: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f1_._(root-tree_t)_=_H10(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f1_._(nt_-tree_ts)_=_H11(nt,_roots_ts,f1_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H10(t) ) assume t in Terminals G ; ::_thesis: f1 . (root-tree t) = H10(t) hence f1 . (root-tree t) = <*t*> by A23 .= H10(t) by A18 ; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts) let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts) ) assume nt ==> roots ts ; ::_thesis: f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts) hence f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f1 * ts)) by A24 .= H11(nt, roots ts,f1 * ts) by A18 ; ::_thesis: verum end; A29: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f2_._(root-tree_t)_=_H10(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f2_._(nt_-tree_ts)_=_H11(nt,_roots_ts,f2_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H10(t) ) assume t in Terminals G ; ::_thesis: f2 . (root-tree t) = H10(t) hence f2 . (root-tree t) = <*t*> by A26 .= H10(t) by A18 ; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts) let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts) ) assume nt ==> roots ts ; ::_thesis: f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts) hence f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f2 * ts)) by A27 .= H11(nt, roots ts,f2 * ts) by A18 ; ::_thesis: verum end; f1 = f2 from DTCONSTR:sch_9(A28, A29); hence it1 = it2 by A22, A25; ::_thesis: verum end; deffunc H12( Symbol of G) -> Element of the carrier of G * = s2s . $1; deffunc H13( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (FlattenSeq $3) ^ (s2s . $1); func PostTraversal tsg -> FinSequence of the carrier of G means :Def13: :: DTCONSTR:def 13 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ); existence ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st ( b1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) proof consider f being Function of (TS G),( the carrier of G *) such that A30: ( ( for t being Symbol of G st t in Terminals G holds f . (root-tree t) = H12(t) ) & ( for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = H13(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8(); f . tsg is Element of the carrier of G * by A1, FUNCT_2:5; then reconsider IT = f . tsg as FinSequence of the carrier of G ; take IT ; ::_thesis: 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) take f ; ::_thesis: ( 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) thus IT = f . tsg ; ::_thesis: ( ( for t being Symbol of G st t in Terminals G holds f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> ) assume t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*> then f . (root-tree t) = s2s . t by A30; hence f . (root-tree t) = <*t*> by A18; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> let ts be FinSequence of TS G; ::_thesis: for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> let rts be FinSequence; ::_thesis: ( rts = roots ts & nt ==> rts implies for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) assume that A31: rts = roots ts and A32: nt ==> rts ; ::_thesis: for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> let x be FinSequence of the carrier of G * ; ::_thesis: ( x = f * ts implies f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) assume x = f * ts ; ::_thesis: f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> hence f . (nt -tree ts) = (FlattenSeq x) ^ (s2s . nt) by A30, A31, A32 .= (FlattenSeq x) ^ <*nt*> by A18 ; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st ( b1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) & ex f being Function of (TS G),( the carrier of G *) st ( b2 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) holds b1 = b2 proof let it1, it2 be FinSequence of the carrier of G; ::_thesis: ( ex f being Function of (TS G),( the carrier of G *) st ( it1 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) & ex f being Function of (TS G),( the carrier of G *) st ( it2 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) implies it1 = it2 ) given f1 being Function of (TS G),( the carrier of G *) such that A33: it1 = f1 . tsg and A34: for t being Symbol of G st t in Terminals G holds f1 . (root-tree t) = <*t*> and A35: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f1 * ts holds f1 . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ; ::_thesis: ( for f being Function of (TS G),( the carrier of G *) holds ( not it2 = f . tsg or ex t being Symbol of G st ( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G ex rts being FinSequence st ( rts = roots ts & nt ==> rts & ex x being FinSequence of the carrier of G * st ( x = f * ts & not f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) ) or it1 = it2 ) given f2 being Function of (TS G),( the carrier of G *) such that A36: it2 = f2 . tsg and A37: for t being Symbol of G st t in Terminals G holds f2 . (root-tree t) = <*t*> and A38: for nt being Symbol of G for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f2 * ts holds f2 . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ; ::_thesis: it1 = it2 A39: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f1_._(root-tree_t)_=_H12(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f1_._(nt_-tree_ts)_=_H13(nt,_roots_ts,f1_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H12(t) ) assume t in Terminals G ; ::_thesis: f1 . (root-tree t) = H12(t) hence f1 . (root-tree t) = <*t*> by A34 .= H12(t) by A18 ; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts) let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts) ) assume nt ==> roots ts ; ::_thesis: f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts) hence f1 . (nt -tree ts) = (FlattenSeq (f1 * ts)) ^ <*nt*> by A35 .= H13(nt, roots ts,f1 * ts) by A18 ; ::_thesis: verum end; A40: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_ f2_._(root-tree_t)_=_H12(t)_)_&_(_for_nt_being_Symbol_of_G for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_ f2_._(nt_-tree_ts)_=_H13(nt,_roots_ts,f2_*_ts)_)_) hereby ::_thesis: for nt being Symbol of G for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts) let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H12(t) ) assume t in Terminals G ; ::_thesis: f2 . (root-tree t) = H12(t) hence f2 . (root-tree t) = <*t*> by A37 .= H12(t) by A18 ; ::_thesis: verum end; let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts) let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts) ) assume nt ==> roots ts ; ::_thesis: f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts) hence f2 . (nt -tree ts) = (FlattenSeq (f2 * ts)) ^ <*nt*> by A38 .= H13(nt, roots ts,f2 * ts) by A18 ; ::_thesis: verum end; f1 = f2 from DTCONSTR:sch_9(A39, A40); hence it1 = it2 by A33, A36; ::_thesis: verum end; end; :: deftheorem Def11 defines TerminalString DTCONSTR:def_11_:_ for G being non empty DTConstrStr for tsg being DecoratedTree of the carrier of G st tsg in TS G holds for b3 being FinSequence of Terminals G holds ( b3 = TerminalString tsg iff ex f being Function of (TS G),((Terminals G) *) st ( b3 = 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 for ts being FinSequence of TS G st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) ) ) ); :: deftheorem Def12 defines PreTraversal DTCONSTR:def_12_:_ for G being non empty DTConstrStr for tsg being DecoratedTree of the carrier of G st tsg in TS G holds for b3 being FinSequence of the carrier of G holds ( b3 = PreTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st ( b3 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) ); :: deftheorem Def13 defines PostTraversal DTCONSTR:def_13_:_ for G being non empty DTConstrStr for tsg being DecoratedTree of the carrier of G st tsg in TS G holds for b3 being FinSequence of the carrier of G holds ( b3 = PostTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st ( b3 = 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 for ts being FinSequence of TS G for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of G * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) ); definition let G be non empty with_nonterminals DTConstrStr ; let nt be Symbol of G; func TerminalLanguage nt -> Subset of ((Terminals G) *) equals :: DTCONSTR:def 14 { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; coherence { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *) proof set TL = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } c= (Terminals G) * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in (Terminals G) * ) assume x in { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in (Terminals G) * then ex tsg being Element of FinTrees the carrier of G st ( x = TerminalString tsg & tsg in TS G & tsg . {} = nt ) ; hence x in (Terminals G) * by FINSEQ_1:def_11; ::_thesis: verum end; hence { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *) ; ::_thesis: verum end; func PreTraversalLanguage nt -> Subset of ( the carrier of G *) equals :: DTCONSTR:def 15 { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; coherence { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *) proof set TL = { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } c= the carrier of G * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in the carrier of G * ) assume x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in the carrier of G * then ex tsg being Element of FinTrees the carrier of G st ( x = PreTraversal tsg & tsg in TS G & tsg . {} = nt ) ; hence x in the carrier of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *) ; ::_thesis: verum end; func PostTraversalLanguage nt -> Subset of ( the carrier of G *) equals :: DTCONSTR:def 16 { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; coherence { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *) proof set TL = { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } c= the carrier of G * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in the carrier of G * ) assume x in { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in the carrier of G * then ex tsg being Element of FinTrees the carrier of G st ( x = PostTraversal tsg & tsg in TS G & tsg . {} = nt ) ; hence x in the carrier of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *) ; ::_thesis: verum end; end; :: deftheorem defines TerminalLanguage DTCONSTR:def_14_:_ for G being non empty with_nonterminals DTConstrStr for nt being Symbol of G holds TerminalLanguage nt = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; :: deftheorem defines PreTraversalLanguage DTCONSTR:def_15_:_ for G being non empty with_nonterminals DTConstrStr for nt being Symbol of G holds PreTraversalLanguage nt = { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; :: deftheorem defines PostTraversalLanguage DTCONSTR:def_16_:_ for G being non empty with_nonterminals DTConstrStr for nt being Symbol of G holds PostTraversalLanguage nt = { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; theorem Th13: :: DTCONSTR:13 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 PeanoNat),((Terminals PeanoNat) *) such that A1: TerminalString (root-tree O) = f . (root-tree O) and A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds f . (root-tree t) = <*t*> and A3: for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds f . (nt -tree ts) = FlattenSeq (f * ts) by Def11; defpred S2[ DecoratedTree of the carrier of PeanoNat] means TerminalString $1 = <*0*>; A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_ S2[_root-tree_s] let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] ) assume s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s] then s = O by Lm10, TARSKI:def_1; hence S2[ root-tree s] by A1, A2; ::_thesis: verum end; A5: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_ S2[t]_)_holds_ S2[nt_-tree_ts] let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) holds S2[nt -tree ts] let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) implies S2[nt -tree ts] ) assume that A6: nt ==> roots ts and A7: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ; ::_thesis: S2[nt -tree ts] A8: nt -tree ts in TS PeanoNat by A6, Def1; ( roots ts = <*O*> or roots ts = <*1*> ) by A6, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider x being Element of FinTrees the carrier of PeanoNat such that A9: ts = <*x*> and A10: x in TS PeanoNat by Th5; reconsider x9 = x as Element of TS PeanoNat by A10; rng ts = {x} by A9, FINSEQ_1:39; then A11: x in rng ts by TARSKI:def_1; f . x9 is Element of (Terminals PeanoNat) * ; then A12: f . x9 = TerminalString x by A2, A3, Def11 .= <*O*> by A7, A11 ; f * ts = <*(f . x)*> by A9, FINSEQ_2:35; then f . (nt -tree ts) = FlattenSeq <*(f . x9)*> by A3, A6 .= <*O*> by A12, PRE_POLY:1 ; hence S2[nt -tree ts] by A2, A3, A8, Def11; ::_thesis: verum end; thus for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds S2[t] from DTCONSTR:sch_7(A4, A5); ::_thesis: verum end; theorem :: DTCONSTR:14 for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>} proof let nt be Symbol of PeanoNat; ::_thesis: TerminalLanguage nt = {<*0*>} A1: ( nt = S or nt = O ) by Lm2, TARSKI:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= TerminalLanguage nt let x be set ; ::_thesis: ( x in TerminalLanguage nt implies x in {<*0*>} ) assume x in TerminalLanguage nt ; ::_thesis: x in {<*0*>} then ex tsg being Element of FinTrees the carrier of PeanoNat st ( x = TerminalString tsg & tsg in TS PeanoNat & tsg . {} = nt ) ; then x = <*O*> by Th13; hence x in {<*0*>} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in TerminalLanguage nt ) assume x in {<*0*>} ; ::_thesis: x in TerminalLanguage nt then A2: x = <*O*> by TARSKI:def_1; reconsider prtO = root-tree O as Element of TS PeanoNat ; reconsider rtO = root-tree O as Element of TS PeanoNat ; reconsider srtO = <*prtO*> as FinSequence of TS PeanoNat ; A3: rtO . {} = O by TREES_4:3; then S ==> roots <*rtO*> by Lm5, Th4; then A4: S -tree <*prtO*> in TS PeanoNat by Def1; then A5: TerminalString (S -tree srtO) = x by A2, Th13; A6: (S -tree <*rtO*>) . {} = S by TREES_4:def_4; TerminalString rtO = x by A2, Th13; hence x in TerminalLanguage nt by A1, A3, A4, A5, A6; ::_thesis: verum end; theorem Th15: :: DTCONSTR:15 for t being Element of TS PeanoNat holds PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> proof consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that A1: PreTraversal (root-tree O) = f . (root-tree O) and A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds f . (root-tree t) = <*t*> and A3: for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) by Def12; reconsider rtO = root-tree O as Element of TS PeanoNat ; defpred S2[ DecoratedTree of the carrier of PeanoNat] means ex t being Element of TS PeanoNat st ( $1 = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> ); A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_ S2[_root-tree_s] let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] ) assume A5: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s] thus S2[ root-tree s] ::_thesis: verum proof take t = rtO; ::_thesis: ( root-tree s = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> ) thus root-tree s = t by A5, Lm10, TARSKI:def_1; ::_thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> thus PreTraversal t = <*O*> by A1, A2 .= {} ^ <*O*> by FINSEQ_1:34 .= (0 |-> 1) ^ <*0*> .= ((height (dom t)) |-> 1) ^ <*0*> by TREES_1:42, TREES_4:3 ; ::_thesis: verum end; end; A6: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_ S2[t]_)_holds_ S2[nt_-tree_ts] let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) holds S2[nt -tree ts] let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) implies S2[nt -tree ts] ) assume that A7: nt ==> roots ts and A8: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ; ::_thesis: S2[nt -tree ts] reconsider t9 = nt -tree ts as Element of TS PeanoNat by A7, Def1; A9: nt = S by A7, Def2; ( roots ts = <*O*> or roots ts = <*1*> ) by A7, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider x being Element of FinTrees the carrier of PeanoNat such that A10: ts = <*x*> and A11: x in TS PeanoNat by Th5; reconsider x9 = x as Element of TS PeanoNat by A11; rng ts = {x} by A10, FINSEQ_1:39; then x in rng ts by TARSKI:def_1; then A12: ex t9 being Element of TS PeanoNat st ( x = t9 & PreTraversal t9 = ((height (dom t9)) |-> 1) ^ <*0*> ) by A8; f . x9 is Element of the carrier of PeanoNat * ; then A13: f . x9 = ((height (dom x9)) |-> 1) ^ <*0*> by A2, A3, A12, Def12; f * ts = <*(f . x)*> by A10, FINSEQ_2:35; then A14: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq <*(f . x9)*>) by A3, A7 .= <*nt*> ^ (((height (dom x9)) |-> 1) ^ <*0*>) by A13, PRE_POLY:1 .= (<*nt*> ^ ((height (dom x9)) |-> 1)) ^ <*0*> by FINSEQ_1:32 .= ((1 |-> 1) ^ ((height (dom x9)) |-> 1)) ^ <*0*> by A9, FINSEQ_2:59 .= (((height (dom x9)) + 1) |-> 1) ^ <*0*> by FINSEQ_2:123 .= ((height (^ (dom x9))) |-> 1) ^ <*0*> by TREES_3:80 ; A15: dom (nt -tree x9) = ^ (dom x9) by TREES_4:13; A16: t9 = nt -tree x9 by A10, TREES_4:def_5; f . t9 is Element of the carrier of PeanoNat * ; then PreTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def12; hence S2[nt -tree ts] by A14, A15, A16; ::_thesis: verum end; A17: for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds S2[t] from DTCONSTR:sch_7(A4, A6); let t be Element of TS PeanoNat; ::_thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> S2[t] by A17; hence PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> ; ::_thesis: verum end; theorem :: DTCONSTR:16 for nt being Symbol of PeanoNat holds ( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) ) proof let nt be Symbol of PeanoNat; ::_thesis: ( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) ) reconsider rtO = root-tree O as Element of TS PeanoNat ; height (dom (root-tree 0)) = 0 by TREES_1:42, TREES_4:3; then PreTraversal rtO = (0 |-> 1) ^ <*O*> by Th15; then A1: PreTraversal rtO = {} ^ <*O*> .= <*O*> by FINSEQ_1:34 ; thus ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) ::_thesis: ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) proof assume A2: nt = 0 ; ::_thesis: PreTraversalLanguage nt = {<*0*>} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= PreTraversalLanguage nt let x be set ; ::_thesis: ( x in PreTraversalLanguage nt implies x in {<*0*>} ) assume x in PreTraversalLanguage nt ; ::_thesis: x in {<*0*>} then consider tsg being Element of FinTrees the carrier of PeanoNat such that A3: x = PreTraversal tsg and A4: tsg in TS PeanoNat and A5: tsg . {} = O by A2; tsg = root-tree O by A4, A5, Th9; hence x in {<*0*>} by A1, A3, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in PreTraversalLanguage nt ) assume x in {<*0*>} ; ::_thesis: x in PreTraversalLanguage nt then A6: x = <*O*> by TARSKI:def_1; rtO . {} = O by TREES_4:3; hence x in PreTraversalLanguage nt by A1, A2, A6; ::_thesis: verum end; assume A7: nt = 1 ; ::_thesis: PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } c= PreTraversalLanguage nt let x be set ; ::_thesis: ( x in PreTraversalLanguage nt implies x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) assume x in PreTraversalLanguage nt ; ::_thesis: x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } then consider tsg being Element of FinTrees the carrier of PeanoNat such that A8: x = PreTraversal tsg and A9: tsg in TS PeanoNat and A10: tsg . {} = S by A7; consider ts being FinSequence of TS PeanoNat such that A11: tsg = S -tree ts and A12: S ==> roots ts by A9, A10, Th10; ( roots ts = <*0*> or roots ts = <*1*> ) by A12, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider t being Element of FinTrees the carrier of PeanoNat such that A13: ts = <*t*> and t in TS PeanoNat by Th5; tsg = S -tree t by A11, A13, TREES_4:def_5; then dom tsg = ^ (dom t) by TREES_4:13; then A14: height (dom tsg) = (height (dom t)) + 1 by TREES_3:80; x = ((height (dom tsg)) |-> 1) ^ <*0*> by A8, A9, Th15; hence x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } by A14; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } or x in PreTraversalLanguage nt ) assume x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ; ::_thesis: x in PreTraversalLanguage nt then consider n being Element of NAT such that A15: x = (n |-> 1) ^ <*0*> and A16: n <> 0 ; defpred S2[ Element of NAT ] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PreTraversal tsg = ($1 |-> 1) ^ <*0*> ) ); A17: S2[ 0 ] ; A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_ S2[n_+_1] let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A19: S2[n] ; ::_thesis: S2[n + 1] thus S2[n + 1] ::_thesis: verum proof assume n + 1 <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> ) percases ( n <> 0 or n = 0 ) ; suppose n <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> ) then consider tsg being Element of TS PeanoNat such that tsg . {} = S and A20: PreTraversal tsg = (n |-> 1) ^ <*0*> by A19; PreTraversal tsg = ((height (dom tsg)) |-> 1) ^ <*0*> by Th15; then A21: n |-> 1 = (height (dom tsg)) |-> 1 by A20, FINSEQ_1:33; len (n |-> 1) = n by CARD_1:def_7; then A22: height (dom tsg) = n by A21, CARD_1:def_7; take tsg9 = S -tree tsg; ::_thesis: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) A23: tsg9 = S -tree <*tsg*> by TREES_4:def_5; height (dom tsg9) = height (^ (dom tsg)) by TREES_4:13 .= n + 1 by A22, TREES_3:80 ; hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A23, Th15, TREES_4:def_4; ::_thesis: verum end; supposeA24: n = 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> ) take tsg9 = S -tree rtO; ::_thesis: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) A25: tsg9 = S -tree <*rtO*> by TREES_4:def_5; height (dom tsg9) = height (^ (dom rtO)) by TREES_4:13 .= (height (dom rtO)) + 1 by TREES_3:80 .= n + 1 by A24, TREES_1:42, TREES_4:3 ; hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A25, Th15, TREES_4:def_4; ::_thesis: verum end; end; end; end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A17, A18); then ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PreTraversal tsg = (n |-> 1) ^ <*0*> ) by A16; hence x in PreTraversalLanguage nt by A7, A15; ::_thesis: verum end; theorem Th17: :: DTCONSTR:17 for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) proof consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that A1: PostTraversal (root-tree O) = f . (root-tree O) and A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds f . (root-tree t) = <*t*> and A3: for nt being Symbol of PeanoNat for ts being FinSequence of TS PeanoNat for rts being FinSequence st rts = roots ts & nt ==> rts holds for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> by Def13; reconsider rtO = root-tree O as Element of TS PeanoNat ; defpred S2[ DecoratedTree of the carrier of PeanoNat] means ex t being Element of TS PeanoNat st ( $1 = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) ); A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_ S2[_root-tree_s] let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] ) assume A5: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s] thus S2[ root-tree s] ::_thesis: verum proof take t = rtO; ::_thesis: ( root-tree s = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) ) thus root-tree s = t by A5, Lm10, TARSKI:def_1; ::_thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) thus PostTraversal t = <*O*> by A1, A2 .= <*O*> ^ {} by FINSEQ_1:34 .= <*0*> ^ (0 |-> 1) .= <*0*> ^ ((height (dom t)) |-> 1) by TREES_1:42, TREES_4:3 ; ::_thesis: verum end; end; A6: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_ S2[t]_)_holds_ S2[nt_-tree_ts] let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) holds S2[nt -tree ts] let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ) implies S2[nt -tree ts] ) assume that A7: nt ==> roots ts and A8: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds S2[t] ; ::_thesis: S2[nt -tree ts] reconsider t9 = nt -tree ts as Element of TS PeanoNat by A7, Def1; A9: nt = S by A7, Def2; ( roots ts = <*O*> or roots ts = <*1*> ) by A7, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider x being Element of FinTrees the carrier of PeanoNat such that A10: ts = <*x*> and A11: x in TS PeanoNat by Th5; reconsider x9 = x as Element of TS PeanoNat by A11; rng ts = {x} by A10, FINSEQ_1:39; then x in rng ts by TARSKI:def_1; then A12: ex t9 being Element of TS PeanoNat st ( x = t9 & PostTraversal t9 = <*O*> ^ ((height (dom t9)) |-> 1) ) by A8; f . x9 is Element of the carrier of PeanoNat * ; then A13: f . x9 = <*O*> ^ ((height (dom x9)) |-> 1) by A2, A3, A12, Def13; f * ts = <*(f . x)*> by A10, FINSEQ_2:35; then A14: f . (nt -tree ts) = (FlattenSeq <*(f . x9)*>) ^ <*nt*> by A3, A7 .= (<*O*> ^ ((height (dom x9)) |-> 1)) ^ <*nt*> by A13, PRE_POLY:1 .= <*O*> ^ (((height (dom x9)) |-> 1) ^ <*nt*>) by FINSEQ_1:32 .= <*O*> ^ (((height (dom x9)) |-> 1) ^ (1 |-> 1)) by A9, FINSEQ_2:59 .= <*O*> ^ (((height (dom x9)) + 1) |-> 1) by FINSEQ_2:123 .= <*O*> ^ ((height (^ (dom x9))) |-> 1) by TREES_3:80 ; A15: dom (nt -tree x9) = ^ (dom x9) by TREES_4:13; A16: t9 = nt -tree x9 by A10, TREES_4:def_5; f . t9 is Element of the carrier of PeanoNat * ; then PostTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def13; hence S2[nt -tree ts] by A14, A15, A16; ::_thesis: verum end; A17: for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds S2[t] from DTCONSTR:sch_7(A4, A6); let t be Element of TS PeanoNat; ::_thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) S2[t] by A17; hence PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) ; ::_thesis: verum end; theorem :: DTCONSTR:18 for nt being Symbol of PeanoNat holds ( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) ) proof let nt be Symbol of PeanoNat; ::_thesis: ( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) ) reconsider rtO = root-tree O as Element of TS PeanoNat ; height (dom (root-tree 0)) = 0 by TREES_1:42, TREES_4:3; then PostTraversal rtO = <*0*> ^ (0 |-> 1) by Th17; then A1: PostTraversal rtO = <*O*> ^ {} .= <*O*> by FINSEQ_1:34 ; thus ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) ::_thesis: ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) proof assume A2: nt = 0 ; ::_thesis: PostTraversalLanguage nt = {<*0*>} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= PostTraversalLanguage nt let x be set ; ::_thesis: ( x in PostTraversalLanguage nt implies x in {<*0*>} ) assume x in PostTraversalLanguage nt ; ::_thesis: x in {<*0*>} then consider tsg being Element of FinTrees the carrier of PeanoNat such that A3: x = PostTraversal tsg and A4: tsg in TS PeanoNat and A5: tsg . {} = O by A2; tsg = root-tree O by A4, A5, Th9; hence x in {<*0*>} by A1, A3, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in PostTraversalLanguage nt ) assume x in {<*0*>} ; ::_thesis: x in PostTraversalLanguage nt then A6: x = <*O*> by TARSKI:def_1; rtO . {} = O by TREES_4:3; hence x in PostTraversalLanguage nt by A1, A2, A6; ::_thesis: verum end; assume A7: nt = 1 ; ::_thesis: PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } c= PostTraversalLanguage nt let x be set ; ::_thesis: ( x in PostTraversalLanguage nt implies x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) assume x in PostTraversalLanguage nt ; ::_thesis: x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } then consider tsg being Element of FinTrees the carrier of PeanoNat such that A8: x = PostTraversal tsg and A9: tsg in TS PeanoNat and A10: tsg . {} = S by A7; consider ts being FinSequence of TS PeanoNat such that A11: tsg = S -tree ts and A12: S ==> roots ts by A9, A10, Th10; ( roots ts = <*0*> or roots ts = <*1*> ) by A12, Def2; then len (roots ts) = 1 by FINSEQ_1:40; then consider t being Element of FinTrees the carrier of PeanoNat such that A13: ts = <*t*> and t in TS PeanoNat by Th5; tsg = S -tree t by A11, A13, TREES_4:def_5; then dom tsg = ^ (dom t) by TREES_4:13; then A14: height (dom tsg) = (height (dom t)) + 1 by TREES_3:80; x = <*0*> ^ ((height (dom tsg)) |-> 1) by A8, A9, Th17; hence x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } by A14; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } or x in PostTraversalLanguage nt ) assume x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ; ::_thesis: x in PostTraversalLanguage nt then consider n being Element of NAT such that A15: x = <*0*> ^ (n |-> 1) and A16: n <> 0 ; defpred S2[ Element of NAT ] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PostTraversal tsg = <*0*> ^ ($1 |-> 1) ) ); A17: S2[ 0 ] ; A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_ S2[n_+_1] let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A19: S2[n] ; ::_thesis: S2[n + 1] thus S2[n + 1] ::_thesis: verum proof assume n + 1 <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) ) percases ( n <> 0 or n = 0 ) ; suppose n <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) ) then consider tsg being Element of TS PeanoNat such that tsg . {} = S and A20: PostTraversal tsg = <*0*> ^ (n |-> 1) by A19; PostTraversal tsg = <*0*> ^ ((height (dom tsg)) |-> 1) by Th17; then A21: n |-> 1 = (height (dom tsg)) |-> 1 by A20, FINSEQ_1:33; len (n |-> 1) = n by CARD_1:def_7; then A22: height (dom tsg) = n by A21, CARD_1:def_7; take tsg9 = S -tree tsg; ::_thesis: ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) A23: tsg9 = S -tree <*tsg*> by TREES_4:def_5; height (dom tsg9) = height (^ (dom tsg)) by TREES_4:13 .= n + 1 by A22, TREES_3:80 ; hence ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A23, Th17, TREES_4:def_4; ::_thesis: verum end; supposeA24: n = 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) ) take tsg9 = S -tree rtO; ::_thesis: ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) A25: tsg9 = S -tree <*rtO*> by TREES_4:def_5; height (dom tsg9) = height (^ (dom rtO)) by TREES_4:13 .= (height (dom rtO)) + 1 by TREES_3:80 .= n + 1 by A24, TREES_1:42, TREES_4:3 ; hence ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A25, Th17, TREES_4:def_4; ::_thesis: verum end; end; end; end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A17, A18); then ex tsg being Element of TS PeanoNat st ( tsg . {} = S & PostTraversal tsg = <*0*> ^ (n |-> 1) ) by A16; hence x in PostTraversalLanguage nt by A7, A15; ::_thesis: verum end;