:: TREES_1 semantic presentation

theorem Th1: :: TREES_1:1

for b₁ being Nat
for b₂, b₃ being FinSequence st b₃ = b₂ | (Seg b₁) holds
len b₃ <= b₁

proof end;

theorem Th2: :: TREES_1:2

for b₁ being Nat
for b₂, b₃ being FinSequence st b₃ = b₂ | (Seg b₁) holds
len b₃ <= len b₂

proof end;

theorem Th3: :: TREES_1:3

for b₁ being Nat
for b₂, b₃ being FinSequence st b₃ = b₂ | (Seg b₁) holds
ex b₄ being FinSequence st b₂ = b₃ ^ b₄

proof end;

theorem Th4: :: TREES_1:4

for b₁ being set holds {} <> <*b₁*> ;

theorem Th5: :: TREES_1:5

for b₁, b₂ being FinSequence st ( b₁ = b₁ ^ b₂ or b₁ = b₂ ^ b₁ ) holds
b₂ = {}

proof end;

theorem Th6: :: TREES_1:6

for b₁ being set
for b₂, b₃ being FinSequence holds
( not b₂ ^ b₃ = <*b₁*> or ( b₂ = <*b₁*> & b₃ = {} ) or ( b₂ = {} & b₃ = <*b₁*> ) )

proof end;

notation

let c₁, c₂ be FinSequence;
synonym c₁ is_a_prefix_of c₂ for c₁ c= c₂;

end;

definition

let c₁, c₂ be FinSequence;
redefine pred c₁ c= c₂ means :Def1: :: TREES_1:def 1
ex b₁ being Nat st a₁ = a₂ | (Seg b₁);
compatibility

proof end;

end;

:: deftheorem Def1 defines is_a_prefix_of TREES_1:def 1 :

theorem Th7: :: TREES_1:7

canceled;

theorem Th8: :: TREES_1:8

for b₁, b₂ being FinSequence holds
( b₁ is_a_prefix_of b₂ iff ex b₃ being FinSequence st b₂ = b₁ ^ b₃ )

proof end;

theorem Th9: :: TREES_1:9

canceled;

theorem Th10: :: TREES_1:10

canceled;

theorem Th11: :: TREES_1:11

canceled;

theorem Th12: :: TREES_1:12

canceled;

theorem Th13: :: TREES_1:13

canceled;

theorem Th14: :: TREES_1:14

canceled;

theorem Th15: :: TREES_1:15

for b₁, b₂ being FinSequence st b₁ is_a_prefix_of b₂ & len b₁ = len b₂ holds
b₁ = b₂

proof end;

theorem Th16: :: TREES_1:16

for b₁, b₂ being set holds
( <*b₁*> is_a_prefix_of <*b₂*> iff b₁ = b₂ )

proof end;

notation

let c₁, c₂ be FinSequence;
synonym c₁ is_a_proper_prefix_of c₂ for c₁ c< c₂;

end;

Lemma7: for b₁, b₂ being finite set st b₁ c= b₂ & card b₁ = card b₂ holds
b₁ = b₂

proof end;

theorem Th17: :: TREES_1:17

canceled;

theorem Th18: :: TREES_1:18

canceled;

theorem Th19: :: TREES_1:19

for b₁, b₂ being finite set st b₁,b₂ are_c=-comparable & card b₁ = card b₂ holds
b₁ = b₂

proof end;

theorem Th20: :: TREES_1:20

canceled;

theorem Th21: :: TREES_1:21

canceled;

theorem Th22: :: TREES_1:22

canceled;

theorem Th23: :: TREES_1:23

for b₁, b₂ being set holds
( <*b₁*>,<*b₂*> are_c=-comparable iff b₁ = b₂ )

proof end;

theorem Th24: :: TREES_1:24

for b₁, b₂ being finite set st b₁ c< b₂ holds
card b₁ < card b₂

proof end;

theorem Th25: :: TREES_1:25

for b₁ being non empty set
for b₂ being FinSequence holds
( not b₂ is_a_proper_prefix_of {} & not b₂ is_a_proper_prefix_of <*> b₁ )

proof end;

theorem Th26: :: TREES_1:26

for b₁, b₂ being FinSequence holds
( not b₁ is_a_proper_prefix_of b₂ or not b₂ is_a_proper_prefix_of b₁ ) ;

theorem Th27: :: TREES_1:27

for b₁, b₂, b₃ being FinSequence st ( ( b₁ is_a_proper_prefix_of b₂ & b₂ is_a_proper_prefix_of b₃ ) or ( b₁ is_a_proper_prefix_of b₂ & b₂ is_a_prefix_of b₃ ) or ( b₁ is_a_prefix_of b₂ & b₂ is_a_proper_prefix_of b₃ ) ) holds
b₁ is_a_proper_prefix_of b₃ by XBOOLE_1:56, XBOOLE_1:58, XBOOLE_1:59;

theorem Th28: :: TREES_1:28

for b₁, b₂ being FinSequence st b₁ is_a_prefix_of b₂ holds
not b₂ is_a_proper_prefix_of b₁

proof end;

theorem Th29: :: TREES_1:29

canceled;

theorem Th30: :: TREES_1:30

for b₁ being set
for b₂, b₃ being FinSequence st b₂ ^ <*b₁*> is_a_prefix_of b₃ holds
b₂ is_a_proper_prefix_of b₃

proof end;

theorem Th31: :: TREES_1:31

for b₁ being set
for b₂, b₃ being FinSequence st b₂ is_a_prefix_of b₃ holds
b₂ is_a_proper_prefix_of b₃ ^ <*b₁*>

proof end;

theorem Th32: :: TREES_1:32

for b₁ being set
for b₂, b₃ being FinSequence st b₂ is_a_proper_prefix_of b₃ ^ <*b₁*> holds
b₂ is_a_prefix_of b₃

proof end;

theorem Th33: :: TREES_1:33

for b₁, b₂ being FinSequence st ( {} is_a_proper_prefix_of b₁ or {} <> b₁ ) holds
b₂ is_a_proper_prefix_of b₂ ^ b₁

proof end;

definition

let c₁ be FinSequence;
canceled;
canceled;
func ProperPrefixes c₁ -> set means :Def4: :: TREES_1:def 4
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being FinSequence st
( b₁ = b₂ & b₂ is_a_proper_prefix_of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 TREES_1:def 2 :

:: deftheorem Def3 TREES_1:def 3 :

:: deftheorem Def4 defines ProperPrefixes TREES_1:def 4 :

theorem Th34: :: TREES_1:34

canceled;

theorem Th35: :: TREES_1:35

for b₁ being set
for b₂ being FinSequence st b₁ in ProperPrefixes b₂ holds
b₁ is FinSequence

proof end;

theorem Th36: :: TREES_1:36

for b₁, b₂ being FinSequence holds
( b₁ in ProperPrefixes b₂ iff b₁ is_a_proper_prefix_of b₂ )

proof end;

theorem Th37: :: TREES_1:37

for b₁, b₂ being FinSequence st b₁ in ProperPrefixes b₂ holds
len b₁ < len b₂

proof end;

theorem Th38: :: TREES_1:38

for b₁, b₂, b₃ being FinSequence st b₂ ^ b₃ in ProperPrefixes b₁ holds
b₂ in ProperPrefixes b₁

proof end;

theorem Th39: :: TREES_1:39

ProperPrefixes {} = {}

proof end;

theorem Th40: :: TREES_1:40

for b₁ being set holds ProperPrefixes <*b₁*> = {{} }

proof end;

theorem Th41: :: TREES_1:41

for b₁, b₂ being FinSequence st b₁ is_a_prefix_of b₂ holds
ProperPrefixes b₁ c= ProperPrefixes b₂

proof end;

theorem Th42: :: TREES_1:42

for b₁, b₂, b₃ being FinSequence st b₂ in ProperPrefixes b₁ & b₃ in ProperPrefixes b₁ holds
b₂,b₃ are_c=-comparable

proof end;

definition

let c₁ be set ;
attr a₁ is Tree-like means :Def5: :: TREES_1:def 5
( a₁ c= NAT * & ( for b₁ being FinSequence of NAT st b₁ in a₁ holds
ProperPrefixes b₁ c= a₁ ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being Nat st b₁ ^ <*b₂*> in a₁ & b₃ <= b₂ holds
b₁ ^ <*b₃*> in a₁ ) );

end;

:: deftheorem Def5 defines Tree-like TREES_1:def 5 :

registration

cluster non empty Tree-like set ;
existence

proof end;

end;

definition

mode Tree is non empty Tree-like set ;

end;

theorem Th43: :: TREES_1:43

canceled;

theorem Th44: :: TREES_1:44

for b₁ being set
for b₂ being Tree st b₁ in b₂ holds
b₁ is FinSequence of NAT

proof end;

definition

let c₁ be Tree;
redefine mode Element as Element of c₁ -> FinSequence of NAT ;
coherence by Th44;

end;

theorem Th45: :: TREES_1:45

for b₁ being Tree
for b₂, b₃ being FinSequence st b₂ in b₁ & b₃ is_a_prefix_of b₂ holds
b₃ in b₁

proof end;

theorem Th46: :: TREES_1:46

for b₁ being FinSequence of NAT
for b₂ being Tree
for b₃ being FinSequence st b₁ ^ b₃ in b₂ holds
b₁ in b₂

proof end;

theorem Th47: :: TREES_1:47

for b₁ being Tree holds
( {} in b₁ & <*> NAT in b₁ )

proof end;

theorem Th48: :: TREES_1:48

{{} } is Tree

proof end;

theorem Th49: :: TREES_1:49

for b₁, b₂ being Tree holds b₁ \/ b₂ is Tree

proof end;

theorem Th50: :: TREES_1:50

for b₁, b₂ being Tree holds b₁ /\ b₂ is Tree

proof end;

registration

cluster finite set ;
existence by Th48;

end;

theorem Th51: :: TREES_1:51

canceled;

theorem Th52: :: TREES_1:52

for b₁, b₂ being finite Tree holds b₁ \/ b₂ is finite Tree by Th49;

theorem Th53: :: TREES_1:53

for b₁ being Tree
for b₂ being finite Tree holds
( b₂ /\ b₁ is finite Tree & b₁ /\ b₂ is finite Tree ) by Th50;

definition

let c₁ be Nat;
canceled;
func elementary_tree c₁ -> finite Tree equals :: TREES_1:def 7
{ <*b₁*> where B is Nat : b₁ < a₁ } \/ {{} };
correctness

proof end;

end;

:: deftheorem Def6 TREES_1:def 6 :

:: deftheorem Def7 defines elementary_tree TREES_1:def 7 :

theorem Th54: :: TREES_1:54

canceled;

theorem Th55: :: TREES_1:55

for b₁, b₂ being Nat st b₁ < b₂ holds
<*b₁*> in elementary_tree b₂

proof end;

theorem Th56: :: TREES_1:56

elementary_tree 0 = {{} }

proof end;

theorem Th57: :: TREES_1:57

for b₁ being Nat
for b₂ being FinSequence of NAT holds
( not b₂ in elementary_tree b₁ or b₂ = {} or ex b₃ being Nat st
( b₃ < b₁ & b₂ = <*b₃*> ) )

proof end;

definition

let c₁ be Tree;
func Leaves c₁ -> Subset of a₁ means :: TREES_1:def 8
for b₁ being FinSequence of NAT holds
( b₁ in a₂ iff ( b₁ in a₁ & ( for b₂ being FinSequence of NAT holds
( not b₂ in a₁ or not b₁ is_a_proper_prefix_of b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

let c₂ be FinSequence of NAT ;
assume E32: c₂ in c₁ ;
func c₁ | c₂ -> Tree means :Def9: :: TREES_1:def 9
for b₁ being FinSequence of NAT holds
( b₁ in a₃ iff a₂ ^ b₁ in a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Leaves TREES_1:def 8 :

:: deftheorem Def9 defines | TREES_1:def 9 :

theorem Th58: :: TREES_1:58

canceled;

theorem Th59: :: TREES_1:59

canceled;

theorem Th60: :: TREES_1:60

for b₁ being Tree holds b₁ | (<*> NAT ) = b₁

proof end;

registration

let c₁ be finite Tree;
let c₂ be Element of c₁;
cluster a₁ | a₂ -> finite ;
coherence

proof end;

end;

definition

let c₁ be Tree;
assume E33: Leaves c₁ <> {} ;
mode Leaf of c₁ -> Element of a₁ means :: TREES_1:def 10
a₂ in Leaves a₁;
existence

proof end;

end;

:: deftheorem Def10 defines Leaf TREES_1:def 10 :

definition

let c₁ be Tree;
mode Subtree of c₁ -> Tree means :: TREES_1:def 11
ex b₁ being Element of a₁ st a₂ = a₁ | b₁;
existence

proof end;

end;

:: deftheorem Def11 defines Subtree TREES_1:def 11 :

definition

let c₁ be Tree;
let c₂ be FinSequence of NAT ;
let c₃ be Tree;
assume E33: c₂ in c₁ ;
func c₁ with-replacement c₂,c₃ -> Tree means :Def12: :: TREES_1:def 12
for b₁ being FinSequence of NAT holds
( b₁ in a₄ iff ( ( b₁ in a₁ & not a₂ is_a_proper_prefix_of b₁ ) or ex b₂ being FinSequence of NAT st
( b₂ in a₃ & b₁ = a₂ ^ b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines with-replacement TREES_1:def 12 :

theorem Th61: :: TREES_1:61

canceled;

theorem Th62: :: TREES_1:62

canceled;

theorem Th63: :: TREES_1:63

canceled;

theorem Th64: :: TREES_1:64

for b₁ being FinSequence of NAT
for b₂, b₃ being Tree st b₁ in b₂ holds
b₂ with-replacement b₁,b₃ = { b₄ where B is Element of b₂ : not b₁ is_a_proper_prefix_of b₄ } \/ { (b₁ ^ b₄) where B is Element of b₃ : b₄ = b₄ }

proof end;

theorem Th65: :: TREES_1:65

canceled;

theorem Th66: :: TREES_1:66

for b₁ being FinSequence of NAT
for b₂, b₃ being Tree st b₁ in b₂ holds
b₃ = (b₂ with-replacement b₁,b₃) | b₁

proof end;

registration

let c₁ be finite Tree;
let c₂ be Element of c₁;
let c₃ be finite Tree;
cluster a₁ with-replacement a₂,a₃ -> finite ;
coherence

proof end;

end;

theorem Th67: :: TREES_1:67

for b₁ being FinSequence holds ProperPrefixes b₁, dom b₁ are_equipotent

proof end;

registration

let c₁ be FinSequence;
cluster ProperPrefixes a₁ -> finite ;
coherence

proof end;

end;

theorem Th68: :: TREES_1:68

for b₁ being FinSequence holds card (ProperPrefixes b₁) = len b₁

proof end;

definition

let c₁ be set ;
attr a₁ is AntiChain_of_Prefixes-like means :Def13: :: TREES_1:def 13
( ( for b₁ being set st b₁ in a₁ holds
b₁ is FinSequence ) & ( for b₁, b₂ being FinSequence st b₁ in a₁ & b₂ in a₁ & b₁ <> b₂ holds
not b₁,b₂ are_c=-comparable ) );

end;

:: deftheorem Def13 defines AntiChain_of_Prefixes-like TREES_1:def 13 :

registration

cluster AntiChain_of_Prefixes-like set ;
existence

proof end;

end;

definition

mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;

end;

theorem Th69: :: TREES_1:69

canceled;

theorem Th70: :: TREES_1:70

for b₁ being FinSequence holds {b₁} is AntiChain_of_Prefixes-like

proof end;

theorem Th71: :: TREES_1:71

for b₁, b₂ being FinSequence st not b₁,b₂ are_c=-comparable holds
{b₁,b₂} is AntiChain_of_Prefixes-like

proof end;

definition

let c₁ be Tree;
mode AntiChain_of_Prefixes of c₁ -> AntiChain_of_Prefixes means :Def14: :: TREES_1:def 14
a₂ c= a₁;
existence

proof end;

end;

:: deftheorem Def14 defines AntiChain_of_Prefixes TREES_1:def 14 :

theorem Th72: :: TREES_1:72

canceled;

theorem Th73: :: TREES_1:73

for b₁ being Tree holds
( {} is AntiChain_of_Prefixes of b₁ & {{} } is AntiChain_of_Prefixes of b₁ )

proof end;

theorem Th74: :: TREES_1:74

for b₁ being Tree
for b₂ being Element of b₁ holds {b₂} is AntiChain_of_Prefixes of b₁

proof end;

theorem Th75: :: TREES_1:75

for b₁ being Tree
for b₂, b₃ being Element of b₁ st not b₂,b₃ are_c=-comparable holds
{b₂,b₃} is AntiChain_of_Prefixes of b₁

proof end;

registration

let c₁ be finite Tree;
cluster -> finite AntiChain_of_Prefixes of a₁;
coherence

proof end;

end;

definition

let c₁ be finite Tree;
func height c₁ -> Nat means :Def15: :: TREES_1:def 15
( ex b₁ being FinSequence of NAT st
( b₁ in a₁ & len b₁ = a₂ ) & ( for b₁ being FinSequence of NAT st b₁ in a₁ holds
len b₁ <= a₂ ) );
existence

proof end;

uniqueness

proof end;

func width c₁ -> Nat means :Def16: :: TREES_1:def 16
ex b₁ being AntiChain_of_Prefixes of a₁ st
( a₂ = card b₁ & ( for b₂ being AntiChain_of_Prefixes of a₁ holds card b₂ <= card b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines height TREES_1:def 15 :

:: deftheorem Def16 defines width TREES_1:def 16 :

theorem Th76: :: TREES_1:76

canceled;

theorem Th77: :: TREES_1:77

canceled;

theorem Th78: :: TREES_1:78

for b₁ being finite Tree holds 1 <= width b₁

proof end;

theorem Th79: :: TREES_1:79

height (elementary_tree 0) = 0

proof end;

theorem Th80: :: TREES_1:80

for b₁ being finite Tree st height b₁ = 0 holds
b₁ = elementary_tree 0

proof end;

theorem Th81: :: TREES_1:81

for b₁ being Nat holds height (elementary_tree (b₁ + 1)) = 1

proof end;

theorem Th82: :: TREES_1:82

width (elementary_tree 0) = 1

proof end;

theorem Th83: :: TREES_1:83

for b₁ being Nat holds width (elementary_tree (b₁ + 1)) = b₁ + 1

proof end;

theorem Th84: :: TREES_1:84

for b₁ being finite Tree
for b₂ being Element of b₁ holds height (b₁ | b₂) <= height b₁

proof end;

theorem Th85: :: TREES_1:85

for b₁ being finite Tree
for b₂ being Element of b₁ st b₂ <> {} holds
height (b₁ | b₂) < height b₁

proof end;

scheme :: TREES_1:sch 1
s1{ P₁[ Tree] } :

for b₁ being finite Tree holds P₁[b₁]

provided

E44: for b₁ being finite Tree st ( for b₂ being Nat st <*b₂*> in b₁ holds
P₁[b₁ | <*b₂*>] ) holds
P₁[b₁]

proof end;