:: Subtreeswyrzucenie slownika daje runtimowke
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994 Association of Mizar Users
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: :: TREES_9:1
theorem Th2: :: TREES_9:2
theorem Th3: :: TREES_9:3
:: deftheorem Def1 defines root TREES_9:def 1 :
theorem Th4: :: TREES_9:4
theorem Th5: :: TREES_9:5
theorem :: TREES_9:6
:: 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: :: TREES_9:7
:: deftheorem Def5 defines succ TREES_9:def 5 :
:: deftheorem Def6 defines succ TREES_9:def 6 :
theorem Th8: :: TREES_9:8
theorem :: TREES_9:9
canceled;
theorem Th10: :: TREES_9:10
:: deftheorem defines Subtrees TREES_9:def 7 :
theorem Th11: :: TREES_9:11
theorem Th12: :: TREES_9:12
theorem :: TREES_9:13
theorem :: TREES_9:14
:: deftheorem defines FixedSubtrees TREES_9:def 8 :
theorem :: TREES_9:15
theorem Th16: :: TREES_9:16
theorem :: TREES_9:17
:: deftheorem defines -Subtrees TREES_9:def 9 :
theorem Th18: :: TREES_9:18
theorem :: TREES_9:19
:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :
:: deftheorem defines Subtrees TREES_9:def 11 :
theorem Th20: :: TREES_9:20
theorem :: TREES_9:21
theorem :: TREES_9:22
theorem :: TREES_9:23
theorem :: TREES_9:24
:: deftheorem defines -Subtrees TREES_9:def 12 :
theorem Th25: :: TREES_9:25
theorem :: TREES_9:26
theorem :: TREES_9:27
theorem :: TREES_9:28
:: deftheorem defines -ImmediateSubtrees TREES_9:def 13 :
theorem :: TREES_9:29
theorem Th30: :: TREES_9:30
theorem :: TREES_9:31
theorem :: TREES_9:32