Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Introduction to Trees

by
Grzegorz Bancerek

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

```environ

vocabulary FUNCT_1, FINSEQ_1, RELAT_1, BOOLE, ARYTM_1, FINSET_1, CARD_1,
ZFMISC_1, TARSKI, ORDINAL2, TREES_1;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, NUMBERS,
RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, CARD_1;
constructors REAL_1, NAT_1, FINSEQ_1, WELLORD2, XREAL_0, MEMBERED, XBOOLE_0;
clusters RELSET_1, FINSEQ_1, CARD_1, FINSET_1, NAT_1, XREAL_0, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin

reserve D for non empty set,
X,x,y,z for set,
k,n,m for Nat,
f for Function,
p,q,r for FinSequence of NAT;

::
::  Auxiliary theorems on finite sequence
::

theorem :: TREES_1:1
for p,q being FinSequence st q = p|Seg n holds len q <= n;

theorem :: TREES_1:2
for p,q being FinSequence st q = p|Seg n holds len q <= len p;

theorem :: TREES_1:3
for p,r being FinSequence st r = p|Seg n
ex q being FinSequence st p = r^q;

theorem :: TREES_1:4
{} <> <*x*>;

theorem :: TREES_1:5
for p,q being FinSequence st p = p^q or p = q^p holds q = {};

theorem :: TREES_1:6
for p,q being FinSequence st p^q = <*x*> holds
p = <*x*> & q = {} or p = {} & q = <*x*>;

::
:: Relations "is a prefix of", "is a proper prefix of" and
:: "are comparable" of finite sequences
::

definition let p,q be FinSequence;
redefine pred p c= q means
:: TREES_1:def 1
ex n st p = q|Seg n;
synonym p is_a_prefix_of q;
end;

canceled;

theorem :: TREES_1:8
for p,q being FinSequence holds p is_a_prefix_of q iff
ex r being FinSequence st q = p^r;

canceled 6;

theorem :: TREES_1:15
for p,q being FinSequence st
p is_a_prefix_of q & len p = len q holds p = q;

theorem :: TREES_1:16
<*x*> is_a_prefix_of <*y*> iff x = y;

definition let p,q be FinSequence;
redefine pred p c< q;
synonym p is_a_proper_prefix_of q;
end;

canceled 2;

theorem :: TREES_1:19
for p,q being finite set st
p,q are_c=-comparable & card p = card q holds
p = q;

reserve p1,p2,p3 for FinSequence;

canceled 3;

theorem :: TREES_1:23
<*x*>,<*y*> are_c=-comparable iff x = y;

theorem :: TREES_1:24
for p,q being finite set st p c< q holds card p < card q;

theorem :: TREES_1:25 :: BOOLE
not ex p being FinSequence st
p is_a_proper_prefix_of {} or p is_a_proper_prefix_of <*>D;

theorem :: TREES_1:26 :: BOOLE
not ex p,q being FinSequence st
p is_a_proper_prefix_of q & q is_a_proper_prefix_of p;

theorem :: TREES_1:27
for p,q,r being FinSequence st
p is_a_proper_prefix_of q & q is_a_proper_prefix_of r or
p is_a_proper_prefix_of q & q is_a_prefix_of r or
p is_a_prefix_of q & q is_a_proper_prefix_of r holds
p is_a_proper_prefix_of r;

theorem :: TREES_1:28 :: BOOLE
p1 is_a_prefix_of p2 implies not p2 is_a_proper_prefix_of p1;

canceled;

theorem :: TREES_1:30
p1^<*x*> is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2;

theorem :: TREES_1:31
p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2^<*x*>;

theorem :: TREES_1:32
p1 is_a_proper_prefix_of p2^<*x*> implies p1 is_a_prefix_of p2;

theorem :: TREES_1:33
{} is_a_proper_prefix_of p2 or {} <> p2 implies
p1 is_a_proper_prefix_of p1^p2;

::
:: The set of proper prefixes of a finite sequence
::

definition let p be FinSequence;
canceled 2;

func ProperPrefixes p -> set means
:: TREES_1:def 4
x in
it iff ex q being FinSequence st x = q & q is_a_proper_prefix_of p;
end;

canceled;

theorem :: TREES_1:35
for p being FinSequence st x in ProperPrefixes p holds x is FinSequence;

theorem :: TREES_1:36
for p,q being FinSequence holds
p in ProperPrefixes q iff p is_a_proper_prefix_of q;

theorem :: TREES_1:37
for p,q being FinSequence st p in ProperPrefixes q holds len p < len q;

theorem :: TREES_1:38
for p,q,r being FinSequence st q^r in ProperPrefixes p holds
q in ProperPrefixes p;

theorem :: TREES_1:39
ProperPrefixes {} = {};

theorem :: TREES_1:40
ProperPrefixes <*x*> = { {} };

theorem :: TREES_1:41
for p,q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q;

theorem :: TREES_1:42
for p,q,r being FinSequence st
q in ProperPrefixes p & r in ProperPrefixes p holds q,r are_c=-comparable;

::
::  Trees and their properties
::

definition let X;
attr X is Tree-like means
:: TREES_1:def 5
X c= NAT* & (for p st p in X holds ProperPrefixes p c= X) &
for p,k,n st p^<*k*> in X & n <= k holds p^<*n*> in X;
end;

definition
cluster non empty Tree-like set;
end;

definition
mode Tree is Tree-like non empty set;
end;

reserve T,T1 for Tree;

canceled;

theorem :: TREES_1:44
x in T implies x is FinSequence of NAT;

definition let T;
redefine mode Element of T -> FinSequence of NAT;
end;

theorem :: TREES_1:45
for p,q being FinSequence st p in T & q is_a_prefix_of p holds q in T;

theorem :: TREES_1:46
for r being FinSequence st q^r in T holds q in T;

theorem :: TREES_1:47
{} in T & <*> NAT in T;

theorem :: TREES_1:48
{ {} } is Tree;

theorem :: TREES_1:49
T \/ T1 is Tree;

theorem :: TREES_1:50
T /\ T1 is Tree;

::
::  Finite trees and their properties
::

definition
cluster finite Tree;
end;

reserve fT,fT1 for finite Tree;

canceled;

theorem :: TREES_1:52
fT \/ fT1 is finite Tree;

theorem :: TREES_1:53
fT /\ T is finite Tree & T /\ fT is finite Tree;

::
::  Elementary trees
::

definition let n;
canceled;

func elementary_tree n -> finite Tree equals
:: TREES_1:def 7
{ <*k*> : k < n } \/ { {} };
end;

canceled;

theorem :: TREES_1:55
k < n implies <*k*> in elementary_tree n;

theorem :: TREES_1:56
elementary_tree 0 = { {} };

theorem :: TREES_1:57
p in elementary_tree n implies p = {} or ex k st k < n & p = <*k*>;

::
::  Leaves and subtrees
::

definition let T;
func Leaves T -> Subset of T means
:: TREES_1:def 8
p in it iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;
let p such that
p in T;
func T|p -> Tree means
:: TREES_1:def 9  :: subtree of T, which root is in p
q in it iff p^q in T;
end;

canceled 2;

theorem :: TREES_1:60
T|(<*> NAT) = T;

definition let T be finite Tree; let p be Element of T;
cluster T|p -> finite;
end;

definition let T;
assume  Leaves T <> {};
mode Leaf of T -> Element of T means
:: TREES_1:def 10
it in Leaves T;
end;

definition let T;
mode Subtree of T -> Tree means
:: TREES_1:def 11
ex p being Element of T st it = T|p;
end;

reserve t for Element of T;

definition let T,p,T1;
assume
p in T;
func T with-replacement (p,T1) -> Tree means
:: TREES_1:def 12
q in it iff q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r;
end;

canceled 3;

theorem :: TREES_1:64
p in T implies T with-replacement (p,T1) =
{ t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/
{ p^s where s is Element of T1 : s = s };

canceled;

theorem :: TREES_1:66
p in T implies T1 = T with-replacement (p,T1)|p;

definition let T be finite Tree, t be Element of T;
let T1 be finite Tree;
cluster T with-replacement (t,T1) -> finite;
end;

reserve w for FinSequence;

theorem :: TREES_1:67
for p being FinSequence holds ProperPrefixes p,dom p are_equipotent;

definition let p be FinSequence;
cluster ProperPrefixes p -> finite;
end;

theorem :: TREES_1:68
for p being FinSequence holds card ProperPrefixes p = len p;

::
::  Height and width of finite trees
::

definition let IT be set;
attr IT is AntiChain_of_Prefixes-like means
:: TREES_1:def 13
(for x st x in IT holds x is FinSequence) &
for p1,p2 st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable;
end;

definition
cluster AntiChain_of_Prefixes-like set;
end;

definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set;
end;

canceled;

theorem :: TREES_1:70
{ w } is AntiChain_of_Prefixes-like;

theorem :: TREES_1:71
not p1,p2 are_c=-comparable implies
{ p1,p2 } is AntiChain_of_Prefixes-like;

definition let T;
mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means
:: TREES_1:def 14
it c= T;
end;

reserve t1,t2 for Element of T;

canceled;

theorem :: TREES_1:73
{} is AntiChain_of_Prefixes of T & { {} } is AntiChain_of_Prefixes of T;

theorem :: TREES_1:74
{ t } is AntiChain_of_Prefixes of T;

theorem :: TREES_1:75
not t1,t2 are_c=-comparable implies { t1,t2 } is AntiChain_of_Prefixes of T
;

definition let T be finite Tree;
cluster -> finite AntiChain_of_Prefixes of T;
end;

definition let T be finite Tree;
func height T -> Nat means
:: TREES_1:def 15
(ex p st p in T & len p = it) & for p st p in T holds len p <= it;
func width T -> Nat means
:: TREES_1:def 16
ex X being AntiChain_of_Prefixes of T st it = card X &
for Y being AntiChain_of_Prefixes of T holds card Y <= card X;
end;

canceled 2;

theorem :: TREES_1:78
1 <= width fT;

theorem :: TREES_1:79
height elementary_tree 0 = 0;

theorem :: TREES_1:80
height fT = 0 implies fT = elementary_tree 0;

theorem :: TREES_1:81
height elementary_tree(n+1) = 1;

theorem :: TREES_1:82
width elementary_tree 0 = 1;

theorem :: TREES_1:83
width elementary_tree(n+1) = n+1;

theorem :: TREES_1:84
for t being Element of fT holds height(fT|t) <= height fT;

theorem :: TREES_1:85
for t being Element of fT st t <> {} holds height(fT|t) < height fT;

scheme Tree_Ind { P[Tree] }:
for fT holds P[fT]
provided
for fT st for n st <*n*> in fT holds P[fT|<*n*>] holds P[fT];
```