:: Introduction to Trees
:: by Grzegorz Bancerek
::
:: Received October 25, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
notation
let
p
,
q
be
FinSequence
;
synonym
p
is_a_prefix_of
q
for
p
c=
q
;
end;
definition
let
p
,
q
be
FinSequence
;
redefine
pred
p
c=
q
means
:
Def1
:
:: TREES_1:def 1
ex
n
being
Element
of
NAT
st
p
=
q
|
(
Seg
n
)
;
compatibility
(
p
is_a_prefix_of
q
iff ex
n
being
Element
of
NAT
st
p
=
q
|
(
Seg
n
)
)
proof
end;
end;
::
deftheorem
Def1
defines
is_a_prefix_of
TREES_1:def 1 :
for
p
,
q
being
FinSequence
holds
(
p
is_a_prefix_of
q
iff ex
n
being
Element
of
NAT
st
p
=
q
|
(
Seg
n
)
);
theorem
Th1
:
:: TREES_1:1
for
p
,
q
being
FinSequence
holds
(
p
is_a_prefix_of
q
iff ex
r
being
FinSequence
st
q
=
p
^
r
)
proof
end;
theorem
Th2
:
:: TREES_1:2
for
p
,
q
being
FinSequence
st
p
is_a_prefix_of
q
&
len
p
=
len
q
holds
p
=
q
proof
end;
theorem
Th3
:
:: TREES_1:3
for
x
,
y
being
set
holds
(
<*
x
*>
is_a_prefix_of
<*
y
*>
iff
x
=
y
)
proof
end;
notation
let
p
,
q
be
FinSequence
;
synonym
p
is_a_proper_prefix_of
q
for
p
c<
q
;
end;
Lm1
:
for
A
,
B
being
finite
set
st
A
c=
B
&
card
A
=
card
B
holds
A
=
B
proof
end;
theorem
Th4
:
:: TREES_1:4
for
p
,
q
being
finite
set
st
p
,
q
are_c=-comparable
&
card
p
=
card
q
holds
p
=
q
proof
end;
theorem
Th5
:
:: TREES_1:5
for
x
,
y
being
set
st
<*
x
*>
,
<*
y
*>
are_c=-comparable
holds
x
=
y
proof
end;
theorem
Th6
:
:: TREES_1:6
for
p
,
q
being
finite
set
st
p
c<
q
holds
card
p
<
card
q
proof
end;
theorem
Th7
:
:: TREES_1:7
for
x
being
set
for
p1
,
p2
being
FinSequence
st
p1
^
<*
x
*>
is_a_prefix_of
p2
holds
p1
is_a_proper_prefix_of
p2
proof
end;
theorem
Th8
:
:: TREES_1:8
for
x
being
set
for
p1
,
p2
being
FinSequence
st
p1
is_a_prefix_of
p2
holds
p1
is_a_proper_prefix_of
p2
^
<*
x
*>
proof
end;
theorem
Th9
:
:: TREES_1:9
for
x
being
set
for
p1
,
p2
being
FinSequence
st
p1
is_a_proper_prefix_of
p2
^
<*
x
*>
holds
p1
is_a_prefix_of
p2
proof
end;
theorem
:: TREES_1:10
for
p2
,
p1
being
FinSequence
st (
{}
is_a_proper_prefix_of
p2
or
{}
<>
p2
) holds
p1
is_a_proper_prefix_of
p1
^
p2
proof
end;
::
:: The set of proper prefixes of a finite sequence
::
definition
let
p
be
FinSequence
;
func
ProperPrefixes
p
->
set
means
:
Def2
:
:: TREES_1:def 2
for
x
being
set
holds
(
x
in
it
iff ex
q
being
FinSequence
st
(
x
=
q
&
q
is_a_proper_prefix_of
p
) );
existence
ex
b
1
being
set
st
for
x
being
set
holds
(
x
in
b
1
iff ex
q
being
FinSequence
st
(
x
=
q
&
q
is_a_proper_prefix_of
p
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
x
being
set
holds
(
x
in
b
1
iff ex
q
being
FinSequence
st
(
x
=
q
&
q
is_a_proper_prefix_of
p
) ) ) & ( for
x
being
set
holds
(
x
in
b
2
iff ex
q
being
FinSequence
st
(
x
=
q
&
q
is_a_proper_prefix_of
p
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
ProperPrefixes
TREES_1:def 2 :
for
p
being
FinSequence
for
b
2
being
set
holds
(
b
2
=
ProperPrefixes
p
iff for
x
being
set
holds
(
x
in
b
2
iff ex
q
being
FinSequence
st
(
x
=
q
&
q
is_a_proper_prefix_of
p
) ) );
theorem
Th11
:
:: TREES_1:11
for
x
being
set
for
p
being
FinSequence
st
x
in
ProperPrefixes
p
holds
x
is
FinSequence
proof
end;
theorem
Th12
:
:: TREES_1:12
for
p
,
q
being
FinSequence
holds
(
p
in
ProperPrefixes
q
iff
p
is_a_proper_prefix_of
q
)
proof
end;
theorem
Th13
:
:: TREES_1:13
for
p
,
q
being
FinSequence
st
p
in
ProperPrefixes
q
holds
len
p
<
len
q
proof
end;
theorem
:: TREES_1:14
for
p
,
q
,
r
being
FinSequence
st
q
^
r
in
ProperPrefixes
p
holds
q
in
ProperPrefixes
p
proof
end;
theorem
Th15
:
:: TREES_1:15
ProperPrefixes
{}
=
{}
proof
end;
set
D
=
{
{}
}
;
theorem
Th16
:
:: TREES_1:16
for
x
being
set
holds
ProperPrefixes
<*
x
*>
=
{
{}
}
proof
end;
theorem
:: TREES_1:17
for
p
,
q
being
FinSequence
st
p
is_a_prefix_of
q
holds
ProperPrefixes
p
c=
ProperPrefixes
q
proof
end;
theorem
Th18
:
:: TREES_1:18
for
p
,
q
,
r
being
FinSequence
st
q
in
ProperPrefixes
p
&
r
in
ProperPrefixes
p
holds
q
,
r
are_c=-comparable
proof
end;
::
:: Trees and their properties
::
definition
let
X
be
set
;
attr
X
is
Tree-like
means
:
Def3
:
:: TREES_1:def 3
(
X
c=
NAT
*
& ( for
p
being
FinSequence
of
NAT
st
p
in
X
holds
ProperPrefixes
p
c=
X
) & ( for
p
being
FinSequence
of
NAT
for
k
,
n
being
Element
of
NAT
st
p
^
<*
k
*>
in
X
&
n
<=
k
holds
p
^
<*
n
*>
in
X
) );
end;
::
deftheorem
Def3
defines
Tree-like
TREES_1:def 3 :
for
X
being
set
holds
(
X
is
Tree-like
iff (
X
c=
NAT
*
& ( for
p
being
FinSequence
of
NAT
st
p
in
X
holds
ProperPrefixes
p
c=
X
) & ( for
p
being
FinSequence
of
NAT
for
k
,
n
being
Element
of
NAT
st
p
^
<*
k
*>
in
X
&
n
<=
k
holds
p
^
<*
n
*>
in
X
) ) );
registration
cluster
{
{}
}
->
Tree-like
;
coherence
{
{}
}
is
Tree-like
proof
end;
end;
registration
cluster
non
empty
Tree-like
for
set
;
existence
ex
b
1
being
set
st
( not
b
1
is
empty
&
b
1
is
Tree-like
)
proof
end;
end;
definition
mode
Tree
is
non
empty
Tree-like
set
;
end;
theorem
Th19
:
:: TREES_1:19
for
x
being
set
for
T
being
Tree
st
x
in
T
holds
x
is
FinSequence
of
NAT
proof
end;
definition
let
T
be
Tree
;
:: original:
Element
redefine
mode
Element
of
T
->
FinSequence
of
NAT
;
coherence
for
b
1
being
Element
of
T
holds
b
1
is
FinSequence
of
NAT
by
Th19
;
end;
theorem
Th20
:
:: TREES_1:20
for
T
being
Tree
for
p
,
q
being
FinSequence
st
p
in
T
&
q
is_a_prefix_of
p
holds
q
in
T
proof
end;
theorem
Th21
:
:: TREES_1:21
for
q
being
FinSequence
of
NAT
for
T
being
Tree
for
r
being
FinSequence
st
q
^
r
in
T
holds
q
in
T
proof
end;
theorem
Th22
:
:: TREES_1:22
for
T
being
Tree
holds
(
{}
in
T
&
<*>
NAT
in
T
)
proof
end;
theorem
:: TREES_1:23
{
{}
}
is
Tree
;
registration
let
T
,
T1
be
Tree
;
cluster
T
\/
T1
->
Tree-like
;
coherence
T
\/
T1
is
Tree-like
proof
end;
cluster
T
/\
T1
->
non
empty
Tree-like
;
coherence
(
T
/\
T1
is
Tree-like
& not
T
/\
T1
is
empty
)
proof
end;
end;
theorem
:: TREES_1:24
for
T
,
T1
being
Tree
holds
T
\/
T1
is
Tree
;
theorem
:: TREES_1:25
for
T
,
T1
being
Tree
holds
T
/\
T1
is
Tree
;
::
:: Finite trees and their properties
::
registration
cluster
non
empty
finite
Tree-like
for
set
;
existence
ex
b
1
being
Tree
st
b
1
is
finite
proof
end;
end;
theorem
:: TREES_1:26
for
fT
,
fT1
being
finite
Tree
holds
fT
\/
fT1
is
finite
Tree
;
theorem
:: TREES_1:27
for
T
being
Tree
for
fT
being
finite
Tree
holds
fT
/\
T
is
finite
Tree
;
::
:: Elementary trees
::
definition
let
n
be
Element
of
NAT
;
func
elementary_tree
n
->
Tree
equals
:: TREES_1:def 4
{
<*
k
*>
where
k
is
Element
of
NAT
:
k
<
n
}
\/
{
{}
}
;
correctness
coherence
{
<*
k
*>
where
k
is
Element
of
NAT
:
k
<
n
}
\/
{
{}
}
is
Tree
;
proof
end;
end;
::
deftheorem
defines
elementary_tree
TREES_1:def 4 :
for
n
being
Element
of
NAT
holds
elementary_tree
n
=
{
<*
k
*>
where
k
is
Element
of
NAT
:
k
<
n
}
\/
{
{}
}
;
registration
let
n
be
Element
of
NAT
;
cluster
elementary_tree
n
->
finite
;
coherence
elementary_tree
n
is
finite
proof
end;
end;
theorem
Th28
:
:: TREES_1:28
for
k
,
n
being
Element
of
NAT
st
k
<
n
holds
<*
k
*>
in
elementary_tree
n
proof
end;
theorem
Th29
:
:: TREES_1:29
elementary_tree
0
=
{
{}
}
proof
end;
theorem
:: TREES_1:30
for
n
being
Element
of
NAT
for
p
being
FinSequence
of
NAT
holds
( not
p
in
elementary_tree
n
or
p
=
{}
or ex
k
being
Element
of
NAT
st
(
k
<
n
&
p
=
<*
k
*>
) )
proof
end;
::
:: Leaves and subtrees
::
definition
let
T
be
Tree
;
func
Leaves
T
->
Subset
of
T
means
:
Def5
:
:: TREES_1:def 5
for
p
being
FinSequence
of
NAT
holds
(
p
in
it
iff (
p
in
T
& ( for
q
being
FinSequence
of
NAT
holds
( not
q
in
T
or not
p
is_a_proper_prefix_of
q
) ) ) );
existence
ex
b
1
being
Subset
of
T
st
for
p
being
FinSequence
of
NAT
holds
(
p
in
b
1
iff (
p
in
T
& ( for
q
being
FinSequence
of
NAT
holds
( not
q
in
T
or not
p
is_a_proper_prefix_of
q
) ) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
T
st ( for
p
being
FinSequence
of
NAT
holds
(
p
in
b
1
iff (
p
in
T
& ( for
q
being
FinSequence
of
NAT
holds
( not
q
in
T
or not
p
is_a_proper_prefix_of
q
) ) ) ) ) & ( for
p
being
FinSequence
of
NAT
holds
(
p
in
b
2
iff (
p
in
T
& ( for
q
being
FinSequence
of
NAT
holds
( not
q
in
T
or not
p
is_a_proper_prefix_of
q
) ) ) ) ) holds
b
1
=
b
2
proof
end;
let
p
be
FinSequence
of
NAT
;
assume
B11
:
p
in
T
;
func
T
|
p
->
Tree
means
:
Def6
:
:: TREES_1:def 6
for
q
being
FinSequence
of
NAT
holds
(
q
in
it
iff
p
^
q
in
T
);
existence
ex
b
1
being
Tree
st
for
q
being
FinSequence
of
NAT
holds
(
q
in
b
1
iff
p
^
q
in
T
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Tree
st ( for
q
being
FinSequence
of
NAT
holds
(
q
in
b
1
iff
p
^
q
in
T
) ) & ( for
q
being
FinSequence
of
NAT
holds
(
q
in
b
2
iff
p
^
q
in
T
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def5
defines
Leaves
TREES_1:def 5 :
for
T
being
Tree
for
b
2
being
Subset
of
T
holds
(
b
2
=
Leaves
T
iff for
p
being
FinSequence
of
NAT
holds
(
p
in
b
2
iff (
p
in
T
& ( for
q
being
FinSequence
of
NAT
holds
( not
q
in
T
or not
p
is_a_proper_prefix_of
q
) ) ) ) );
::
deftheorem
Def6
defines
|
TREES_1:def 6 :
for
T
being
Tree
for
p
being
FinSequence
of
NAT
st
p
in
T
holds
for
b
3
being
Tree
holds
(
b
3
=
T
|
p
iff for
q
being
FinSequence
of
NAT
holds
(
q
in
b
3
iff
p
^
q
in
T
) );
theorem
:: TREES_1:31
for
T
being
Tree
holds
T
|
(
<*>
NAT
)
=
T
proof
end;
registration
let
T
be
finite
Tree
;
let
p
be
Element
of
T
;
cluster
T
|
p
->
finite
;
coherence
T
|
p
is
finite
proof
end;
end;
definition
let
T
be
Tree
;
assume
A1
:
Leaves
T
<>
{}
;
mode
Leaf
of
T
->
Element
of
T
means
:: TREES_1:def 7
it
in
Leaves
T
;
existence
ex
b
1
being
Element
of
T
st
b
1
in
Leaves
T
proof
end;
end;
::
deftheorem
defines
Leaf
TREES_1:def 7 :
for
T
being
Tree
st
Leaves
T
<>
{}
holds
for
b
2
being
Element
of
T
holds
(
b
2
is
Leaf
of
T
iff
b
2
in
Leaves
T
);
definition
let
T
be
Tree
;
mode
Subtree
of
T
->
Tree
means
:: TREES_1:def 8
ex
p
being
Element
of
T
st
it
=
T
|
p
;
existence
ex
b
1
being
Tree
ex
p
being
Element
of
T
st
b
1
=
T
|
p
proof
end;
end;
::
deftheorem
defines
Subtree
TREES_1:def 8 :
for
T
,
b
2
being
Tree
holds
(
b
2
is
Subtree
of
T
iff ex
p
being
Element
of
T
st
b
2
=
T
|
p
);
definition
let
T
be
Tree
;
let
p
be
FinSequence
of
NAT
;
let
T1
be
Tree
;
assume
A1
:
p
in
T
;
func
T
with-replacement
(
p
,
T1
)
->
Tree
means
:
Def9
:
:: TREES_1:def 9
for
q
being
FinSequence
of
NAT
holds
(
q
in
it
iff ( (
q
in
T
& not
p
is_a_proper_prefix_of
q
) or ex
r
being
FinSequence
of
NAT
st
(
r
in
T1
&
q
=
p
^
r
) ) );
existence
ex
b
1
being
Tree
st
for
q
being
FinSequence
of
NAT
holds
(
q
in
b
1
iff ( (
q
in
T
& not
p
is_a_proper_prefix_of
q
) or ex
r
being
FinSequence
of
NAT
st
(
r
in
T1
&
q
=
p
^
r
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Tree
st ( for
q
being
FinSequence
of
NAT
holds
(
q
in
b
1
iff ( (
q
in
T
& not
p
is_a_proper_prefix_of
q
) or ex
r
being
FinSequence
of
NAT
st
(
r
in
T1
&
q
=
p
^
r
) ) ) ) & ( for
q
being
FinSequence
of
NAT
holds
(
q
in
b
2
iff ( (
q
in
T
& not
p
is_a_proper_prefix_of
q
) or ex
r
being
FinSequence
of
NAT
st
(
r
in
T1
&
q
=
p
^
r
) ) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def9
defines
with-replacement
TREES_1:def 9 :
for
T
being
Tree
for
p
being
FinSequence
of
NAT
for
T1
being
Tree
st
p
in
T
holds
for
b
4
being
Tree
holds
(
b
4
=
T
with-replacement
(
p
,
T1
) iff for
q
being
FinSequence
of
NAT
holds
(
q
in
b
4
iff ( (
q
in
T
& not
p
is_a_proper_prefix_of
q
) or ex
r
being
FinSequence
of
NAT
st
(
r
in
T1
&
q
=
p
^
r
) ) ) );
theorem
Th32
:
:: TREES_1:32
for
p
being
FinSequence
of
NAT
for
T
,
T1
being
Tree
st
p
in
T
holds
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
}
proof
end;
theorem
:: TREES_1:33
for
p
being
FinSequence
of
NAT
for
T
,
T1
being
Tree
st
p
in
T
holds
T1
=
(
T
with-replacement
(
p
,
T1
)
)
|
p
proof
end;
registration
let
T
be
finite
Tree
;
let
t
be
Element
of
T
;
let
T1
be
finite
Tree
;
cluster
T
with-replacement
(
t
,
T1
)
->
finite
;
coherence
T
with-replacement
(
t
,
T1
) is
finite
proof
end;
end;
theorem
Th34
:
:: TREES_1:34
for
p
being
FinSequence
holds
ProperPrefixes
p
,
dom
p
are_equipotent
proof
end;
registration
let
p
be
FinSequence
;
cluster
ProperPrefixes
p
->
finite
;
coherence
ProperPrefixes
p
is
finite
proof
end;
end;
theorem
:: TREES_1:35
for
p
being
FinSequence
holds
card
(
ProperPrefixes
p
)
=
len
p
proof
end;
::
:: Height and width of finite trees
::
definition
let
IT
be
set
;
attr
IT
is
AntiChain_of_Prefixes-like
means
:
Def10
:
:: TREES_1:def 10
( ( for
x
being
set
st
x
in
IT
holds
x
is
FinSequence
) & ( for
p1
,
p2
being
FinSequence
st
p1
in
IT
&
p2
in
IT
&
p1
<>
p2
holds
not
p1
,
p2
are_c=-comparable
) );
end;
::
deftheorem
Def10
defines
AntiChain_of_Prefixes-like
TREES_1:def 10 :
for
IT
being
set
holds
(
IT
is
AntiChain_of_Prefixes-like
iff ( ( for
x
being
set
st
x
in
IT
holds
x
is
FinSequence
) & ( for
p1
,
p2
being
FinSequence
st
p1
in
IT
&
p2
in
IT
&
p1
<>
p2
holds
not
p1
,
p2
are_c=-comparable
) ) );
registration
cluster
AntiChain_of_Prefixes-like
for
set
;
existence
ex
b
1
being
set
st
b
1
is
AntiChain_of_Prefixes-like
proof
end;
end;
definition
mode
AntiChain_of_Prefixes
is
AntiChain_of_Prefixes-like
set
;
end;
theorem
Th36
:
:: TREES_1:36
for
w
being
FinSequence
holds
{
w
}
is
AntiChain_of_Prefixes-like
proof
end;
theorem
Th37
:
:: TREES_1:37
for
p1
,
p2
being
FinSequence
st not
p1
,
p2
are_c=-comparable
holds
{
p1
,
p2
}
is
AntiChain_of_Prefixes-like
proof
end;
definition
let
T
be
Tree
;
mode
AntiChain_of_Prefixes
of
T
->
AntiChain_of_Prefixes
means
:
Def11
:
:: TREES_1:def 11
it
c=
T
;
existence
ex
b
1
being
AntiChain_of_Prefixes
st
b
1
c=
T
proof
end;
end;
::
deftheorem
Def11
defines
AntiChain_of_Prefixes
TREES_1:def 11 :
for
T
being
Tree
for
b
2
being
AntiChain_of_Prefixes
holds
(
b
2
is
AntiChain_of_Prefixes
of
T
iff
b
2
c=
T
);
theorem
Th38
:
:: TREES_1:38
for
T
being
Tree
holds
(
{}
is
AntiChain_of_Prefixes
of
T
&
{
{}
}
is
AntiChain_of_Prefixes
of
T
)
proof
end;
theorem
:: TREES_1:39
for
T
being
Tree
for
t
being
Element
of
T
holds
{
t
}
is
AntiChain_of_Prefixes
of
T
proof
end;
theorem
:: TREES_1:40
for
T
being
Tree
for
t1
,
t2
being
Element
of
T
st not
t1
,
t2
are_c=-comparable
holds
{
t1
,
t2
}
is
AntiChain_of_Prefixes
of
T
proof
end;
registration
let
T
be
finite
Tree
;
cluster
->
finite
for
AntiChain_of_Prefixes
of
T
;
coherence
for
b
1
being
AntiChain_of_Prefixes
of
T
holds
b
1
is
finite
proof
end;
end;
definition
let
T
be
finite
Tree
;
func
height
T
->
Element
of
NAT
means
:
Def12
:
:: TREES_1:def 12
( ex
p
being
FinSequence
of
NAT
st
(
p
in
T
&
len
p
=
it
) & ( for
p
being
FinSequence
of
NAT
st
p
in
T
holds
len
p
<=
it
) );
existence
ex
b
1
being
Element
of
NAT
st
( ex
p
being
FinSequence
of
NAT
st
(
p
in
T
&
len
p
=
b
1
) & ( for
p
being
FinSequence
of
NAT
st
p
in
T
holds
len
p
<=
b
1
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
NAT
st ex
p
being
FinSequence
of
NAT
st
(
p
in
T
&
len
p
=
b
1
) & ( for
p
being
FinSequence
of
NAT
st
p
in
T
holds
len
p
<=
b
1
) & ex
p
being
FinSequence
of
NAT
st
(
p
in
T
&
len
p
=
b
2
) & ( for
p
being
FinSequence
of
NAT
st
p
in
T
holds
len
p
<=
b
2
) holds
b
1
=
b
2
proof
end;
func
width
T
->
Element
of
NAT
means
:
Def13
:
:: TREES_1:def 13
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
) );
existence
ex
b
1
being
Element
of
NAT
ex
X
being
AntiChain_of_Prefixes
of
T
st
(
b
1
=
card
X
& ( for
Y
being
AntiChain_of_Prefixes
of
T
holds
card
Y
<=
card
X
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
NAT
st ex
X
being
AntiChain_of_Prefixes
of
T
st
(
b
1
=
card
X
& ( for
Y
being
AntiChain_of_Prefixes
of
T
holds
card
Y
<=
card
X
) ) & ex
X
being
AntiChain_of_Prefixes
of
T
st
(
b
2
=
card
X
& ( for
Y
being
AntiChain_of_Prefixes
of
T
holds
card
Y
<=
card
X
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def12
defines
height
TREES_1:def 12 :
for
T
being
finite
Tree
for
b
2
being
Element
of
NAT
holds
(
b
2
=
height
T
iff ( ex
p
being
FinSequence
of
NAT
st
(
p
in
T
&
len
p
=
b
2
) & ( for
p
being
FinSequence
of
NAT
st
p
in
T
holds
len
p
<=
b
2
) ) );
::
deftheorem
Def13
defines
width
TREES_1:def 13 :
for
T
being
finite
Tree
for
b
2
being
Element
of
NAT
holds
(
b
2
=
width
T
iff ex
X
being
AntiChain_of_Prefixes
of
T
st
(
b
2
=
card
X
& ( for
Y
being
AntiChain_of_Prefixes
of
T
holds
card
Y
<=
card
X
) ) );
theorem
:: TREES_1:41
for
fT
being
finite
Tree
holds 1
<=
width
fT
proof
end;
theorem
:: TREES_1:42
height
(
elementary_tree
0
)
=
0
proof
end;
theorem
:: TREES_1:43
for
fT
being
finite
Tree
st
height
fT
=
0
holds
fT
=
elementary_tree
0
proof
end;
theorem
:: TREES_1:44
for
n
being
Element
of
NAT
holds
height
(
elementary_tree
(
n
+
1
)
)
=
1
proof
end;
theorem
:: TREES_1:45
width
(
elementary_tree
0
)
=
1
proof
end;
theorem
:: TREES_1:46
for
n
being
Element
of
NAT
holds
width
(
elementary_tree
(
n
+
1
)
)
=
n
+
1
proof
end;
theorem
:: TREES_1:47
for
fT
being
finite
Tree
for
t
being
Element
of
fT
holds
height
(
fT
|
t
)
<=
height
fT
proof
end;
theorem
Th48
:
:: TREES_1:48
for
fT
being
finite
Tree
for
t
being
Element
of
fT
st
t
<>
{}
holds
height
(
fT
|
t
)
<
height
fT
proof
end;
scheme
:: TREES_1:sch 1
TreeInd
{
P
1
[
Tree
] } :
for
fT
being
finite
Tree
holds
P
1
[
fT
]
provided
A1
: for
fT
being
finite
Tree
st ( for
n
being
Element
of
NAT
st
<*
n
*>
in
fT
holds
P
1
[
fT
|
<*
n
*>
] ) holds
P
1
[
fT
]
proof
end;
begin
theorem
:: TREES_1:49
for
w
,
t
,
s
being
FinSequence
st
w
^
t
is_a_proper_prefix_of
w
^
s
holds
t
is_a_proper_prefix_of
s
proof
end;
theorem
:: TREES_1:50
for
n
,
m
being
Element
of
NAT
for
s
being
FinSequence
st
n
<>
m
holds
not
<*
n
*>
is_a_prefix_of
<*
m
*>
^
s
proof
end;
theorem
:: TREES_1:51
elementary_tree
1
=
{
{}
,
<*
0
*>
}
proof
end;
theorem
:: TREES_1:52
for
n
,
m
being
Element
of
NAT
holds not
<*
n
*>
is_a_proper_prefix_of
<*
m
*>
proof
end;
theorem
:: TREES_1:53
elementary_tree
2
=
{
{}
,
<*
0
*>
,
<*
1
*>
}
proof
end;
:: from BINTREE1
theorem
:: TREES_1:54
for
T
being
Tree
for
t
being
Element
of
T
holds
(
t
in
Leaves
T
iff not
t
^
<*
0
*>
in
T
)
proof
end;
theorem
:: TREES_1:55
for
T
being
Tree
for
t
being
Element
of
T
holds
(
t
in
Leaves
T
iff for
n
being
Element
of
NAT
holds not
t
^
<*
n
*>
in
T
)
proof
end;
definition
func
TrivialInfiniteTree
->
set
equals
:: TREES_1:def 14
{
(
k
|->
0
)
where
k
is
Element
of
NAT
: verum
}
;
coherence
{
(
k
|->
0
)
where
k
is
Element
of
NAT
: verum
}
is
set
;
end;
::
deftheorem
defines
TrivialInfiniteTree
TREES_1:def 14 :
TrivialInfiniteTree
=
{
(
k
|->
0
)
where
k
is
Element
of
NAT
: verum
}
;
registration
cluster
TrivialInfiniteTree
->
non
empty
Tree-like
;
coherence
( not
TrivialInfiniteTree
is
empty
&
TrivialInfiniteTree
is
Tree-like
)
proof
end;
end;
theorem
Th56
:
:: TREES_1:56
NAT
,
TrivialInfiniteTree
are_equipotent
proof
end;
registration
cluster
TrivialInfiniteTree
->
infinite
;
coherence
not
TrivialInfiniteTree
is
finite
by
Th56
,
CARD_1:38
;
end;
:: The set of proper prefixes of a finite sequence
::