:: Introduction to Trees
:: by Grzegorz Bancerek
::
:: Received October 25, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: TREES_1:1
theorem :: TREES_1:2
theorem :: TREES_1:3
theorem :: TREES_1:4
theorem :: TREES_1:5
theorem Th6: :: TREES_1:6
:: deftheorem Def1 defines is_a_prefix_of TREES_1:def 1 :
theorem :: TREES_1:7
canceled;
theorem Th8: :: TREES_1:8
theorem :: TREES_1:9
canceled;
theorem :: TREES_1:10
canceled;
theorem :: TREES_1:11
canceled;
theorem :: TREES_1:12
canceled;
theorem :: TREES_1:13
canceled;
theorem :: TREES_1:14
canceled;
theorem Th15: :: TREES_1:15
theorem Th16: :: TREES_1:16
Lm1:
for A, B being finite set st A c= B & card A = card B holds
A = B
theorem :: TREES_1:17
canceled;
theorem :: TREES_1:18
canceled;
theorem Th19: :: TREES_1:19
theorem :: TREES_1:20
canceled;
theorem :: TREES_1:21
canceled;
theorem :: TREES_1:22
canceled;
theorem Th23: :: TREES_1:23
theorem Th24: :: TREES_1:24
theorem :: TREES_1:25
canceled;
theorem :: TREES_1:26
canceled;
theorem :: TREES_1:27
canceled;
theorem :: TREES_1:28
canceled;
theorem :: TREES_1:29
canceled;
theorem Th30: :: TREES_1:30
theorem Th31: :: TREES_1:31
theorem Th32: :: TREES_1:32
theorem :: TREES_1:33
:: deftheorem TREES_1:def 2 :
canceled;
:: deftheorem TREES_1:def 3 :
canceled;
:: deftheorem Def4 defines ProperPrefixes TREES_1:def 4 :
theorem :: TREES_1:34
canceled;
theorem Th35: :: TREES_1:35
theorem Th36: :: TREES_1:36
theorem Th37: :: TREES_1:37
theorem :: TREES_1:38
theorem Th39: :: TREES_1:39
theorem Th40: :: TREES_1:40
theorem :: TREES_1:41
theorem Th42: :: TREES_1:42
:: deftheorem Def5 defines Tree-like TREES_1:def 5 :
theorem :: TREES_1:43
canceled;
theorem Th44: :: TREES_1:44
theorem Th45: :: TREES_1:45
theorem Th46: :: TREES_1:46
theorem Th47: :: TREES_1:47
theorem Th48: :: TREES_1:48
theorem Th49: :: TREES_1:49
theorem Th50: :: TREES_1:50
theorem :: TREES_1:51
canceled;
theorem :: TREES_1:52
theorem :: TREES_1:53
:: deftheorem TREES_1:def 6 :
canceled;
:: deftheorem defines elementary_tree TREES_1:def 7 :
theorem :: TREES_1:54
canceled;
theorem Th55: :: TREES_1:55
theorem Th56: :: TREES_1:56
theorem :: TREES_1:57
:: deftheorem Def8 defines Leaves TREES_1:def 8 :
:: deftheorem Def9 defines | TREES_1:def 9 :
theorem :: TREES_1:58
canceled;
theorem :: TREES_1:59
canceled;
theorem :: TREES_1:60
:: deftheorem defines Leaf TREES_1:def 10 :
:: deftheorem defines Subtree TREES_1:def 11 :
:: deftheorem Def12 defines with-replacement TREES_1:def 12 :
theorem :: TREES_1:61
canceled;
theorem :: TREES_1:62
canceled;
theorem :: TREES_1:63
canceled;
theorem Th64: :: TREES_1:64
theorem :: TREES_1:65
canceled;
theorem :: TREES_1:66
theorem Th67: :: TREES_1:67
theorem :: TREES_1:68
:: deftheorem Def13 defines AntiChain_of_Prefixes-like TREES_1:def 13 :
theorem :: TREES_1:69
canceled;
theorem Th70: :: TREES_1:70
theorem Th71: :: TREES_1:71
:: deftheorem Def14 defines AntiChain_of_Prefixes TREES_1:def 14 :
theorem :: TREES_1:72
canceled;
theorem Th73: :: TREES_1:73
theorem :: TREES_1:74
theorem :: TREES_1:75
:: deftheorem Def15 defines height TREES_1:def 15 :
:: deftheorem Def16 defines width TREES_1:def 16 :
theorem :: TREES_1:76
canceled;
theorem :: TREES_1:77
canceled;
theorem :: TREES_1:78
theorem :: TREES_1:79
theorem :: TREES_1:80
theorem :: TREES_1:81
theorem :: TREES_1:82
theorem :: TREES_1:83
theorem :: TREES_1:84
theorem Th85: :: TREES_1:85
theorem :: TREES_1:86
theorem :: TREES_1:87
theorem :: TREES_1:88
theorem :: TREES_1:89
theorem :: TREES_1:90
theorem :: TREES_1:91
theorem :: TREES_1:92