Promotion of bare decorations & comparisons

["Nathan T. Hayes" <nh@xxxxxxxxxxxxxxxxx>]

Jurgen,

Motion 42 requires bare decorations dac, def and trv must promote to
decorated intervals Entire_dac, Entire_def and Entire_trv, respectively.
This gives two implications:

	-- decoration emp is mostly superfluous, because only Empty can have
this decoration (except for ill decoration, which IMO still needs to be
dropped)

	-- certain comparison relations on bare decorations such as [1,2]
\subseteq def will always be true, and this seems very dangerous to me

In the decoration system with EIN, the decorated intervals Empty_EIN,
Empty_DAC, Empty_DEF and Empty_GAP are not contradictions. This means a bare
decoration can be defined as a compressed decorated empty set. This gives
the implications:

	-- decoration NDF is not superfluous, because Empty can have any
decoration

	-- all comparison relations on bare decorations are the same as the
equivalent comparison relations on Empty (since all bare decorations can be
viewed as compressed decorated empty sets), e. g., [1,2] \subseteq DEF is
false

Nate