Wiki

Maximal elements of a non-empty partially ordered set

Let (S,R) be an arbitrary partially ordered set and x be an element which belongs to S. In this section, x is called maximal over S if forall y∈S, the proposition y R x is not true. Then the following theorem holds.

Theorem Let (S,R) be an partially ordered set. If S is not empty, the set { x∈S | x is maximal over S } is not empty.

This theorem enables us to declare the following module.

#!python

module MAXIMAL
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T)
)
{
  imports
  {
    pr(DEDUCIBLE)
  }
  signature
  {
    op  maximal : Set PartialOrder -> Set
  }
  axioms
  {
    vars X Y : Elt
    vars S : Set
    vars R : PartialOrder
    eq maximal(nil,R) = nil .
    cq (maximal(S,R) = nil) = false
       if (not S = nil) .
    eq deducible((X @ maximal(S,R)) |- (X @ S)) =  true .
    eq deducible(((X @ S),(Y @ maximal(S,R))) |- (not X R Y)) =  true .
  }
}

The avobe module is used to verify the deadlock freedom of the scheduling mechanism of the OSEK OS.