:: Replacement of Subtrees in a Tree
:: by Oleg Okhotnikov
::
:: Received October 1, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: TREES_A:1
:: deftheorem Def1 defines tree TREES_A:def 1 :
theorem Th2: :: TREES_A:2
theorem Th3: :: TREES_A:3
theorem Th4: :: TREES_A:4
theorem Th5: :: TREES_A:5
theorem Th6: :: TREES_A:6
theorem Th7: :: TREES_A:7
theorem :: TREES_A:8
canceled;
theorem :: TREES_A:9
theorem Th10: :: TREES_A:10
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
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 :: TREES_A:11
canceled;
theorem :: TREES_A:12
canceled;
theorem Th13: :: TREES_A:13
theorem Th14: :: TREES_A:14
theorem Th15: :: TREES_A:15
theorem Th16: :: TREES_A:16
theorem Th17: :: TREES_A:17
theorem Th18: :: TREES_A:18
theorem :: TREES_A:19
:: deftheorem defines tree TREES_A:def 3 :