let b be object ; for c being set
for d being DecoratedTree
for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let c be set ; for d being DecoratedTree
for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let d be DecoratedTree; for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let p, q be non empty DTree-yielding FinSequence; ( dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) implies ((b -tree p),c) <- d = b -tree q )
assume that
A1:
dom q = dom p
and
A2:
for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d
; ((b -tree p),c) <- d = b -tree q
A3:
( dom (b -tree p) = tree (doms p) & dom (b -tree q) = tree (doms q) )
by TREES_4:10;
A4:
Leaves (tree (doms p)) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom (doms p) & d = (doms p) . (i + 1) ) }
by ThL0;
A5:
( dom (doms p) = dom p & dom (doms q) = dom q )
by FUNCT_6:def 2;
then A6:
( len (doms p) = len p & len p = len q & len q = len (doms q) )
by A1, FINSEQ_3:29;
AA:
dom (((b -tree p),c) <- d) = dom (b -tree q)
proof
let x be
FinSequence of
NAT ;
TREES_2:def 1 ( ( not x in dom (((b -tree p),c) <- d) or x in dom (b -tree q) ) & ( not x in dom (b -tree q) or x in dom (((b -tree p),c) <- d) ) )
hereby ( not x in dom (b -tree q) or x in dom (((b -tree p),c) <- d) )
assume
x in dom (((b -tree p),c) <- d)
;
x in dom (b -tree q)then reconsider r =
x as
Node of
(((b -tree p),c) <- d) ;
per cases
( r in dom (b -tree p) or ex q being Node of (b -tree p) ex s being Node of d st
( q in Leaves (dom (b -tree p)) & (b -tree p) . q = c & r = q ^ s ) )
by TREES_4:def 7;
suppose
r in dom (b -tree p)
;
x in dom (b -tree q)per cases then
( r = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) )
by A3, TREES_3:def 15;
suppose
ex
n being
Nat ex
q being
FinSequence st
(
n < len (doms p) &
q in (doms p) . (n + 1) &
x = <*n*> ^ q )
;
x in dom (b -tree q)then consider n being
Nat,
w being
FinSequence such that A7:
(
n < len (doms p) &
w in (doms p) . (n + 1) &
x = <*n*> ^ w )
;
A9:
( 1
<= n + 1 &
n + 1
<= len (doms p) )
by A7, NAT_1:11, NAT_1:13;
reconsider pn =
p . (n + 1) as
DecoratedTree by A5, A9, FINSEQ_3:25, TREES_3:24;
reconsider qn =
q . (n + 1) as
DecoratedTree by A1, A9, A5, FINSEQ_3:25, TREES_3:24;
qn = (
pn,
c)
<- d
by A2, A5, A9, FINSEQ_3:25;
then
(
(doms p) . (n + 1) = dom pn &
dom pn c= dom qn &
dom qn = (doms q) . (n + 1) )
by A1, A5, A9, TREES_4:def 7, FINSEQ_3:25, FUNCT_6:def 2;
hence
x in dom (b -tree q)
by A3, A6, A7, TREES_3:def 15;
verum end; end; end; suppose
ex
q being
Node of
(b -tree p) ex
s being
Node of
d st
(
q in Leaves (dom (b -tree p)) &
(b -tree p) . q = c &
r = q ^ s )
;
x in dom (b -tree q)then consider w being
Node of
(b -tree p),
s being
Node of
d such that A8:
(
w in Leaves (dom (b -tree p)) &
(b -tree p) . w = c &
r = w ^ s )
;
consider i being
Nat,
u being
FinSequence of
NAT ,
d2 being
Tree such that A9:
(
w = <*i*> ^ u &
u in Leaves d2 &
i + 1
in dom (doms p) &
d2 = (doms p) . (i + 1) )
by A8, A3, A4;
reconsider p1 =
p . (i + 1) as
DecoratedTree by A5, A9, TREES_3:24;
B1:
w ^ s = <*i*> ^ (u ^ s)
by A9, FINSEQ_1:32;
B2:
q . (i + 1) = (
p1,
c)
<- d
by A2, A5, A9;
B3:
dom p1 = d2
by A5, A9, FUNCT_6:def 2;
reconsider u =
u as
Node of
p1 by A5, A9, FUNCT_6:def 2;
B6:
i + 1
<= len (doms p)
by A9, FINSEQ_3:25;
then B4:
i < len (doms p)
by NAT_1:13;
p1 . u = c
by B6, A6, A8, A9, NAT_1:13, TREES_4:12;
then B5:
(
u ^ s in dom ((p1,c) <- d) &
dom ((p1,c) <- d) = (doms q) . (i + 1) )
by B3, A1, A5, A9, B2, TREES_4:def 7, FUNCT_6:def 2;
thus
x in dom (b -tree q)
by B1, B4, B5, A3, A6, A8, TREES_3:def 15;
verum end; end;
end;
assume
x in dom (b -tree q)
;
x in dom (((b -tree p),c) <- d)
then reconsider r =
x as
Node of
(b -tree q) ;
per cases
( r = {} or ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) )
by A3, TREES_3:def 15;
suppose
ex
i being
Nat ex
w being
FinSequence st
(
i < len (doms q) &
w in (doms q) . (i + 1) &
x = <*i*> ^ w )
;
x in dom (((b -tree p),c) <- d)then consider n being
Nat,
w being
FinSequence such that C1:
(
n < len (doms q) &
w in (doms q) . (n + 1) &
x = <*n*> ^ w )
;
C4:
( 1
<= n + 1 &
n + 1
<= len (doms q) )
by C1, NAT_1:11, NAT_1:13;
then C2:
n + 1
in dom (doms q)
by FINSEQ_3:25;
reconsider qi =
q . (n + 1) as
DecoratedTree by C4, A5, FINSEQ_3:25, TREES_3:24;
reconsider p1 =
p . (n + 1) as
DecoratedTree by A1, A5, C4, FINSEQ_3:25, TREES_3:24;
C3:
(
dom qi = (doms q) . (n + 1) &
dom p1 = (doms p) . (n + 1) )
by A1, A5, C4, FINSEQ_3:25, FUNCT_6:def 2;
qi = (
p1,
c)
<- d
by C4, A1, A2, A5, FINSEQ_3:25;
per cases then
( w in dom p1 or ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) )
by C1, C3, TREES_4:def 7;
suppose
ex
u being
Node of
p1 ex
s being
Node of
d st
(
u in Leaves (dom p1) &
p1 . u = c &
w = u ^ s )
;
x in dom (((b -tree p),c) <- d)then consider u being
Node of
p1,
s being
Node of
d such that C4:
(
u in Leaves (dom p1) &
p1 . u = c &
w = u ^ s )
;
C5:
<*n*> ^ u in Leaves (tree (doms p))
by A4, C4, A5, A1, C2, C3;
(b -tree p) . (<*n*> ^ u) = c
by C1, A6, C4, TREES_4:12;
then
(<*n*> ^ u) ^ s in dom (((b -tree p),c) <- d)
by A3, C5, TREES_4:def 7;
hence
x in dom (((b -tree p),c) <- d)
by C1, C4, FINSEQ_1:32;
verum end; end; end; end;
end;
now for x being object st x in dom (b -tree q) holds
(((b -tree p),c) <- d) . x = (b -tree q) . xlet x be
object ;
( x in dom (b -tree q) implies (((b -tree p),c) <- d) . b1 = (b -tree q) . b1 )assume
x in dom (b -tree q)
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1then reconsider r =
x as
Node of
(b -tree q) ;
per cases
( r = {} or ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) )
by A3, TREES_3:def 15;
suppose
ex
i being
Nat ex
w being
FinSequence st
(
i < len (doms q) &
w in (doms q) . (i + 1) &
x = <*i*> ^ w )
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1then consider n being
Nat,
w being
FinSequence such that C1:
(
n < len (doms q) &
w in (doms q) . (n + 1) &
x = <*n*> ^ w )
;
C5:
( 1
<= n + 1 &
n + 1
<= len (doms q) )
by C1, NAT_1:11, NAT_1:13;
then C2:
n + 1
in dom (doms q)
by FINSEQ_3:25;
reconsider qi =
q . (n + 1) as
DecoratedTree by C5, A5, FINSEQ_3:25, TREES_3:24;
reconsider p1 =
p . (n + 1) as
DecoratedTree by A1, A5, C5, FINSEQ_3:25, TREES_3:24;
C3:
(
dom qi = (doms q) . (n + 1) &
dom p1 = (doms p) . (n + 1) )
by A1, A5, C5, FINSEQ_3:25, FUNCT_6:def 2;
C4:
qi = (
p1,
c)
<- d
by C5, A1, A2, A5, FINSEQ_3:25;
per cases then
( ( w in dom p1 & w nin Leaves (dom p1) ) or ( w in dom p1 & p1 . w <> c ) or ( w in dom p1 & w in Leaves (dom p1) & p1 . w = c ) or ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) )
by C1, C3, TREES_4:def 7;
suppose D1:
(
w in dom p1 &
w nin Leaves (dom p1) )
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1D4:
(
qi . w = p1 . w &
dom p1 c= dom qi )
by D1, C4, TREES_4:def 7;
D5:
x is
Node of
(b -tree p)
by C1, A6, A3, C3, D1, TREES_3:def 15;
then
r nin Leaves (dom (b -tree p))
by A4, A3;
hence (((b -tree p),c) <- d) . x =
(b -tree p) . r
by D5, TREES_4:def 7
.=
p1 . w
by C1, A6, D1, TREES_4:12
.=
(b -tree q) . x
by C1, A6, D1, D4, TREES_4:12
;
verum end; suppose D1:
(
w in dom p1 &
p1 . w <> c )
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1D4:
(
qi . w = p1 . w &
dom p1 c= dom qi )
by D1, C4, TREES_4:def 7;
D5:
x is
Node of
(b -tree p)
by C1, A6, A3, C3, D1, TREES_3:def 15;
(b -tree p) . r <> c
by C1, A6, D1, TREES_4:12;
hence (((b -tree p),c) <- d) . x =
(b -tree p) . r
by D5, TREES_4:def 7
.=
p1 . w
by C1, A6, D1, TREES_4:12
.=
(b -tree q) . x
by C1, A6, D1, D4, TREES_4:12
;
verum end; suppose C7:
(
w in dom p1 &
w in Leaves (dom p1) &
p1 . w = c )
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1then reconsider u =
w as
Node of
p1 ;
reconsider s =
{} as
Node of
d by TREES_1:22;
C71:
w = u ^ s
;
C5:
<*n*> ^ u in Leaves (tree (doms p))
by A4, C7, A5, A1, C2, C3;
C6:
(b -tree p) . (<*n*> ^ u) = c
by C1, A6, C7, TREES_4:12;
(((b -tree p),c) <- d) . ((<*n*> ^ u) ^ s) =
d . s
by A3, C5, C6, TREES_4:def 7
.=
qi . w
by C4, C7, C71, TREES_4:def 7
.=
(b -tree q) . x
by C1, A6, C3, TREES_4:12
;
hence
(((b -tree p),c) <- d) . x = (b -tree q) . x
by C1;
verum end; suppose
ex
u being
Node of
p1 ex
s being
Node of
d st
(
u in Leaves (dom p1) &
p1 . u = c &
w = u ^ s )
;
(((b -tree p),c) <- d) . b1 = (b -tree q) . b1then consider u being
Node of
p1,
s being
Node of
d such that C7:
(
u in Leaves (dom p1) &
p1 . u = c &
w = u ^ s )
;
C5:
<*n*> ^ u in Leaves (tree (doms p))
by A4, C7, A5, A1, C2, C3;
C6:
(b -tree p) . (<*n*> ^ u) = c
by C1, A6, C7, TREES_4:12;
(((b -tree p),c) <- d) . ((<*n*> ^ u) ^ s) =
d . s
by A3, C5, C6, TREES_4:def 7
.=
qi . w
by C4, C7, TREES_4:def 7
.=
(b -tree q) . x
by C1, A6, C3, TREES_4:12
;
hence
(((b -tree p),c) <- d) . x = (b -tree q) . x
by C1, C7, FINSEQ_1:32;
verum end; end; end; end; end;
hence
((b -tree p),c) <- d = b -tree q
by AA, FUNCT_1:2; verum