let T, T1 be DecoratedTree; for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)
let t be Element of dom T; tree (T,{t},T1) = T with-replacement (t,T1)
A1: dom (tree (T,{t},T1)) =
tree ((dom T),{t},(dom T1))
by Def2
.=
(dom T) with-replacement (t,(dom T1))
by Th9
.=
dom (T with-replacement (t,T1))
by TREES_2:def 11
;
for q being FinSequence of NAT st q in dom (tree (T,{t},T1)) holds
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
proof
let q be
FinSequence of
NAT ;
( q in dom (tree (T,{t},T1)) implies (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q )
assume A2:
q in dom (tree (T,{t},T1))
;
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
then A3:
q in tree (
(dom T),
{t},
(dom T1))
by Def2;
A4:
tree (
(dom T),
{t},
(dom T1))
= { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in {t} }
by Th7;
per cases
( q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 } or q in { (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t} } )
by A3, A4, XBOOLE_0:def 3;
suppose A5:
q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 }
;
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . qthen consider t9 being
Element of
dom T such that A6:
q = t9
and A7:
for
p being
FinSequence of
NAT st
p in {t} holds
not
p is_a_prefix_of t9
;
consider p being
FinSequence of
NAT such that A8:
p = t
;
p in {t}
by A8, TARSKI:def 1;
then A9:
not
p is_a_prefix_of t9
by A7;
(
q in dom (T with-replacement (t,T1)) &
q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } implies
(T with-replacement (t,T1)) . q = T . q )
by A8, Th13;
hence
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
by A1, A2, A5, A6, A9, Th12;
verum end; suppose A10:
q in { (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t} }
;
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . qthen consider p being
Element of
dom T,
r being
Element of
dom T1 such that A11:
q = p ^ r
and A12:
p in {t}
;
A13:
q in { (p ^ s) where s is Element of dom T1 : verum }
by A11;
consider p1 being
Element of
dom T,
r1 being
Element of
dom T1 such that A14:
q = p1 ^ r1
and A15:
p1 in {t}
and A16:
(tree (T,{t},T1)) . q = T1 . r1
by A2, A10, Th14;
A17:
p1 = t
by A15, TARSKI:def 1;
A18:
p = t
by A12, TARSKI:def 1;
then
ex
r2 being
Element of
dom T1 st
(
q = p ^ r2 &
(T with-replacement (p,T1)) . q = T1 . r2 )
by A1, A2, A13, Th15;
hence
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
by A14, A16, A17, A18, FINSEQ_1:33;
verum end;
end;
hence
tree (T,{t},T1) = T with-replacement (t,T1)
by A1, TREES_2:31; verum