begin
theorem Th1:
:: deftheorem Def1 defines tree TREES_A:def 1 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
canceled;
theorem
theorem Th10:
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:
(
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
ex b1 being DecoratedTree st
( dom b1 = 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 & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
uniqueness
for b1, b2 being DecoratedTree st dom b1 = 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 & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = 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 & b2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines tree TREES_A:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
:: deftheorem defines tree TREES_A:def 3 :