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 ; :: according to TARSKI:def 3 :: thesis: ( 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() } ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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() } ; :: thesis: ( ( 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 :: thesis: ( ( 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 ) )
let t be Symbol of F2(); :: thesis: ( t in Terminals F2() implies root-tree t in X1 )
assume A10: t in Terminals F2() ; :: thesis: root-tree t in X1
A11: (root-tree [t,F4(t)]) `1 = root-tree t by TREES_4:25;
root-tree [t,F4(t)] in Union F1() by A6, A10;
hence root-tree t in X1 by A11; :: thesis: verum
end;
hereby :: thesis: 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(); :: thesis: for ts being FinSequence of X1 st nt ==> roots ts holds
nt -tree ts in X1
let ts be FinSequence of X1; :: thesis: ( nt ==> roots ts implies nt -tree ts in X1 )
assume A12: nt ==> roots ts ; :: thesis: nt -tree ts in X1
A13: 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]
proof
let k be Nat; :: thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] )
assume k in Seg (len ts) ; :: thesis: ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x]
then A15: ts . k in rng ts by A13, FUNCT_1:def 3;
rng ts c= X1 by FINSEQ_1:def 4;
then ts . k in X1 by A15;
then ex x being Element of FinTrees [: the carrier of F2(),F3():] st
( ts . k = x `1 & x in Union F1() ) ;
hence ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] ; :: thesis: verum
end;
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()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng dts or x in Union F1() )
assume x in rng dts ; :: thesis: x in Union F1()
then consider k being object such that
A18: k in dom ts and
A19: x = dts . k by A13, A16, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A18;
ex dt being DecoratedTree of [: the carrier of F2(),F3():] st
( dt = x & dt `1 = ts . k & dt in Union F1() ) by A13, A17, A18, A19;
hence x in Union F1() ; :: thesis: verum
end;
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 :: thesis: for k being Nat st k in dom ts holds
(roots ts) . k = (pr1 (roots dts)) . k
let k be Nat; :: thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A23: k in dom ts ; :: thesis: (roots ts) . k = (pr1 (roots dts)) . k
then 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; :: thesis: 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;
now :: thesis: for i being Nat st i in dom dts holds
for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds
ts . i = T `1
let i be Nat; :: thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; :: thesis: for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds
ts . i = T `1
then A30: ex dt being DecoratedTree of [: the carrier of F2(),F3():] st
( dt = dts . i & dt `1 = ts . i & dt in Union F1() ) by A16, A17;
let T be DecoratedTree of [: the carrier of F2(),F3():]; :: thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; :: thesis: ts . i = T `1
hence ts . i = T `1 by A30; :: thesis: verum
end;
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; :: thesis: verum
end;
let F be Subset of (FinTrees the carrier of F2()); :: thesis: ( ( 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 ; :: thesis: X1 c= F
thus X1 c= F :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in F )
assume x in X1 ; :: thesis: 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():]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } or x in FinTrees [: the carrier of F2(),F3():] )
assume x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ; :: thesis: x in FinTrees [: the carrier of F2(),F3():]
then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( x = dt & dt `1 in F ) ;
hence x in FinTrees [: the carrier of F2(),F3():] ; :: thesis: verum
end;
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():]) ;
A35: now :: thesis: for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in FF
let d be Symbol of F2(); :: thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in FF )
assume d in Terminals F2() ; :: thesis: root-tree [d,F4(d)] in FF
then A36: root-tree d in F by A31;
(root-tree [d,F4(d)]) `1 = root-tree d by TREES_4:25;
hence root-tree [d,F4(d)] in FF by A36; :: thesis: verum
end;
now :: thesis: 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 FF
let o be Symbol of F2(); :: thesis: for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in FF
let p be FinSequence of FF; :: thesis: ( o ==> pr1 (roots p) implies [o,H3(o,p)] -tree p in FF )
assume A37: o ==> pr1 (roots p) ; :: thesis: [o,H3(o,p)] -tree p in FF
consider 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p1 or x in F )
assume x in rng p1 ; :: thesis: x in F
then consider k being object such that
A41: k in dom p1 and
A42: x = p1 . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A41;
A43: p . k in rng p by A38, A41, FUNCT_1:def 3;
A44: ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( dt = p . k & x = dt `1 ) by A38, A39, A41, A42;
rng p c= FF by FINSEQ_1:def 4;
then p . k in FF by A43;
then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( p . k = dt & dt `1 in F ) ;
hence x in F by A44; :: thesis: verum
end;
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 :: thesis: for k being Nat st k in dom p1 holds
(roots p1) . k = (pr1 (roots p)) . k
let k be Nat; :: thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )
assume A48: k in dom p1 ; :: thesis: (roots p1) . k = (pr1 (roots p)) . k
then 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;