:: BINTREE1 semantic presentation

definition
let c1 be non empty set ;
let c2 be DecoratedTree of c1;
func root-label c2 -> Element of a1 equals :: BINTREE1:def 1
a2 . {} ;
coherence
c2 . {} is Element of c1
proof end;
end;

:: deftheorem Def1 defines root-label BINTREE1:def 1 :
for b1 being non empty set
for b2 being DecoratedTree of b1 holds root-label b2 = b2 . {} ;

theorem Th1: :: BINTREE1:1
for b1 being non empty set
for b2 being DecoratedTree of b1 holds roots <*b2*> = <*(root-label b2)*> by DTCONSTR:4;

theorem Th2: :: BINTREE1:2
for b1 being non empty set
for b2, b3 being DecoratedTree of b1 holds roots <*b2,b3*> = <*(root-label b2),(root-label b3)*> by DTCONSTR:6;

definition
let c1 be Tree;
attr a1 is binary means :Def2: :: BINTREE1:def 2
for b1 being Element of a1 st not b1 in Leaves a1 holds
succ b1 = {(b1 ^ <*0*>),(b1 ^ <*1*>)};
end;

:: deftheorem Def2 defines binary BINTREE1:def 2 :
for b1 being Tree holds
( b1 is binary iff for b2 being Element of b1 st not b2 in Leaves b1 holds
succ b2 = {(b2 ^ <*0*>),(b2 ^ <*1*>)} );

theorem Th3: :: BINTREE1:3
canceled;

theorem Th4: :: BINTREE1:4
canceled;

theorem Th5: :: BINTREE1:5
for b1 being Tree
for b2 being Element of b1 holds
( succ b2 = {} iff b2 in Leaves b1 )
proof end;

theorem Th6: :: BINTREE1:6
elementary_tree 0 is binary
proof end;

theorem Th7: :: BINTREE1:7
elementary_tree 2 is binary
proof end;

registration
cluster finite binary set ;
existence
ex b1 being Tree st
( b1 is binary & b1 is finite ) by Th6;
end;

definition
let c1 be DecoratedTree;
attr a1 is binary means :Def3: :: BINTREE1:def 3
 dom a1 is binary;
end;

:: deftheorem Def3 defines binary BINTREE1:def 3 :
for b1 being DecoratedTree holds
( b1 is binary iff dom b1 is binary );

registration
let c1 be non empty set ;
cluster finite binary ParametrizedSubset of a1;
existence
ex b1 being DecoratedTree of c1 st
( b1 is binary & b1 is finite )
proof end;
end;

registration
cluster finite binary set ;
existence
ex b1 being DecoratedTree st
( b1 is binary & b1 is finite )
proof end;
end;

registration
cluster binary -> finite-order set ;
coherence
for b1 being Tree st b1 is binary holds
b1 is finite-order
proof end;
end;

theorem Th8: :: BINTREE1:8
for b1, b2 being Tree
for b3 being Element of tree b1,b2 holds
( ( for b4 being Element of b1 st b3 = <*0*> ^ b4 holds
( b3 in Leaves (tree b1,b2) iff b4 in Leaves b1 ) ) & ( for b4 being Element of b2 st b3 = <*1*> ^ b4 holds
( b3 in Leaves (tree b1,b2) iff b4 in Leaves b2 ) ) )
proof end;

theorem Th9: :: BINTREE1:9
for b1, b2 being Tree
for b3 being Element of tree b1,b2 holds
( ( b3 = {} implies succ b3 = {(b3 ^ <*0*>),(b3 ^ <*1*>)} ) & ( for b4 being Element of b1 st b3 = <*0*> ^ b4 holds
for b5 being FinSequence holds
( b5 in succ b4 iff <*0*> ^ b5 in succ b3 ) ) & ( for b4 being Element of b2 st b3 = <*1*> ^ b4 holds
for b5 being FinSequence holds
( b5 in succ b4 iff <*1*> ^ b5 in succ b3 ) ) )
proof end;

theorem Th10: :: BINTREE1:10
for b1, b2 being Tree holds
( ( b1 is binary & b2 is binary ) iff tree b1,b2 is binary )
proof end;

theorem Th11: :: BINTREE1:11
for b1, b2 being DecoratedTree
for b3 being set holds
( ( b1 is binary & b2 is binary ) iff b3 -tree b1,b2 is binary )
proof end;

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3, c4 be finite binary DecoratedTree of c1;
redefine func -tree as c2 -tree c3,c4 -> finite binary DecoratedTree of a1;
coherence
c2 -tree c3,c4 is finite binary DecoratedTree of c1
proof end;
end;

definition
let c1 be non empty DTConstrStr ;
attr a1 is binary means :Def4: :: BINTREE1:def 4
for b1 being Symbol of a1
for b2 being FinSequence st b1 ==> b2 holds
ex b3, b4 being Symbol of a1 st b2 = <*b3,b4*>;
end;

:: deftheorem Def4 defines binary BINTREE1:def 4 :
for b1 being non empty DTConstrStr holds
( b1 is binary iff for b2 being Symbol of b1
for b3 being FinSequence st b2 ==> b3 holds
ex b4, b5 being Symbol of b1 st b3 = <*b4,b5*> );

registration
cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals binary 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 end;
end;

scheme :: BINTREE1:sch 1
s1{ F1() -> non empty set , P1[ set , set , set ] } :
ex b1 being non empty strict binary DTConstrStr st
( the carrier of b1 = F1() & ( for b2, b3, b4 being Symbol of b1 holds
( b2 ==> <*b3,b4*> iff P1[b2,b3,b4] ) ) )
proof end;

theorem Th12: :: BINTREE1:12
for b1 being non empty with_terminals with_nonterminals binary DTConstrStr
for b2 being FinSequence of TS b1
for b3 being Symbol of b1 st b3 ==> roots b2 holds
( b3 is NonTerminal of b1 & dom b2 = {1,2} & 1 in dom b2 & 2 in dom b2 & ex b4, b5 being Element of TS b1 st
( roots b2 = <*(root-label b4),(root-label b5)*> & b4 = b2 . 1 & b5 = b2 . 2 & b3 -tree b2 = b3 -tree b4,b5 & b4 in rng b2 & b5 in rng b2 ) )
proof end;

scheme :: BINTREE1:sch 2
s2{ F1() -> non empty with_terminals with_nonterminals binary DTConstrStr , P1[ set ] } :
for b1 being Element of TS F1() holds P1[b1]
provided
E10: for b1 being Terminal of F1() holds P1[ root-tree b1] and
E11: for b1 being NonTerminal of F1()
for b2, b3 being Element of TS F1() st b1 ==> <*(root-label b2),(root-label b3)*> & P1[b2] & P1[b3] holds
P1[b1 -tree b2,b3]
proof end;

scheme :: BINTREE1:sch 3
s3{ 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 b1 being Function of TS F1(),F2() st
( ( for b2 being Terminal of F1() holds b1 . (root-tree b2) = F3(b2) ) & ( for b2 being NonTerminal of F1()
for b3, b4 being Element of TS F1()
for b5, b6 being Symbol of F1() st b5 = root-label b3 & b6 = root-label b4 & b2 ==> <*b5,b6*> holds
for b7, b8 being Element of F2() st b7 = b1 . b3 & b8 = b1 . b4 holds
b1 . (b2 -tree b3,b4) = F4(b2,b5,b6,b7,b8) ) )
proof end;

scheme :: BINTREE1:sch 4
s4{ 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
E10: ( ( for b1 being Terminal of F1() holds F3() . (root-tree b1) = F5(b1) ) & ( for b1 being NonTerminal of F1()
for b2, b3 being Element of TS F1()
for b4, b5 being Symbol of F1() st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
for b6, b7 being Element of F2() st b6 = F3() . b2 & b7 = F3() . b3 holds
F3() . (b1 -tree b2,b3) = F6(b1,b4,b5,b6,b7) ) ) and
E11: ( ( for b1 being Terminal of F1() holds F4() . (root-tree b1) = F5(b1) ) & ( for b1 being NonTerminal of F1()
for b2, b3 being Element of TS F1()
for b4, b5 being Symbol of F1() st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
for b6, b7 being Element of F2() st b6 = F4() . b2 & b7 = F4() . b3 holds
F4() . (b1 -tree b2,b3) = F6(b1,b4,b5,b6,b7) ) )
proof end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Element of c1;
let c5 be Element of c2;
let c6 be Element of c3;
redefine func [ as [c4,c5,c6] -> Element of [:a1,a2,a3:];
coherence
[c4,c5,c6] is Element of [:c1,c2,c3:] by MCART_1:73;
end;

scheme :: BINTREE1:sch 5
s5{ 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 b1 being Function of TS F1(), Funcs F2(),F3() st
( ( for b2 being Terminal of F1() ex b3 being Function of F2(),F3() st
( b3 = b1 . (root-tree b2) & ( for b4 being Element of F2() holds b3 . b4 = F4(b2,b4) ) ) ) & ( for b2 being NonTerminal of F1()
for b3, b4 being Element of TS F1()
for b5, b6 being Symbol of F1() st b5 = root-label b3 & b6 = root-label b4 & b2 ==> <*b5,b6*> holds
ex b7, b8, b9 being Function of F2(),F3() st
( b7 = b1 . (b2 -tree b3,b4) & b8 = b1 . b3 & b9 = b1 . b4 & ( for b10 being Element of F2() holds b7 . b10 = F5(b2,b8,b9,b10) ) ) ) )
proof end;

scheme :: BINTREE1:sch 6
s6{ 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
E10: ( ( for b1 being Terminal of F1() ex b2 being Function of F2(),F3() st
( b2 = F4() . (root-tree b1) & ( for b3 being Element of F2() holds b2 . b3 = F6(b1,b3) ) ) ) & ( for b1 being NonTerminal of F1()
for b2, b3 being Element of TS F1()
for b4, b5 being Symbol of F1() st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
ex b6, b7, b8 being Function of F2(),F3() st
( b6 = F4() . (b1 -tree b2,b3) & b7 = F4() . b2 & b8 = F4() . b3 & ( for b9 being Element of F2() holds b6 . b9 = F7(b1,b7,b8,b9) ) ) ) ) and
E11: ( ( for b1 being Terminal of F1() ex b2 being Function of F2(),F3() st
( b2 = F5() . (root-tree b1) & ( for b3 being Element of F2() holds b2 . b3 = F6(b1,b3) ) ) ) & ( for b1 being NonTerminal of F1()
for b2, b3 being Element of TS F1()
for b4, b5 being Symbol of F1() st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
ex b6, b7, b8 being Function of F2(),F3() st
( b6 = F5() . (b1 -tree b2,b3) & b7 = F5() . b2 & b8 = F5() . b3 & ( for b9 being Element of F2() holds b6 . b9 = F7(b1,b7,b8,b9) ) ) ) )
proof end;

registration
let c1 be non empty with_terminals with_nonterminals binary DTConstrStr ;
cluster -> binary Element of TS a1;
coherence
for b1 being Element of TS c1 holds b1 is binary
proof end;
end;