:: by Grzegorz Bancerek

::

:: Received October 25, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let p, q be FinSequence;

compatibility

( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) )

end;
compatibility

( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) )

proof end;

:: deftheorem 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 Nat st p = q | (Seg n) );

for p, q being FinSequence holds

( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) );

::$CT

theorem Th6: :: 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

for p1, p2 being FinSequence st p1 ^ <*x*> is_a_prefix_of p2 holds

p1 is_a_proper_prefix_of p2

proof end;

theorem Th7: :: 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*>

for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds

p1 is_a_proper_prefix_of p2 ^ <*x*>

proof end;

theorem Th8: :: 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

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 p1, p2 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds

p1 is_a_proper_prefix_of p1 ^ p2

p1 is_a_proper_prefix_of p1 ^ p2

proof end;

::

:: The set of proper prefixes of a finite sequence

::

:: The set of proper prefixes of a finite sequence

::

definition

let p be FinSequence;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex q being FinSequence st

( x = q & q is_a_proper_prefix_of p ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex q being FinSequence st

( x = q & q is_a_proper_prefix_of p ) ) ) & ( for x being object 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}

end;
func ProperPrefixes p -> set means :Def2: :: TREES_1:def 2

for x being object holds

( x in it iff ex q being FinSequence st

( x = q & q is_a_proper_prefix_of p ) );

existence for x being object holds

( x in it iff ex q being FinSequence st

( x = q & q is_a_proper_prefix_of p ) );

ex b

for x being object holds

( x in b

( x = q & q is_a_proper_prefix_of p ) )

proof end;

uniqueness for b

( x in b

( x = q & q is_a_proper_prefix_of p ) ) ) & ( for x being object holds

( x in b

( x = q & q is_a_proper_prefix_of p ) ) ) holds

b

proof 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 object holds

( x in b_{2} iff ex q being FinSequence st

( x = q & q is_a_proper_prefix_of p ) ) );

for p being FinSequence

for b

( b

( x in b

( x = q & q is_a_proper_prefix_of p ) ) );

set D = {{}};

theorem Th17: :: TREES_1:18

for p, q, r being FinSequence st q in ProperPrefixes p & r in ProperPrefixes p holds

q,r are_c=-comparable

q,r are_c=-comparable

proof end;

::

:: Trees and their properties

::

:: Trees and their properties

::

:: 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 Nat st p ^ <*k*> in X & n <= k holds

p ^ <*n*> in X ) ) );

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 Nat st p ^ <*k*> in X & n <= k holds

p ^ <*n*> in X ) ) );

registration
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 Th18;

end;
:: original: Element

redefine mode Element of T -> FinSequence of NAT ;

coherence

for b

registration

let T, T1 be Tree;

coherence

T \/ T1 is Tree-like

( T /\ T1 is Tree-like & not T /\ T1 is empty )

end;
coherence

T \/ T1 is Tree-like

proof end;

coherence ( T /\ T1 is Tree-like & not T /\ T1 is empty )

proof end;

::

:: Finite trees and their properties

::

:: Finite trees and their properties

::

::

:: Elementary trees

::

:: Elementary trees

::

definition
end;

:: deftheorem defines elementary_tree TREES_1:def 4 :

for n being Nat holds elementary_tree n = { <*k*> where k is Nat : k < n } \/ {{}};

for n being Nat holds elementary_tree n = { <*k*> where k is Nat : k < n } \/ {{}};

theorem :: TREES_1:30

for n being Nat

for p being FinSequence of NAT holds

( not p in elementary_tree n or p = {} or ex k being Nat st

( k < n & p = <*k*> ) )

for p being FinSequence of NAT holds

( not p in elementary_tree n or p = {} or ex k being Nat st

( k < n & p = <*k*> ) )

proof end;

::

:: Leaves and subtrees

::

:: Leaves and subtrees

::

definition

let T be Tree;

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 ) ) ) )

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}

assume A11: p in T ;

ex b_{1} being Tree st

for q being FinSequence of NAT holds

( q in b_{1} iff p ^ q in T )

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}

end;
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 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 ) ) ) );

ex b

for p being FinSequence of NAT holds

( p in b

( not q in T or not p is_a_proper_prefix_of q ) ) ) )

proof end;

uniqueness for b

( p in b

( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) & ( for p being FinSequence of NAT holds

( p in b

( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) holds

b

proof end;

let p be FinSequence of NAT ;assume A11: 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 for q being FinSequence of NAT holds

( q in it iff p ^ q in T );

ex b

for q being FinSequence of NAT holds

( q in b

proof end;

uniqueness for b

( q in b

( q in b

b

proof 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 ) ) ) ) );

for T being Tree

for b

( b

( p in b

( 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 ) );

for T being Tree

for p being FinSequence of NAT st p in T holds

for b

( b

( q in b

definition

let T be Tree;

assume A1: Leaves T <> {} ;

existence

ex b_{1} being Element of T st b_{1} in Leaves T

end;
assume A1: Leaves T <> {} ;

existence

ex b

proof 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 );

for T being Tree st Leaves T <> {} holds

for b

( b

definition
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 );

for T, b

( b

definition

let T be Tree;

let p be FinSequence of NAT ;

let T1 be Tree;

assume A1: p in T ;

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 ) ) )

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}

end;
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 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 ) ) );

ex b

for q being FinSequence of NAT holds

( q in b

( r in T1 & q = p ^ r ) ) )

proof end;

uniqueness for b

( q in b

( r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds

( q in b

( r in T1 & q = p ^ r ) ) ) ) holds

b

proof 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 ) ) ) );

for T being Tree

for p being FinSequence of NAT

for T1 being Tree st p in T holds

for b

( b

( q in b

( r in T1 & q = p ^ r ) ) ) );

theorem Th31: :: 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 : verum }

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 : verum }

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

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;

coherence

T with-replacement (t,T1) is finite

end;
let t be Element of T;

let T1 be finite Tree;

coherence

T with-replacement (t,T1) is finite

proof end;

::

:: Height and width of finite trees

::

:: Height and width of finite trees

::

definition

let IT be set ;

end;
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 ) );

( ( 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 ) );

:: 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 ) ) );

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 ) ) );

theorem Th36: :: TREES_1:37

for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds

{p1,p2} is AntiChain_of_Prefixes-like

{p1,p2} is AntiChain_of_Prefixes-like

proof end;

definition
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 );

for T being Tree

for b

( b

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

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;

coherence

for b_{1} being AntiChain_of_Prefixes of T holds b_{1} is finite

end;
coherence

for b

proof end;

definition

let T be finite Tree;

ex b_{1} being 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} ) )

for b_{1}, b_{2} being 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}

ex b_{1} being 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 ) )

for b_{1}, b_{2} being 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}

end;
func height T -> 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 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 ) );

ex b

( ex p being FinSequence of NAT st

( p in T & len p = b

len p <= b

proof end;

uniqueness for b

( p in T & len p = b

len p <= b

( p in T & len p = b

len p <= b

b

proof end;

func width T -> 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 X being AntiChain_of_Prefixes of T st

( it = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def12 defines height TREES_1:def 12 :

for T being finite Tree

for b_{2} being 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} ) ) );

for T being finite Tree

for b

( b

( p in T & len p = b

len p <= b

:: deftheorem Def13 defines width TREES_1:def 13 :

for T being finite Tree

for b_{2} being 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 ) ) );

for T being finite Tree

for b

( b

( b

:: from BINTREE1

theorem :: TREES_1:55

for T being Tree

for t being Element of T holds

( t in Leaves T iff for n being Nat holds not t ^ <*n*> in T )

for t being Element of T holds

( t in Leaves T iff for n being Nat holds not t ^ <*n*> in T )

proof end;

:: deftheorem defines TrivialInfiniteTree TREES_1:def 14 :

TrivialInfiniteTree = { (k |-> 0) where k is Nat : verum } ;

TrivialInfiniteTree = { (k |-> 0) where k is Nat : verum } ;

registration
end;