:: TREES_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TREES_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: TREES_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: TREES_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}
proof end;

scheme :: TREES_2:sch 1
TreeStructInd{ F1() -> Tree, P1[ set ] } :
for t being Element of F1() holds P1[t]
provided
A1: P1[ {} ] and
A2: for t being Element of F1()
for n being Nat st P1[t] & t ^ <*n*> in F1() holds
P1[t ^ <*n*>]
proof end;

theorem Th7: :: TREES_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
( W1 = W2 iff for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) )
by Th7;
end;

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

theorem :: TREES_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 );

registration
cluster finite-order set ;
existence
ex b1 being Tree st b1 is finite-order
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
ex b1 being Subset of W st
for p, q being FinSequence of NAT st p in b1 & q in b1 holds
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 b1 being Subset of W ex n being Nat st b1 = { w where w is Element of W : len w = n }
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 } is Subset of W
proof end;
end;

:: deftheorem Def3 defines Chain TREES_2:def 3 :
for W being Tree
for b2 being Subset of W holds
( b2 is Chain of W iff for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p,q are_c=-comparable );

:: deftheorem Def4 defines Level TREES_2:def 4 :
for W being Tree
for b2 being Subset of W holds
( b2 is Level of W iff ex n being Nat st b2 = { w where w is Element of W : len w = n } );

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

theorem :: TREES_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree
for L being Level of W holds L is AntiChain_of_Prefixes of W
proof end;

theorem :: TREES_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ w where w is Element of W : len w = n } is Level of W
proof end;
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 } ;

theorem :: TREES_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree
for w being Element of W st w = {} holds
W -level 1 = succ w
proof end;

theorem :: TREES_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree holds W = union { (W -level n) where n is Nat : verum }
proof end;

theorem :: TREES_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being finite Tree holds W = union { (W -level n) where n is Nat : n <= height W }
proof end;

theorem :: TREES_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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{ F1() -> non empty set , F2() -> set , F3( set ) -> set } :
Card { F3(w) where w is Element of F1() : w in F2() } <=` Card F2()
proof end;

scheme :: TREES_2:sch 3
FraenkelFinCard{ F1() -> non empty set , F2() -> finite set , F3() -> finite set , F4( set ) -> set } :
card F3() <= card F2()
provided
A1: F3() = { F4(w) where w is Element of F1() : w in F2() }
proof end;

theorem Th19: :: TREES_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
succ w is finite
by Th20;
end;

theorem Th21: :: TREES_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree holds {} is Chain of W
proof end;

theorem Th22: :: TREES_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree holds {{} } is Chain of W
proof end;

registration
let W be Tree;
cluster non empty Chain of W;
existence
not for b1 being Chain of W holds b1 is empty
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 :
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
let W be Tree;
cluster Branch-like Chain of W;
existence
ex b1 being Chain of W st b1 is Branch-like
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
for b1 being Chain of W st b1 is Branch-like holds
not b1 is empty
proof end;
end;

theorem Th23: :: TREES_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Chain of W st b1 is finite
proof end;
end;

theorem Th25: :: TREES_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Tree
for B being Branch of W holds {} in B
proof end;

theorem Th29: :: TREES_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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{ P1[ set , Nat], F1() -> set } :
ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
ex n being Nat st
( f . x = n & P1[x,n] & ( for m being Nat st P1[x,m] holds
n <= m ) ) ) )
provided
A1: for x being set st x in F1() holds
ex n being Nat st P1[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{ F1() -> set , F2() -> set , P1[ set ], P2[ set , set ] } :
ex f being Function st
( dom f = NAT & rng f c= F1() & f . 0 = F2() & ( for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
provided
A1: ( F2() in F1() & P1[F2()] ) and
A2: for x being set st x in F1() & P1[x] holds
ex y being set st
( y in F1() & P2[x,y] & P1[y] )
proof end;

theorem Th31: :: TREES_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for IT being Relation holds
( IT is DecoratedTree-like iff dom IT is Tree );

registration
cluster DecoratedTree-like set ;
existence
ex b1 being Function st b1 is DecoratedTree-like
proof end;
end;

definition
mode DecoratedTree is DecoratedTree-like Function;
end;

registration
let T be DecoratedTree;
cluster dom T -> non empty Tree-like ;
coherence
( not dom T is empty & dom T is Tree-like )
by Def8;
end;

definition
let X be set ;
mode ParametrizedSubset of X -> Relation means :Def9: :: TREES_2:def 9
rng it c= X;
existence
ex b1 being Relation st rng b1 c= X
proof end;
end;

:: deftheorem Def9 defines ParametrizedSubset TREES_2:def 9 :
for X being set
for b2 being Relation holds
( b2 is ParametrizedSubset of X iff rng b2 c= X );

registration
let D be non empty set ;
cluster Function-like DecoratedTree-like ParametrizedSubset of D;
existence
ex b1 being ParametrizedSubset of D st
( b1 is DecoratedTree-like & b1 is Function-like )
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
T . t is Element of D
proof end;
end;

theorem Th33: :: TREES_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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{ F1() -> Tree, P1[ set , set ] } :
ex T being DecoratedTree st
( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds
P1[p,T . p] ) )
provided
A1: for p being FinSequence of NAT st p in F1() holds
ex x being set st P1[p,x]
proof end;

scheme :: TREES_2:sch 7
DTreeLambda{ F1() -> Tree, F2( set ) -> set } :
ex T being DecoratedTree st
( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds
T . p = F2(p) ) )
proof end;

definition
let T be DecoratedTree;
func Leaves T -> set equals :: TREES_2:def 10
T .: (Leaves (dom T));
correctness
coherence
T .: (Leaves (dom T)) is set
;
;
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
ex b1 being DecoratedTree st
( dom b1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st dom b1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) & dom b2 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b2 . q = T . (p ^ q) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Leaves TREES_2:def 10 :
for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T));

:: deftheorem Def11 defines | TREES_2:def 11 :
for T being DecoratedTree
for p being FinSequence of NAT
for b3 being DecoratedTree holds
( b3 = T | p iff ( dom b3 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b3 . q = T . (p ^ q) ) ) );

theorem Th34: :: TREES_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
Leaves T is Subset of D
proof end;
let p be Element of dom T;
:: original: |
redefine func T | p -> DecoratedTree of D;
coherence
T | p is DecoratedTree of D
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
ex b1 being DecoratedTree st
( dom b1 = (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 & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st dom b1 = (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 & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = (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 & b2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines with-replacement TREES_2:def 12 :
for T being DecoratedTree
for p being FinSequence of NAT
for T1 being DecoratedTree st p in dom T holds
for b4 being DecoratedTree holds
( b4 = T with-replacement p,T1 iff ( dom b4 = (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 & b4 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b4 . q = T1 . r ) ) ) ) );

registration
let W be Tree;
let x be set ;
cluster W --> x -> DecoratedTree-like ;
coherence
W --> x is DecoratedTree-like
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
W --> d is DecoratedTree of D
proof end;
end;

theorem Th35: :: TREES_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> set , F4() -> Function of [:F1(),NAT :],F1() } :
ex T being DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T . t)) } & ( for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . [(T . t),n] ) ) ) )
provided
A1: for d being Element of F1()
for k1, k2 being Nat st k1 <= k2 & k2 in F3(d) holds
k1 in F3(d)
proof end;

scheme :: TREES_2:sch 9
DTreeStructFinEx{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> Nat, F4() -> Function of [:F1(),NAT :],F1() } :
ex T being DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F3((T . t)) } & ( for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . [(T . t),n] ) ) ) )
proof end;

registration
let Tr be finite Tree;
let v be Element of Tr;
cluster succ v -> finite ;
coherence
succ v is finite
;
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
coherence
card (succ v) is set
;
;
end;

:: deftheorem defines branchdeg TREES_2:def 13 :
for Tr being finite Tree
for v being Element of Tr holds branchdeg v = card (succ v);

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
ex b1 being DecoratedTree st b1 is finite
proof end;
end;

registration
let D be non empty set ;
cluster finite ParametrizedSubset of D;
existence
ex b1 being DecoratedTree of D st b1 is finite
proof end;
end;

registration
let R be finite Relation;
cluster dom R -> finite ;
coherence
dom R is finite
proof end;
end;

registration
let a, b be non empty set ;
cluster non empty Relation of a,b;
existence
not for b1 being Relation of a,b holds b1 is empty
proof end;
end;