:: TREES_2 semantic presentation

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

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

proof end;

Lm1: for x being set
for v being FinSequence holds len (v ^ <*x*>) = (len v) + 1

proof end;

theorem :: TREES_2:3

canceled;

theorem Th4: :: TREES_2:4

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 )

proof end;

theorem :: TREES_2:5

canceled;

theorem Th6: :: TREES_2:6

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

proof end;

scheme :: TREES_2:sch 1
TreeStructInd{ F₁() -> Tree, P₁[ set ] } :

for t being Element of F₁() holds P₁[t]

provided

A1: P₁[ {} ] and
A2: for t being Element of F₁()
for n being Nat st P₁[t] & t ^ <*n*> in F₁() holds
P₁[t ^ <*n*>]

proof end;

theorem Th7: :: TREES_2:7

for W1, W2 being Tree st ( for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) ) holds
W1 = W2

proof end;

definition

let W1, W2 be Tree;
redefine pred W1 = W2 means :: TREES_2:def 1
for p being FinSequence of NAT holds
( p in W1 iff p in W2 );
compatibility by Th7;

end;

:: deftheorem defines = TREES_2:def 1 :

theorem :: TREES_2:8

for W being Tree
for p being FinSequence of NAT st p in W holds
W = W with-replacement p,(W | p)

proof end;

theorem Th9: :: TREES_2:9

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

proof end;

theorem :: TREES_2:10

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

proof end;

definition

let IT be Tree;
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;

end;

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

registration

cluster finite-order set ;
existence

proof end;

end;

definition

let W be Tree;
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

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

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

proof end;

end;

:: deftheorem Def3 defines Chain TREES_2:def 3 :

:: deftheorem Def4 defines Level TREES_2:def 4 :

:: deftheorem defines succ TREES_2:def 5 :

theorem :: TREES_2:11

for W being Tree
for L being Level of W holds L is AntiChain_of_Prefixes of W

proof end;

theorem :: TREES_2:12

for W being Tree
for w being Element of W holds succ w is AntiChain_of_Prefixes of W

proof end;

theorem :: TREES_2:13

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}

proof end;

definition

let W be Tree;
let n be Nat;
func W -level n -> Level of W equals :: TREES_2:def 6
{ w where w is Element of W : len w = n } ;
coherence

proof end;

end;

:: deftheorem defines -level TREES_2:def 6 :

theorem :: TREES_2:14

for W being Tree
for w being Element of W
for n being Nat holds
( w ^ <*n*> in succ w iff w ^ <*n*> in W ) ;

theorem :: TREES_2:15

for W being Tree
for w being Element of W st w = {} holds
W -level 1 = succ w

proof end;

theorem :: TREES_2:16

for W being Tree holds W = union { (W -level n) where n is Nat : verum }

proof end;

theorem :: TREES_2:17

for W being finite Tree holds W = union { (W -level n) where n is Nat : n <= height W }

proof end;

theorem :: TREES_2:18

for W being Tree
for L being Level of W ex n being Nat st L = W -level n

proof end;

scheme :: TREES_2:sch 2
FraenkelCard{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set } :

Card { F₃(w) where w is Element of F₁() : w in F₂() } <=` Card F₂()

proof end;

scheme :: TREES_2:sch 3
FraenkelFinCard{ F₁() -> non empty set , F₂() -> finite set , F₃() -> finite set , F₄( set ) -> set } :

card F₃() <= card F₂()

provided

A1: F₃() = { F₄(w) where w is Element of F₁() : w in F₂() }

proof end;

theorem Th19: :: TREES_2:19

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 )

proof end;

theorem Th20: :: TREES_2:20

for W being Tree
for w being Element of W st W is finite-order holds
succ w is finite

proof end;

registration

let W be finite-order Tree;
let w be Element of W;
cluster succ w -> finite ;
coherence by Th20;

end;

theorem Th21: :: TREES_2:21

for W being Tree holds {} is Chain of W

proof end;

theorem Th22: :: TREES_2:22

for W being Tree holds {{} } is Chain of W

proof end;

registration

let W be Tree;
cluster non empty Chain of W;
existence

proof end;

end;

definition

let W be Tree;
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 ) ) ) );

end;

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

registration

let W be Tree;
cluster Branch-like Chain of W;
existence

proof end;

end;

definition

let W be Tree;
mode Branch of W is Branch-like Chain of W;

end;

registration

let W be Tree;
cluster Branch-like -> non empty Chain of W;
coherence

proof end;

end;

theorem Th23: :: TREES_2:23

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

proof end;

theorem Th24: :: TREES_2:24

for W being Tree
for v1, v2, v 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;

registration

let W be Tree;
cluster finite Chain of W;
existence

proof end;

end;

theorem Th25: :: TREES_2:25

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 )

proof end;

theorem Th26: :: TREES_2:26

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

proof end;

theorem Th27: :: TREES_2:27

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

proof end;

theorem Th28: :: TREES_2:28

for W being Tree
for B being Branch of W holds {} in B

proof end;

theorem Th29: :: TREES_2:29

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

proof end;

theorem Th30: :: TREES_2:30

for W being Tree
for C being Chain of W ex B being Branch of W st C c= B

proof end;

scheme :: TREES_2:sch 4
FuncExOfMinNat{ P₁[ set , Nat], F₁() -> set } :

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
ex n being Nat st
( f . x = n & P₁[x,n] & ( for m being Nat st P₁[x,m] holds
n <= m ) ) ) )

provided

A1: for x being set st x in F₁() holds
ex n being Nat st P₁[x,n]

proof end;

Lm2: 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₁() -> set , F₂() -> set , P₁[ set ], P₂[ set , set ] } :

ex f being Function st
( dom f = NAT & rng f c= F₁() & f . 0 = F₂() & ( for k being Nat holds
( P₂[f . k,f . (k + 1)] & P₁[f . k] ) ) )

provided

A1: ( F₂() in F₁() & P₁[F₂()] ) and
A2: for x being set st x in F₁() & P₁[x] holds
ex y being set st
( y in F₁() & P₂[x,y] & P₁[y] )

proof end;

theorem Th31: :: TREES_2:31

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

proof end;

theorem :: TREES_2:32

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

proof end;

definition

let IT be Relation;
attr IT is DecoratedTree-like means :Def8: :: TREES_2:def 8
dom IT is Tree;

end;

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

registration

cluster DecoratedTree-like set ;
existence

proof end;

end;

definition

mode DecoratedTree is DecoratedTree-like Function;

end;

registration

let T be DecoratedTree;
cluster dom T -> non empty Tree-like ;
coherence by Def8;

end;

definition

let X be set ;
mode ParametrizedSubset of X -> Relation means :Def9: :: TREES_2:def 9
rng it c= X;
existence

proof end;

end;

:: deftheorem Def9 defines ParametrizedSubset TREES_2:def 9 :

registration

let D be non empty set ;
cluster Function-like DecoratedTree-like ParametrizedSubset of D;
existence

proof end;

end;

definition

let D be non empty set ;
mode DecoratedTree of D is Function-like DecoratedTree-like ParametrizedSubset of D;

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

proof end;

end;

theorem Th33: :: TREES_2:33

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

proof end;

scheme :: TREES_2:sch 6
DTreeEx{ F₁() -> Tree, P₁[ set , set ] } :

ex T being DecoratedTree st
( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
P₁[p,T . p] ) )

provided

A1: for p being FinSequence of NAT st p in F₁() holds
ex x being set st P₁[p,x]

proof end;

scheme :: TREES_2:sch 7
DTreeLambda{ F₁() -> Tree, F₂( set ) -> set } :

ex T being DecoratedTree st
( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
T . p = F₂(p) ) )

proof end;

definition

let T be DecoratedTree;
func Leaves T -> set equals :: TREES_2:def 10
T .: (Leaves (dom T));
correctness ;
let p be FinSequence of NAT ;
func T | p -> DecoratedTree means :Def11: :: TREES_2:def 11
( dom it = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
it . q = T . (p ^ q) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Leaves TREES_2:def 10 :

:: deftheorem Def11 defines | TREES_2:def 11 :

theorem Th34: :: TREES_2:34

for p being FinSequence of NAT
for T being DecoratedTree st p in dom T holds
rng (T | p) c= rng T

proof end;

definition

let D be non empty set ;
let T be DecoratedTree of D;
:: original: Leaves
redefine func Leaves T -> Subset of D;
coherence

proof end;

let p be Element of dom T;
:: original: |
redefine func T | p -> DecoratedTree of D;
coherence

proof end;

end;

definition

let T be DecoratedTree;
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 12
( 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

proof end;

uniqueness

proof end;

end;

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

registration

let W be Tree;
let x be set ;
cluster W --> x -> DecoratedTree-like ;
coherence

proof end;

end;

definition

let D be non empty set ;
let W be Tree;
let d be Element of D;
:: original: -->
redefine func W --> d -> DecoratedTree of D;
coherence

proof end;

end;

theorem Th35: :: TREES_2:35

for D being non empty set st ( for x being set st x in D holds
x is Tree ) holds
union D is Tree

proof end;

theorem Th36: :: TREES_2:36

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 )

proof end;

theorem Th37: :: TREES_2:37

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

proof end;

theorem Th38: :: TREES_2:38

for D', D being non empty set st ( for x being set st x in D' holds
x is DecoratedTree of D ) & D' is c=-linear holds
union D' is DecoratedTree of D

proof end;

scheme :: TREES_2:sch 8
DTreeStructEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> set , F₄() -> Function of [:F₁(),NAT :],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F₃((T . t)) } & ( for n being Nat st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . [(T . t),n] ) ) ) )

provided

A1: for d being Element of F₁()
for k1, k2 being Nat st k1 <= k2 & k2 in F₃(d) holds
k1 in F₃(d)

proof end;

scheme :: TREES_2:sch 9
DTreeStructFinEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> Nat, F₄() -> Function of [:F₁(),NAT :],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F₃((T . t)) } & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . [(T . t),n] ) ) ) )

proof end;

registration

let Tr be finite Tree;
let v be Element of Tr;
cluster succ v -> finite ;
coherence ;

end;

definition

let Tr be finite Tree;
let v be Element of Tr;
func branchdeg v -> set equals :: TREES_2:def 13
card (succ v);
correctness ;

end;

:: deftheorem defines branchdeg TREES_2:def 13 :

Lm3: for f being Function holds (pr1 (dom f),(rng f)) .: f = dom f

proof end;

Lm4: for f being Function holds
( dom f is finite iff f is finite )

proof end;

registration

cluster finite set ;
existence

proof end;

end;

registration

let D be non empty set ;
cluster finite ParametrizedSubset of D;
existence

proof end;

end;

registration

let R be finite Relation;
cluster dom R -> finite ;
coherence

proof end;

end;

registration

let a, b be non empty set ;
cluster non empty Relation of a,b;
existence

proof end;

end;