begin
Lm1:
for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
Lm3:
for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines root TREES_9:def 1 :
for IT being DecoratedTree holds
( IT is root iff dom IT = elementary_tree 0 );
theorem Th4:
theorem Th5:
theorem
:: deftheorem Def2 defines finite-branching TREES_9:def 2 :
for IT being Tree holds
( IT is finite-branching iff for x being Element of IT holds succ x is finite );
:: deftheorem Def3 defines finite-order TREES_9:def 3 :
for IT being DecoratedTree holds
( IT is finite-order iff dom IT is finite-order );
:: deftheorem Def4 defines finite-branching TREES_9:def 4 :
for IT being DecoratedTree holds
( IT is finite-branching iff dom IT is finite-branching );
theorem Th7:
:: deftheorem Def5 defines succ TREES_9:def 5 :
for t being finite-branching Tree
for p being Element of t
for b3 being one-to-one FinSequence of t holds
( b3 = p succ iff ( len b3 = card (succ p) & rng b3 = succ p & ( for i being Element of NAT st i < len b3 holds
b3 . (i + 1) = p ^ <*i*> ) ) );
:: deftheorem Def6 defines succ TREES_9:def 6 :
for t being finite-branching DecoratedTree
for p being FinSequence st p in dom t holds
for b3 being FinSequence holds
( b3 = succ (t,p) iff ex q being Element of dom t st
( q = p & b3 = t * (q succ) ) );
theorem Th8:
theorem
canceled;
theorem Th10:
begin
:: deftheorem defines Subtrees TREES_9:def 7 :
for t being DecoratedTree holds Subtrees t = { (t | p) where p is Node of t : verum } ;
theorem Th11:
theorem Th12:
theorem
theorem
:: deftheorem defines FixedSubtrees TREES_9:def 8 :
for t being DecoratedTree holds FixedSubtrees t = { [p,(t | p)] where p is Node of t : verum } ;
theorem
theorem Th16:
theorem
:: deftheorem defines -Subtrees TREES_9:def 9 :
for t being DecoratedTree
for C being set holds C -Subtrees t = { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
theorem Th18:
theorem
:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :
for t being finite DecoratedTree
for C being set
for b3 being Function of (C -Subtrees t),((Subtrees t) *) holds
( b3 = C -ImmediateSubtrees t iff for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b3 . d holds
d = (d . {}) -tree p );
begin
:: deftheorem defines Subtrees TREES_9:def 11 :
for X being non empty constituted-DTrees set holds Subtrees X = { (t | p) where t is Element of X, p is Node of t : verum } ;
theorem Th20:
theorem
theorem
theorem
theorem
:: deftheorem defines -Subtrees TREES_9:def 12 :
for X being non empty constituted-DTrees set
for C being set holds C -Subtrees X = { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
theorem Th25:
theorem
theorem
theorem
:: deftheorem defines -ImmediateSubtrees TREES_9:def 13 :
for X being non empty constituted-DTrees set st ( for t being Element of X holds t is finite ) holds
for C being set
for b3 being Function of (C -Subtrees X),((Subtrees X) *) holds
( b3 = C -ImmediateSubtrees X iff for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b3 . d holds
d = (d . {}) -tree p );
theorem
theorem Th30:
theorem
theorem
begin
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53: