let T, T1 be DecoratedTree; :: thesis: for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)

let t be Element of dom T; :: thesis: 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

let t be Element of dom T; :: thesis: 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

hence
tree (T,{t},T1) = T with-replacement (t,T1)
by A1, TREES_2:31; :: thesis: verum
let q be FinSequence of NAT ; :: thesis: ( 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)) ; :: thesis: (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;

end;assume A2: q in dom (tree (T,{t},T1)) ; :: thesis: (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;

end;

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 } ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

not p is_a_prefix_of t1 } ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

then 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; :: thesis: verum

end;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; :: thesis: verum

suppose A10:
q in { (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t} }
; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

then 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; :: thesis: verum

end;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; :: thesis: verum