:: QC_LANG4 semantic presentation

theorem Th1: :: QC_LANG4:1

canceled;

theorem Th2: :: QC_LANG4:2

canceled;

theorem Th3: :: QC_LANG4:3

canceled;

theorem Th4: :: QC_LANG4:4

for b₁ being Nat
for b₂ being FinSequence ex b₃ being FinSequence st
( b₃ = b₂ | (Seg b₁) & b₃ is_a_prefix_of b₂ )

proof end;

theorem Th5: :: QC_LANG4:5

canceled;

theorem Th6: :: QC_LANG4:6

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being FinSequence
for b₅ being Nat st b₅ + 1 <= len b₂ & b₃ = b₂ | (Seg (b₅ + 1)) & b₄ = b₂ | (Seg b₅) holds
ex b₆ being Element of b₁ st b₃ = b₄ ^ <*b₆*>

proof end;

theorem Th7: :: QC_LANG4:7

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being FinSequence st 1 <= len b₂ & b₃ = b₂ | (Seg 1) holds
ex b₄ being Element of b₁ st b₃ = <*b₄*>

proof end;

registration

let c₁ be non empty set ;
cluster finite ParametrizedSubset of a₁;
existence

proof end;

end;

theorem Th8: :: QC_LANG4:8

for b₁ being DecoratedTree
for b₂ being FinSequence of NAT holds b₁ . b₂ = (b₁ | b₂) . {}

proof end;

theorem Th9: :: QC_LANG4:9

for b₁ being finite-branching DecoratedTree
for b₂ being Element of dom b₁ holds succ b₁,b₂ = b₁ * (b₂ succ )

proof end;

theorem Th10: :: QC_LANG4:10

for b₁ being finite-branching DecoratedTree
for b₂ being Element of dom b₁ holds dom (b₁ * (b₂ succ )) = dom (b₂ succ )

proof end;

theorem Th11: :: QC_LANG4:11

for b₁ being finite-branching DecoratedTree
for b₂ being Element of dom b₁ holds dom (succ b₁,b₂) = dom (b₂ succ )

proof end;

theorem Th12: :: QC_LANG4:12

for b₁ being finite-branching DecoratedTree
for b₂ being Element of dom b₁
for b₃ being Nat holds
( b₂ ^ <*b₃*> in dom b₁ iff b₃ + 1 in dom (b₂ succ ) )

proof end;

theorem Th13: :: QC_LANG4:13

for b₁ being finite-branching DecoratedTree
for b₂ being FinSequence
for b₃ being Nat st b₂ ^ <*b₃*> in dom b₁ holds
b₁ . (b₂ ^ <*b₃*>) = (succ b₁,b₂) . (b₃ + 1)

proof end;

theorem Th14: :: QC_LANG4:14

for b₁ being finite-branching DecoratedTree
for b₂, b₃ being Element of dom b₁ st b₂ in succ b₃ holds
b₁ . b₂ in rng (succ b₁,b₃)

proof end;

theorem Th15: :: QC_LANG4:15

for b₁ being finite-branching DecoratedTree
for b₂ being Element of dom b₁
for b₃ being set st b₃ in rng (succ b₁,b₂) holds
ex b₄ being Element of dom b₁ st
( b₃ = b₁ . b₄ & b₄ in succ b₂ )

proof end;

scheme :: QC_LANG4:sch 1
s1{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> FinSequence of F₁() } :

ex b₁ being finite-branching DecoratedTree of F₁() st
( b₁ . {} = F₂() & ( for b₂ being Element of dom b₁
for b₃ being Element of F₁() st b₃ = b₁ . b₂ holds
succ b₁,b₂ = F₃(b₃) ) )

proof end;

theorem Th16: :: QC_LANG4:16

for b₁ being Tree
for b₂ being Element of b₁ holds ProperPrefixes b₂ is finite Chain of b₁

proof end;

theorem Th17: :: QC_LANG4:17

for b₁ being Tree holds b₁ -level 0 = {{} }

proof end;

theorem Th18: :: QC_LANG4:18

for b₁ being Nat
for b₂ being Tree holds b₂ -level (b₁ + 1) = union { (succ b₃) where B is Element of b₂ : len b₃ = b₁ }

proof end;

theorem Th19: :: QC_LANG4:19

for b₁ being finite-branching Tree
for b₂ being Nat holds b₁ -level b₂ is finite

proof end;

theorem Th20: :: QC_LANG4:20

for b₁ being finite-branching Tree holds
( b₁ is finite iff ex b₂ being Nat st b₁ -level b₂ = {} )

proof end;

theorem Th21: :: QC_LANG4:21

for b₁ being finite-branching Tree st not b₁ is finite holds
ex b₂ being Chain of b₁ st not b₂ is finite

proof end;

theorem Th22: :: QC_LANG4:22

for b₁ being finite-branching Tree st not b₁ is finite holds
ex b₂ being Branch of b₁ st not b₂ is finite

proof end;

theorem Th23: :: QC_LANG4:23

for b₁ being Tree
for b₂ being Chain of b₁
for b₃ being Element of b₁ st b₃ in b₂ & not b₂ is finite holds
ex b₄ being Element of b₁ st
( b₄ in b₂ & b₃ is_a_proper_prefix_of b₄ )

proof end;

theorem Th24: :: QC_LANG4:24

for b₁ being Tree
for b₂ being Branch of b₁
for b₃ being Element of b₁ st b₃ in b₂ & not b₂ is finite holds
ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ in succ b₃ )

proof end;

theorem Th25: :: QC_LANG4:25

for b₁ being Function of NAT , NAT st ( for b₂ being Nat holds b₁ . (b₂ + 1) <= b₁ . b₂ ) holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ = b₁ . b₂

proof end;

scheme :: QC_LANG4:sch 2
s2{ F₁() -> non empty set , F₂() -> finite-branching DecoratedTree of F₁(), F₃( Element of F₁()) -> Nat } :

F₂() is finite

provided

E22: for b₁, b₂ being Element of dom F₂()
for b₃ being Element of F₁() st b₂ in succ b₁ & b₃ = F₂() . b₂ holds
F₃(b₃) < F₃((F₂() . b₁))

proof end;

theorem Th26: :: QC_LANG4:26

for b₁ being non empty set
for b₂ being DecoratedTree of b₁
for b₃ being set st b₃ in rng b₂ holds
b₃ is Element of b₁

proof end;

theorem Th27: :: QC_LANG4:27

for b₁ being non empty set
for b₂ being DecoratedTree of b₁
for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ is Element of b₁

proof end;

theorem Th28: :: QC_LANG4:28

for b₁, b₂ being Element of QC-WFF st b₁ is_subformula_of b₂ holds
len (@ b₁) <= len (@ b₂)

proof end;

theorem Th29: :: QC_LANG4:29

for b₁, b₂ being Element of QC-WFF st b₁ is_subformula_of b₂ & len (@ b₁) = len (@ b₂) holds
b₁ = b₂

proof end;

definition

let c₁ be Element of QC-WFF ;
func list_of_immediate_constituents c₁ -> FinSequence of QC-WFF equals :Def1: :: QC_LANG4:def 1
<*> QC-WFF if ( a₁ = VERUM or a₁ is atomic )
<*(the_argument_of a₁)*> if a₁ is negative
<*(the_left_argument_of a₁),(the_right_argument_of a₁)*> if a₁ is conjunctive
otherwise <*(the_scope_of a₁)*>;
coherence ;
consistency by QC_LANG1:51;

end;

:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :

theorem Th30: :: QC_LANG4:30

for b₁ being Nat
for b₂, b₃ being Element of QC-WFF st b₁ in dom (list_of_immediate_constituents b₂) & b₃ = (list_of_immediate_constituents b₂) . b₁ holds
b₃ is_immediate_constituent_of b₂

proof end;

theorem Th31: :: QC_LANG4:31

for b₁ being Element of QC-WFF holds rng (list_of_immediate_constituents b₁) = { b₂ where B is Element of QC-WFF : b₂ is_immediate_constituent_of b₁ }

proof end;

definition

let c₁ be Element of QC-WFF ;
func tree_of_subformulae c₁ -> finite DecoratedTree of QC-WFF means :Def2: :: QC_LANG4:def 2
( a₂ . {} = a₁ & ( for b₁ being Element of dom a₂ holds succ a₂,b₁ = list_of_immediate_constituents (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :

theorem Th32: :: QC_LANG4:32

canceled;

theorem Th33: :: QC_LANG4:33

canceled;

theorem Th34: :: QC_LANG4:34

for b₁ being Element of QC-WFF holds b₁ in rng (tree_of_subformulae b₁)

proof end;

theorem Th35: :: QC_LANG4:35

for b₁ being Nat
for b₂ being Element of QC-WFF
for b₃ being Element of dom (tree_of_subformulae b₂) st b₃ ^ <*b₁*> in dom (tree_of_subformulae b₂) holds
ex b₄ being Element of QC-WFF st
( b₄ = (tree_of_subformulae b₂) . (b₃ ^ <*b₁*>) & b₄ is_immediate_constituent_of (tree_of_subformulae b₂) . b₃ )

proof end;

theorem Th36: :: QC_LANG4:36

for b₁, b₂ being Element of QC-WFF
for b₃ being Element of dom (tree_of_subformulae b₂) holds
( b₁ is_immediate_constituent_of (tree_of_subformulae b₂) . b₃ iff ex b₄ being Nat st
( b₃ ^ <*b₄*> in dom (tree_of_subformulae b₂) & b₁ = (tree_of_subformulae b₂) . (b₃ ^ <*b₄*>) ) )

proof end;

theorem Th37: :: QC_LANG4:37

for b₁, b₂, b₃ being Element of QC-WFF st b₁ in rng (tree_of_subformulae b₂) & b₃ is_immediate_constituent_of b₁ holds
b₃ in rng (tree_of_subformulae b₂)

proof end;

theorem Th38: :: QC_LANG4:38

for b₁, b₂, b₃ being Element of QC-WFF st b₁ in rng (tree_of_subformulae b₂) & b₃ is_subformula_of b₁ holds
b₃ in rng (tree_of_subformulae b₂)

proof end;

theorem Th39: :: QC_LANG4:39

for b₁, b₂ being Element of QC-WFF holds
( b₁ in rng (tree_of_subformulae b₂) iff b₁ is_subformula_of b₂ )

proof end;

theorem Th40: :: QC_LANG4:40

for b₁ being Element of QC-WFF holds rng (tree_of_subformulae b₁) = Subformulae b₁

proof end;

theorem Th41: :: QC_LANG4:41

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ in succ b₃ holds
(tree_of_subformulae b₁) . b₂ is_immediate_constituent_of (tree_of_subformulae b₁) . b₃

proof end;

theorem Th42: :: QC_LANG4:42

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ is_a_prefix_of b₃ holds
(tree_of_subformulae b₁) . b₃ is_subformula_of (tree_of_subformulae b₁) . b₂

proof end;

theorem Th43: :: QC_LANG4:43

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ is_a_proper_prefix_of b₃ holds
len (@ ((tree_of_subformulae b₁) . b₃)) < len (@ ((tree_of_subformulae b₁) . b₂))

proof end;

theorem Th44: :: QC_LANG4:44

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ is_a_proper_prefix_of b₃ holds
(tree_of_subformulae b₁) . b₃ <> (tree_of_subformulae b₁) . b₂

proof end;

theorem Th45: :: QC_LANG4:45

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ is_a_proper_prefix_of b₃ holds
(tree_of_subformulae b₁) . b₃ is_proper_subformula_of (tree_of_subformulae b₁) . b₂

proof end;

theorem Th46: :: QC_LANG4:46

for b₁ being Element of QC-WFF
for b₂ being Element of dom (tree_of_subformulae b₁) holds
( (tree_of_subformulae b₁) . b₂ = b₁ iff b₂ = {} )

proof end;

theorem Th47: :: QC_LANG4:47

for b₁ being Element of QC-WFF
for b₂, b₃ being Element of dom (tree_of_subformulae b₁) st b₂ <> b₃ & (tree_of_subformulae b₁) . b₂ = (tree_of_subformulae b₁) . b₃ holds
not b₂,b₃ are_c=-comparable

proof end;

definition

let c₁, c₂ be Element of QC-WFF ;
func c₁ -entry_points_in_subformula_tree_of c₂ -> AntiChain_of_Prefixes of dom (tree_of_subformulae a₁) means :Def3: :: QC_LANG4:def 3
for b₁ being Element of dom (tree_of_subformulae a₁) holds
( b₁ in a₃ iff (tree_of_subformulae a₁) . b₁ = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :

theorem Th48: :: QC_LANG4:48

canceled;

theorem Th49: :: QC_LANG4:49

for b₁, b₂ being Element of QC-WFF holds b₁ -entry_points_in_subformula_tree_of b₂ = { b₃ where B is Element of dom (tree_of_subformulae b₁) : (tree_of_subformulae b₁) . b₃ = b₂ }

proof end;

theorem Th50: :: QC_LANG4:50

for b₁, b₂ being Element of QC-WFF holds
( b₁ is_subformula_of b₂ iff b₂ -entry_points_in_subformula_tree_of b₁ <> {} )

proof end;

theorem Th51: :: QC_LANG4:51

for b₁ being Nat
for b₂ being Element of QC-WFF
for b₃, b₄ being Element of dom (tree_of_subformulae b₂) st b₃ = b₄ ^ <*b₁*> & (tree_of_subformulae b₂) . b₄ is negative holds
( (tree_of_subformulae b₂) . b₃ = the_argument_of ((tree_of_subformulae b₂) . b₄) & b₁ = 0 )

proof end;

theorem Th52: :: QC_LANG4:52

for b₁ being Nat
for b₂ being Element of QC-WFF
for b₃, b₄ being Element of dom (tree_of_subformulae b₂) st b₃ = b₄ ^ <*b₁*> & (tree_of_subformulae b₂) . b₄ is conjunctive & not ( (tree_of_subformulae b₂) . b₃ = the_left_argument_of ((tree_of_subformulae b₂) . b₄) & b₁ = 0 ) holds
( (tree_of_subformulae b₂) . b₃ = the_right_argument_of ((tree_of_subformulae b₂) . b₄) & b₁ = 1 )

proof end;

theorem Th53: :: QC_LANG4:53

for b₁ being Nat
for b₂ being Element of QC-WFF
for b₃, b₄ being Element of dom (tree_of_subformulae b₂) st b₃ = b₄ ^ <*b₁*> & (tree_of_subformulae b₂) . b₄ is universal holds
( (tree_of_subformulae b₂) . b₃ = the_scope_of ((tree_of_subformulae b₂) . b₄) & b₁ = 0 )

proof end;

theorem Th54: :: QC_LANG4:54

for b₁ being Element of QC-WFF
for b₂ being Element of dom (tree_of_subformulae b₁) st (tree_of_subformulae b₁) . b₂ is negative holds
( b₂ ^ <*0*> in dom (tree_of_subformulae b₁) & (tree_of_subformulae b₁) . (b₂ ^ <*0*>) = the_argument_of ((tree_of_subformulae b₁) . b₂) )

proof end;

Lemma47: for b₁, b₂ being set holds dom <*b₁,b₂*> = Seg 2

proof end;

theorem Th55: :: QC_LANG4:55

for b₁ being Element of QC-WFF
for b₂ being Element of dom (tree_of_subformulae b₁) st (tree_of_subformulae b₁) . b₂ is conjunctive holds
( b₂ ^ <*0*> in dom (tree_of_subformulae b₁) & (tree_of_subformulae b₁) . (b₂ ^ <*0*>) = the_left_argument_of ((tree_of_subformulae b₁) . b₂) & b₂ ^ <*1*> in dom (tree_of_subformulae b₁) & (tree_of_subformulae b₁) . (b₂ ^ <*1*>) = the_right_argument_of ((tree_of_subformulae b₁) . b₂) )

proof end;

theorem Th56: :: QC_LANG4:56

for b₁ being Element of QC-WFF
for b₂ being Element of dom (tree_of_subformulae b₁) st (tree_of_subformulae b₁) . b₂ is universal holds
( b₂ ^ <*0*> in dom (tree_of_subformulae b₁) & (tree_of_subformulae b₁) . (b₂ ^ <*0*>) = the_scope_of ((tree_of_subformulae b₁) . b₂) )

proof end;

theorem Th57: :: QC_LANG4:57

for b₁, b₂, b₃ being Element of QC-WFF
for b₄ being Element of dom (tree_of_subformulae b₁)
for b₅ being Element of dom (tree_of_subformulae b₂) st b₄ in b₁ -entry_points_in_subformula_tree_of b₂ & b₅ in b₂ -entry_points_in_subformula_tree_of b₃ holds
b₄ ^ b₅ in b₁ -entry_points_in_subformula_tree_of b₃

proof end;

theorem Th58: :: QC_LANG4:58

for b₁, b₂, b₃ being Element of QC-WFF
for b₄ being Element of dom (tree_of_subformulae b₁)
for b₅ being FinSequence st b₄ in b₁ -entry_points_in_subformula_tree_of b₂ & b₄ ^ b₅ in b₁ -entry_points_in_subformula_tree_of b₃ holds
b₅ in b₂ -entry_points_in_subformula_tree_of b₃

proof end;

theorem Th59: :: QC_LANG4:59

for b₁, b₂, b₃ being Element of QC-WFF holds { (b₄ ^ b₅) where B is Element of dom (tree_of_subformulae b₁), B is Element of dom (tree_of_subformulae b₂) : ( b₄ in b₁ -entry_points_in_subformula_tree_of b₂ & b₅ in b₂ -entry_points_in_subformula_tree_of b₃ ) } c= b₁ -entry_points_in_subformula_tree_of b₃

proof end;

theorem Th60: :: QC_LANG4:60

for b₁ being Element of QC-WFF
for b₂ being Element of dom (tree_of_subformulae b₁) holds (tree_of_subformulae b₁) | b₂ = tree_of_subformulae ((tree_of_subformulae b₁) . b₂)

proof end;

theorem Th61: :: QC_LANG4:61

for b₁, b₂ being Element of QC-WFF
for b₃ being Element of dom (tree_of_subformulae b₁) holds
( b₃ in b₁ -entry_points_in_subformula_tree_of b₂ iff (tree_of_subformulae b₁) | b₃ = tree_of_subformulae b₂ )

proof end;

theorem Th62: :: QC_LANG4:62

for b₁, b₂ being Element of QC-WFF holds b₁ -entry_points_in_subformula_tree_of b₂ = { b₃ where B is Element of dom (tree_of_subformulae b₁) : (tree_of_subformulae b₁) | b₃ = tree_of_subformulae b₂ }

proof end;

theorem Th63: :: QC_LANG4:63

for b₁, b₂, b₃ being Element of QC-WFF
for b₄ being Chain of dom (tree_of_subformulae b₁) st b₂ in { ((tree_of_subformulae b₁) . b₅) where B is Element of dom (tree_of_subformulae b₁) : b₅ in b₄ } & b₃ in { ((tree_of_subformulae b₁) . b₅) where B is Element of dom (tree_of_subformulae b₁) : b₅ in b₄ } & not b₂ is_subformula_of b₃ holds
b₃ is_subformula_of b₂

proof end;

definition

let c₁ be Element of QC-WFF ;
mode Subformula of c₁ -> Element of QC-WFF means :Def4: :: QC_LANG4:def 4
a₂ is_subformula_of a₁;
existence ;

end;

:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :

definition

let c₁ be Element of QC-WFF ;
let c₂ be Subformula of c₁;
mode Entry_Point_in_Subformula_Tree of c₂ -> Element of dom (tree_of_subformulae a₁) means :Def5: :: QC_LANG4:def 5
(tree_of_subformulae a₁) . a₃ = a₂;
existence

proof end;

end;

:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :

theorem Th64: :: QC_LANG4:64

canceled;

theorem Th65: :: QC_LANG4:65

for b₁ being Element of QC-WFF
for b₂ being Subformula of b₁
for b₃, b₄ being Entry_Point_in_Subformula_Tree of b₂ st b₃ <> b₄ holds
not b₃,b₄ are_c=-comparable

proof end;

definition

let c₁ be Element of QC-WFF ;
let c₂ be Subformula of c₁;
func entry_points_in_subformula_tree c₂ -> non empty AntiChain_of_Prefixes of dom (tree_of_subformulae a₁) equals :: QC_LANG4:def 6
a₁ -entry_points_in_subformula_tree_of a₂;
coherence

proof end;

end;

:: deftheorem Def6 defines entry_points_in_subformula_tree QC_LANG4:def 6 :

theorem Th66: :: QC_LANG4:66

canceled;

theorem Th67: :: QC_LANG4:67

for b₁ being Element of QC-WFF
for b₂ being Subformula of b₁
for b₃ being Entry_Point_in_Subformula_Tree of b₂ holds b₃ in entry_points_in_subformula_tree b₂

proof end;

theorem Th68: :: QC_LANG4:68

for b₁ being Element of QC-WFF
for b₂ being Subformula of b₁ holds entry_points_in_subformula_tree b₂ = { b₃ where B is Entry_Point_in_Subformula_Tree of b₂ : b₃ = b₃ }

proof end;

theorem Th69: :: QC_LANG4:69

for b₁ being Element of QC-WFF
for b₂, b₃ being Subformula of b₁
for b₄ being Entry_Point_in_Subformula_Tree of b₂
for b₅ being Element of dom (tree_of_subformulae b₂) st b₅ in b₂ -entry_points_in_subformula_tree_of b₃ holds
b₄ ^ b₅ is Entry_Point_in_Subformula_Tree of b₃

proof end;

theorem Th70: :: QC_LANG4:70

for b₁ being Element of QC-WFF
for b₂, b₃ being Subformula of b₁
for b₄ being Entry_Point_in_Subformula_Tree of b₃
for b₅ being FinSequence st b₄ ^ b₅ is Entry_Point_in_Subformula_Tree of b₂ holds
b₅ in b₃ -entry_points_in_subformula_tree_of b₂

proof end;

theorem Th71: :: QC_LANG4:71

for b₁ being Element of QC-WFF
for b₂, b₃ being Subformula of b₁ holds { (b₄ ^ b₅) where B is Entry_Point_in_Subformula_Tree of b₂, B is Element of dom (tree_of_subformulae b₂) : b₅ in b₂ -entry_points_in_subformula_tree_of b₃ } = { (b₄ ^ b₅) where B is Element of dom (tree_of_subformulae b₁), B is Element of dom (tree_of_subformulae b₂) : ( b₄ in b₁ -entry_points_in_subformula_tree_of b₂ & b₅ in b₂ -entry_points_in_subformula_tree_of b₃ ) }

proof end;

theorem Th72: :: QC_LANG4:72

proof end;

theorem Th73: :: QC_LANG4:73

for b₁ being Element of QC-WFF
for b₂, b₃ being Subformula of b₁ st ex b₄ being Entry_Point_in_Subformula_Tree of b₂ex b₅ being Entry_Point_in_Subformula_Tree of b₃ st b₄ is_a_prefix_of b₅ holds
b₃ is_subformula_of b₂

proof end;

theorem Th74: :: QC_LANG4:74

for b₁ being Element of QC-WFF
for b₂, b₃ being Subformula of b₁ st b₂ is_subformula_of b₃ holds
for b₄ being Entry_Point_in_Subformula_Tree of b₃ ex b₅ being Entry_Point_in_Subformula_Tree of b₂ st b₄ is_a_prefix_of b₅

proof end;