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():]; :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: for t being Symbol of F2() st t ==> {} holds
not t in Terminals F2()
let t be Symbol of F2(); :: thesis: ( t ==> {} implies not t in Terminals F2() )
assume t ==> {} ; :: thesis: not t in Terminals F2()
then for t9 being Symbol of F2() holds
( not t = t9 or ex tnt being FinSequence st t9 ==> tnt ) ;
then not t in { t9 where t9 is Symbol of F2() : for tnt being FinSequence holds not t9 ==> tnt } ;
hence not t in Terminals F2() by LANG1:def 2; :: thesis: verum
end;
hence dt1 = dt2 by A10, A11, A12, A13, A15; :: thesis: verum
end;
A16: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A17: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; :: thesis: ( 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 ; :: thesis: 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 A26: dt1 in F1() . n ; :: thesis: dt1 = dt2
then height (dom dt19) <= n by A23, A25;
then dt29 in F1() . n by A21, A22, A24, A25;
hence dt1 = dt2 by A17, A20, A26; :: thesis: verum
end;
suppose A27: not dt1 in F1() . n ; :: thesis: dt1 = dt2
A28: 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 :: thesis: for k being Nat st k in dom p11 holds
p1 . k = p2 . k
let k be Nat; :: thesis: ( k in dom p11 implies p1 . k = p2 . k )
assume A42: k in dom p11 ; :: thesis: p1 . k = p2 . k
then 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; :: thesis: verum
end;
then p1 = p2 by A34, A37, A41, FINSEQ_1:13;
hence dt1 = dt2 by A29, A32, A40; :: thesis: verum
end;
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():]; :: thesis: ( 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 ; :: thesis: 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)
proof
let n be Nat; :: thesis: F1() . n c= F1() . (n + 1)
F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3;
hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; :: thesis: verum
end;
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; :: thesis: verum