SPO_PO.maude

fmod STRICT_PARTIAL_ORDER is
    sort Elt .
    op _<_ : Elt Elt -> Bool .
    vars X Y Z : Elt .
    eq X < X = false [nonexec label strict] .
    ceq Y < X = false
        if X < Y [nonexec label asymmetric] .
    ceq X < Z = true
        if X < Y /\ Y < Z [nonexec label transitive] .
endfm

fmod PARTIAL_ORDER is
    including STRICT_PARTIAL_ORDER .
    op _<=_ : Elt Elt -> Bool .
    vars X Y : Elt .
    eq X <= Y = X < Y or X == Y .
endfm

fth PROVE_PARTIAL_ORDER is
    protecting BOOL .
    including TRIV .
    op _<=_ : Elt Elt -> Bool .
    vars X Y Z : Elt .
    eq X <= X = true [nonexec label reflexive] .
    ceq X == Y = true
        if X <= Y /\ Y <= X [nonexec label antisymmetric] .
    ceq X <= Z = true
        if X <= Y /\ Y <= Z [nonexec label transitive] .
endfth

view ProvePartialOrder from PROVE_PARTIAL_ORDER
                         to PARTIAL_ORDER is
    sort Elt to Elt .
    op _<=_ to _<=_ .
endv