next node: OrderingByInjection,
prev node: Subsystem Orderings,
up to node: Subsystem Orderings


InducedRel

Signature of InducedRel

List of Import References :
See BOOL
See DENOTATION

SIGNATURE InducedRel[data1, data2, rel : data2 ** data2 -> bool, f]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

induce relation on data1 by corresponding relation on data2

Parameter

SORT data1 data2
FUN rel: data2 ** data2 -> bool
FUN f : data1 -> data2

FUN rel : data1 ** data1 -> bool
-- LAW rel_def : ALL d1 d2: d1 rel d2 <=> f(d1) rel f(d2)


next node: OrderingByInjection,
prev node: Subsystem Orderings,
up to node: Subsystem Orderings