begin
:: deftheorem Def1 defines is_a_prefix_of TREES_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
Lm1:
for A, B being finite set st A c= B & card A = card B holds
A = B
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th23:
theorem Th24:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem
:: deftheorem TREES_1:def 2 :
canceled;
:: deftheorem TREES_1:def 3 :
canceled;
:: deftheorem Def4 defines ProperPrefixes TREES_1:def 4 :
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem
theorem Th42:
:: deftheorem Def5 defines Tree-like TREES_1:def 5 :
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
canceled;
theorem
theorem
:: deftheorem TREES_1:def 6 :
canceled;
:: deftheorem defines elementary_tree TREES_1:def 7 :
theorem
canceled;
theorem Th55:
theorem Th56:
theorem
:: deftheorem Def8 defines Leaves TREES_1:def 8 :
:: deftheorem Def9 defines | TREES_1:def 9 :
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines Leaf TREES_1:def 10 :
:: deftheorem defines Subtree TREES_1:def 11 :
:: deftheorem Def12 defines with-replacement TREES_1:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th64:
theorem
canceled;
theorem
theorem Th67:
theorem
:: deftheorem Def13 defines AntiChain_of_Prefixes-like TREES_1:def 13 :
theorem
canceled;
theorem Th70:
theorem Th71:
:: deftheorem Def14 defines AntiChain_of_Prefixes TREES_1:def 14 :
theorem
canceled;
theorem Th73:
theorem
theorem
:: deftheorem Def15 defines height TREES_1:def 15 :
:: deftheorem Def16 defines width TREES_1:def 16 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th85:
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem