let a be object ; for i being Nat
for xi, w being FinSequence of NAT
for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let i be Nat; for xi, w being FinSequence of NAT
for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let xi, w be FinSequence of NAT ; for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let p, q be DTree-yielding FinSequence; for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let d, t be DecoratedTree; ( i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) implies (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z0:
i < len p
; ( not xi = <*i*> ^ w or not d = p . (i + 1) or not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z1:
xi = <*i*> ^ w
; ( not d = p . (i + 1) or not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z2:
d = p . (i + 1)
; ( not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z3:
q = p +* ((i + 1),(d with-replacement (w,t)))
; ( not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z4:
xi in tree (doms p)
; (a -tree p) with-replacement (xi,t) = a -tree q
A1:
( dom (a -tree p) = tree (doms p) & dom (a -tree q) = tree (doms q) )
by TREES_4:10;
AA:
doms q = (doms p) +* ((i + 1),(dom (d with-replacement (w,t))))
by Z3, Lem12;
consider j being Nat, u being FinSequence such that
A2:
( j < len (doms p) & u in (doms p) . (j + 1) & xi = <*j*> ^ u )
by Z1, Z4, TREES_3:def 15;
A3:
( i = xi . 1 & xi . 1 = j & w = u )
by Z1, A2, FINSEQ_1:41, HILBERT2:2;
( 1 <= i + 1 & i + 1 <= len p )
by Z0, NAT_1:12, NAT_1:13;
then
i + 1 in dom p
by FINSEQ_3:25;
then A4:
( w in dom d & dom d = (doms p) . (i + 1) )
by Z2, A2, A3, FUNCT_6:def 2;
then
dom (d with-replacement (w,t)) = (dom d) with-replacement (w,(dom t))
by TREES_2:def 11;
then A5:
( dom ((a -tree p) with-replacement (xi,t)) = (tree (doms p)) with-replacement (xi,(dom t)) & (tree (doms p)) with-replacement (xi,(dom t)) = tree (doms q) )
by Z4, A1, AA, A2, A3, A4, Th124, TREES_2:def 11;
hence
dom ((a -tree p) with-replacement (xi,t)) = dom (a -tree q)
by TREES_4:10; TREES_4:def 1 for b1 being Element of proj1 ((a -tree p) with-replacement (xi,t)) holds ((a -tree p) with-replacement (xi,t)) . b1 = (a -tree q) . b1
A8:
( dom (doms q) = dom q & dom q = dom p & dom p = dom (doms p) )
by Z3, FUNCT_6:def 2, FUNCT_7:30;
then A7:
( len (doms q) = len q & len q = len p & len p = len (doms p) )
by FINSEQ_3:29;
let nu be Element of dom ((a -tree p) with-replacement (xi,t)); ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu
per cases
( nu = {} or ex j being Nat ex r being FinSequence st
( j < len (doms q) & r in (doms q) . (j + 1) & nu = <*j*> ^ r ) )
by A5, TREES_3:def 15;
suppose
ex
j being
Nat ex
r being
FinSequence st
(
j < len (doms q) &
r in (doms q) . (j + 1) &
nu = <*j*> ^ r )
;
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nuthen consider j being
Nat,
r being
FinSequence such that A6:
(
j < len (doms q) &
r in (doms q) . (j + 1) &
nu = <*j*> ^ r )
;
AB:
( 1
<= j + 1 &
j + 1
<= len p )
by A6, A7, NAT_1:12, NAT_1:13;
then A9:
j + 1
in dom p
by FINSEQ_3:25;
per cases
( j <> i or j = i )
;
suppose A10:
j <> i
;
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nuthen
j + 1
<> i + 1
;
then A11:
(
dom (q . (j + 1)) = (doms q) . (j + 1) &
(doms q) . (j + 1) = (doms p) . (j + 1) &
(doms p) . (j + 1) = dom (p . (j + 1)) &
q . (j + 1) = p . (j + 1) )
by Z3, AA, A8, AB, FINSEQ_3:25, FUNCT_7:32, FUNCT_6:def 2;
reconsider t1 =
p . (j + 1) as
DecoratedTree by A9, TREES_3:24;
not
xi c= nu
by A6, Z1, Lem8, A10, TREES_1:50;
then
for
r being
FinSequence of
NAT holds
( not
r in dom t or not
nu = xi ^ r or not
((a -tree p) with-replacement (xi,t)) . nu = t . r )
by TREES_1:1;
hence ((a -tree p) with-replacement (xi,t)) . nu =
(a -tree p) . nu
by Z4, A1, A5, TREES_2:def 11
.=
t1 . r
by A6, A7, A11, TREES_4:12
.=
(a -tree q) . nu
by A6, A7, A11, TREES_4:12
;
verum end; suppose A10:
j = i
;
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nuthen A11:
(
dom (q . (j + 1)) = (doms q) . (j + 1) &
(doms p) . (j + 1) = dom (p . (j + 1)) &
q . (j + 1) = d with-replacement (
w,
t) )
by Z3, A8, AB, FINSEQ_3:25, FUNCT_7:31, FUNCT_6:def 2;
then reconsider r =
r as
Element of
(dom d) with-replacement (
w,
(dom t))
by A6, Z2, A2, A3, A10, TREES_2:def 11;
per cases
( w c= r or not w c= r )
;
suppose A12:
w c= r
;
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nuthen consider r2 being
FinSequence of
NAT such that A13:
(
r2 in dom t &
r = w ^ r2 &
(d with-replacement (w,t)) . r = t . r2 )
by Z2, A2, A3, A10, A11, TREES_2:def 11;
xi c= nu
by Z1, A6, A10, A12, FINSEQ_6:13;
then consider r3 being
FinSequence of
NAT such that A15:
(
r3 in dom t &
nu = xi ^ r3 &
((a -tree p) with-replacement (xi,t)) . nu = t . r3 )
by Z4, A5, A1, TREES_2:def 11;
nu = xi ^ r2
by Z1, A6, A10, A13, FINSEQ_1:32;
then
((a -tree p) with-replacement (xi,t)) . nu = t . r2
by A15, FINSEQ_1:33;
hence
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu
by A13, A6, A7, A11, TREES_4:12;
verum end; suppose A12:
not
w c= r
;
((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nuthen A13:
for
r2 being
FinSequence of
NAT holds
( not
r2 in dom t or not
r = w ^ r2 or not
(d with-replacement (w,t)) . r = t . r2 )
by TREES_1:1;
for
r2 being
FinSequence of
NAT holds
( not
r2 in dom t or not
r = w ^ r2 )
by A12, TREES_1:1;
then A15:
r in dom d
by Z2, A2, A3, A10, A11, TREES_1:def 9;
for
r being
FinSequence of
NAT holds
( not
r in dom t or not
nu = xi ^ r or not
((a -tree p) with-replacement (xi,t)) . nu = t . r )
by A12, A10, A6, Z1, Lem8A, TREES_1:1;
hence ((a -tree p) with-replacement (xi,t)) . nu =
(a -tree p) . nu
by Z4, A1, A5, TREES_2:def 11
.=
d . r
by Z2, A15, A6, A7, A10, TREES_4:12
.=
(d with-replacement (w,t)) . r
by A13, A4, TREES_2:def 11
.=
(a -tree q) . nu
by A6, A7, A11, TREES_4:12
;
verum end; end; end;