environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4, RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1, FINSEQ_2, FUNCOP_1, FUNCT_6, ZFMISC_1, PARTFUN1, MCART_1, NAT_1, ARYTM_3, TREES_A, ARYTM_1, TREES_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, FUNCOP_1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUNCT_1, TREES_1, TREES_2, FUNCOP_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, MCART_1, NAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCOP_1, FUNCT_6, FINSEQ_2, FINSEQ_3, ENUMSET1, TREES_1, TREES_2, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, CARD_1;
schemes NAT_1, CARD_2, XBOOLE_0, FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, FINSEQ_2;
constructors HIDDEN, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, SQUARE_1, NAT_1, FINSEQ_2, FUNCT_6, TREES_2, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TREES_1, TREES_2, BINOP_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, TREES_1, TREES_2;
Lm1:
for n being Nat
for p, q being FinSequence st 1 <= n & n <= len p holds
(p ^ q) . n = p . n
Lm2:
for D being non empty set
for T being DecoratedTree of D holds T is Function of (dom T),D
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 Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
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 )