:: BINTREE1 semantic presentation begin definition let D be non empty set ; let t be DecoratedTree of D; func root-label t -> Element of D equals :: BINTREE1:def 1 t . {}; coherence t . {} is Element of D proof reconsider r = {} as Node of t by TREES_1:22; t . r is Element of D ; hence t . {} is Element of D ; ::_thesis: verum end; end; :: deftheorem defines root-label BINTREE1:def_1_:_ for D being non empty set for t being DecoratedTree of D holds root-label t = t . {}; theorem :: BINTREE1:1 for D being non empty set for t being DecoratedTree of D holds roots <*t*> = <*(root-label t)*> by DTCONSTR:4; theorem :: BINTREE1:2 for D being non empty set for t1, t2 being DecoratedTree of D holds roots <*t1,t2*> = <*(root-label t1),(root-label t2)*> by DTCONSTR:6; definition let IT be Tree; attrIT is binary means :Def2: :: BINTREE1:def 2 for t being Element of IT st not t in Leaves IT holds succ t = {(t ^ <*0*>),(t ^ <*1*>)}; end; :: deftheorem Def2 defines binary BINTREE1:def_2_:_ for IT being Tree holds ( IT is binary iff for t being Element of IT st not t in Leaves IT holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ); theorem :: BINTREE1:3 for T being Tree for t being Element of T holds ( succ t = {} iff t in Leaves T ) proof let T be Tree; ::_thesis: for t being Element of T holds ( succ t = {} iff t in Leaves T ) let t be Element of T; ::_thesis: ( succ t = {} iff t in Leaves T ) hereby ::_thesis: ( t in Leaves T implies succ t = {} ) assume succ t = {} ; ::_thesis: t in Leaves T then not t ^ <*0*> in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by TREES_2:def_5; then not t ^ <*0*> in T ; hence t in Leaves T by TREES_1:54; ::_thesis: verum end; set x = the Element of succ t; assume t in Leaves T ; ::_thesis: succ t = {} then A1: not t ^ <*0*> in T by TREES_1:54; assume succ t <> {} ; ::_thesis: contradiction then the Element of succ t in succ t ; then the Element of succ t in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by TREES_2:def_5; then consider n being Element of NAT such that the Element of succ t = t ^ <*n*> and A2: t ^ <*n*> in T ; 0 <= n by NAT_1:2; hence contradiction by A1, A2, TREES_1:def_3; ::_thesis: verum end; registration cluster elementary_tree 0 -> binary ; coherence elementary_tree 0 is binary proof set T = elementary_tree 0; let t be Element of elementary_tree 0; :: according to BINTREE1:def_2 ::_thesis: ( not t in Leaves (elementary_tree 0) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) now__::_thesis:_for_s_being_FinSequence_of_NAT_st_s_in_elementary_tree_0_holds_ not_t_is_a_proper_prefix_of_s let s be FinSequence of NAT ; ::_thesis: ( s in elementary_tree 0 implies not t is_a_proper_prefix_of s ) assume s in elementary_tree 0 ; ::_thesis: not t is_a_proper_prefix_of s then s = {} by TARSKI:def_1, TREES_1:29; hence not t is_a_proper_prefix_of s by TARSKI:def_1, TREES_1:29; ::_thesis: verum end; hence ( not t in Leaves (elementary_tree 0) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) by TREES_1:def_5; ::_thesis: verum end; cluster elementary_tree 2 -> binary ; coherence elementary_tree 2 is binary proof set T = elementary_tree 2; let t be Element of elementary_tree 2; :: according to BINTREE1:def_2 ::_thesis: ( not t in Leaves (elementary_tree 2) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) assume A1: not t in Leaves (elementary_tree 2) ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} percases ( t = {} or t = <*0*> or t = <*1*> ) by ENUMSET1:def_1, MODAL_1:7; supposeA2: t = {} ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} A3: for x being set holds ( x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } iff x in {(t ^ <*0*>),(t ^ <*1*>)} ) proof let x be set ; ::_thesis: ( x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } iff x in {(t ^ <*0*>),(t ^ <*1*>)} ) hereby ::_thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } ) assume x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then A4: ex n being Element of NAT st ( x = t ^ <*n*> & t ^ <*n*> in elementary_tree 2 ) ; then reconsider x9 = x as FinSequence ; percases ( x = {} or x = <*0*> or x = <*1*> ) by A4, ENUMSET1:def_1, MODAL_1:7; suppose x = {} ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} hence x in {(t ^ <*0*>),(t ^ <*1*>)} by A4; ::_thesis: verum end; suppose x = <*0*> ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x9 = t ^ <*0*> by A2, FINSEQ_1:34; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; suppose x = <*1*> ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x9 = t ^ <*1*> by A2, FINSEQ_1:34; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; end; end; assume A5: x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } then reconsider x9 = x as FinSequence by TARSKI:def_2; A6: ( x = t ^ <*0*> or x = t ^ <*1*> ) by A5, TARSKI:def_2; then ( x9 = <*0*> or x9 = <*1*> ) by A2, FINSEQ_1:34; then x9 in elementary_tree 2 by ENUMSET1:def_1, MODAL_1:7; hence x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } by A6; ::_thesis: verum end; succ t = { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in elementary_tree 2 } by TREES_2:def_5; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, TARSKI:1; ::_thesis: verum end; supposeA7: t = <*0*> ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} now__::_thesis:_not_t_^_<*0*>_in_elementary_tree_2 assume A8: t ^ <*0*> in elementary_tree 2 ; ::_thesis: contradiction percases ( t ^ <*0*> = {} or t ^ <*0*> = <*0*> or t ^ <*0*> = <*1*> ) by A8, ENUMSET1:def_1, MODAL_1:7; suppose t ^ <*0*> = {} ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose t ^ <*0*> = <*0*> ; ::_thesis: contradiction then (len <*0*>) + (len <*0*>) = len <*0*> by A7, FINSEQ_1:22; hence contradiction by FINSEQ_1:39; ::_thesis: verum end; suppose t ^ <*0*> = <*1*> ; ::_thesis: contradiction then (len <*0*>) + (len <*0*>) = len <*1*> by A7, FINSEQ_1:22; then 1 + (len <*0*>) = len <*1*> by FINSEQ_1:39; then 1 + 1 = len <*1*> by FINSEQ_1:39; hence contradiction by FINSEQ_1:39; ::_thesis: verum end; end; end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, TREES_1:54; ::_thesis: verum end; supposeA9: t = <*1*> ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} now__::_thesis:_not_t_^_<*0*>_in_elementary_tree_2 assume A10: t ^ <*0*> in elementary_tree 2 ; ::_thesis: contradiction percases ( t ^ <*0*> = {} or t ^ <*0*> = <*0*> or t ^ <*0*> = <*1*> ) by A10, ENUMSET1:def_1, MODAL_1:7; suppose t ^ <*0*> = {} ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose t ^ <*0*> = <*0*> ; ::_thesis: contradiction then (len <*1*>) + (len <*0*>) = len <*0*> by A9, FINSEQ_1:22; hence contradiction by FINSEQ_1:39; ::_thesis: verum end; suppose t ^ <*0*> = <*1*> ; ::_thesis: contradiction then (len <*1*>) + (len <*0*>) = len <*1*> by A9, FINSEQ_1:22; hence contradiction by FINSEQ_1:39; ::_thesis: verum end; end; end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, TREES_1:54; ::_thesis: verum end; end; end; end; theorem :: BINTREE1:4 elementary_tree 0 is binary ; theorem :: BINTREE1:5 elementary_tree 2 is binary ; registration cluster non empty finite Tree-like binary for set ; existence ex b1 being Tree st ( b1 is binary & b1 is finite ) proof take elementary_tree 0 ; ::_thesis: ( elementary_tree 0 is binary & elementary_tree 0 is finite ) thus ( elementary_tree 0 is binary & elementary_tree 0 is finite ) ; ::_thesis: verum end; end; definition let IT be DecoratedTree; attrIT is binary means :Def3: :: BINTREE1:def 3 dom IT is binary ; end; :: deftheorem Def3 defines binary BINTREE1:def_3_:_ for IT being DecoratedTree holds ( IT is binary iff dom IT is binary ); registration let D be non empty set ; cluster Relation-like D -valued Function-like finite DecoratedTree-like binary for set ; existence ex b1 being DecoratedTree of D st ( b1 is binary & b1 is finite ) proof set t = the finite binary Tree; set T = the Function of the finite binary Tree,D; reconsider T = the Function of the finite binary Tree,D as DecoratedTree of D ; take T ; ::_thesis: ( T is binary & T is finite ) thus ( dom T is binary & T is finite ) by FUNCT_2:def_1; :: according to BINTREE1:def_3 ::_thesis: verum end; end; registration cluster Relation-like Function-like finite DecoratedTree-like binary for set ; existence ex b1 being DecoratedTree st ( b1 is binary & b1 is finite ) proof set t = the finite binary DecoratedTree of {{}}; take the finite binary DecoratedTree of {{}} ; ::_thesis: ( the finite binary DecoratedTree of {{}} is binary & the finite binary DecoratedTree of {{}} is finite ) thus ( the finite binary DecoratedTree of {{}} is binary & the finite binary DecoratedTree of {{}} is finite ) ; ::_thesis: verum end; end; registration cluster non empty Tree-like binary -> finite-order for set ; coherence for b1 being Tree st b1 is binary holds b1 is finite-order proof let T be Tree; ::_thesis: ( T is binary implies T is finite-order ) assume A1: T is binary ; ::_thesis: T is finite-order now__::_thesis:_for_t_being_Element_of_T_holds_not_t_^_<*2*>_in_T let t be Element of T; ::_thesis: not t ^ <*2*> in T assume A2: t ^ <*2*> in T ; ::_thesis: contradiction then A3: t ^ <*0*> in T by TREES_1:def_3; percases ( t in Leaves T or not t in Leaves T ) ; suppose t in Leaves T ; ::_thesis: contradiction hence contradiction by A3, TREES_1:54; ::_thesis: verum end; supposeA4: not t in Leaves T ; ::_thesis: contradiction A5: now__::_thesis:_not_<*2*>_=_<*0*> A6: <*2*> . 1 = 2 by FINSEQ_1:40; assume <*2*> = <*0*> ; ::_thesis: contradiction hence contradiction by A6, FINSEQ_1:40; ::_thesis: verum end; A7: now__::_thesis:_not_<*2*>_=_<*1*> A8: <*2*> . 1 = 2 by FINSEQ_1:40; assume <*2*> = <*1*> ; ::_thesis: contradiction hence contradiction by A8, FINSEQ_1:40; ::_thesis: verum end; t ^ <*2*> in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by A2; then A9: t ^ <*2*> in succ t by TREES_2:def_5; succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, A4, Def2; then ( t ^ <*2*> = t ^ <*0*> or t ^ <*2*> = t ^ <*1*> ) by A9, TARSKI:def_2; hence contradiction by A5, A7, FINSEQ_1:33; ::_thesis: verum end; end; end; hence T is finite-order by TREES_2:def_2; ::_thesis: verum end; end; theorem Th6: :: BINTREE1:6 for T0, T1 being Tree for t being Element of tree (T0,T1) holds ( ( for p being Element of T0 st t = <*0*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) ) proof let T0, T1 be Tree; ::_thesis: for t being Element of tree (T0,T1) holds ( ( for p being Element of T0 st t = <*0*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) ) let t be Element of tree (T0,T1); ::_thesis: ( ( for p being Element of T0 st t = <*0*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) ) set RT = tree (T0,T1); hereby ::_thesis: for p being Element of T1 st t = <*1*> ^ p holds ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) let p be Element of T0; ::_thesis: ( t = <*0*> ^ p implies ( ( t in Leaves (tree (T0,T1)) implies p in Leaves T0 ) & ( p in Leaves T0 implies t in Leaves (tree (T0,T1)) ) ) ) assume A1: t = <*0*> ^ p ; ::_thesis: ( ( t in Leaves (tree (T0,T1)) implies p in Leaves T0 ) & ( p in Leaves T0 implies t in Leaves (tree (T0,T1)) ) ) hereby ::_thesis: ( p in Leaves T0 implies t in Leaves (tree (T0,T1)) ) assume A2: t in Leaves (tree (T0,T1)) ; ::_thesis: p in Leaves T0 assume not p in Leaves T0 ; ::_thesis: contradiction then consider n being Element of NAT such that A3: p ^ <*n*> in T0 by TREES_1:55; <*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A3, TREES_3:69; then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32; hence contradiction by A1, A2, TREES_1:55; ::_thesis: verum end; assume A4: p in Leaves T0 ; ::_thesis: t in Leaves (tree (T0,T1)) assume not t in Leaves (tree (T0,T1)) ; ::_thesis: contradiction then consider n being Element of NAT such that A5: t ^ <*n*> in tree (T0,T1) by TREES_1:55; <*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A1, A5, FINSEQ_1:32; then p ^ <*n*> in T0 by TREES_3:69; hence contradiction by A4, TREES_1:55; ::_thesis: verum end; let p be Element of T1; ::_thesis: ( t = <*1*> ^ p implies ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) assume A6: t = <*1*> ^ p ; ::_thesis: ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) hereby ::_thesis: ( p in Leaves T1 implies t in Leaves (tree (T0,T1)) ) assume A7: t in Leaves (tree (T0,T1)) ; ::_thesis: p in Leaves T1 assume not p in Leaves T1 ; ::_thesis: contradiction then consider n being Element of NAT such that A8: p ^ <*n*> in T1 by TREES_1:55; <*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, TREES_3:70; then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32; hence contradiction by A6, A7, TREES_1:55; ::_thesis: verum end; assume A9: p in Leaves T1 ; ::_thesis: t in Leaves (tree (T0,T1)) assume not t in Leaves (tree (T0,T1)) ; ::_thesis: contradiction then consider n being Element of NAT such that A10: t ^ <*n*> in tree (T0,T1) by TREES_1:55; <*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A6, A10, FINSEQ_1:32; then p ^ <*n*> in T1 by TREES_3:70; hence contradiction by A9, TREES_1:55; ::_thesis: verum end; theorem Th7: :: BINTREE1:7 for T0, T1 being Tree for t being Element of tree (T0,T1) holds ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) ) ) proof let T0, T1 be Tree; ::_thesis: for t being Element of tree (T0,T1) holds ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) ) ) let t be Element of tree (T0,T1); ::_thesis: ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) ) ) set RT = tree (T0,T1); hereby ::_thesis: ( ( for p being Element of T0 st t = <*0*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) ) ) assume A1: t = {} ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} ( {} in T1 & <*1*> = <*1*> ^ {} ) by FINSEQ_1:34, TREES_1:22; then <*1*> in tree (T0,T1) by TREES_3:68; then A2: t ^ <*1*> in tree (T0,T1) by A1, FINSEQ_1:34; A3: succ t = { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in tree (T0,T1) } by TREES_2:def_5; ( {} in T0 & <*0*> = <*0*> ^ {} ) by FINSEQ_1:34, TREES_1:22; then <*0*> in tree (T0,T1) by TREES_3:68; then A4: t ^ <*0*> in tree (T0,T1) by A1, FINSEQ_1:34; now__::_thesis:_for_x1_being_set_holds_ (_(_x1_in_succ_t_implies_x1_in_{(t_^_<*0*>),(t_^_<*1*>)}_)_&_(_x1_in_{(t_^_<*0*>),(t_^_<*1*>)}_implies_x1_in_succ_t_)_) let x1 be set ; ::_thesis: ( ( x1 in succ t implies x1 in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x1 in {(t ^ <*0*>),(t ^ <*1*>)} implies x1 in succ t ) ) hereby ::_thesis: ( x1 in {(t ^ <*0*>),(t ^ <*1*>)} implies x1 in succ t ) assume x1 in succ t ; ::_thesis: x1 in {(t ^ <*0*>),(t ^ <*1*>)} then consider n being Element of NAT such that A5: x1 = t ^ <*n*> and A6: t ^ <*n*> in tree (T0,T1) by A3; reconsider x = x1 as FinSequence by A5; ex p being FinSequence st ( ( p in T0 & x = <*0*> ^ p ) or ( p in T1 & x = <*1*> ^ p ) ) by A5, A6, TREES_3:68; then A7: ( x . 1 = 0 or x . 1 = 1 ) by FINSEQ_1:41; x1 = <*n*> by A1, A5, FINSEQ_1:34; then ( x = <*0*> or x = <*1*> ) by A7, FINSEQ_1:40; then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A1, FINSEQ_1:34; hence x1 in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; assume x1 in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x1 in succ t then ( x1 = t ^ <*0*> or x1 = t ^ <*1*> ) by TARSKI:def_2; hence x1 in succ t by A3, A4, A2; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:1; ::_thesis: verum end; hereby ::_thesis: for p being Element of T1 st t = <*1*> ^ p holds for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) let p be Element of T0; ::_thesis: ( t = <*0*> ^ p implies for sp being FinSequence holds ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) ) assume A8: t = <*0*> ^ p ; ::_thesis: for sp being FinSequence holds ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) let sp be FinSequence; ::_thesis: ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) hereby ::_thesis: ( <*0*> ^ sp in succ t implies sp in succ p ) assume sp in succ p ; ::_thesis: <*0*> ^ sp in succ t then sp in { (p ^ <*n*>) where n is Element of NAT : p ^ <*n*> in T0 } by TREES_2:def_5; then consider n being Element of NAT such that A9: sp = p ^ <*n*> and A10: p ^ <*n*> in T0 ; <*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A10, TREES_3:69; then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32; then t ^ <*n*> in { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in tree (T0,T1) } by A8; then t ^ <*n*> in succ t by TREES_2:def_5; hence <*0*> ^ sp in succ t by A8, A9, FINSEQ_1:32; ::_thesis: verum end; set zsp = <*0*> ^ sp; assume <*0*> ^ sp in succ t ; ::_thesis: sp in succ p then <*0*> ^ sp in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in tree (T0,T1) } by TREES_2:def_5; then consider n being Element of NAT such that A11: <*0*> ^ sp = t ^ <*n*> and A12: t ^ <*n*> in tree (T0,T1) ; <*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, A12, FINSEQ_1:32; then p ^ <*n*> in T0 by TREES_3:69; then p ^ <*n*> in { (p ^ <*k*>) where k is Element of NAT : p ^ <*k*> in T0 } ; then A13: p ^ <*n*> in succ p by TREES_2:def_5; <*0*> ^ sp = <*0*> ^ (p ^ <*n*>) by A8, A11, FINSEQ_1:32; hence sp in succ p by A13, FINSEQ_1:33; ::_thesis: verum end; let p be Element of T1; ::_thesis: ( t = <*1*> ^ p implies for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) ) assume A14: t = <*1*> ^ p ; ::_thesis: for sp being FinSequence holds ( sp in succ p iff <*1*> ^ sp in succ t ) let sp be FinSequence; ::_thesis: ( sp in succ p iff <*1*> ^ sp in succ t ) hereby ::_thesis: ( <*1*> ^ sp in succ t implies sp in succ p ) assume sp in succ p ; ::_thesis: <*1*> ^ sp in succ t then sp in { (p ^ <*n*>) where n is Element of NAT : p ^ <*n*> in T1 } by TREES_2:def_5; then consider n being Element of NAT such that A15: sp = p ^ <*n*> and A16: p ^ <*n*> in T1 ; <*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A16, TREES_3:70; then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32; then t ^ <*n*> in { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in tree (T0,T1) } by A14; then t ^ <*n*> in succ t by TREES_2:def_5; hence <*1*> ^ sp in succ t by A14, A15, FINSEQ_1:32; ::_thesis: verum end; set zsp = <*1*> ^ sp; assume <*1*> ^ sp in succ t ; ::_thesis: sp in succ p then <*1*> ^ sp in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in tree (T0,T1) } by TREES_2:def_5; then consider n being Element of NAT such that A17: <*1*> ^ sp = t ^ <*n*> and A18: t ^ <*n*> in tree (T0,T1) ; <*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A14, A18, FINSEQ_1:32; then p ^ <*n*> in T1 by TREES_3:70; then p ^ <*n*> in { (p ^ <*k*>) where k is Element of NAT : p ^ <*k*> in T1 } ; then A19: p ^ <*n*> in succ p by TREES_2:def_5; <*1*> ^ sp = <*1*> ^ (p ^ <*n*>) by A14, A17, FINSEQ_1:32; hence sp in succ p by A19, FINSEQ_1:33; ::_thesis: verum end; theorem Th8: :: BINTREE1:8 for T1, T2 being Tree holds ( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary ) proof let T1, T2 be Tree; ::_thesis: ( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary ) set RT = tree (T1,T2); hereby ::_thesis: ( tree (T1,T2) is binary implies ( T1 is binary & T2 is binary ) ) assume that A1: T1 is binary and A2: T2 is binary ; ::_thesis: tree (T1,T2) is binary now__::_thesis:_for_t_being_Element_of_tree_(T1,T2)_st_not_t_in_Leaves_(tree_(T1,T2))_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of tree (T1,T2); ::_thesis: ( not t in Leaves (tree (T1,T2)) implies succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} ) assume A3: not t in Leaves (tree (T1,T2)) ; ::_thesis: succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} percases ( t = {} or ex p being FinSequence st ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ) by TREES_3:68; suppose t = {} ; ::_thesis: succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by Th7; ::_thesis: verum end; suppose ex p being FinSequence st ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; ::_thesis: succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)} then consider p being FinSequence such that A4: ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; A5: now__::_thesis:_(_p_in_T2_&_t_=_<*1*>_^_p_implies_succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)}_) assume that A6: p in T2 and A7: t = <*1*> ^ p ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} reconsider p = p as Element of T2 by A6; percases ( p in Leaves T2 or not p in Leaves T2 ) ; suppose p in Leaves T2 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, A7, Th6; ::_thesis: verum end; suppose not p in Leaves T2 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} then A8: succ p = {(p ^ <*0*>),(p ^ <*1*>)} by A2, Def2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_t_implies_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_)_&_(_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_implies_x_in_succ_t_)_) let x be set ; ::_thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) ) hereby ::_thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) assume A9: x in succ t ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in tree (T1,T2) } by TREES_2:def_5; then consider n being Element of NAT such that A10: x = t ^ <*n*> and A11: t ^ <*n*> in tree (T1,T2) ; A12: x = <*1*> ^ (p ^ <*n*>) by A7, A10, FINSEQ_1:32; then reconsider pn = p ^ <*n*> as Element of T2 by A10, A11, TREES_3:70; pn in succ p by A7, A9, A12, Th7; then ( pn = p ^ <*0*> or pn = p ^ <*1*> ) by A8, TARSKI:def_2; then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A10, FINSEQ_1:33; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in succ t then ( x = (<*1*> ^ p) ^ <*0*> or x = (<*1*> ^ p) ^ <*1*> ) by A7, TARSKI:def_2; then A13: ( x = <*1*> ^ (p ^ <*0*>) or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:32; ( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A8, TARSKI:def_2; hence x in succ t by A7, A13, Th7; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:1; ::_thesis: verum end; end; end; now__::_thesis:_(_p_in_T1_&_t_=_<*0*>_^_p_implies_succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)}_) assume that A14: p in T1 and A15: t = <*0*> ^ p ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} reconsider p = p as Element of T1 by A14; percases ( p in Leaves T1 or not p in Leaves T1 ) ; suppose p in Leaves T1 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, A15, Th6; ::_thesis: verum end; suppose not p in Leaves T1 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} then A16: succ p = {(p ^ <*0*>),(p ^ <*1*>)} by A1, Def2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_t_implies_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_)_&_(_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_implies_x_in_succ_t_)_) let x be set ; ::_thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) ) hereby ::_thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) assume A17: x in succ t ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in tree (T1,T2) } by TREES_2:def_5; then consider n being Element of NAT such that A18: x = t ^ <*n*> and A19: t ^ <*n*> in tree (T1,T2) ; A20: x = <*0*> ^ (p ^ <*n*>) by A15, A18, FINSEQ_1:32; then reconsider pn = p ^ <*n*> as Element of T1 by A18, A19, TREES_3:69; pn in succ p by A15, A17, A20, Th7; then ( pn = p ^ <*0*> or pn = p ^ <*1*> ) by A16, TARSKI:def_2; then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A18, FINSEQ_1:33; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in succ t then ( x = (<*0*> ^ p) ^ <*0*> or x = (<*0*> ^ p) ^ <*1*> ) by A15, TARSKI:def_2; then A21: ( x = <*0*> ^ (p ^ <*0*>) or x = <*0*> ^ (p ^ <*1*>) ) by FINSEQ_1:32; ( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A16, TARSKI:def_2; hence x in succ t by A15, A21, Th7; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:1; ::_thesis: verum end; end; end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A4, A5; ::_thesis: verum end; end; end; hence tree (T1,T2) is binary by Def2; ::_thesis: verum end; assume A22: tree (T1,T2) is binary ; ::_thesis: ( T1 is binary & T2 is binary ) now__::_thesis:_for_t_being_Element_of_T1_st_not_t_in_Leaves_T1_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of T1; ::_thesis: ( not t in Leaves T1 implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) reconsider zt = <*0*> ^ t as Element of tree (T1,T2) by TREES_3:69; assume not t in Leaves T1 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} then not zt in Leaves (tree (T1,T2)) by Th6; then A23: succ zt = {((<*0*> ^ t) ^ <*0*>),((<*0*> ^ t) ^ <*1*>)} by A22, Def2; A24: succ zt = { (zt ^ <*n*>) where n is Element of NAT : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def_5; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_t_implies_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_)_&_(_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_implies_x_in_succ_t_)_) let x be set ; ::_thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) ) hereby ::_thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) assume x in succ t ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T1 } by TREES_2:def_5; then consider n being Element of NAT such that A25: x = t ^ <*n*> and A26: t ^ <*n*> in T1 ; <*0*> ^ (t ^ <*n*>) in tree (T1,T2) by A26, TREES_3:69; then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32; then zt ^ <*n*> in { (zt ^ <*k*>) where k is Element of NAT : zt ^ <*k*> in tree (T1,T2) } ; then ( zt ^ <*n*> = zt ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A23, A24, TARSKI:def_2; then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A25, FINSEQ_1:33; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in succ t then A27: ( x = t ^ <*0*> or x = t ^ <*1*> ) by TARSKI:def_2; (<*0*> ^ t) ^ <*1*> in succ zt by A23, TARSKI:def_2; then A28: <*0*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32; (<*0*> ^ t) ^ <*0*> in succ zt by A23, TARSKI:def_2; then <*0*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32; hence x in succ t by A27, A28, Th7; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:1; ::_thesis: verum end; hence T1 is binary by Def2; ::_thesis: T2 is binary now__::_thesis:_for_t_being_Element_of_T2_st_not_t_in_Leaves_T2_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of T2; ::_thesis: ( not t in Leaves T2 implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) reconsider zt = <*1*> ^ t as Element of tree (T1,T2) by TREES_3:70; assume not t in Leaves T2 ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} then not zt in Leaves (tree (T1,T2)) by Th6; then A29: succ zt = {((<*1*> ^ t) ^ <*0*>),((<*1*> ^ t) ^ <*1*>)} by A22, Def2; A30: succ zt = { (zt ^ <*n*>) where n is Element of NAT : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def_5; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_t_implies_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_)_&_(_x_in_{(t_^_<*0*>),(t_^_<*1*>)}_implies_x_in_succ_t_)_) let x be set ; ::_thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) ) hereby ::_thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) assume x in succ t ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T2 } by TREES_2:def_5; then consider n being Element of NAT such that A31: x = t ^ <*n*> and A32: t ^ <*n*> in T2 ; <*1*> ^ (t ^ <*n*>) in tree (T1,T2) by A32, TREES_3:70; then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32; then zt ^ <*n*> in { (zt ^ <*k*>) where k is Element of NAT : zt ^ <*k*> in tree (T1,T2) } ; then ( zt ^ <*n*> = zt ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A29, A30, TARSKI:def_2; then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A31, FINSEQ_1:33; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def_2; ::_thesis: verum end; assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in succ t then A33: ( x = t ^ <*0*> or x = t ^ <*1*> ) by TARSKI:def_2; (<*1*> ^ t) ^ <*1*> in succ zt by A29, TARSKI:def_2; then A34: <*1*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32; (<*1*> ^ t) ^ <*0*> in succ zt by A29, TARSKI:def_2; then <*1*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32; hence x in succ t by A33, A34, Th7; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:1; ::_thesis: verum end; hence T2 is binary by Def2; ::_thesis: verum end; theorem Th9: :: BINTREE1:9 for T1, T2 being DecoratedTree for x being set holds ( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary ) proof let T1, T2 be DecoratedTree; ::_thesis: for x being set holds ( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary ) let x be set ; ::_thesis: ( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary ) hereby ::_thesis: ( x -tree (T1,T2) is binary implies ( T1 is binary & T2 is binary ) ) assume ( T1 is binary & T2 is binary ) ; ::_thesis: x -tree (T1,T2) is binary then ( dom T1 is binary & dom T2 is binary ) by Def3; then A1: tree ((dom T1),(dom T2)) is binary by Th8; dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_4:14; hence x -tree (T1,T2) is binary by A1, Def3; ::_thesis: verum end; assume x -tree (T1,T2) is binary ; ::_thesis: ( T1 is binary & T2 is binary ) then A2: dom (x -tree (T1,T2)) is binary by Def3; dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_4:14; then ( dom T1 is binary & dom T2 is binary ) by A2, Th8; hence ( T1 is binary & T2 is binary ) by Def3; ::_thesis: verum end; registration let D be non empty set ; let x be Element of D; let T1, T2 be finite binary DecoratedTree of D; clusterx -tree (T1,T2) -> D -valued finite binary ; coherence ( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued ) proof set t1t2 = <*T1,T2*>; dom T1 is finite ; then A1: T1 in FinTrees D by TREES_3:def_8; dom T2 is finite ; then A2: T2 in FinTrees D by TREES_3:def_8; rng <*T1,T2*> = rng (<*T1*> ^ <*T2*>) by FINSEQ_1:def_9 .= (rng <*T1*>) \/ (rng <*T2*>) by FINSEQ_1:31 .= {T1} \/ (rng <*T2*>) by FINSEQ_1:39 .= {T1} \/ {T2} by FINSEQ_1:39 .= {T1,T2} by ENUMSET1:1 ; then for x being set st x in rng <*T1,T2*> holds x in FinTrees D by A1, A2, TARSKI:def_2; then rng <*T1,T2*> c= FinTrees D by TARSKI:def_3; then reconsider T1T2 = <*T1,T2*> as FinSequence of FinTrees D by FINSEQ_1:def_4; x -tree (T1,T2) = x -tree T1T2 by TREES_4:def_6; then dom (x -tree (T1,T2)) is finite ; hence ( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued ) by Th9, FINSET_1:10; ::_thesis: verum end; end; definition let IT be non empty DTConstrStr ; attrIT is binary means :Def4: :: BINTREE1:def 4 for s being Symbol of IT for p being FinSequence st s ==> p holds ex x1, x2 being Symbol of IT st p = <*x1,x2*>; end; :: deftheorem Def4 defines binary BINTREE1:def_4_:_ for IT being non empty DTConstrStr holds ( IT is binary iff for s being Symbol of IT for p being FinSequence st s ==> p holds ex x1, x2 being Symbol of IT st p = <*x1,x2*> ); registration cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals binary for DTConstrStr ; existence ex b1 being non empty DTConstrStr st ( b1 is binary & b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict ) proof reconsider 01 = {0,1} as non empty set ; reconsider a90 = 0 , a91 = 1 as Element of 01 by TARSKI:def_2; reconsider a9119 = <*a91*> ^ <*a91*> as Element of 01 * ; reconsider P = {[a90,a9119]} as Relation of 01,(01 *) by RELSET_1:3; take cherry = DTConstrStr(# 01,P #); ::_thesis: ( cherry is binary & cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict ) reconsider a90 = a90, a91 = a91 as Symbol of cherry ; hereby :: according to BINTREE1:def_4 ::_thesis: ( cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict ) let s be Symbol of cherry; ::_thesis: for p being FinSequence st s ==> p holds ex x1, x2 being Symbol of cherry st p = <*x1,x2*> let p be FinSequence; ::_thesis: ( s ==> p implies ex x1, x2 being Symbol of cherry st p = <*x1,x2*> ) assume A1: s ==> p ; ::_thesis: ex x1, x2 being Symbol of cherry st p = <*x1,x2*> take x1 = a91; ::_thesis: ex x2 being Symbol of cherry st p = <*x1,x2*> take x2 = a91; ::_thesis: p = <*x1,x2*> [s,p] in P by A1, LANG1:def_1; then [s,p] = [0,a9119] by TARSKI:def_1; then p = a9119 by XTUPLE_0:1 .= <*1,1*> by FINSEQ_1:def_9 ; hence p = <*x1,x2*> ; ::_thesis: verum end; now__::_thesis:_for_s_being_FinSequence_holds_not_a91_==>_s let s be FinSequence; ::_thesis: not a91 ==> s assume a91 ==> s ; ::_thesis: contradiction then [1,s] in P by LANG1:def_1; then [1,s] = [0,a9119] by TARSKI:def_1; hence contradiction by XTUPLE_0:1; ::_thesis: verum end; then A2: a91 in { t where t is Symbol of cherry : for s being FinSequence holds not t ==> s } ; then A3: a91 in Terminals cherry by LANG1:def_2; thus Terminals cherry <> {} by A2, LANG1:def_2; :: according to DTCONSTR:def_3 ::_thesis: ( cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict ) [a90,a9119] in P by TARSKI:def_1; then a90 ==> a9119 by LANG1:def_1; then a90 in { t where t is Symbol of cherry : ex s being FinSequence st t ==> s } ; hence NonTerminals cherry <> {} by LANG1:def_3; :: according to DTCONSTR:def_4 ::_thesis: ( cherry is with_useful_nonterminals & cherry is strict ) A4: { s where s is Symbol of cherry : ex p being FinSequence st s ==> p } = NonTerminals cherry by LANG1:def_3; hereby :: according to DTCONSTR:def_5 ::_thesis: cherry is strict reconsider X = TS cherry as non empty set by A3, DTCONSTR:def_1; let nt be Symbol of cherry; ::_thesis: ( nt in NonTerminals cherry implies ex q9 being FinSequence of TS cherry st nt ==> roots q9 ) reconsider rt1 = root-tree a91 as Element of X by A3, DTCONSTR:def_1; reconsider q = <*rt1*> ^ <*rt1*> as FinSequence of TS cherry ; q = <*(root-tree 1),(root-tree 1)*> by FINSEQ_1:def_9; then A5: roots q = <*((root-tree a91) . {}),((root-tree a91) . {})*> by DTCONSTR:6; assume nt in NonTerminals cherry ; ::_thesis: ex q9 being FinSequence of TS cherry st nt ==> roots q9 then ex s being Symbol of cherry st ( nt = s & ex p being FinSequence st s ==> p ) by A4; then consider p being FinSequence such that A6: nt ==> p ; take q9 = q; ::_thesis: nt ==> roots q9 [nt,p] in P by A6, LANG1:def_1; then A7: [nt,p] = [0,a9119] by TARSKI:def_1; ( a9119 = <*1,1*> & (root-tree 1) . {} = 1 ) by FINSEQ_1:def_9, TREES_4:3; hence nt ==> roots q9 by A6, A7, A5, XTUPLE_0:1; ::_thesis: verum end; thus cherry is strict ; ::_thesis: verum end; end; scheme :: BINTREE1:sch 1 BinDTConstrStrEx{ F1() -> non empty set , P1[ set , set , set ] } : ex G being non empty strict binary DTConstrStr st ( the carrier of G = F1() & ( for x, y, z being Symbol of G holds ( x ==> <*y,z*> iff P1[x,y,z] ) ) ) proof defpred S1[ set , FinSequence] means ( P1[$1,$2 . 1,$2 . 2] & $2 = <*($2 . 1),($2 . 2)*> ); consider G being non empty strict DTConstrStr such that A1: the carrier of G = F1() and A2: 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(); now__::_thesis:_for_s_being_Symbol_of_G for_p_being_FinSequence_st_s_==>_p_holds_ ex_pp1,_pp2_being_Symbol_of_G_st_p_=_<*pp1,pp2*> let s be Symbol of G; ::_thesis: for p being FinSequence st s ==> p holds ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> let p be FinSequence; ::_thesis: ( s ==> p implies ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> ) assume A3: s ==> p ; ::_thesis: ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> then [s,p] in the Rules of G by LANG1:def_1; then p in the carrier of G * by ZFMISC_1:87; then reconsider pp = p as FinSequence of the carrier of G by FINSEQ_2:def_3; pp = <*(pp . 1),(pp . 2)*> by A2, A3; then rng pp = rng (<*(pp . 1)*> ^ <*(pp . 2)*>) by FINSEQ_1:def_9 .= (rng <*(pp . 1)*>) \/ (rng <*(pp . 2)*>) by FINSEQ_1:31 .= {(pp . 1)} \/ (rng <*(pp . 2)*>) by FINSEQ_1:39 .= {(pp . 1)} \/ {(pp . 2)} by FINSEQ_1:39 .= {(pp . 1),(pp . 2)} by ENUMSET1:1 ; then ( pp . 1 in rng pp & pp . 2 in rng pp ) by TARSKI:def_2; then reconsider pp1 = pp . 1, pp2 = pp . 2 as Symbol of G ; take pp1 = pp1; ::_thesis: ex pp2 being Symbol of G st p = <*pp1,pp2*> take pp2 = pp2; ::_thesis: p = <*pp1,pp2*> thus p = <*pp1,pp2*> by A2, A3; ::_thesis: verum end; then A4: G is binary by Def4; now__::_thesis:_for_x,_y,_z_being_Symbol_of_G_holds_ (_x_==>_<*y,z*>_iff_P1[x,y,z]_) let x, y, z be Symbol of G; ::_thesis: ( x ==> <*y,z*> iff P1[x,y,z] ) reconsider yz = <*y,z*> as FinSequence of the carrier of G ; ( yz . 1 = y & yz . 2 = z ) by FINSEQ_1:44; hence ( x ==> <*y,z*> iff P1[x,y,z] ) by A2; ::_thesis: verum end; hence ex G being non empty strict binary DTConstrStr st ( the carrier of G = F1() & ( for x, y, z being Symbol of G holds ( x ==> <*y,z*> iff P1[x,y,z] ) ) ) by A1, A4; ::_thesis: verum end; theorem Th10: :: BINTREE1:10 for G being non empty with_terminals with_nonterminals binary DTConstrStr for ts being FinSequence of TS G for nt being Symbol of G st nt ==> roots ts holds ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) proof let G be non empty with_terminals with_nonterminals binary DTConstrStr ; ::_thesis: for ts being FinSequence of TS G for nt being Symbol of G st nt ==> roots ts holds ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) let ts be FinSequence of TS G; ::_thesis: for nt being Symbol of G st nt ==> roots ts holds ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) let nt be Symbol of G; ::_thesis: ( nt ==> roots ts implies ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) ) assume A1: nt ==> roots ts ; ::_thesis: ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) then consider rtl, rtr being Symbol of G such that A2: roots ts = <*rtl,rtr*> by Def4; nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } by A1; hence nt is NonTerminal of G by LANG1:def_3; ::_thesis: ( dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) A3: len <*rtl,rtr*> = 2 by FINSEQ_1:44; A4: dom <*rtl,rtr*> = dom ts by A2, TREES_3:def_18; hence dom ts = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def_3; ::_thesis: ( 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) hence A5: ( 1 in dom ts & 2 in dom ts ) by TARSKI:def_2; ::_thesis: ex tl, tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) then consider tl being DecoratedTree such that A6: tl = ts . 1 and A7: <*rtl,rtr*> . 1 = tl . {} by A2, TREES_3:def_18; A8: ( rng ts c= TS G & tl in rng ts ) by A5, A6, FINSEQ_1:def_4, FUNCT_1:def_3; consider tr being DecoratedTree such that A9: tr = ts . 2 and A10: <*rtl,rtr*> . 2 = tr . {} by A2, A5, TREES_3:def_18; tr in rng ts by A5, A9, FUNCT_1:def_3; then reconsider tl = tl, tr = tr as Element of TS G by A8; take tl ; ::_thesis: ex tr being Element of TS G st ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) take tr ; ::_thesis: ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) <*rtl,rtr*> . 1 = rtl by FINSEQ_1:44; hence roots ts = <*(root-label tl),(root-label tr)*> by A2, A7, A10, FINSEQ_1:44; ::_thesis: ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def_3 .= Seg (len ts) by A4, FINSEQ_1:def_3 ; then len ts = 2 by A3, FINSEQ_1:6; then ts = <*tl,tr*> by A6, A9, FINSEQ_1:44; hence ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) ) by A6, A9, TREES_4:def_6; ::_thesis: ( tl in rng ts & tr in rng ts ) thus ( tl in rng ts & tr in rng ts ) by A5, A6, A9, FUNCT_1:def_3; ::_thesis: verum end; scheme :: BINTREE1:sch 2 BinDTConstrInd{ F1() -> non empty with_terminals with_nonterminals binary DTConstrStr , P1[ set ] } : for t being Element of TS F1() holds P1[t] provided A1: for s being Terminal of F1() holds P1[ root-tree s] and A2: for nt being NonTerminal of F1() for tl, tr being Element of TS F1() st nt ==> <*(root-label tl),(root-label tr)*> & P1[tl] & P1[tr] holds P1[nt -tree (tl,tr)] proof A3: 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 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 P1[t] ) holds P1[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 P1[t] ) implies P1[nt -tree ts] ) assume that A4: nt ==> roots ts and A5: for t being DecoratedTree of the carrier of F1() st t in rng ts holds P1[t] ; ::_thesis: P1[nt -tree ts] A6: nt is NonTerminal of F1() by A4, Th10; consider tl, tr being Element of TS F1() such that A7: roots ts = <*(root-label tl),(root-label tr)*> and tl = ts . 1 and tr = ts . 2 and A8: nt -tree ts = nt -tree (tl,tr) and A9: ( tl in rng ts & tr in rng ts ) by A4, Th10; ( P1[tl] & P1[tr] ) by A5, A9; hence P1[nt -tree ts] by A2, A4, A6, A7, A8; ::_thesis: verum end; A10: for s being Symbol of F1() st s in Terminals F1() holds P1[ root-tree s] by A1; for t being DecoratedTree of the carrier of F1() st t in TS F1() holds P1[t] from DTCONSTR:sch_7(A10, A3); hence for t being Element of TS F1() holds P1[t] ; ::_thesis: verum end; scheme :: BINTREE1:sch 3 BinDTConstrIndDef{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set , set , set ) -> Element of F2() } : ex f being Function of (TS F1()),F2() st ( ( for t being Terminal of F1() holds f . (root-tree t) = F3(t) ) & ( for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) ) proof deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F4($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2)); consider f being Function of (TS F1()),F2() such that A1: for t being Symbol of F1() st t in Terminals F1() holds f . (root-tree t) = F3(t) and A2: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds f . (nt -tree ts) = H1(nt, roots ts,f * ts) from DTCONSTR:sch_8(); take f ; ::_thesis: ( ( for t being Terminal of F1() holds f . (root-tree t) = F3(t) ) & ( for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) ) thus for t being Terminal of F1() holds f . (root-tree t) = F3(t) by A1; ::_thesis: for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) let nt be NonTerminal of F1(); ::_thesis: for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) let tl, tr be Element of TS F1(); ::_thesis: for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) let rtl, rtr be Symbol of F1(); ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) assume that A3: rtl = root-label tl and A4: rtr = root-label tr and A5: nt ==> <*rtl,rtr*> ; ::_thesis: for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) reconsider rts = <*rtl,rtr*> as FinSequence ; reconsider ts = <*tl,tr*> as FinSequence of TS F1() ; A6: ts . 1 = tl by FINSEQ_1:44; let xl, xr be Element of F2(); ::_thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) A7: dom ts = {1,2} by FINSEQ_1:2, FINSEQ_1:89; reconsider x = <*xl,xr*> as FinSequence of F2() ; A8: dom x = {1,2} by FINSEQ_1:2, FINSEQ_1:89; A9: ts . 2 = tr by FINSEQ_1:44; A10: dom f = TS F1() by FUNCT_2:def_1; A11: now__::_thesis:_for_y_being_set_holds_ (_y_in_dom_x_iff_(_y_in_dom_ts_&_ts_._y_in_dom_f_)_) let y be set ; ::_thesis: ( y in dom x iff ( y in dom ts & ts . y in dom f ) ) A12: now__::_thesis:_(_y_in_dom_ts_&_ts_._y_in_dom_f_implies_y_in_dom_x_) assume that A13: y in dom ts and ts . y in dom f ; ::_thesis: y in dom x percases ( y = 1 or y = 2 ) by A7, A13, TARSKI:def_2; suppose y = 1 ; ::_thesis: y in dom x hence y in dom x by A8, TARSKI:def_2; ::_thesis: verum end; suppose y = 2 ; ::_thesis: y in dom x hence y in dom x by A8, TARSKI:def_2; ::_thesis: verum end; end; end; now__::_thesis:_(_y_in_dom_x_implies_(_y_in_dom_ts_&_ts_._y_in_dom_f_)_) assume A14: y in dom x ; ::_thesis: ( y in dom ts & ts . y in dom f ) percases ( y = 1 or y = 2 ) by A8, A14, TARSKI:def_2; suppose y = 1 ; ::_thesis: ( y in dom ts & ts . y in dom f ) hence ( y in dom ts & ts . y in dom f ) by A10, A6, A7, TARSKI:def_2; ::_thesis: verum end; suppose y = 2 ; ::_thesis: ( y in dom ts & ts . y in dom f ) hence ( y in dom ts & ts . y in dom f ) by A10, A9, A7, TARSKI:def_2; ::_thesis: verum end; end; end; hence ( y in dom x iff ( y in dom ts & ts . y in dom f ) ) by A12; ::_thesis: verum end; assume A15: ( xl = f . tl & xr = f . tr ) ; ::_thesis: f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) now__::_thesis:_for_y_being_set_st_y_in_dom_x_holds_ x_._y_=_f_._(ts_._y) let y be set ; ::_thesis: ( y in dom x implies x . y = f . (ts . y) ) assume y in dom x ; ::_thesis: x . y = f . (ts . y) then ( y = 1 or y = 2 ) by A8, TARSKI:def_2; hence x . y = f . (ts . y) by A15, A6, A9, FINSEQ_1:44; ::_thesis: verum end; then A16: x = f * ts by A11, FUNCT_1:10; A17: rts . 2 = rtr by FINSEQ_1:44; A18: rts . 1 = rtl by FINSEQ_1:44; A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_ts_holds_ ex_T_being_DecoratedTree_st_ (_T_=_ts_._i_&_rts_._i_=_T_._{}_) let i be Element of NAT ; ::_thesis: ( i in dom ts implies ex T being DecoratedTree st ( b2 = ts . T & rts . T = b2 . {} ) ) assume i in dom ts ; ::_thesis: ex T being DecoratedTree st ( b2 = ts . T & rts . T = b2 . {} ) then i in Seg (len ts) by FINSEQ_1:def_3; then A20: i in Seg 2 by FINSEQ_1:44; percases ( i = 1 or i = 2 ) by A20, FINSEQ_1:2, TARSKI:def_2; suppose i = 1 ; ::_thesis: ex T being DecoratedTree st ( b2 = ts . T & rts . T = b2 . {} ) hence ex T being DecoratedTree st ( T = ts . i & rts . i = T . {} ) by A3, A6, A18; ::_thesis: verum end; suppose i = 2 ; ::_thesis: ex T being DecoratedTree st ( b2 = ts . T & rts . T = b2 . {} ) hence ex T being DecoratedTree st ( T = ts . i & rts . i = T . {} ) by A4, A9, A17; ::_thesis: verum end; end; end; dom rts = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then rts = roots ts by A7, A19, TREES_3:def_18; then A21: f . (nt -tree ts) = F4(nt,(rts . 1),(rts . 2),(x . 1),(x . 2)) by A2, A5, A16; A22: ( x . 1 = xl & x . 2 = xr ) by FINSEQ_1:44; ( rts . 1 = rtl & rts . 2 = rtr ) by FINSEQ_1:44; hence f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) by A21, A22, TREES_4:def_6; ::_thesis: verum end; scheme :: BINTREE1:sch 4 BinDTConstrUniqDef{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> Function of (TS F1()),F2(), F4() -> Function of (TS F1()),F2(), F5( set ) -> Element of F2(), F6( set , set , set , set , set ) -> Element of F2() } : F3() = F4() provided A1: ( ( for t being Terminal of F1() holds F3() . (root-tree t) = F5(t) ) & ( for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = F3() . tl & xr = F3() . tr holds F3() . (nt -tree (tl,tr)) = F6(nt,rtl,rtr,xl,xr) ) ) and A2: ( ( for t being Terminal of F1() holds F4() . (root-tree t) = F5(t) ) & ( for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of F2() st xl = F4() . tl & xr = F4() . tr holds F4() . (nt -tree (tl,tr)) = F6(nt,rtl,rtr,xl,xr) ) ) proof deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F6($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2)); A3: now__::_thesis:_(_(_for_t_being_Symbol_of_F1()_st_t_in_Terminals_F1()_holds_ F4()_._(root-tree_t)_=_F5(t)_)_&_(_for_nt_being_Symbol_of_F1() for_ts_being_FinSequence_of_TS_F1()_st_nt_==>_roots_ts_holds_ F4()_._(nt_-tree_ts)_=_H1(nt,_roots_ts,F4()_*_ts)_)_) thus for t being Symbol of F1() st t in Terminals F1() holds F4() . (root-tree t) = F5(t) by A2; ::_thesis: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts implies F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) ) set rts = roots ts; set x = F4() * ts; assume A4: nt ==> roots ts ; ::_thesis: F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) then consider tl, tr being Element of TS F1() such that A5: roots ts = <*(root-label tl),(root-label tr)*> and A6: tl = ts . 1 and A7: tr = ts . 2 and A8: nt -tree ts = nt -tree (tl,tr) and tl in rng ts and tr in rng ts by Th10; A9: nt is NonTerminal of F1() by A4, Th10; reconsider xr = F4() . tr as Element of F2() ; 2 in dom ts by A4, Th10; then A10: (F4() * ts) . 2 = xr by A7, FUNCT_1:13; reconsider xl = F4() . tl as Element of F2() ; 1 in dom ts by A4, Th10; then A11: (F4() * ts) . 1 = xl by A6, FUNCT_1:13; ( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A5, FINSEQ_1:44; hence F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) by A2, A4, A5, A8, A9, A11, A10; ::_thesis: verum end; A12: now__::_thesis:_(_(_for_t_being_Symbol_of_F1()_st_t_in_Terminals_F1()_holds_ F3()_._(root-tree_t)_=_F5(t)_)_&_(_for_nt_being_Symbol_of_F1() for_ts_being_FinSequence_of_TS_F1()_st_nt_==>_roots_ts_holds_ F3()_._(nt_-tree_ts)_=_H1(nt,_roots_ts,F3()_*_ts)_)_) thus for t being Symbol of F1() st t in Terminals F1() holds F3() . (root-tree t) = F5(t) by A1; ::_thesis: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts holds F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts implies F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) ) set rts = roots ts; set x = F3() * ts; assume A13: nt ==> roots ts ; ::_thesis: F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) then consider tl, tr being Element of TS F1() such that A14: roots ts = <*(root-label tl),(root-label tr)*> and A15: tl = ts . 1 and A16: tr = ts . 2 and A17: nt -tree ts = nt -tree (tl,tr) and tl in rng ts and tr in rng ts by Th10; A18: nt is NonTerminal of F1() by A13, Th10; reconsider xr = F3() . tr as Element of F2() ; 2 in dom ts by A13, Th10; then A19: (F3() * ts) . 2 = xr by A16, FUNCT_1:13; reconsider xl = F3() . tl as Element of F2() ; 1 in dom ts by A13, Th10; then A20: (F3() * ts) . 1 = xl by A15, FUNCT_1:13; ( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A14, FINSEQ_1:44; hence F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) by A1, A13, A14, A17, A18, A20, A19; ::_thesis: verum end; thus F3() = F4() from DTCONSTR:sch_9(A12, A3); ::_thesis: verum end; definition let A, B, C be non empty set ; let a be Element of A; let b be Element of B; let c be Element of C; :: original: [ redefine func[a,b,c] -> Element of [:A,B,C:]; coherence [a,b,c] is Element of [:A,B,C:] by MCART_1:69; end; scheme :: BINTREE1:sch 5 BinDTCDefLambda{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), F5( set , set , set , set ) -> Element of F3() } : ex f being Function of (TS F1()),(Funcs (F2(),F3())) st ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st ( g = f . (root-tree t) & ( for a being Element of F2() holds g . a = F4(t,a) ) ) ) & ( for nt being NonTerminal of F1() for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) ) proof defpred S1[ set , set , set , set ] means for a being Element of F2() for ntv being Function of F2(),F3() st ntv = $4 holds ntv . a = F5($1,$2,$3,a); defpred S2[ set , set ] means for tv being Function of F2(),F3() st tv = $2 holds for a being Element of F2() holds tv . a = F4($1,a); reconsider FAB = Funcs (F2(),F3()) as non empty set ; A1: now__::_thesis:_for_x_being_Element_of_Terminals_F1()_ex_y_being_Element_of_FAB_st_S2[x,y] let x be Element of Terminals F1(); ::_thesis: ex y being Element of FAB st S2[x,y] deffunc H1( set ) -> Element of F3() = F4(x,$1); consider y being Function of F2(),F3() such that A2: for a being Element of F2() holds y . a = H1(a) from FUNCT_2:sch_4(); ( F2() = dom y & rng y c= F3() ) by FUNCT_2:def_1; then reconsider y = y as Element of FAB by FUNCT_2:def_2; take y = y; ::_thesis: S2[x,y] thus S2[x,y] by A2; ::_thesis: verum end; consider TV being Function of (Terminals F1()),FAB such that A3: for e being Element of Terminals F1() holds S2[e,TV . e] from FUNCT_2:sch_3(A1); deffunc H1( Terminal of F1()) -> Element of FAB = TV . $1; A4: now__::_thesis:_for_x_being_Element_of_NonTerminals_F1() for_y,_z_being_Element_of_FAB_ex_fab_being_Element_of_FAB_st_S1[x,y,z,fab] let x be Element of NonTerminals F1(); ::_thesis: for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab] let y, z be Element of FAB; ::_thesis: ex fab being Element of FAB st S1[x,y,z,fab] deffunc H2( set ) -> Element of F3() = F5(x,y,z,$1); consider fab being Function of F2(),F3() such that A5: for a being Element of F2() holds fab . a = H2(a) from FUNCT_2:sch_4(); ( F2() = dom fab & rng fab c= F3() ) by FUNCT_2:def_1; then reconsider fab = fab as Element of FAB by FUNCT_2:def_2; take fab = fab; ::_thesis: S1[x,y,z,fab] thus S1[x,y,z,fab] by A5; ::_thesis: verum end; consider NTV being Function of [:(NonTerminals F1()),FAB,FAB:],FAB such that A6: for x being Element of NonTerminals F1() for y, z being Element of FAB holds S1[x,y,z,NTV . [x,y,z]] from MULTOP_1:sch_1(A4); deffunc H2( Element of NonTerminals F1(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5]; consider f being Function of (TS F1()),FAB such that A7: ( ( for t being Terminal of F1() holds f . (root-tree t) = H1(t) ) & ( for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f . tl & xr = f . tr holds f . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch_3(); reconsider f9 = f as Function of (TS F1()),(Funcs (F2(),F3())) ; take f9 ; ::_thesis: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st ( g = f9 . (root-tree t) & ( for a being Element of F2() holds g . a = F4(t,a) ) ) ) & ( for nt being NonTerminal of F1() for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) ) hereby ::_thesis: for nt being NonTerminal of F1() for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) let t be Terminal of F1(); ::_thesis: ex TVt being Function of F2(),F3() st ( TVt = f9 . (root-tree t) & ( for a being Element of F2() holds TVt . a = F4(t,a) ) ) consider TVt being Function such that A8: TV . t = TVt and A9: ( dom TVt = F2() & rng TVt c= F3() ) by FUNCT_2:def_2; reconsider TVt = TVt as Function of F2(),F3() by A9, FUNCT_2:def_1, RELSET_1:4; take TVt = TVt; ::_thesis: ( TVt = f9 . (root-tree t) & ( for a being Element of F2() holds TVt . a = F4(t,a) ) ) thus TVt = f9 . (root-tree t) by A7, A8; ::_thesis: for a being Element of F2() holds TVt . a = F4(t,a) let a be Element of F2(); ::_thesis: TVt . a = F4(t,a) thus TVt . a = F4(t,a) by A3, A8; ::_thesis: verum end; let nt be NonTerminal of F1(); ::_thesis: for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) let t1, t2 be Element of TS F1(); ::_thesis: for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) let rtl, rtr be Symbol of F1(); ::_thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) assume A10: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; ::_thesis: ex g, f1, f2 being Function of F2(),F3() st ( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ex f2 being Function st ( f . t2 = f2 & dom f2 = F2() & rng f2 c= F3() ) by FUNCT_2:def_2; then reconsider f2 = f . t2 as Function of F2(),F3() by FUNCT_2:def_1, RELSET_1:4; ex f1 being Function st ( f . t1 = f1 & dom f1 = F2() & rng f1 c= F3() ) by FUNCT_2:def_2; then reconsider f1 = f . t1 as Function of F2(),F3() by FUNCT_2:def_1, RELSET_1:4; NTV . [nt,(f . t1),(f . t2)] in FAB ; then consider ntvval being Function such that A11: ntvval = NTV . [nt,f1,f2] and A12: ( dom ntvval = F2() & rng ntvval c= F3() ) by FUNCT_2:def_2; reconsider ntvval = ntvval as Function of F2(),F3() by A12, FUNCT_2:def_1, RELSET_1:4; take ntvval ; ::_thesis: ex f1, f2 being Function of F2(),F3() st ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) ) ) take f1 ; ::_thesis: ex f2 being Function of F2(),F3() st ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) ) ) take f2 ; ::_thesis: ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) ) ) thus ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 ) by A7, A10, A11; ::_thesis: for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) thus for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) by A6, A11; ::_thesis: verum end; scheme :: BINTREE1:sch 6 BinDTCDefLambdaUniq{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> non empty set , F4() -> Function of (TS F1()),(Funcs (F2(),F3())), F5() -> Function of (TS F1()),(Funcs (F2(),F3())), F6( set , set ) -> Element of F3(), F7( set , set , set , set ) -> Element of F3() } : F4() = F5() provided A1: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st ( g = F4() . (root-tree t) & ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) & ( for nt being NonTerminal of F1() for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = F4() . (nt -tree (t1,t2)) & f1 = F4() . t1 & f2 = F4() . t2 & ( for a being Element of F2() holds g . a = F7(nt,f1,f2,a) ) ) ) ) and A2: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st ( g = F5() . (root-tree t) & ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) & ( for nt being NonTerminal of F1() for t1, t2 being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds ex g, f1, f2 being Function of F2(),F3() st ( g = F5() . (nt -tree (t1,t2)) & f1 = F5() . t1 & f2 = F5() . t2 & ( for a being Element of F2() holds g . a = F7(nt,f1,f2,a) ) ) ) ) proof defpred S1[ set , set , set , set ] means for a being Element of F2() for ntv being Function of F2(),F3() st ntv = $4 holds ntv . a = F7($1,$2,$3,a); defpred S2[ set , set ] means for tv being Function of F2(),F3() st tv = $2 holds for a being Element of F2() holds tv . a = F6($1,a); reconsider FAB = Funcs (F2(),F3()) as non empty set ; reconsider f29 = F5() as Function of (TS F1()),FAB ; A3: now__::_thesis:_for_x_being_Element_of_Terminals_F1()_ex_y_being_Element_of_FAB_st_S2[x,y] let x be Element of Terminals F1(); ::_thesis: ex y being Element of FAB st S2[x,y] deffunc H1( Element of F2()) -> Element of F3() = F6(x,$1); consider y being Function of F2(),F3() such that A4: for a being Element of F2() holds y . a = H1(a) from FUNCT_2:sch_4(); ( F2() = dom y & rng y c= F3() ) by FUNCT_2:def_1; then reconsider y = y as Element of FAB by FUNCT_2:def_2; take y = y; ::_thesis: S2[x,y] thus S2[x,y] by A4; ::_thesis: verum end; consider TV being Function of (Terminals F1()),FAB such that A5: for e being Element of Terminals F1() holds S2[e,TV . e] from FUNCT_2:sch_3(A3); deffunc H1( Terminal of F1()) -> Element of FAB = TV . $1; A6: now__::_thesis:_for_x_being_Element_of_NonTerminals_F1() for_y,_z_being_Element_of_FAB_ex_fab_being_Element_of_FAB_st_S1[x,y,z,fab] let x be Element of NonTerminals F1(); ::_thesis: for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab] let y, z be Element of FAB; ::_thesis: ex fab being Element of FAB st S1[x,y,z,fab] deffunc H2( Element of F2()) -> Element of F3() = F7(x,y,z,$1); consider fab being Function of F2(),F3() such that A7: for a being Element of F2() holds fab . a = H2(a) from FUNCT_2:sch_4(); ( F2() = dom fab & rng fab c= F3() ) by FUNCT_2:def_1; then reconsider fab = fab as Element of FAB by FUNCT_2:def_2; take fab = fab; ::_thesis: S1[x,y,z,fab] thus S1[x,y,z,fab] by A7; ::_thesis: verum end; consider NTV being Function of [:(NonTerminals F1()),FAB,FAB:],FAB such that A8: for x being Element of NonTerminals F1() for y, z being Element of FAB holds S1[x,y,z,NTV . [x,y,z]] from MULTOP_1:sch_1(A6); deffunc H2( NonTerminal of F1(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5]; A9: now__::_thesis:_(_(_for_t_being_Terminal_of_F1()_holds_f29_._(root-tree_t)_=_H1(t)_)_&_(_for_nt_being_NonTerminal_of_F1() for_tl,_tr_being_Element_of_TS_F1() for_rtl,_rtr_being_Symbol_of_F1()_st_rtl_=_root-label_tl_&_rtr_=_root-label_tr_&_nt_==>_<*rtl,rtr*>_holds_ for_xl,_xr_being_Element_of_FAB_st_xl_=_f29_._tl_&_xr_=_f29_._tr_holds_ f29_._(nt_-tree_(tl,tr))_=_H2(nt,rtl,rtr,xl,xr)_)_) hereby ::_thesis: for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let t be Terminal of F1(); ::_thesis: f29 . (root-tree t) = H1(t) consider TVt being Function such that A10: TV . t = TVt and A11: dom TVt = F2() and A12: rng TVt c= F3() by FUNCT_2:def_2; reconsider TVt = TVt as Function of F2(),F3() by A11, A12, FUNCT_2:def_1, RELSET_1:4; consider g being Function of F2(),F3() such that A13: g = F5() . (root-tree t) and A14: for a being Element of F2() holds g . a = F6(t,a) by A2; now__::_thesis:_(_F2()_=_dom_g_&_F2()_=_dom_TVt_&_(_for_x_being_set_st_x_in_F2()_holds_ g_._x_=_TVt_._x_)_) thus F2() = dom g by FUNCT_2:def_1; ::_thesis: ( F2() = dom TVt & ( for x being set st x in F2() holds g . x = TVt . x ) ) thus F2() = dom TVt by A11; ::_thesis: for x being set st x in F2() holds g . x = TVt . x let x be set ; ::_thesis: ( x in F2() implies g . x = TVt . x ) assume x in F2() ; ::_thesis: g . x = TVt . x then reconsider xx = x as Element of F2() ; g . xx = F6(t,xx) by A14 .= TVt . xx by A5, A10 ; hence g . x = TVt . x ; ::_thesis: verum end; hence f29 . (root-tree t) = H1(t) by A13, A10, FUNCT_1:2; ::_thesis: verum end; let nt be NonTerminal of F1(); ::_thesis: for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let tl, tr be Element of TS F1(); ::_thesis: for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let rtl, rtr be Symbol of F1(); ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; ::_thesis: for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) then consider g, ff1, ff2 being Function of F2(),F3() such that A15: g = F5() . (nt -tree (tl,tr)) and A16: ( ff1 = F5() . tl & ff2 = F5() . tr & ( for a being Element of F2() holds g . a = F7(nt,ff1,ff2,a) ) ) by A2; let xl, xr be Element of FAB; ::_thesis: ( xl = f29 . tl & xr = f29 . tr implies f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) consider ntvnt being Function such that A17: ntvnt = NTV . [nt,xl,xr] and A18: ( dom ntvnt = F2() & rng ntvnt c= F3() ) by FUNCT_2:def_2; reconsider ntvnt = ntvnt as Function of F2(),F3() by A18, FUNCT_2:def_1, RELSET_1:4; assume A19: ( xl = f29 . tl & xr = f29 . tr ) ; ::_thesis: f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) now__::_thesis:_(_F2()_=_dom_g_&_F2()_=_dom_ntvnt_&_(_for_x_being_set_st_x_in_F2()_holds_ g_._x_=_ntvnt_._x_)_) thus F2() = dom g by FUNCT_2:def_1; ::_thesis: ( F2() = dom ntvnt & ( for x being set st x in F2() holds g . x = ntvnt . x ) ) thus F2() = dom ntvnt by FUNCT_2:def_1; ::_thesis: for x being set st x in F2() holds g . x = ntvnt . x let x be set ; ::_thesis: ( x in F2() implies g . x = ntvnt . x ) assume x in F2() ; ::_thesis: g . x = ntvnt . x then reconsider xx = x as Element of F2() ; g . xx = F7(nt,xl,xr,xx) by A19, A16 .= ntvnt . xx by A8, A17 ; hence g . x = ntvnt . x ; ::_thesis: verum end; hence f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) by A15, A17, FUNCT_1:2; ::_thesis: verum end; reconsider f19 = F4() as Function of (TS F1()),FAB ; A20: now__::_thesis:_(_(_for_t_being_Terminal_of_F1()_holds_f19_._(root-tree_t)_=_H1(t)_)_&_(_for_nt_being_NonTerminal_of_F1() for_tl,_tr_being_Element_of_TS_F1() for_rtl,_rtr_being_Symbol_of_F1()_st_rtl_=_root-label_tl_&_rtr_=_root-label_tr_&_nt_==>_<*rtl,rtr*>_holds_ for_xl,_xr_being_Element_of_FAB_st_xl_=_f19_._tl_&_xr_=_f19_._tr_holds_ f19_._(nt_-tree_(tl,tr))_=_H2(nt,rtl,rtr,xl,xr)_)_) hereby ::_thesis: for nt being NonTerminal of F1() for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let t be Terminal of F1(); ::_thesis: f19 . (root-tree t) = H1(t) consider TVt being Function such that A21: TV . t = TVt and A22: dom TVt = F2() and A23: rng TVt c= F3() by FUNCT_2:def_2; reconsider TVt = TVt as Function of F2(),F3() by A22, A23, FUNCT_2:def_1, RELSET_1:4; consider g being Function of F2(),F3() such that A24: g = F4() . (root-tree t) and A25: for a being Element of F2() holds g . a = F6(t,a) by A1; now__::_thesis:_(_F2()_=_dom_g_&_F2()_=_dom_TVt_&_(_for_x_being_set_st_x_in_F2()_holds_ g_._x_=_TVt_._x_)_) thus F2() = dom g by FUNCT_2:def_1; ::_thesis: ( F2() = dom TVt & ( for x being set st x in F2() holds g . x = TVt . x ) ) thus F2() = dom TVt by A22; ::_thesis: for x being set st x in F2() holds g . x = TVt . x let x be set ; ::_thesis: ( x in F2() implies g . x = TVt . x ) assume x in F2() ; ::_thesis: g . x = TVt . x then reconsider xx = x as Element of F2() ; g . xx = F6(t,xx) by A25 .= TVt . xx by A5, A21 ; hence g . x = TVt . x ; ::_thesis: verum end; hence f19 . (root-tree t) = H1(t) by A24, A21, FUNCT_1:2; ::_thesis: verum end; let nt be NonTerminal of F1(); ::_thesis: for tl, tr being Element of TS F1() for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let tl, tr be Element of TS F1(); ::_thesis: for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) let rtl, rtr be Symbol of F1(); ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; ::_thesis: for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) then consider g, ff1, ff2 being Function of F2(),F3() such that A26: g = F4() . (nt -tree (tl,tr)) and A27: ( ff1 = F4() . tl & ff2 = F4() . tr & ( for a being Element of F2() holds g . a = F7(nt,ff1,ff2,a) ) ) by A1; let xl, xr be Element of FAB; ::_thesis: ( xl = f19 . tl & xr = f19 . tr implies f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) consider ntvnt being Function such that A28: ntvnt = NTV . [nt,xl,xr] and A29: ( dom ntvnt = F2() & rng ntvnt c= F3() ) by FUNCT_2:def_2; reconsider ntvnt = ntvnt as Function of F2(),F3() by A29, FUNCT_2:def_1, RELSET_1:4; assume A30: ( xl = f19 . tl & xr = f19 . tr ) ; ::_thesis: f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) now__::_thesis:_(_F2()_=_dom_g_&_F2()_=_dom_ntvnt_&_(_for_x_being_set_st_x_in_F2()_holds_ g_._x_=_ntvnt_._x_)_) thus F2() = dom g by FUNCT_2:def_1; ::_thesis: ( F2() = dom ntvnt & ( for x being set st x in F2() holds g . x = ntvnt . x ) ) thus F2() = dom ntvnt by FUNCT_2:def_1; ::_thesis: for x being set st x in F2() holds g . x = ntvnt . x let x be set ; ::_thesis: ( x in F2() implies g . x = ntvnt . x ) assume x in F2() ; ::_thesis: g . x = ntvnt . x then reconsider xx = x as Element of F2() ; g . xx = F7(nt,xl,xr,xx) by A30, A27 .= ntvnt . xx by A8, A28 ; hence g . x = ntvnt . x ; ::_thesis: verum end; hence f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) by A26, A28, FUNCT_1:2; ::_thesis: verum end; f19 = f29 from BINTREE1:sch_4(A20, A9); hence F4() = F5() ; ::_thesis: verum end; registration let G be non empty with_terminals with_nonterminals binary DTConstrStr ; cluster -> binary for Element of TS G; coherence for b1 being Element of TS G holds b1 is binary proof defpred S1[ DecoratedTree] means G is binary ; A1: now__::_thesis:_for_s_being_Terminal_of_G_holds_S1[_root-tree_s] let s be Terminal of G; ::_thesis: S1[ root-tree s] dom (root-tree s) is binary by TREES_4:3; hence S1[ root-tree s] by Def3; ::_thesis: verum end; A2: for nt being NonTerminal of G for tl, tr being Element of TS G st nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] holds S1[nt -tree (tl,tr)] by Th9; thus for x being Element of TS G holds S1[x] from BINTREE1:sch_2(A1, A2); ::_thesis: verum end; end;