List of Import References :
See BOOL
See DENOTATION
See Nat
SIGNATURE OrderingByInjection[data, inj]
$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)
-- construct ordering relations from injection in natural numbers
-- Parameter
SORT data
FUN inj: data -> nat
-- inj must be injective: inj(a1) = inj(a2) => a1 = a2
IMPORT Nat ONLY nat
FUN < > <= >= = |= : data ** data -> bool
-- ordering constructed from the given inj function
-- a1 REL a2 <=> inj(a1) REL inj(a2)
-- REL taken from < > <= >= = |=
next node: OrderingByLess,
prev node: InducedRel,
up to node: Subsystem Orderings