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