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;
consider X being Subset of (FinTrees [: the carrier of F2(),F3():]) such that
A6:
( 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);
set X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ;
{ (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } c= FinTrees the carrier of F2()
proof
let x be
object ;
TARSKI:def 3 ( not x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } or x in FinTrees the carrier of F2() )
assume
x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() }
;
x in FinTrees the carrier of F2()
then consider tt being
Element of
FinTrees [: the carrier of F2(),F3():] such that A7:
x = tt `1
and
tt in Union F1()
;
A8:
tt `1 = (pr1 ( the carrier of F2(),F3())) * tt
by TREES_3:def 12;
A9:
rng tt c= [: the carrier of F2(),F3():]
by RELAT_1:def 19;
dom (pr1 ( the carrier of F2(),F3())) = [: the carrier of F2(),F3():]
by FUNCT_2:def 1;
then
dom (tt `1) = dom tt
by A8, A9, RELAT_1:27;
hence
x in FinTrees the
carrier of
F2()
by A7, TREES_3:def 8;
verum
end;
then reconsider X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } as Subset of (FinTrees the carrier of F2()) ;
take X1 = X9; ( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) & ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
thus
X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() }
; ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) & ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
hereby for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F
let nt be
Symbol of
F2();
for ts being FinSequence of X1 st nt ==> roots ts holds
nt -tree ts in X1let ts be
FinSequence of
X1;
( nt ==> roots ts implies nt -tree ts in X1 )assume A12:
nt ==> roots ts
;
nt -tree ts in X1A13:
dom ts = Seg (len ts)
by FINSEQ_1:def 3;
defpred S1[
set ,
set ]
means ex
dt being
DecoratedTree of
[: the carrier of F2(),F3():] st
(
dt = $2 &
dt `1 = ts . $1 &
dt in Union F1() );
A14:
for
k being
Nat st
k in Seg (len ts) holds
ex
x being
Element of
FinTrees [: the carrier of F2(),F3():] st
S1[
k,
x]
consider dts being
FinSequence of
FinTrees [: the carrier of F2(),F3():] such that A16:
dom dts = Seg (len ts)
and A17:
for
k being
Nat st
k in Seg (len ts) holds
S1[
k,
dts . k]
from FINSEQ_1:sch 5(A14);
rng dts c= Union F1()
then reconsider dts =
dts as
FinSequence of
X by A6, FINSEQ_1:def 4;
A20:
dom (roots ts) = dom ts
by TREES_3:def 18;
A21:
dom (pr1 (roots dts)) = dom (roots dts)
by MCART_1:def 12;
then A22:
dom (pr1 (roots dts)) = dom ts
by A13, A16, TREES_3:def 18;
now for k being Nat st k in dom ts holds
(roots ts) . k = (pr1 (roots dts)) . klet k be
Nat;
( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )assume A23:
k in dom ts
;
(roots ts) . k = (pr1 (roots dts)) . kthen consider dt being
DecoratedTree of
[: the carrier of F2(),F3():] such that A24:
dt = dts . k
and A25:
dt `1 = ts . k
and
dt in Union F1()
by A13, A17;
reconsider r =
{} as
Node of
dt by TREES_1:22;
ex
T being
DecoratedTree st
(
T = ts . k &
(roots ts) . k = T . {} )
by A23, TREES_3:def 18;
then A26:
(roots ts) . k = (dt . r) `1
by A25, TREES_3:39;
ex
T being
DecoratedTree st
(
T = dts . k &
(roots dts) . k = T . {} )
by A13, A16, A23, TREES_3:def 18;
hence
(roots ts) . k = (pr1 (roots dts)) . k
by A21, A22, A23, A24, A26, MCART_1:def 12;
verum end; then
roots ts = pr1 (roots dts)
by A20, A22, FINSEQ_1:13;
then A27:
[nt,H3(nt,dts)] -tree dts in X
by A6, A12;
A28:
rng dts c= FinTrees [: the carrier of F2(),F3():]
by FINSEQ_1:def 4;
FinTrees [: the carrier of F2(),F3():] c= Trees [: the carrier of F2(),F3():]
by TREES_3:21;
then
rng dts c= Trees [: the carrier of F2(),F3():]
by A28;
then reconsider dts9 =
dts as
FinSequence of
Trees [: the carrier of F2(),F3():] by FINSEQ_1:def 4;
A29:
rng ts c= FinTrees the
carrier of
F2()
by FINSEQ_1:def 4;
FinTrees the
carrier of
F2()
c= Trees the
carrier of
F2()
by TREES_3:21;
then
rng ts c= Trees the
carrier of
F2()
by A29;
then reconsider ts9 =
ts as
FinSequence of
Trees the
carrier of
F2()
by FINSEQ_1:def 4;
then
([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9
by A13, A16, TREES_4:27;
hence
nt -tree ts in X1
by A6, A27;
verum
end;
let F be Subset of (FinTrees the carrier of F2()); ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) implies X1 c= F )
assume that
A31:
for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F
and
A32:
for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F
; X1 c= F
thus
X1 c= F
verumproof
let x be
object ;
TARSKI:def 3 ( not x in X1 or x in F )
assume
x in X1
;
x in F
then consider tt being
Element of
FinTrees [: the carrier of F2(),F3():] such that A33:
x = tt `1
and A34:
tt in Union F1()
;
set FF =
{ dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ;
{ dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } c= FinTrees [: the carrier of F2(),F3():]
then reconsider FF =
{ dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } as
Subset of
(FinTrees [: the carrier of F2(),F3():]) ;
now for o being Symbol of F2()
for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in FFlet o be
Symbol of
F2();
for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in FFlet p be
FinSequence of
FF;
( o ==> pr1 (roots p) implies [o,H3(o,p)] -tree p in FF )assume A37:
o ==> pr1 (roots p)
;
[o,H3(o,p)] -tree p in FFconsider p1 being
FinSequence of
FinTrees the
carrier of
F2()
such that A38:
dom p1 = dom p
and A39:
for
i being
Nat st
i in dom p holds
ex
T being
Element of
FinTrees [: the carrier of F2(),F3():] st
(
T = p . i &
p1 . i = T `1 )
and A40:
([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 = o -tree p1
by TREES_4:31;
rng p1 c= F
then reconsider p1 =
p1 as
FinSequence of
F by FINSEQ_1:def 4;
A45:
dom (roots p1) = dom p1
by TREES_3:def 18;
A46:
dom (pr1 (roots p)) = dom (roots p)
by MCART_1:def 12;
then A47:
dom (pr1 (roots p)) = dom p1
by A38, TREES_3:def 18;
now for k being Nat st k in dom p1 holds
(roots p1) . k = (pr1 (roots p)) . klet k be
Nat;
( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )assume A48:
k in dom p1
;
(roots p1) . k = (pr1 (roots p)) . kthen A49:
p . k in rng p
by A38, FUNCT_1:def 3;
A50:
ex
dt being
Element of
FinTrees [: the carrier of F2(),F3():] st
(
dt = p . k &
p1 . k = dt `1 )
by A38, A39, A48;
rng p c= FF
by FINSEQ_1:def 4;
then
p . k in FF
by A49;
then consider dt being
Element of
FinTrees [: the carrier of F2(),F3():] such that A51:
p . k = dt
and
dt `1 in F
;
reconsider r =
{} as
Node of
dt by TREES_1:22;
ex
T being
DecoratedTree st
(
T = p1 . k &
(roots p1) . k = T . {} )
by A48, TREES_3:def 18;
then A52:
(roots p1) . k = (dt . r) `1
by A50, A51, TREES_3:39;
ex
T being
DecoratedTree st
(
T = p . k &
(roots p) . k = T . {} )
by A38, A48, TREES_3:def 18;
hence
(roots p1) . k = (pr1 (roots p)) . k
by A46, A47, A48, A51, A52, MCART_1:def 12;
verum end; then
pr1 (roots p) = roots p1
by A45, A47, FINSEQ_1:13;
then
([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 in F
by A32, A37, A40;
hence
[o,H3(o,p)] -tree p in FF
;
verum end;
then
X c= FF
by A6, A35;
then
tt in FF
by A6, A34;
then
ex
dt being
Element of
FinTrees [: the carrier of F2(),F3():] st
(
tt = dt &
dt `1 in F )
;
hence
x in F
by A33;
verum
end;