Operation

right operation of f on x. This class is rather technical, because on this abstract level it is not possible to define the exact behavior of the operation, i.e. for which values f and x the expression x <* f is valid. For a precise definition see for example TotalOpr or OrientedOpr where the behavior can be stated.

left operation of f on x. This class is rather technical, because on this abstract level it is not possible to define the exact behavior of the operation, i.e. for which values f and x the expression f *> x is valid. For a precise definition see for example TotalOpl or OrientedOpl where the behavior can be stated.

right operation of a Total Multiplicative structure f on x.

Property Let f be a Total Multiplicative structure and x an instance of Entity, then holds:

1. For all x in x holds: x <* one u == x where u = unit is the singleton element in Point f.
2. For all x in x and f, g in f holds: x <* f <* g == x <* (f * g).

Note If f is invertible, then it gives rise of a bijection <* f on x with inverse <* invert f.

left operation of a Total Multiplicative structure f on x.

Property Let f be a Total Multiplicative structure and x an instance of Entity, then holds:

1. For all x in x holds: one u *> x == x where u = unit is the singleton element in Point f.
2. For all x in x and f, g in f holds: f *> g *> x == (f * g) *> x.

Note If f is invertible, then it gives rise of a bijection f *> on x with inverse invert f *>.

right operation of a Multiplicative structure f on a Oriented structure x.

Property Let f be a Multiplicative and x a Oriented structure, then holds:

1. For all f in f and x in x holds.

   1. If start x == end f then x <* f is valid and orientation (x <* f) == start f :> end x.
   2. If start x /= end f then x <* f is not valid and its evaluation will end up in a NotApplicable exception.
2. For all x in x holds: x <* one (start x) == x.
3. For all x in x and f, g in f with end f == start x, end g == start f holds: x <* f <* g == x <* (f * g).

Note If f is invertible, then it rise of a bijection <* f from all x in x with start x == end f to all y in x with start y == start f. Its inverse is given by <* invert f.

left operation of a Multiplicative structure f on a Oriented structure x.

Property Let f be a Multiplicative and x a Oriented structure, and f, x an instance of OrientedOpl, then holds:

1. For all f in f and x in x holds.

   1. If end x == start f then f *> x is valid and orientation (f *> x) == start x :> end f.
   2. If end x /= start f then f *> x is not valid and its evaluation will end up in a NotApplicable exception.
2. For all x in x holds: one (end x) *> x== x.
3. For all x in x and f, g in f with start g == end x, start f == end g holds: f *> g *> x == (f * g) *> x .

Note If f is invertible, then it rise of a bijection f *> from all x in x with end x == start f to all y in x with end y == end f. Its inverse is given by invert f *>.