:: TREES_A semantic presentation

theorem Th1: :: TREES_A:1

for p, q, r, s being FinSequence st p ^ q = s ^ r holds
p,s are_c=-comparable

proof end;

definition

let T, T1 be Tree;
let P be AntiChain_of_Prefixes of T;
assume A1: P <> {} ;
func tree T,P,T1 -> Tree means :Def1: :: TREES_A:def 1
for q being FinSequence of NAT holds
( q in it iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines tree TREES_A:def 1 :

theorem Th2: :: TREES_A:2

for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree T,P,T1 = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

proof end;

theorem Th3: :: TREES_A:3

for T being Tree
for P being AntiChain_of_Prefixes of T holds { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } c= { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 }

proof end;

theorem Th4: :: TREES_A:4

for T being Tree
for P being AntiChain_of_Prefixes of T holds P c= { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 }

proof end;

theorem Th5: :: TREES_A:5

for T being Tree
for P being AntiChain_of_Prefixes of T holds { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \ { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } = P

proof end;

theorem Th6: :: TREES_A:6

for T, T1 being Tree
for P being AntiChain_of_Prefixes of T holds P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

proof end;

theorem Th7: :: TREES_A:7

for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree T,P,T1 = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

proof end;

theorem :: TREES_A:8

canceled;

theorem :: TREES_A:9

for T1, T being Tree
for P being AntiChain_of_Prefixes of T
for p being FinSequence of NAT st p in P holds
T1 = (tree T,P,T1) | p

proof end;

registration

let T be Tree;
cluster non empty AntiChain_of_Prefixes of T;
existence

proof end;

end;

definition

let T be Tree;
let t be Element of T;
:: original: {
redefine func {t} -> non empty AntiChain_of_Prefixes of T;
correctness by TREES_1:74;

end;

theorem Th10: :: TREES_A:10

for T, T1 being Tree
for t being Element of T holds tree T,{t},T1 = T with-replacement t,T1

proof end;

definition

let T be DecoratedTree;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree;
assume A1: P <> {} ;
func tree T,P,T1 -> DecoratedTree means :Def2: :: TREES_A:def 2
( dom it = tree (dom T),P,(dom T1) & ( for q being FinSequence of NAT holds
( not q in tree (dom T),P,(dom T1) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & it . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines tree TREES_A:def 2 :

theorem :: TREES_A:11

canceled;

theorem :: TREES_A:12

canceled;

theorem Th13: :: TREES_A:13

for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT holds
( not q in dom (tree T,P,T1) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree T,P,T1) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree T,P,T1) . q = T1 . r ) )

proof end;

theorem Th14: :: TREES_A:14

for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT holds
( not q in dom (T with-replacement p,T1) or ( not p is_a_prefix_of q & (T with-replacement p,T1) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) )

proof end;

theorem Th15: :: TREES_A:15

for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st q in dom (tree T,P,T1) & q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } holds
(tree T,P,T1) . q = T . q

proof end;

theorem Th16: :: TREES_A:16

for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } holds
(T with-replacement p,T1) . q = T . q

proof end;

theorem Th17: :: TREES_A:17

for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT st q in dom (tree T,P,T1) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds
ex p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' in P & (tree T,P,T1) . q = T1 . r )

proof end;

theorem Th18: :: TREES_A:18

for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { (p ^ s) where s is Element of dom T1 : s = s } holds
ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r )

proof end;

theorem :: TREES_A:19

for T, T1 being DecoratedTree
for t being Element of dom T holds tree T,{t},T1 = T with-replacement t,T1

proof end;

definition

let D be non empty set ;
let T be DecoratedTree of D;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree of D;
assume A1: P <> {} ;
func tree T,P,T1 -> DecoratedTree of D equals :: TREES_A:def 3
tree T,P,T1;
coherence

proof end;

end;

:: deftheorem defines tree TREES_A:def 3 :