:: TREES_A semantic presentation

theorem Th1: :: TREES_A:1

for b₁, b₂, b₃, b₄ being FinSequence st b₁ ^ b₂ = b₄ ^ b₃ holds
b₁,b₄ are_c=-comparable

proof end;

definition

let c₁, c₂ be Tree;
let c₃ be AntiChain_of_Prefixes of c₁;
assume E2: c₃ <> {} ;
func tree c₁,c₃,c₂ -> Tree means :Def1: :: TREES_A:def 1
for b₁ being FinSequence of NAT holds
( b₁ in a₄ iff ( ( b₁ in a₁ & ( for b₂ being FinSequence of NAT st b₂ in a₃ holds
not b₂ is_a_proper_prefix_of b₁ ) ) or ex b₂, b₃ being FinSequence of NAT st
( b₂ in a₃ & b₃ in a₂ & b₁ = b₂ ^ b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines tree TREES_A:def 1 :

theorem Th2: :: TREES_A:2

for b₁, b₂ being Tree
for b₃ being AntiChain_of_Prefixes of b₁ st b₃ <> {} holds
tree b₁,b₃,b₂ = { b₄ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₅ in b₃ holds
not b₅ is_a_proper_prefix_of b₄ } \/ { (b₄ ^ b₅) where B is Element of b₁, B is Element of b₂ : b₄ in b₃ }

proof end;

theorem Th3: :: TREES_A:3

for b₁ being Tree
for b₂ being AntiChain_of_Prefixes of b₁ holds { b₃ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₄ in b₂ holds
not b₄ is_a_prefix_of b₃ } c= { b₃ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₄ in b₂ holds
not b₄ is_a_proper_prefix_of b₃ }

proof end;

theorem Th4: :: TREES_A:4

for b₁ being Tree
for b₂ being AntiChain_of_Prefixes of b₁ holds b₂ c= { b₃ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₄ in b₂ holds
not b₄ is_a_proper_prefix_of b₃ }

proof end;

theorem Th5: :: TREES_A:5

for b₁ being Tree
for b₂ being AntiChain_of_Prefixes of b₁ holds { b₃ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₄ in b₂ holds
not b₄ is_a_proper_prefix_of b₃ } \ { b₃ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₄ in b₂ holds
not b₄ is_a_prefix_of b₃ } = b₂

proof end;

theorem Th6: :: TREES_A:6

for b₁, b₂ being Tree
for b₃ being AntiChain_of_Prefixes of b₁ holds b₃ c= { (b₄ ^ b₅) where B is Element of b₁, B is Element of b₂ : b₄ in b₃ }

proof end;

theorem Th7: :: TREES_A:7

for b₁, b₂ being Tree
for b₃ being AntiChain_of_Prefixes of b₁ st b₃ <> {} holds
tree b₁,b₃,b₂ = { b₄ where B is Element of b₁ : for b₁ being FinSequence of NAT st b₅ in b₃ holds
not b₅ is_a_prefix_of b₄ } \/ { (b₄ ^ b₅) where B is Element of b₁, B is Element of b₂ : b₄ in b₃ }

proof end;

theorem Th8: :: TREES_A:8

canceled;

theorem Th9: :: TREES_A:9

for b₁, b₂ being Tree
for b₃ being AntiChain_of_Prefixes of b₂
for b₄ being FinSequence of NAT st b₄ in b₃ holds
b₁ = (tree b₂,b₃,b₁) | b₄

proof end;

registration

let c₁ be Tree;
cluster non empty AntiChain_of_Prefixes of a₁;
existence

proof end;

end;

definition

let c₁ be Tree;
let c₂ be Element of c₁;
redefine func { as {c₂} -> non empty AntiChain_of_Prefixes of a₁;
correctness by TREES_1:74;

end;

theorem Th10: :: TREES_A:10

for b₁, b₂ being Tree
for b₃ being Element of b₁ holds tree b₁,{b₃},b₂ = b₁ with-replacement b₃,b₂

proof end;

definition

let c₁ be DecoratedTree;
let c₂ be AntiChain_of_Prefixes of dom c₁;
let c₃ be DecoratedTree;
assume E10: c₂ <> {} ;
func tree c₁,c₂,c₃ -> DecoratedTree means :Def2: :: TREES_A:def 2
( dom a₄ = tree (dom a₁),a₂,(dom a₃) & ( for b₁ being FinSequence of NAT holds
( not b₁ in tree (dom a₁),a₂,(dom a₃) or for b₂ being FinSequence of NAT st b₂ in a₂ holds
( not b₂ is_a_prefix_of b₁ & a₄ . b₁ = a₁ . b₁ ) or ex b₂, b₃ being FinSequence of NAT st
( b₂ in a₂ & b₃ in dom a₃ & b₁ = b₂ ^ b₃ & a₄ . b₁ = a₃ . b₃ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines tree TREES_A:def 2 :

theorem Th11: :: TREES_A:11

canceled;

theorem Th12: :: TREES_A:12

canceled;

theorem Th13: :: TREES_A:13

for b₁, b₂ being DecoratedTree
for b₃ being AntiChain_of_Prefixes of dom b₁ st b₃ <> {} holds
for b₄ being FinSequence of NAT holds
( not b₄ in dom (tree b₁,b₃,b₂) or for b₅ being FinSequence of NAT st b₅ in b₃ holds
( not b₅ is_a_prefix_of b₄ & (tree b₁,b₃,b₂) . b₄ = b₁ . b₄ ) or ex b₅, b₆ being FinSequence of NAT st
( b₅ in b₃ & b₆ in dom b₂ & b₄ = b₅ ^ b₆ & (tree b₁,b₃,b₂) . b₄ = b₂ . b₆ ) )

proof end;

theorem Th14: :: TREES_A:14

for b₁ being FinSequence of NAT
for b₂, b₃ being DecoratedTree st b₁ in dom b₂ holds
for b₄ being FinSequence of NAT holds
( not b₄ in dom (b₂ with-replacement b₁,b₃) or ( not b₁ is_a_prefix_of b₄ & (b₂ with-replacement b₁,b₃) . b₄ = b₂ . b₄ ) or ex b₅ being FinSequence of NAT st
( b₅ in dom b₃ & b₄ = b₁ ^ b₅ & (b₂ with-replacement b₁,b₃) . b₄ = b₃ . b₅ ) )

proof end;

theorem Th15: :: TREES_A:15

for b₁, b₂ being DecoratedTree
for b₃ being AntiChain_of_Prefixes of dom b₁ st b₃ <> {} holds
for b₄ being FinSequence of NAT st b₄ in dom (tree b₁,b₃,b₂) & b₄ in { b₅ where B is Element of dom b₁ : for b₁ being FinSequence of NAT st b₆ in b₃ holds
not b₆ is_a_prefix_of b₅ } holds
(tree b₁,b₃,b₂) . b₄ = b₁ . b₄

proof end;

theorem Th16: :: TREES_A:16

for b₁ being FinSequence of NAT
for b₂, b₃ being DecoratedTree st b₁ in dom b₂ holds
for b₄ being FinSequence of NAT st b₄ in dom (b₂ with-replacement b₁,b₃) & b₄ in { b₅ where B is Element of dom b₂ : not b₁ is_a_prefix_of b₅ } holds
(b₂ with-replacement b₁,b₃) . b₄ = b₂ . b₄

proof end;

theorem Th17: :: TREES_A:17

for b₁, b₂ being DecoratedTree
for b₃ being AntiChain_of_Prefixes of dom b₁
for b₄ being FinSequence of NAT st b₄ in dom (tree b₁,b₃,b₂) & b₄ in { (b₅ ^ b₆) where B is Element of dom b₁, B is Element of dom b₂ : b₅ in b₃ } holds
ex b₅ being Element of dom b₁ex b₆ being Element of dom b₂ st
( b₄ = b₅ ^ b₆ & b₅ in b₃ & (tree b₁,b₃,b₂) . b₄ = b₂ . b₆ )

proof end;

theorem Th18: :: TREES_A:18

for b₁ being FinSequence of NAT
for b₂, b₃ being DecoratedTree st b₁ in dom b₂ holds
for b₄ being FinSequence of NAT st b₄ in dom (b₂ with-replacement b₁,b₃) & b₄ in { (b₁ ^ b₅) where B is Element of dom b₃ : b₅ = b₅ } holds
ex b₅ being Element of dom b₃ st
( b₄ = b₁ ^ b₅ & (b₂ with-replacement b₁,b₃) . b₄ = b₃ . b₅ )

proof end;

theorem Th19: :: TREES_A:19

for b₁, b₂ being DecoratedTree
for b₃ being Element of dom b₁ holds tree b₁,{b₃},b₂ = b₁ with-replacement b₃,b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be DecoratedTree of c₁;
let c₃ be AntiChain_of_Prefixes of dom c₂;
let c₄ be DecoratedTree of c₁;
assume E17: c₃ <> {} ;
func tree c₂,c₃,c₄ -> DecoratedTree of a₁ equals :: TREES_A:def 3
tree a₂,a₃,a₄;
coherence

proof end;

end;

:: deftheorem Def3 defines tree TREES_A:def 3 :