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 :
:: deftheorem Def3 defines constituted-Trees TREES_3:def 3 :
:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :
:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :
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 :
:: deftheorem Def7 defines Trees TREES_3:def 7 :
:: deftheorem Def8 defines FinTrees TREES_3:def 8 :
theorem
begin
:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :
:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :
:: deftheorem Def11 defines DTree-yielding TREES_3:def 11 :
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
Lm3:
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 :
:: deftheorem defines `2 TREES_3:def 13 :
theorem Th41:
theorem
:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :
theorem
theorem
Lm4:
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 :
:: deftheorem defines ^ TREES_3:def 16 :
:: deftheorem defines tree TREES_3:def 17 :
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 :