:: On Defining Functions on Binary Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


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

registration
cluster elementary_tree 0 ->  binary ;
coherence
 elementary_tree 0 is binary
proofend;
cluster elementary_tree 2 ->  binary ;
coherence
 elementary_tree 2 is binary
proofend;
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 &amp; b1 is finite )
proofend;
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 &amp; b1 is finite )
proofend;
end;

registration
cluster Relation-like Function-like finite DecoratedTree-like binary for set ;
existence
 ex b1 being DecoratedTree st
( b1 is binary &amp; b1 is finite )
proofend;
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
proofend;
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 ) ) &amp; ( for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) )
proofend;

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*>)} ) &amp; ( 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 ) ) &amp; ( 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 ) ) )
proofend;

theorem Th8: :: BINTREE1:8
for T1, T2 being Tree holds
( ( T1 is binary &amp; T2 is binary ) iff tree (T1,T2) is binary )
proofend;

theorem Th9: :: BINTREE1:9
for T1, T2 being DecoratedTree
for x being set holds
( ( T1 is binary &amp; T2 is binary ) iff x -tree (T1,T2) is binary )
proofend;

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 &amp; x -tree (T1,T2) is finite &amp; x -tree (T1,T2) is D -valued )
proofend;
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 &amp; b1 is with_terminals &amp; b1 is with_nonterminals &amp; b1 is with_useful_nonterminals &amp; b1 is strict )
proofend;
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() &amp; ( for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P1[x,y,z] ) ) )
proofend;

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 &amp; dom ts = {1,2} &amp; 1 in dom ts &amp; 2 in dom ts &amp; ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> &amp; tl = ts . 1 &amp; tr = ts . 2 &amp; nt -tree ts = nt -tree (tl,tr) &amp; tl in rng ts &amp; tr in rng ts ) )
proofend;

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)*> &amp; P1[tl] &amp; P1[tr] holds
P1[nt -tree (tl,tr)]
proofend;

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) ) &amp; ( 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 &amp; rtr = root-label tr &amp; nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl &amp; xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) )
proofend;

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) ) &amp; ( 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 &amp; rtr = root-label tr &amp; nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = F3() . tl &amp; 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) ) &amp; ( 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 &amp; rtr = root-label tr &amp; nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = F4() . tl &amp; xr = F4() . tr holds
F4() . (nt -tree (tl,tr)) = F6(nt,rtl,rtr,xl,xr) ) )
proofend;

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) &amp; ( for a being Element of F2() holds g . a = F4(t,a) ) ) ) &amp; ( 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 &amp; rtr = root-label t2 &amp; nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f . (nt -tree (t1,t2)) &amp; f1 = f . t1 &amp; f2 = f . t2 &amp; ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) )
proofend;

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) &amp; ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) &amp; ( 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 &amp; rtr = root-label t2 &amp; nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = F4() . (nt -tree (t1,t2)) &amp; f1 = F4() . t1 &amp; f2 = F4() . t2 &amp; ( 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) &amp; ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) &amp; ( 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 &amp; rtr = root-label t2 &amp; nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = F5() . (nt -tree (t1,t2)) &amp; f1 = F5() . t1 &amp; f2 = F5() . t2 &amp; ( for a being Element of F2() holds g . a = F7(nt,f1,f2,a) ) ) ) )
proofend;

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