:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received December 30, 1993

:: Copyright (c) 1993-2018 Association of Mizar Users

definition
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 . {};

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;

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;

for t1, t2 being DecoratedTree of D holds roots <*t1,t2*> = <*(root-label t1),(root-label t2)*> by DTCONSTR:6;

:: deftheorem 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*>)} );

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*>)} );

registration
end;

definition
end;

:: deftheorem Def3 defines binary BINTREE1:def 3 :

for IT being DecoratedTree holds

( IT is binary iff dom IT is binary );

for IT being DecoratedTree holds

( IT is binary iff dom IT is binary );

registration

let D be non empty set ;

ex b_{1} being DecoratedTree of D st

( b_{1} is binary & b_{1} is finite )

end;
cluster Relation-like D -valued Function-like finite DecoratedTree-like binary for DecoratedTree of ;

existence ex b

( b

proof end;

registration
end;

registration
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 ) ) )

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 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 ) ) )

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 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 )

for x being set holds

( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary )

proof end;

registration

let D be non empty set ;

let x be Element of D;

let T1, T2 be finite binary DecoratedTree of D;

coherence

( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued )

end;
let x be Element of D;

let T1, T2 be finite binary DecoratedTree of D;

coherence

( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued )

proof end;

definition

let IT be non empty DTConstrStr ;

end;
attr IT 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*>;

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*>;

:: 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*> );

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

ex b_{1} being non empty DTConstrStr st

( b_{1} is binary & b_{1} is with_terminals & b_{1} is with_nonterminals & b_{1} is with_useful_nonterminals & b_{1} is strict )
end;

cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals binary for DTConstrStr ;

existence ex b

( b

proof 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 ) )

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 end;

scheme :: BINTREE1:sch 2

BinDTConstrInd{ F_{1}() -> non empty with_terminals with_nonterminals binary DTConstrStr , P_{1}[ set ] } :

provided

BinDTConstrInd{ F

provided

A1:
for s being Terminal of F_{1}() holds P_{1}[ root-tree s]
and

A2: for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}() st nt ==> <*(root-label tl),(root-label tr)*> & P_{1}[tl] & P_{1}[tr] holds

P_{1}[nt -tree (tl,tr)]

A2: for nt being NonTerminal of F

for tl, tr being Element of TS F

P

proof end;

scheme :: BINTREE1:sch 3

BinDTConstrIndDef{ F_{1}() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}( set , set , set , set , set ) -> Element of F_{2}() } :

BinDTConstrIndDef{ F

ex f being Function of (TS F_{1}()),F_{2}() st

( ( for t being Terminal of F_{1}() holds f . (root-tree t) = F_{3}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr) ) )

( ( for t being Terminal of F

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

proof end;

scheme :: BINTREE1:sch 4

BinDTConstrUniqDef{ F_{1}() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F_{2}() -> non empty set , F_{3}() -> Function of (TS F_{1}()),F_{2}(), F_{4}() -> Function of (TS F_{1}()),F_{2}(), F_{5}( set ) -> Element of F_{2}(), F_{6}( set , set , set , set , set ) -> Element of F_{2}() } :

provided

BinDTConstrUniqDef{ F

provided

A1:
( ( for t being Terminal of F_{1}() holds F_{3}() . (root-tree t) = F_{5}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = F_{3}() . tl & xr = F_{3}() . tr holds

F_{3}() . (nt -tree (tl,tr)) = F_{6}(nt,rtl,rtr,xl,xr) ) )
and

A2: ( ( for t being Terminal of F_{1}() holds F_{4}() . (root-tree t) = F_{5}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = F_{4}() . tl & xr = F_{4}() . tr holds

F_{4}() . (nt -tree (tl,tr)) = F_{6}(nt,rtl,rtr,xl,xr) ) )

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

F

A2: ( ( for t being Terminal of F

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

F

proof end;

scheme :: BINTREE1:sch 5

BinDTCDefLambda{ F_{1}() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( set , set ) -> Element of F_{3}(), F_{5}( set , set , set , set ) -> Element of F_{3}() } :

BinDTCDefLambda{ F

ex f being Function of (TS F_{1}()),(Funcs (F_{2}(),F_{3}())) st

( ( for t being Terminal of F_{1}() ex g being Function of F_{2}(),F_{3}() st

( g = f . (root-tree t) & ( for a being Element of F_{2}() holds g . a = F_{4}(t,a) ) ) ) & ( for nt being NonTerminal of F_{1}()

for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) ) ) )

( ( for t being Terminal of F

( g = f . (root-tree t) & ( for a being Element of F

for t1, t2 being Element of TS F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for a being Element of F

proof end;

scheme :: BINTREE1:sch 6

BinDTCDefLambdaUniq{ F_{1}() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> Function of (TS F_{1}()),(Funcs (F_{2}(),F_{3}())), F_{5}() -> Function of (TS F_{1}()),(Funcs (F_{2}(),F_{3}())), F_{6}( set , set ) -> Element of F_{3}(), F_{7}( set , set , set , set ) -> Element of F_{3}() } :

provided

BinDTCDefLambdaUniq{ F

provided

A1:
( ( for t being Terminal of F_{1}() ex g being Function of F_{2}(),F_{3}() st

( g = F_{4}() . (root-tree t) & ( for a being Element of F_{2}() holds g . a = F_{6}(t,a) ) ) ) & ( for nt being NonTerminal of F_{1}()

for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = F_{4}() . (nt -tree (t1,t2)) & f1 = F_{4}() . t1 & f2 = F_{4}() . t2 & ( for a being Element of F_{2}() holds g . a = F_{7}(nt,f1,f2,a) ) ) ) )
and

A2: ( ( for t being Terminal of F_{1}() ex g being Function of F_{2}(),F_{3}() st

( g = F_{5}() . (root-tree t) & ( for a being Element of F_{2}() holds g . a = F_{6}(t,a) ) ) ) & ( for nt being NonTerminal of F_{1}()

for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = F_{5}() . (nt -tree (t1,t2)) & f1 = F_{5}() . t1 & f2 = F_{5}() . t2 & ( for a being Element of F_{2}() holds g . a = F_{7}(nt,f1,f2,a) ) ) ) )

( g = F

for t1, t2 being Element of TS F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = F

A2: ( ( for t being Terminal of F

( g = F

for t1, t2 being Element of TS F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = F

proof end;

registration

let G be non empty with_terminals with_nonterminals binary DTConstrStr ;

coherence

for b_{1} being Element of TS G holds b_{1} is binary

end;
coherence

for b

proof end;