Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Sets and Functions of Trees and Joining Operations of Trees

by
Grzegorz Bancerek

MML identifier: TREES_3
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FUNCT_1, RELAT_1, FINSET_1, MCART_1, TREES_1, TREES_2,
BOOLE, FUNCT_2, TARSKI, FINSEQ_2, FUNCOP_1, FUNCT_6, PARTFUN1, FUNCT_3,
ARYTM_1, SQUARE_1, TREES_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, SQUARE_1,
FUNCOP_1, RELSET_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2,
FUNCT_6;
constructors FUNCT_5, NAT_1, DOMAIN_1, SQUARE_1, FUNCT_3, FINSEQ_2, TREES_2,
FUNCT_6, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSEQ_1, TREES_1, TREES_2, FINSET_1, RELSET_1, CARD_1,
XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin :: Finite sets

reserve x,y,z for set, i,k,n for Nat, p,q,r,s for FinSequence,
w for FinSequence of NAT, X,Y for set, f for Function;

begin :: Sets of trees

definition
func Trees -> set means
:: TREES_3:def 1
x in it iff x is Tree;
end;

definition
cluster Trees -> non empty;
end;

definition
func FinTrees -> Subset of Trees means
:: TREES_3:def 2

x in it iff x is finite Tree;
end;

definition
cluster FinTrees -> non empty;
end;

definition let IT be set;
attr IT is constituted-Trees means
:: TREES_3:def 3

for x st x in IT holds x is Tree;
attr IT is constituted-FinTrees means
:: TREES_3:def 4

for x st x in IT holds x is finite Tree;
attr IT is constituted-DTrees means
:: TREES_3:def 5

for x st x in IT holds x is DecoratedTree;
end;

theorem :: TREES_3:1
X is constituted-Trees iff X c= Trees;

theorem :: TREES_3:2
X is constituted-FinTrees iff X c= FinTrees;

theorem :: TREES_3:3
X is constituted-Trees & Y is constituted-Trees iff X \/
Y is constituted-Trees;

theorem :: TREES_3:4
X is constituted-Trees & Y is constituted-Trees implies
X \+\ Y is constituted-Trees;

theorem :: TREES_3:5
X is constituted-Trees implies X /\ Y is constituted-Trees &
Y /\ X is constituted-Trees & X \ Y is constituted-Trees;

theorem :: TREES_3:6
X is constituted-FinTrees & Y is constituted-FinTrees iff
X \/ Y is constituted-FinTrees;

theorem :: TREES_3:7
X is constituted-FinTrees & Y is constituted-FinTrees implies
X \+\ Y is constituted-FinTrees;

theorem :: TREES_3:8
X is constituted-FinTrees implies X /\ Y is constituted-FinTrees &
Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees;

theorem :: TREES_3:9
X is constituted-DTrees & Y is constituted-DTrees iff
X \/ Y is constituted-DTrees;

theorem :: TREES_3:10
X is constituted-DTrees & Y is constituted-DTrees implies
X \+\ Y is constituted-DTrees;

theorem :: TREES_3:11
X is constituted-DTrees implies X /\ Y is constituted-DTrees &
Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees;

theorem :: TREES_3:12
{} is constituted-Trees constituted-FinTrees constituted-DTrees;

theorem :: TREES_3:13
{x} is constituted-Trees iff x is Tree;

theorem :: TREES_3:14
{x} is constituted-FinTrees iff x is finite Tree;

theorem :: TREES_3:15
{x} is constituted-DTrees iff x is DecoratedTree;

theorem :: TREES_3:16
{x,y} is constituted-Trees iff x is Tree & y is Tree;

theorem :: TREES_3:17
{x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:18
{x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:19
X is constituted-Trees & Y c= X implies Y is constituted-Trees;

theorem :: TREES_3:20
X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees;

theorem :: TREES_3:21
X is constituted-DTrees & Y c= X implies Y is constituted-DTrees;

definition
cluster finite constituted-Trees constituted-FinTrees non empty set;
cluster finite constituted-DTrees non empty set;
end;

definition
cluster constituted-FinTrees -> constituted-Trees set;
end;

definition let X be constituted-Trees set;
cluster -> constituted-Trees Subset of X;
end;

definition let X be constituted-FinTrees set;
cluster -> constituted-FinTrees Subset of X;
end;

definition let X be constituted-DTrees set;
cluster -> constituted-DTrees Subset of X;
end;

definition
let D be constituted-Trees non empty set;
redefine mode Element of D -> Tree;
end;

definition
let D be constituted-FinTrees non empty set;
redefine mode Element of D -> finite Tree;
end;

definition
let D be constituted-DTrees non empty set;
redefine mode Element of D -> DecoratedTree;
end;

definition
cluster Trees -> constituted-Trees;
end;

definition
cluster constituted-FinTrees non empty Subset of Trees;
end;

definition
cluster FinTrees -> constituted-FinTrees;
end;

definition let D be non empty set;
mode DTree-set of D -> set means
:: TREES_3:def 6

for x st x in it holds x is DecoratedTree of D;
end;

definition let D be non empty set;
cluster -> constituted-DTrees DTree-set of D;
end;

definition let D be non empty set;
cluster finite non empty DTree-set of D;
end;

definition let D be non empty set, E be non empty DTree-set of D;
redefine mode Element of E -> DecoratedTree of D;
end;

definition let T be Tree, D be non empty set;
redefine func Funcs(T,D) -> non empty DTree-set of D;
mode Relation of T,D -> ParametrizedSubset of D;
end;

definition let T be Tree, D be non empty set;
cluster -> DecoratedTree-like Function of T,D;
end;

definition
let D be non empty set;
func Trees(D) -> DTree-set of D means
:: TREES_3:def 7

for T being DecoratedTree of D holds T in it;
end;

definition
let D be non empty set;
cluster Trees(D) -> non empty;
end;

definition let D be non empty set;
func FinTrees(D) -> DTree-set of D means
:: TREES_3:def 8
for T being DecoratedTree of D holds dom T is finite iff T in it;
end;

definition let D be non empty set;
cluster FinTrees D -> non empty;
end;

theorem :: TREES_3:22
for D being non empty set holds FinTrees D c= Trees D;

begin :: Functions yielding trees

definition let IT be Function;
attr IT is Tree-yielding means
:: TREES_3:def 9

rng IT is constituted-Trees;
attr IT is FinTree-yielding means
:: TREES_3:def 10

rng IT is constituted-FinTrees;
attr IT is DTree-yielding means
:: TREES_3:def 11

rng IT is constituted-DTrees;
end;

theorem :: TREES_3:23
{} is Tree-yielding FinTree-yielding DTree-yielding;

theorem :: TREES_3:24
f is Tree-yielding iff for x st x in dom f holds f.x is Tree;

theorem :: TREES_3:25
f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree;

theorem :: TREES_3:26
f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree;

theorem :: TREES_3:27
p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding;

theorem :: TREES_3:28
p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding;

theorem :: TREES_3:29
p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding;

theorem :: TREES_3:30
<*x*> is Tree-yielding iff x is Tree;

theorem :: TREES_3:31
<*x*> is FinTree-yielding iff x is finite Tree;

theorem :: TREES_3:32
<*x*> is DTree-yielding iff x is DecoratedTree;

theorem :: TREES_3:33
<*x,y*> is Tree-yielding iff x is Tree & y is Tree;

theorem :: TREES_3:34
<*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:35
<*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:36
i <> 0 implies (i |-> x is Tree-yielding iff x is Tree);

theorem :: TREES_3:37
i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree);

theorem :: TREES_3:38
i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree);

definition
cluster Tree-yielding FinTree-yielding non empty FinSequence;
cluster DTree-yielding non empty FinSequence;
end;

definition
cluster Tree-yielding FinTree-yielding non empty Function;
cluster DTree-yielding non empty Function;
end;

definition
cluster FinTree-yielding -> Tree-yielding Function;
end;

definition
let D be constituted-Trees non empty set;
cluster -> Tree-yielding FinSequence of D;
end;

definition let p,q be Tree-yielding FinSequence;
cluster p^q -> Tree-yielding;
end;

definition
let D be constituted-FinTrees non empty set;
cluster -> FinTree-yielding FinSequence of D;
end;

definition let p,q be FinTree-yielding FinSequence;
cluster p^q -> FinTree-yielding;
end;

definition
let D be constituted-DTrees non empty set;
cluster -> DTree-yielding FinSequence of D;
end;

definition let p,q be DTree-yielding FinSequence;
cluster p^q -> DTree-yielding;
end;

definition let T be Tree;
cluster <*T*> -> Tree-yielding non empty;
let S be Tree;
cluster <*T,S*> -> Tree-yielding non empty;
end;

definition let n be Nat, T be Tree;
cluster n |-> T -> Tree-yielding;
end;

definition let T be finite Tree;
cluster <*T*> -> FinTree-yielding;
let S be finite Tree;
cluster <*T,S*> -> FinTree-yielding;
end;

definition let n be Nat, T be finite Tree;
cluster n |-> T -> FinTree-yielding;
end;

definition let T be DecoratedTree;
cluster <*T*> -> DTree-yielding non empty;
let S be DecoratedTree;
cluster <*T,S*> -> DTree-yielding non empty;
end;

definition let n be Nat, T be DecoratedTree;
cluster n |-> T -> DTree-yielding;
end;

theorem :: TREES_3:39
for f being DTree-yielding Function holds dom doms f = dom f &
doms f is Tree-yielding;

definition let p be DTree-yielding FinSequence;
cluster doms p -> Tree-yielding FinSequence-like;
end;

theorem :: TREES_3:40
for p being DTree-yielding FinSequence holds len doms p = len p;

begin :: Trees decorated by Cartesian product and structure of substitution

definition let D,E be non empty set;
mode DecoratedTree of D,E is DecoratedTree of [:D,E:];
mode DTree-set of D,E is DTree-set of [:D,E:];
end;

definition let T1,T2 be DecoratedTree;
cluster <:T1,T2:> -> DecoratedTree-like;
end;

definition let D1,D2 be non empty set;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
redefine func <:T1,T2:> -> DecoratedTree of D1,D2;
end;

definition let D,E be non empty set;
let T be DecoratedTree of D;
let f be Function of D,E;
redefine func f*T -> DecoratedTree of E;
end;

definition let D1,D2 be non empty set; redefine
func pr1(D1,D2) -> Function of [:D1,D2:], D1;
func pr2(D1,D2) -> Function of [:D1,D2:], D2;
end;

definition let D1,D2 be non empty set, T be DecoratedTree of D1,D2;
func T`1 -> DecoratedTree of D1 equals
:: TREES_3:def 12
pr1(D1,D2)*T;
func T`2 -> DecoratedTree of D2 equals
:: TREES_3:def 13
pr2(D1,D2)*T;
end;

theorem :: TREES_3:41
for D1,D2 being non empty set, T being DecoratedTree of D1,D2,
t being Element of dom T holds (T.t)`1 = T`1.t & T`2.t = (T.t)`2;

theorem :: TREES_3:42
for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds
<:T`1,T`2:> = T;

definition let T be finite Tree;
cluster Leaves T -> finite non empty;
end;

definition let T be Tree, S be non empty Subset of T;
redefine mode Element of S -> Element of T;
end;

definition let T be finite Tree;
redefine mode Leaf of T -> Element of Leaves T;
end;

definition
let T be finite Tree;
mode T-Substitution of T -> Tree means
:: TREES_3:def 14

for t being Element of it holds t in T or
ex l being Leaf of T st l is_a_proper_prefix_of t;
end;

definition let T be finite Tree, t be Leaf of T, S be Tree;
redefine func T with-replacement (t,S) -> T-Substitution of T;
end;

definition let T be finite Tree;
cluster finite T-Substitution of T;
end;

definition let n;
mode T-Substitution of n is T-Substitution of elementary_tree n;
end;

theorem :: TREES_3:43
for T being Tree holds T is T-Substitution of 0;

theorem :: TREES_3:44
for T1, T2 being Tree st T1-level 1 c= T2-level 1 &
for n st <*n*> in T1 holds T1|<*n*> = T2|<*n*> holds T1 c= T2;

begin :: Joining of trees

canceled;

theorem :: TREES_3:46
for T,T' being Tree, p being FinSequence of NAT st
p in Leaves T holds T c= T with-replacement (p,T');

theorem :: TREES_3:47
for T,T' being DecoratedTree, p being Element of dom T holds
(T with-replacement (p,T')).p = T'.{};

theorem :: TREES_3:48
for T,T' being DecoratedTree, p,q being Element of dom T st
not p is_a_prefix_of q holds (T with-replacement (p,T')).q = T.q;

theorem :: TREES_3:49
for T,T' being DecoratedTree, p being Element of dom T,
q being Element of dom T' holds (T with-replacement (p,T')).(p^q) = T'.q;

definition let T1,T2 be Tree;
cluster T1 \/ T2 -> non empty Tree-like;
end;

theorem :: TREES_3:50
for T1,T2 being Tree, 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);

definition let p such that
p is Tree-yielding;
func tree p -> Tree means
:: TREES_3:def 15

x in it iff x = {} or ex n,q st n < len p & q in p.(n+1) & x = <*n*>^q;
end;

definition let T be Tree;
func ^T -> Tree equals
:: TREES_3:def 16

tree<*T*>;
end;

definition let T1,T2 be Tree;
func tree(T1,T2) -> Tree equals
:: TREES_3:def 17

tree(<*T1,T2*>);
end;

theorem :: TREES_3:51
p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+1))
;

theorem :: TREES_3:52
p is Tree-yielding implies
tree(p)-level 1 = {<*n*>: n < len p} &
for n st n < len p holds (tree(p))|<*n*> = p.(n+1);

theorem :: TREES_3:53
for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q;

theorem :: TREES_3:54
for p1,p2 being Tree-yielding FinSequence, T being Tree holds
p in T iff <*len p1*>^p in tree(p1^<*T*>^p2);

theorem :: TREES_3:55
tree({}) = elementary_tree 0;

theorem :: TREES_3:56
p is Tree-yielding implies elementary_tree len p c= tree(p);

theorem :: TREES_3:57
elementary_tree i = tree(i|->elementary_tree 0);

theorem :: TREES_3:58
for T being Tree, p being Tree-yielding FinSequence holds
tree(p^<*T*>) = (tree(p) \/ elementary_tree (len p + 1))
with-replacement (<*len p*>, T);

theorem :: TREES_3:59
for p being Tree-yielding FinSequence holds
tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1);

theorem :: TREES_3:60
for p, q being Tree-yielding FinSequence for T1,T2 be Tree holds
tree(p^<*T1*>^q) = tree(p^<*T2*>^q) with-replacement(<*len p*>,T1);

theorem :: TREES_3:61
for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T);

theorem :: TREES_3:62
for T1,T2 being Tree holds
tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1))
with-replacement (<*1*>, T2);

definition let p be FinTree-yielding FinSequence;
cluster tree(p) -> finite;
end;

definition let T be finite Tree;
cluster ^T -> finite;
end;

definition let T1,T2 be finite Tree;
cluster tree(T1,T2) -> finite;
end;

theorem :: TREES_3:63
for T being Tree, x being set holds x in ^T iff x = {} or
ex p st p in T & x = <*0*>^p;

theorem :: TREES_3:64
for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T;

theorem :: TREES_3:65
for T being Tree holds elementary_tree 1 c= ^T;

theorem :: TREES_3:66
for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2;

theorem :: TREES_3:67
for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2;

theorem :: TREES_3:68
for T being Tree holds (^T)|<*0*> = T;

theorem :: TREES_3:69
for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2;

theorem :: TREES_3:70
^elementary_tree 0 = elementary_tree 1;

theorem :: TREES_3:71
for T1,T2 being Tree, x being set holds x in tree(T1,T2) iff x = {} or
ex p st p in T1 & x = <*0*>^p or p in T2 & x = <*1*>^p;

theorem :: TREES_3:72
for T1,T2 being Tree, p being FinSequence holds
p in T1 iff <*0*>^p in tree(T1,T2);

theorem :: TREES_3:73
for T1,T2 being Tree, p being FinSequence holds
p in T2 iff <*1*>^p in tree(T1,T2);

theorem :: TREES_3:74
for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2);

theorem :: TREES_3:75
for T1,T2, W1,W2 being Tree st T1 c= W1 & T2 c= W2 holds
tree(T1,T2) c= tree(W1,W2);

theorem :: TREES_3:76
for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds
T1 = W1 & T2 = W2;

theorem :: TREES_3:77
for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2;

theorem :: TREES_3:78
for T,T1,T2 being Tree holds
tree(T1,T2) with-replacement (<*0*>, T) = tree(T,T2) &
tree(T1,T2) with-replacement (<*1*>, T) = tree(T1,T);

theorem :: TREES_3:79
tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2;

reserve w for FinTree-yielding FinSequence;

theorem :: TREES_3:80
for w st for t being finite Tree st t in rng w holds height t <= n holds
height tree(w) <= n+1;

theorem :: TREES_3:81
for t being finite Tree st t in rng w holds height tree(w) > height t;

theorem :: TREES_3:82
for t being finite Tree st t in rng w &
for t' being finite Tree st t' in rng w holds height t' <= height t holds
height tree(w) = (height t) + 1;

theorem :: TREES_3:83
for T being finite Tree holds height ^T = (height T) + 1;

theorem :: TREES_3:84
for T1,T2 being finite Tree holds
height tree(T1,T2) = max(height T1, height T2)+1;

```