:: by Grzegorz Bancerek

::

:: Received January 10, 1991

:: Copyright (c) 1991-2017 Association of Mizar Users

theorem Th1: :: TREES_2:1

for v1, v2, v being FinSequence st v1 is_a_prefix_of v & v2 is_a_prefix_of v holds

v1,v2 are_c=-comparable

v1,v2 are_c=-comparable

proof end;

theorem Th2: :: TREES_2:2

for v1, v2, v being FinSequence st v1 is_a_proper_prefix_of v & v2 is_a_prefix_of v holds

v1,v2 are_c=-comparable by Th1;

v1,v2 are_c=-comparable by Th1;

theorem Th3: :: TREES_2:3

for k being Nat

for v1 being FinSequence st len v1 = k + 1 holds

ex v2 being FinSequence ex x being set st

( v1 = v2 ^ <*x*> & len v2 = k )

for v1 being FinSequence st len v1 = k + 1 holds

ex v2 being FinSequence ex x being set st

( v1 = v2 ^ <*x*> & len v2 = k )

proof end;

theorem Th4: :: TREES_2:4

for x being set

for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}

for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}

proof end;

theorem Th5: :: TREES_2:5

for W1, W2 being Tree st ( for p being FinSequence of NAT holds

( p in W1 iff p in W2 ) ) holds

W1 = W2

( p in W1 iff p in W2 ) ) holds

W1 = W2

proof end;

definition

let W1, W2 be Tree;

( W1 = W2 iff for p being FinSequence of NAT holds

( p in W1 iff p in W2 ) ) by Th5;

end;
redefine pred W1 = W2 means :: TREES_2:def 1

for p being FinSequence of NAT holds

( p in W1 iff p in W2 );

compatibility for p being FinSequence of NAT holds

( p in W1 iff p in W2 );

( W1 = W2 iff for p being FinSequence of NAT holds

( p in W1 iff p in W2 ) ) by Th5;

:: deftheorem defines = TREES_2:def 1 :

for W1, W2 being Tree holds

( W1 = W2 iff for p being FinSequence of NAT holds

( p in W1 iff p in W2 ) );

for W1, W2 being Tree holds

( W1 = W2 iff for p being FinSequence of NAT holds

( p in W1 iff p in W2 ) );

theorem Th7: :: TREES_2:7

for W, W1 being Tree

for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds

q in W with-replacement (p,W1)

for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds

q in W with-replacement (p,W1)

proof end;

theorem :: TREES_2:8

for W, W1, W2 being Tree

for p, q being FinSequence of NAT st p in W & q in W & not p,q are_c=-comparable holds

(W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1)

for p, q being FinSequence of NAT st p in W & q in W & not p,q are_c=-comparable holds

(W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1)

proof end;

definition

let IT be Tree;

end;
attr IT is finite-order means :: TREES_2:def 2

ex n being Nat st

for t being Element of IT holds not t ^ <*n*> in IT;

ex n being Nat st

for t being Element of IT holds not t ^ <*n*> in IT;

:: deftheorem defines finite-order TREES_2:def 2 :

for IT being Tree holds

( IT is finite-order iff ex n being Nat st

for t being Element of IT holds not t ^ <*n*> in IT );

for IT being Tree holds

( IT is finite-order iff ex n being Nat st

for t being Element of IT holds not t ^ <*n*> in IT );

definition

let W be Tree;

ex b_{1} being Subset of W st

for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p,q are_c=-comparable

ex b_{1} being Subset of W ex n being Nat st b_{1} = { w where w is Element of W : len w = n }

{ (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } is Subset of W

end;
mode Chain of W -> Subset of W means :Def3: :: TREES_2:def 3

for p, q being FinSequence of NAT st p in it & q in it holds

p,q are_c=-comparable ;

existence for p, q being FinSequence of NAT st p in it & q in it holds

p,q are_c=-comparable ;

ex b

for p, q being FinSequence of NAT st p in b

p,q are_c=-comparable

proof end;

mode Level of W -> Subset of W means :Def4: :: TREES_2:def 4

ex n being Nat st it = { w where w is Element of W : len w = n } ;

existence ex n being Nat st it = { w where w is Element of W : len w = n } ;

ex b

proof end;

let w be Element of W;
func succ w -> Subset of W equals :: TREES_2:def 5

{ (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ;

coherence { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ;

{ (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } is Subset of W

proof end;

:: deftheorem Def3 defines Chain TREES_2:def 3 :

for W being Tree

for b_{2} being Subset of W holds

( b_{2} is Chain of W iff for p, q being FinSequence of NAT st p in b_{2} & q in b_{2} holds

p,q are_c=-comparable );

for W being Tree

for b

( b

p,q are_c=-comparable );

:: deftheorem Def4 defines Level TREES_2:def 4 :

for W being Tree

for b_{2} being Subset of W holds

( b_{2} is Level of W iff ex n being Nat st b_{2} = { w where w is Element of W : len w = n } );

for W being Tree

for b

( b

:: deftheorem defines succ TREES_2:def 5 :

for W being Tree

for w being Element of W holds succ w = { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ;

for W being Tree

for w being Element of W holds succ w = { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ;

theorem :: TREES_2:11

for W being Tree

for A being AntiChain_of_Prefixes of W

for C being Chain of W ex w being Element of W st A /\ C c= {w}

for A being AntiChain_of_Prefixes of W

for C being Chain of W ex w being Element of W st A /\ C c= {w}

proof end;

definition

let W be Tree;

let n be Nat;

coherence

{ w where w is Element of W : len w = n } is Level of W

end;
let n be Nat;

coherence

{ w where w is Element of W : len w = n } is Level of W

proof end;

:: deftheorem defines -level TREES_2:def 6 :

for W being Tree

for n being Nat holds W -level n = { w where w is Element of W : len w = n } ;

for W being Tree

for n being Nat holds W -level n = { w where w is Element of W : len w = n } ;

theorem :: TREES_2:12

theorem Th17: :: TREES_2:17

for W being Tree st W is finite-order holds

ex n being Nat st

for w being Element of W ex B being finite set st

( B = succ w & card B <= n )

ex n being Nat st

for w being Element of W ex B being finite set st

( B = succ w & card B <= n )

proof end;

registration
end;

registration
end;

definition

let W be Tree;

let IT be Chain of W;

end;
let IT be Chain of W;

attr IT is Branch-like means :Def7: :: TREES_2:def 7

( ( for p being FinSequence of NAT st p in IT holds

ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds

( not p in W or ex q being FinSequence of NAT st

( q in IT & not q is_a_proper_prefix_of p ) ) ) );

( ( for p being FinSequence of NAT st p in IT holds

ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds

( not p in W or ex q being FinSequence of NAT st

( q in IT & not q is_a_proper_prefix_of p ) ) ) );

:: deftheorem Def7 defines Branch-like TREES_2:def 7 :

for W being Tree

for IT being Chain of W holds

( IT is Branch-like iff ( ( for p being FinSequence of NAT st p in IT holds

ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds

( not p in W or ex q being FinSequence of NAT st

( q in IT & not q is_a_proper_prefix_of p ) ) ) ) );

for W being Tree

for IT being Chain of W holds

( IT is Branch-like iff ( ( for p being FinSequence of NAT st p in IT holds

ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds

( not p in W or ex q being FinSequence of NAT st

( q in IT & not q is_a_proper_prefix_of p ) ) ) ) );

registration
end;

registration

let W be Tree;

coherence

for b_{1} being Chain of W st b_{1} is Branch-like holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

theorem Th21: :: TREES_2:21

for W being Tree

for v1, v2 being FinSequence

for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds

v2 is_a_prefix_of v1

for v1, v2 being FinSequence

for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds

v2 is_a_prefix_of v1

proof end;

theorem Th22: :: TREES_2:22

for W being Tree

for v, v1, v2 being FinSequence

for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds

v is_a_prefix_of v1

for v, v1, v2 being FinSequence

for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds

v is_a_prefix_of v1

proof end;

theorem Th23: :: TREES_2:23

for W being Tree

for n being Nat

for C being finite Chain of W st card C > n holds

ex p being FinSequence of NAT st

( p in C & len p >= n )

for n being Nat

for C being finite Chain of W st card C > n holds

ex p being FinSequence of NAT st

( p in C & len p >= n )

proof end;

theorem Th24: :: TREES_2:24

for W being Tree

for C being Chain of W holds { w where w is Element of W : ex p being FinSequence of NAT st

( p in C & w is_a_prefix_of p ) } is Chain of W

for C being Chain of W holds { w where w is Element of W : ex p being FinSequence of NAT st

( p in C & w is_a_prefix_of p ) } is Chain of W

proof end;

theorem Th25: :: TREES_2:25

for W being Tree

for p, q being FinSequence of NAT

for B being Branch of W st p is_a_prefix_of q & q in B holds

p in B

for p, q being FinSequence of NAT

for B being Branch of W st p is_a_prefix_of q & q in B holds

p in B

proof end;

theorem Th27: :: TREES_2:27

for W being Tree

for p, q being FinSequence of NAT

for C being Chain of W st p in C & q in C & len p <= len q holds

p is_a_prefix_of q

for p, q being FinSequence of NAT

for C being Chain of W st p in C & q in C & len p <= len q holds

p is_a_prefix_of q

proof end;

Lm1: for X being set st X is finite holds

ex n being Nat st

for k being Nat st k in X holds

k <= n

proof end;

scheme :: TREES_2:sch 5

InfiniteChain{ F_{1}() -> set , F_{2}() -> object , P_{1}[ object ], P_{2}[ object , object ] } :

InfiniteChain{ F

ex f being Function st

( dom f = NAT & rng f c= F_{1}() & f . 0 = F_{2}() & ( for k being Nat holds

( P_{2}[f . k,f . (k + 1)] & P_{1}[f . k] ) ) )

provided( dom f = NAT & rng f c= F

( P

A1:
( F_{2}() in F_{1}() & P_{1}[F_{2}()] )
and

A2: for x being object st x in F_{1}() & P_{1}[x] holds

ex y being object st

( y in F_{1}() & P_{2}[x,y] & P_{1}[y] )

A2: for x being object st x in F

ex y being object st

( y in F

proof end;

theorem Th29: :: TREES_2:29

for T being Tree st ( for n being Nat ex C being finite Chain of T st card C = n ) & ( for t being Element of T holds succ t is finite ) holds

ex B being Chain of T st not B is finite

ex B being Chain of T st not B is finite

proof end;

:: Koenig Lemma

theorem :: TREES_2:30

for T being finite-order Tree st ( for n being Nat ex C being finite Chain of T st card C = n ) holds

ex B being Chain of T st not B is finite

ex B being Chain of T st not B is finite

proof end;

definition
end;

:: deftheorem Def8 defines DecoratedTree-like TREES_2:def 8 :

for IT being Relation holds

( IT is DecoratedTree-like iff dom IT is Tree );

for IT being Relation holds

( IT is DecoratedTree-like iff dom IT is Tree );

registration
end;

registration

let D be non empty set ;

existence

ex b_{1} being Function st

( b_{1} is DecoratedTree-like & b_{1} is D -valued )

end;
existence

ex b

( b

proof end;

definition

let D be non empty set ;

let T be DecoratedTree of D;

let t be Element of dom T;

:: original: .

redefine func T . t -> Element of D;

coherence

T . t is Element of D

end;
let T be DecoratedTree of D;

let t be Element of dom T;

:: original: .

redefine func T . t -> Element of D;

coherence

T . t is Element of D

proof end;

theorem Th31: :: TREES_2:31

for T1, T2 being DecoratedTree st dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds

T1 . p = T2 . p ) holds

T1 = T2

T1 . p = T2 . p ) holds

T1 = T2

proof end;

scheme :: TREES_2:sch 6

DTreeEx{ F_{1}() -> Tree, P_{1}[ object , object ] } :

DTreeEx{ F

ex T being DecoratedTree st

( dom T = F_{1}() & ( for p being FinSequence of NAT st p in F_{1}() holds

P_{1}[p,T . p] ) )

provided
( dom T = F

P

proof end;

scheme :: TREES_2:sch 7

DTreeLambda{ F_{1}() -> Tree, F_{2}( object ) -> set } :

DTreeLambda{ F

ex T being DecoratedTree st

( dom T = F_{1}() & ( for p being FinSequence of NAT st p in F_{1}() holds

T . p = F_{2}(p) ) )

( dom T = F

T . p = F

proof end;

definition

let T be DecoratedTree;

correctness

coherence

T .: (Leaves (dom T)) is set ;

;

let p be FinSequence of NAT ;

ex b_{1} being DecoratedTree st

( dom b_{1} = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

b_{1} . q = T . (p ^ q) ) )

for b_{1}, b_{2} being DecoratedTree st dom b_{1} = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

b_{1} . q = T . (p ^ q) ) & dom b_{2} = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

b_{2} . q = T . (p ^ q) ) holds

b_{1} = b_{2}

end;
correctness

coherence

T .: (Leaves (dom T)) is set ;

;

let p be FinSequence of NAT ;

func T | p -> DecoratedTree means :Def10: :: TREES_2:def 10

( dom it = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

it . q = T . (p ^ q) ) );

existence ( dom it = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

it . q = T . (p ^ q) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines Leaves TREES_2:def 9 :

for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T));

for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T));

:: deftheorem Def10 defines | TREES_2:def 10 :

for T being DecoratedTree

for p being FinSequence of NAT

for b_{3} being DecoratedTree holds

( b_{3} = T | p iff ( dom b_{3} = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds

b_{3} . q = T . (p ^ q) ) ) );

for T being DecoratedTree

for p being FinSequence of NAT

for b

( b

b

definition

let D be non empty set ;

let T be DecoratedTree of D;

:: original: Leaves

redefine func Leaves T -> Subset of D;

coherence

Leaves T is Subset of D

end;
let T be DecoratedTree of D;

:: original: Leaves

redefine func Leaves T -> Subset of D;

coherence

Leaves T is Subset of D

proof end;

registration

let D be non empty set ;

let T be DecoratedTree of D;

let p be Element of dom T;

coherence

T | p is D -valued

end;
let T be DecoratedTree of D;

let p be Element of dom T;

coherence

T | p is D -valued

proof end;

definition

let T be DecoratedTree;

let p be FinSequence of NAT ;

let T1 be DecoratedTree;

assume A1: p in dom T ;

ex b_{1} being DecoratedTree st

( dom b_{1} = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b_{1} . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & b_{1} . q = T1 . r ) ) ) )

for b_{1}, b_{2} being DecoratedTree st dom b_{1} = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b_{1} . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & b_{1} . q = T1 . r ) ) ) & dom b_{2} = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b_{2} . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & b_{2} . q = T1 . r ) ) ) holds

b_{1} = b_{2}

end;
let p be FinSequence of NAT ;

let T1 be DecoratedTree;

assume A1: p in dom T ;

func T with-replacement (p,T1) -> DecoratedTree means :: TREES_2:def 11

( dom it = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & it . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );

existence ( dom it = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & it . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );

ex b

( dom b

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b

( r in dom T1 & q = p ^ r & b

proof end;

uniqueness for b

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b

( r in dom T1 & q = p ^ r & b

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b

( r in dom T1 & q = p ^ r & b

b

proof end;

:: deftheorem defines with-replacement TREES_2:def 11 :

for T being DecoratedTree

for p being FinSequence of NAT

for T1 being DecoratedTree st p in dom T holds

for b_{4} being DecoratedTree holds

( b_{4} = T with-replacement (p,T1) iff ( dom b_{4} = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b_{4} . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & b_{4} . q = T1 . r ) ) ) ) );

for T being DecoratedTree

for p being FinSequence of NAT

for T1 being DecoratedTree st p in dom T holds

for b

( b

( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b

( r in dom T1 & q = p ^ r & b

registration
end;

theorem Th34: :: TREES_2:34

for X being set st ( for x being set st x in X holds

x is Function ) & X is c=-linear holds

( union X is Relation-like & union X is Function-like )

x is Function ) & X is c=-linear holds

( union X is Relation-like & union X is Function-like )

proof end;

theorem Th35: :: TREES_2:35

for D being non empty set st ( for x being set st x in D holds

x is DecoratedTree ) & D is c=-linear holds

union D is DecoratedTree

x is DecoratedTree ) & D is c=-linear holds

union D is DecoratedTree

proof end;

theorem Th36: :: TREES_2:36

for D, D9 being non empty set st ( for x being set st x in D9 holds

x is DecoratedTree of D ) & D9 is c=-linear holds

union D9 is DecoratedTree of D

x is DecoratedTree of D ) & D9 is c=-linear holds

union D9 is DecoratedTree of D

proof end;

scheme :: TREES_2:sch 8

DTreeStructEx{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( set ) -> set , F_{4}() -> Function of [:F_{1}(),NAT:],F_{1}() } :

DTreeStructEx{ F

ex T being DecoratedTree of F_{1}() st

( T . {} = F_{2}() & ( for t being Element of dom T holds

( succ t = { (t ^ <*k*>) where k is Nat : k in F_{3}((T . t)) } & ( for n being Nat st n in F_{3}((T . t)) holds

T . (t ^ <*n*>) = F_{4}() . ((T . t),n) ) ) ) )

provided( T . {} = F

( succ t = { (t ^ <*k*>) where k is Nat : k in F

T . (t ^ <*n*>) = F

A1:
for d being Element of F_{1}()

for k1, k2 being Nat st k1 <= k2 & k2 in F_{3}(d) holds

k1 in F_{3}(d)

for k1, k2 being Nat st k1 <= k2 & k2 in F

k1 in F

proof end;

scheme :: TREES_2:sch 9

DTreeStructFinEx{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( set ) -> Nat, F_{4}() -> Function of [:F_{1}(),NAT:],F_{1}() } :

DTreeStructFinEx{ F

ex T being DecoratedTree of F_{1}() st

( T . {} = F_{2}() & ( for t being Element of dom T holds

( succ t = { (t ^ <*k*>) where k is Nat : k < F_{3}((T . t)) } & ( for n being Nat st n < F_{3}((T . t)) holds

T . (t ^ <*n*>) = F_{4}() . ((T . t),n) ) ) ) )

( T . {} = F

( succ t = { (t ^ <*k*>) where k is Nat : k < F

T . (t ^ <*n*>) = F

proof end;

:: from PRELAMB

definition
end;

:: deftheorem defines branchdeg TREES_2:def 12 :

for Tr being finite Tree

for v being Element of Tr holds branchdeg v = card (succ v);

for Tr being finite Tree

for v being Element of Tr holds branchdeg v = card (succ v);

registration
end;

registration

let a, b be non empty set ;

existence

not for b_{1} being Relation of a,b holds b_{1} is empty

end;
existence

not for b

proof end;

theorem :: TREES_2:37

for Z1, Z2 being Tree

for p being FinSequence of NAT st p in Z1 holds

for v being Element of Z1 with-replacement (p,Z2)

for w being Element of Z2 st v = p ^ w holds

succ v, succ w are_equipotent

for p being FinSequence of NAT st p in Z1 holds

for v being Element of Z1 with-replacement (p,Z2)

for w being Element of Z2 st v = p ^ w holds

succ v, succ w are_equipotent

proof end;

scheme :: TREES_2:sch 10

DTreeStructEx{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), P_{1}[ set , set ], F_{3}() -> Function of [:F_{1}(),NAT:],F_{1}() } :

DTreeStructEx{ F

ex T being DecoratedTree of F_{1}() st

( T . {} = F_{2}() & ( for t being Element of dom T holds

( succ t = { (t ^ <*k*>) where k is Nat : P_{1}[k,T . t] } & ( for n being Nat st P_{1}[n,T . t] holds

T . (t ^ <*n*>) = F_{3}() . ((T . t),n) ) ) ) )

provided
( T . {} = F

( succ t = { (t ^ <*k*>) where k is Nat : P

T . (t ^ <*n*>) = F

proof end;

:: from AMISTD_3, 2010.01.10, A.T.