Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### On Defining Functions on Binary Trees

**by****Grzegorz Bancerek, and****Piotr Rudnicki**- Received December 30, 1993
- MML identifier: BINTREE1

- [ Mizar article, MML identifier index ]

environ vocabulary TREES_2, FUNCT_1, BOOLE, TREES_4, DTCONSTR, FINSEQ_1, TREES_1, ORDINAL1, FINSET_1, RELAT_1, TREES_3, LANG1, TDGROUP, FUNCT_2, BINTREE1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, RELSET_1, STRUCT_0, MCART_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR; constructors DOMAIN_1, NAT_1, DTCONSTR, FINSOP_1, XREAL_0, MEMBERED, XBOOLE_0, FINSEQOP; clusters SUBSET_1, TREES_2, TREES_3, DTCONSTR, RELSET_1, FINSEQ_1, STRUCT_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin definition let D be non empty set, t be DecoratedTree of D; func root-label t -> Element of D equals :: BINTREE1:def 1 t.{}; end; theorem :: BINTREE1:1 for D being non empty set, t being DecoratedTree of D holds roots <*t*> = <*root-label t*>; theorem :: BINTREE1:2 for D being non empty set, t1, t2 being DecoratedTree of D holds roots <*t1, t2*> = <*root-label t1, root-label t2*>; definition let IT be Tree; attr IT is binary means :: BINTREE1:def 2 for t being Element of IT st not t in Leaves IT holds succ t = { t^<*0*>, t^<*1*> }; end; theorem :: BINTREE1:3 for T being Tree, t being Element of T holds t in Leaves T iff not t^<*0*> in T; theorem :: BINTREE1:4 for T being Tree, t being Element of T holds t in Leaves T iff not ex n being Nat st t^<*n*> in T; theorem :: BINTREE1:5 :: LeavesDef3: for T being Tree, t being Element of T holds succ t = {} iff t in Leaves T; theorem :: BINTREE1:6 elementary_tree 0 is binary; theorem :: BINTREE1:7 :: BinEx2: elementary_tree 2 is binary; definition cluster binary finite Tree; end; definition let IT be DecoratedTree; attr IT is binary means :: BINTREE1:def 3 dom IT is binary; end; definition let D be non empty set; cluster binary finite DecoratedTree of D; end; definition cluster binary finite DecoratedTree; end; definition cluster binary -> finite-order Tree; end; theorem :: BINTREE1:8 for T0,T1 being Tree, 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); theorem :: BINTREE1:9 for T0,T1 being Tree, 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 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 for sp being FinSequence holds sp in succ p iff <*1*>^sp in succ t); theorem :: BINTREE1:10 for T1,T2 being Tree holds T1 is binary & T2 is binary iff tree(T1,T2) is binary; theorem :: BINTREE1:11 for T1,T2 being DecoratedTree, x being set holds T1 is binary & T2 is binary iff x-tree (T1,T2) is binary; definition let D be non empty set, x be Element of D, T1, T2 be binary finite DecoratedTree of D; redefine func x-tree (T1,T2) -> binary finite DecoratedTree of D; end; definition let IT be non empty DTConstrStr; attr IT is binary means :: BINTREE1:def 4 for s being Symbol of IT, p being FinSequence st s ==> p ex x1, x2 being Symbol of IT st p = <* x1, x2 *>; end; definition cluster binary with_terminals with_nonterminals with_useful_nonterminals strict (non empty DTConstrStr); end; scheme BinDTConstrStrEx { S() -> non empty set, P[set, set, set] }: ex G be binary strict (non empty DTConstrStr) st the carrier of G = S() & for x, y, z being Symbol of G holds x ==> <*y,z*> iff P[x, y, z]; theorem :: BINTREE1:12 for G being binary with_terminals with_nonterminals (non empty DTConstrStr), ts being FinSequence of TS G, 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; scheme BinDTConstrInd { G() -> binary with_terminals with_nonterminals (non empty DTConstrStr), P[set] }: for t being Element of TS(G()) holds P[t] provided for s being Terminal of G() holds P[root-tree s] and for nt being NonTerminal of G(), tl, tr being Element of TS(G()) st nt ==> <*root-label tl, root-label tr*> & P[tl] & P[tr] holds P[nt-tree(tl, tr)]; scheme BinDTConstrIndDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals (non empty DTConstrStr), D()->non empty set, TermVal(set) -> Element of D(), NTermVal(set, set, set, set, set) -> Element of D() }: ex f being Function of TS(G()), D() st (for t being Terminal of G() holds f.(root-tree t) = TermVal(t)) & (for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr)); scheme BinDTConstrUniqDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals (non empty DTConstrStr), D()->non empty set, f1, f2() -> Function of TS(G()), D(), TermVal(set) -> Element of D(), NTermVal(set, set, set, set, set) -> Element of D() }: f1() = f2() provided (for t being Terminal of G() holds f1().(root-tree t) = TermVal(t)) & (for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f1().tl & xr = f1().tr holds f1().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr)) and (for t being Terminal of G() holds f2().(root-tree t) = TermVal(t)) & (for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f2().tl & xr = f2().tr holds f2().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr)); definition let A, B, C be non empty set, a be Element of A, b be Element of B, c be Element of C; redefine func [a, b, c] -> Element of [:A, B, C:]; end; scheme BinDTC_DefLambda { G() -> binary with_terminals with_nonterminals with_useful_nonterminals (non empty DTConstrStr), A, B() -> non empty set, F(set, set) -> Element of B(), H(set, set, set, set) -> Element of B() }: ex f being Function of TS G(), Funcs(A(), B()) st (for t being Terminal of G() ex g being Function of A(), B() st g = f.(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & (for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a)); scheme BinDTC_DefLambdaUniq { G() -> binary with_terminals with_nonterminals with_useful_nonterminals (non empty DTConstrStr), A, B() -> non empty set, f1, f2() -> Function of TS G(), Funcs (A(), B()), F(set, set) -> Element of B(), H(set, set, set, set) -> Element of B() }: f1() = f2() provided (for t being Terminal of G() ex g being Function of A(), B() st g = f1().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & (for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f1().(nt-tree (t1, t2)) & f1 = f1().t1 & f2 = f1().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a)) and (for t being Terminal of G() ex g being Function of A(), B() st g = f2().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & (for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f2().(nt-tree (t1, t2)) & f1 = f2().t1 & f2 = f2().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a)); definition let G be binary with_terminals with_nonterminals (non empty DTConstrStr); cluster -> binary Element of TS G; end;

Back to top