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
begin
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;
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 Th47:
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 ) )
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
for
T1,
T2,
W1,
W2 being
Tree st
tree (
T1,
T2)
= tree (
W1,
W2) holds
(
T1 = W1 &
T2 = W2 )
begin