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 :
theorem Th4:
theorem Th5:
theorem
:: deftheorem Def2 defines finite-branching TREES_9:def 2 :
:: deftheorem Def3 defines finite-order TREES_9:def 3 :
:: deftheorem Def4 defines finite-branching TREES_9:def 4 :
theorem Th7:
:: deftheorem Def5 defines succ TREES_9:def 5 :
:: deftheorem Def6 defines succ TREES_9:def 6 :
theorem Th8:
theorem
canceled;
theorem Th10:
begin
:: deftheorem defines Subtrees TREES_9:def 7 :
theorem Th11:
theorem Th12:
theorem
theorem
:: deftheorem defines FixedSubtrees TREES_9:def 8 :
theorem
theorem Th16:
theorem
:: deftheorem defines -Subtrees TREES_9:def 9 :
theorem Th18:
theorem
:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :
begin
:: deftheorem defines Subtrees TREES_9:def 11 :
theorem Th20:
theorem
theorem
theorem
theorem
:: deftheorem defines -Subtrees TREES_9:def 12 :
theorem Th25:
theorem
theorem
theorem
:: deftheorem defines -ImmediateSubtrees TREES_9:def 13 :
theorem
theorem Th30:
theorem
theorem