set f = F1();
set G = F2();
set D = F3();
set S = the carrier of F2();
set SxD = [: the carrier of F2(),F3():];
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
A4:
F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) }
by A2;
A5:
for n being Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
by A3;
defpred S1[ Nat] means for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in F1() . $1 & dt2 in F1() . $1 & dt1 `1 = dt2 `1 holds
dt1 = dt2;
A6:
S1[ 0 ]
proof
let dt1,
dt2 be
DecoratedTree of
[: the carrier of F2(),F3():];
( dt1 in F1() . 0 & dt2 in F1() . 0 & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that A7:
dt1 in F1()
. 0
and A8:
dt2 in F1()
. 0
and A9:
dt1 `1 = dt2 `1
;
dt1 = dt2
consider t1 being
Symbol of
F2(),
d1 being
Element of
F3()
such that A10:
dt1 = root-tree [t1,d1]
and A11:
( (
t1 in Terminals F2() &
d1 = F4(
t1) ) or (
t1 ==> {} &
d1 = F5(
t1,
{},
{}) ) )
by A2, A7;
consider t2 being
Symbol of
F2(),
d2 being
Element of
F3()
such that A12:
dt2 = root-tree [t2,d2]
and A13:
( (
t2 in Terminals F2() &
d2 = F4(
t2) ) or (
t2 ==> {} &
d2 = F5(
t2,
{},
{}) ) )
by A2, A8;
A14:
root-tree t1 = dt1 `1
by A10, TREES_4:25;
root-tree t2 = dt2 `1
by A12, TREES_4:25;
then A15:
t1 = t2
by A9, A14, TREES_4:4;
hence
dt1 = dt2
by A10, A11, A12, A13, A15;
verum
end;
A16:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A17:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let dt1,
dt2 be
DecoratedTree of
[: the carrier of F2(),F3():];
( dt1 in F1() . (n + 1) & dt2 in F1() . (n + 1) & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that A18:
dt1 in F1()
. (n + 1)
and A19:
dt2 in F1()
. (n + 1)
and A20:
dt1 `1 = dt2 `1
;
dt1 = dt2
A21:
dom dt1 = dom (dt1 `1)
by TREES_4:24;
A22:
dom dt2 = dom (dt1 `1)
by A20, TREES_4:24;
A23:
dt1 in Union F1()
by A1, A18, CARD_5:2;
A24:
dt2 in Union F1()
by A1, A19, CARD_5:2;
ex
X being
Subset of
(FinTrees [: the carrier of F2(),F3():]) st
(
X = Union F1() & ( for
d being
Symbol of
F2() st
d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for
o being
Symbol of
F2()
for
p being
FinSequence of
X st
o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for
F being
Subset of
(FinTrees [: the carrier of F2(),F3():]) st ( for
d being
Symbol of
F2() st
d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for
o being
Symbol of
F2()
for
p being
FinSequence of
F st
o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
from DTCONSTR:sch 3(A1, A4, A5);
then reconsider dt19 =
dt1,
dt29 =
dt2 as
Element of
FinTrees [: the carrier of F2(),F3():] by A23, A24;
A25:
for
n being
Nat for
dt being
Element of
FinTrees [: the carrier of F2(),F3():] st
dt in Union F1() holds
(
dt in F1()
. n iff
height (dom dt) <= n )
from DTCONSTR:sch 5(A1, A4, A5);
per cases
( dt1 in F1() . n or not dt1 in F1() . n )
;
suppose A27:
not
dt1 in F1()
. n
;
dt1 = dt2A28:
F1()
. (n + 1) = (F1() . n) \/ { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) }
by A3;
then
(
dt1 in F1()
. n or
dt1 in { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) } )
by A18, XBOOLE_0:def 3;
then consider o1 being
Symbol of
F2(),
p1 being
Element of
(F1() . n) * such that A29:
dt1 = [o1,H3(o1,p1)] -tree p1
and A30:
ex
q being
FinSequence of
FinTrees [: the carrier of F2(),F3():] st
(
p1 = q &
o1 ==> pr1 (roots q) )
by A27;
height (dom dt19) > n
by A23, A25, A27;
then A31:
not
dt29 in F1()
. n
by A21, A22, A24, A25;
(
dt2 in F1()
. n or
dt2 in { ([o2,H3(o2,p2)] -tree p2) where o2 is Symbol of F2(), p2 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p2 = q & o2 ==> pr1 (roots q) ) } )
by A19, A28, XBOOLE_0:def 3;
then consider o2 being
Symbol of
F2(),
p2 being
Element of
(F1() . n) * such that A32:
dt2 = [o2,H3(o2,p2)] -tree p2
and A33:
ex
q being
FinSequence of
FinTrees [: the carrier of F2(),F3():] st
(
p2 = q &
o2 ==> pr1 (roots q) )
by A31;
reconsider p1 =
p1 as
FinSequence of
FinTrees [: the carrier of F2(),F3():] by A30;
consider p11 being
FinSequence of
FinTrees the
carrier of
F2()
such that A34:
dom p11 = dom p1
and A35:
for
i being
Nat st
i in dom p1 holds
ex
T being
Element of
FinTrees [: the carrier of F2(),F3():] st
(
T = p1 . i &
p11 . i = T `1 )
and A36:
([o1,H3(o1,p1)] -tree p1) `1 = o1 -tree p11
by TREES_4:31;
reconsider p2 =
p2 as
FinSequence of
FinTrees [: the carrier of F2(),F3():] by A33;
consider p21 being
FinSequence of
FinTrees the
carrier of
F2()
such that A37:
dom p21 = dom p2
and A38:
for
i being
Nat st
i in dom p2 holds
ex
T being
Element of
FinTrees [: the carrier of F2(),F3():] st
(
T = p2 . i &
p21 . i = T `1 )
and A39:
([o2,H3(o2,p2)] -tree p2) `1 = o2 -tree p21
by TREES_4:31;
A40:
o1 = o2
by A20, A29, A32, A36, A39, TREES_4:15;
A41:
p11 = p21
by A20, A29, A32, A36, A39, TREES_4:15;
now for k being Nat st k in dom p11 holds
p1 . k = p2 . klet k be
Nat;
( k in dom p11 implies p1 . k = p2 . k )assume A42:
k in dom p11
;
p1 . k = p2 . kthen consider p1k being
Element of
FinTrees [: the carrier of F2(),F3():] such that A43:
p1k = p1 . k
and A44:
p11 . k = p1k `1
by A34, A35;
consider p2k being
Element of
FinTrees [: the carrier of F2(),F3():] such that A45:
p2k = p2 . k
and A46:
p21 . k = p2k `1
by A37, A38, A41, A42;
A47:
p1k in F1()
. n
by A34, A42, A43, Th2;
p2k in F1()
. n
by A37, A41, A42, A45, Th2;
hence
p1 . k = p2 . k
by A17, A41, A43, A44, A45, A46, A47;
verum end; then
p1 = p2
by A34, A37, A41, FINSEQ_1:13;
hence
dt1 = dt2
by A29, A32, A40;
verum end;
end; end;
A48:
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A16);
let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ( dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that
A49:
dt1 in Union F1()
and
A50:
dt2 in Union F1()
and
A51:
dt1 `1 = dt2 `1
; dt1 = dt2
consider n1 being object such that
A52:
n1 in NAT
and
A53:
dt1 in F1() . n1
by A1, A49, CARD_5:2;
consider n2 being object such that
A54:
n2 in NAT
and
A55:
dt2 in F1() . n2
by A1, A50, CARD_5:2;
reconsider n1 = n1, n2 = n2 as Element of NAT by A52, A54;
deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ;
A56:
for n being Nat holds F1() . n c= F1() . (n + 1)
A57:
for k, s being Nat holds F1() . k c= F1() . (k + s)
by NAT_1:11, A56, MEASURE2:18;
( n1 <= n2 or n1 >= n2 )
;
then
( ex s being Nat st n2 = n1 + s or ex s being Nat st n1 = n2 + s )
by NAT_1:10;
then
( F1() . n1 c= F1() . n2 or F1() . n2 c= F1() . n1 )
by A57;
hence
dt1 = dt2
by A48, A51, A53, A55; verum