# In a partial order, a greatest lower bound is unique.
@prefix : <https://eyereasoner.github.io/eye/reasoning#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

{ ?x :inP true. } => { ?x :leq ?x. }.
{ ?x :leq ?y. ?y :leq ?z. } => { ?x :leq ?z. }.
{ ?x :leq ?y. ?y :leq ?x. } => { (?x ?y) :sameTerm true. }.
{ (?x ?y) :sameTerm true. } => { (?y ?x) :sameTerm true. }.
{ ?m :glbOf (?a ?b). } => { ?m :lowerBoundOf (?a ?b). ?m :leq ?a. ?m :leq ?b. }.
{ ?m :glbOf (?a ?b). ?l :lowerBoundOf (?a ?b). } => { ?l :leq ?m. }.
{ ?m :glbOf (?a ?b). ?n :glbOf (?a ?b). (?m ?n) :sameTerm true. } => { (?a ?b ?m ?n) :sameGlb true. }.

:a :inP true.
:b :inP true.
:g1 :inP true.
:g2 :inP true.
:g1 :glbOf (:a :b).
:g2 :glbOf (:a :b).

{ (?a ?b ?m ?n) :sameGlb true. ?m log:notEqualTo ?n. } log:query { :result :sameGreatestLowerBound (?a ?b ?m ?n). }.