begin
Lm1:
for n being Element of NAT
for p, q being FinSequence st 1 <= n & n <= len p holds
(p ^ q) . n = p . n
begin
:: deftheorem Def1 defines Trees TREES_3:def 1 :
for b1 being set holds
( b1 = Trees iff for x being set holds
( x in b1 iff x is Tree ) );
:: deftheorem Def2 defines FinTrees TREES_3:def 2 :
for b1 being Subset of Trees holds
( b1 = FinTrees iff for x being set holds
( x in b1 iff x is finite Tree ) );
:: deftheorem Def3 defines constituted-Trees TREES_3:def 3 :
for IT being set holds
( IT is constituted-Trees iff for x being set st x in IT holds
x is Tree );
:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :
for IT being set holds
( IT is constituted-FinTrees iff for x being set st x in IT holds
x is finite Tree );
:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :
for IT being set holds
( IT is constituted-DTrees iff for x being set st x in IT holds
x is DecoratedTree );
theorem
theorem
theorem Th3:
theorem
theorem
theorem Th6:
theorem
theorem
theorem Th9:
theorem
theorem
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem
:: deftheorem Def6 defines DTree-set TREES_3:def 6 :
for D being non empty set
for b2 being set holds
( b2 is DTree-set of D iff for x being set st x in b2 holds
x is DecoratedTree of D );
:: deftheorem Def7 defines Trees TREES_3:def 7 :
for D being non empty set
for b2 being DTree-set of D holds
( b2 = Trees D iff for T being DecoratedTree of D holds T in b2 );
:: deftheorem Def8 defines FinTrees TREES_3:def 8 :
for D being non empty set
for b2 being DTree-set of D holds
( b2 = FinTrees D iff for T being DecoratedTree of D holds
( dom T is finite iff T in b2 ) );
theorem
begin
:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :
for IT being Function holds
( IT is Tree-yielding iff rng IT is constituted-Trees );
:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :
for IT being Function holds
( IT is FinTree-yielding iff rng IT is constituted-FinTrees );
:: deftheorem Def11 defines DTree-yielding TREES_3:def 11 :
for IT being Function holds
( IT is DTree-yielding iff rng IT is constituted-DTrees );
theorem
canceled;
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
Lm2:
for D being non empty set
for T being DecoratedTree of D holds T is Function of (dom T),D
begin
definition
let D1,
D2 be non
empty set ;
pr1redefine func pr1 (
D1,
D2)
-> Function of
[:D1,D2:],
D1;
coherence
pr1 (D1,D2) is Function of [:D1,D2:],D1
pr2redefine func pr2 (
D1,
D2)
-> Function of
[:D1,D2:],
D2;
coherence
pr2 (D1,D2) is Function of [:D1,D2:],D2
end;
:: deftheorem defines `1 TREES_3:def 12 :
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds T `1 = (pr1 (D1,D2)) * T;
:: deftheorem defines `2 TREES_3:def 13 :
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds T `2 = (pr2 (D1,D2)) * T;
theorem Th41:
theorem
:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :
for T being finite Tree
for b2 being Tree holds
( b2 is T-Substitution of T iff for t being Element of b2 holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) );
theorem
theorem
Lm3:
for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
begin
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th50:
for
T1,
T2 being
Tree for
p being
Element of
T1 \/ T2 holds
( (
p in T1 &
p in T2 implies
(T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) & ( not
p in T1 implies
(T1 \/ T2) | p = T2 | p ) & ( not
p in T2 implies
(T1 \/ T2) | p = T1 | p ) )
:: deftheorem Def15 defines tree TREES_3:def 15 :
for p being FinSequence st p is Tree-yielding holds
for b2 being Tree holds
( b2 = tree p iff for x being set holds
( x in b2 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) );
:: deftheorem defines ^ TREES_3:def 16 :
for T being Tree holds ^ T = tree <*T*>;
:: deftheorem defines tree TREES_3:def 17 :
for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>;
theorem
theorem Th52:
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem
theorem
theorem Th63:
theorem Th64:
theorem
theorem
for
T1,
T2 being
Tree st
T1 c= T2 holds
^ T1 c= ^ T2
theorem
for
T1,
T2 being
Tree st
^ T1 = ^ T2 holds
T1 = T2
theorem
theorem
theorem
theorem Th71:
theorem Th72:
theorem Th73:
theorem
theorem
theorem
for
T1,
T2,
W1,
W2 being
Tree st
tree (
T1,
T2)
= tree (
W1,
W2) holds
(
T1 = W1 &
T2 = W2 )
theorem
theorem
theorem
theorem Th80:
theorem Th81:
theorem Th82:
theorem
theorem
begin
:: deftheorem defines roots TREES_3:def 18 :
for p being FinSequence st p is DTree-yielding holds
for b2 being FinSequence holds
( b2 = roots p iff ( dom b2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b2 . i = T . {} ) ) ) );