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 Element of 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[ Element of NAT ] means for dt1, dt2 being DecoratedTree of 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 ; :: thesis: ( dt1 in F1() . 0 & dt2 in F1() . 0 & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume A7: ( dt1 in F1() . 0 & dt2 in F1() . 0 & dt1 `1 = dt2 `1 ) ; :: thesis: dt1 = dt2
then consider t1 being Symbol of F2(), d1 being Element of F3() such that
A8: ( dt1 = root-tree [t1,d1] & ( ( t1 in Terminals F2() & d1 = F4(t1) ) or ( t1 ==> {} & d1 = F5(t1,{} ,{} ) ) ) ) by A2;
consider t2 being Symbol of F2(), d2 being Element of F3() such that
A9: ( dt2 = root-tree [t2,d2] & ( ( t2 in Terminals F2() & d2 = F4(t2) ) or ( t2 ==> {} & d2 = F5(t2,{} ,{} ) ) ) ) by A2, A7;
( root-tree t1 = dt1 `1 & root-tree t2 = dt2 `1 ) by A8, A9, TREES_4:25;
then A10: t1 = t2 by A7, TREES_4:4;
now
let t be Symbol of F2(); :: thesis: ( t ==> {} implies not t in Terminals F2() )
assume t ==> {} ; :: thesis: not t in Terminals F2()
then for t' being Symbol of F2() holds
( not t = t' or ex tnt being FinSequence st t' ==> tnt ) ;
then not t in { t' where t' is Symbol of F2() : for tnt being FinSequence holds not t' ==> tnt } ;
hence not t in Terminals F2() by LANG1:def 2; :: thesis: verum
end;
hence dt1 = dt2 by A8, A9, A10; :: thesis: verum
end;
A11: now
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A12: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let dt1, dt2 be DecoratedTree of ; :: thesis: ( dt1 in F1() . (n + 1) & dt2 in F1() . (n + 1) & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume A13: ( dt1 in F1() . (n + 1) & dt2 in F1() . (n + 1) & dt1 `1 = dt2 `1 ) ; :: thesis: dt1 = dt2
then A14: ( dom dt1 = dom (dt1 `1 ) & dom dt2 = dom (dt1 `1 ) ) by TREES_4:24;
A15: ( dt1 in Union F1() & dt2 in Union F1() ) by A1, A13, CARD_5:10;
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 dt1' = dt1, dt2' = dt2 as Element of FinTrees [:the carrier of F2(),F3():] by A15;
A16: for n being Element of 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 A17: dt1 in F1() . n ; :: thesis: dt1 = dt2
then height (dom dt1') <= n by A15, A16;
then dt2' in F1() . n by A14, A15, A16;
hence dt1 = dt2 by A12, A13, A17; :: thesis: verum
end;
suppose A18: not dt1 in F1() . n ; :: thesis: dt1 = dt2
A19: 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 A13, XBOOLE_0:def 3;
then consider o1 being Symbol of F2(), p1 being Element of (F1() . n) * such that
A20: ( dt1 = [o1,H3(o1,p1)] -tree p1 & ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) ) by A18;
height (dom dt1') > n by A15, A16, A18;
then A21: not dt2' in F1() . n by A14, A15, A16;
( 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 A13, A19, XBOOLE_0:def 3;
then consider o2 being Symbol of F2(), p2 being Element of (F1() . n) * such that
A22: ( dt2 = [o2,H3(o2,p2)] -tree p2 & ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p2 = q & o2 ==> pr1 (roots q) ) ) by A21;
reconsider p1 = p1 as FinSequence of FinTrees [:the carrier of F2(),F3():] by A20;
consider p11 being FinSequence of FinTrees the carrier of F2() such that
A23: ( dom p11 = dom p1 & ( for i being Element of 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 ) ) & ([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 A22;
consider p21 being FinSequence of FinTrees the carrier of F2() such that
A24: ( dom p21 = dom p2 & ( for i being Element of 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 ) ) & ([o2,H3(o2,p2)] -tree p2) `1 = o2 -tree p21 ) by TREES_4:31;
A25: ( o1 = o2 & p11 = p21 ) by A13, A20, A22, A23, A24, TREES_4:15;
now
let k be Nat; :: thesis: ( k in dom p11 implies p1 . k = p2 . k )
assume A26: k in dom p11 ; :: thesis: p1 . k = p2 . k
then consider p1k being Element of FinTrees [:the carrier of F2(),F3():] such that
A27: ( p1k = p1 . k & p11 . k = p1k `1 ) by A23;
consider p2k being Element of FinTrees [:the carrier of F2(),F3():] such that
A28: ( p2k = p2 . k & p21 . k = p2k `1 ) by A24, A25, A26;
( p1k in F1() . n & p2k in F1() . n ) by A23, A24, A25, A26, A27, A28, Th2;
hence p1 . k = p2 . k by A12, A25, A27, A28; :: thesis: verum
end;
then p1 = p2 by A23, A24, A25, FINSEQ_1:17;
hence dt1 = dt2 by A20, A22, A25; :: thesis: verum
end;
end;
end;
end;
A29: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A6, A11);
 let dt1, dt2 be DecoratedTree of ; :: thesis: ( dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume A30: ( dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 ) ; :: thesis: dt1 = dt2
then consider n1 being set such that
A31: ( n1 in NAT & dt1 in F1() . n1 ) by A1, CARD_5:10;
consider n2 being set such that
A32: ( n2 in NAT & dt2 in F1() . n2 ) by A1, A30, CARD_5:10;
reconsider n1 = n1, n2 = n2 as Element of NAT by A31, A32;
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) ) } ;
A33: for n being Element of NAT holds F1() . n c= F1() . (n + 1)
proof
let n be Element of 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;
A34: for k, s being Nat holds F1() . k c= F1() . (k + s)
proof
let k, s be Nat; :: thesis: F1() . k c= F1() . (k + s)
reconsider k = k, s = s as Element of NAT by ORDINAL1:def 13;
k <= k + s by NAT_1:11;
hence F1() . k c= F1() . (k + s) by A33, MEASURE2:22; :: thesis: verum
end;
( 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 A34;
hence dt1 = dt2 by A29, A30, A31, A32; :: thesis: verum