deffunc H₃( set , set ) -> set = $2 \/ { ([o,H₂(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of G, p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of G,NAT:] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = { (root-tree [t,d]) where t is Symbol of G, d is Element of NAT : ( ( t in Terminals G & d = H₁(t) ) or ( t ==> {} & d = H₂(t, {} , {} ) ) ) } and
A3: for n being Nat holds f . (n + 1) = H₃(n,f . n) from NAT_1:sch 11();
A4: for n being Nat holds f . (n + 1) = (f . n) \/ { ([o,H₂(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of G, p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of G,NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A3;
ex X1 being Subset of (FinTrees the carrier of G) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of G,NAT:] : t in Union f } & ( for d being Symbol of G st d in Terminals G holds
root-tree d in X1 ) & ( for o being Symbol of G
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 G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) ) from DTCONSTR:sch 4(A1, A2, A4);
hence ex b₁ being Subset of (FinTrees the carrier of G) st
( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b₁ ) & ( for o being Symbol of G
for p being FinSequence of b₁ st o ==> roots p holds
o -tree p in b₁ ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b₁ c= F ) ) ; :: thesis: verum