see

In a partial order, a greatest lower bound is unique.

Insight

The compiled query selected 2 fact(s) after the rule closure was computed.
Main conclusion: :result :sameGreatestLowerBound (:a :b :g2 :g1).

Selected conclusions:

• :result :sameGreatestLowerBound (:a :b :g2 :g1) .
• :result :sameGreatestLowerBound (:a :b :g1 :g2) .

Explanation

The generated JavaScript starts from 6 compiled source fact(s), applies 7 compiled rule(s), and stops only after a fixpoint is reached.
After saturation, the compiled log:query directive projects only the matching facts shown in the insight, rather than dumping the whole graph.

A compact derivation path is:

• Rule 1: if ?x :inP true, then ?x :leq ?x. This produced :a :leq :a .
  • Premises used:
    • :a :inP true . (source fact)
• Rule 1: if ?x :inP true, then ?x :leq ?x. This produced :b :leq :b .
  • Premises used:
    • :b :inP true . (source fact)
• Rule 1: if ?x :inP true, then ?x :leq ?x. This produced :g1 :leq :g1 .
  • Premises used:
    • :g1 :inP true . (source fact)
• Rule 1: if ?x :inP true, then ?x :leq ?x. This produced :g2 :leq :g2 .
  • Premises used:
    • :g2 :inP true . (source fact)
• Rule 3: if ?x :leq ?y; ?y :leq ?x, then (?x ?y) :sameTerm true. This produced (:a :a) :sameTerm true .
  • Premises used:
    • :a :leq :a . (derived fact)
• Rule 3: if ?x :leq ?y; ?y :leq ?x, then (?x ?y) :sameTerm true. This produced (:b :b) :sameTerm true .
  • Premises used:
    • :b :leq :b . (derived fact)
• Rule 3: if ?x :leq ?y; ?y :leq ?x, then (?x ?y) :sameTerm true. This produced (:g1 :g1) :sameTerm true .
  • Premises used:
    • :g1 :leq :g1 . (derived fact)
• Rule 3: if ?x :leq ?y; ?y :leq ?x, then (?x ?y) :sameTerm true. This produced (:g2 :g2) :sameTerm true .
  • Premises used:
    • :g2 :leq :g2 . (derived fact)

Evidence

These are the facts selected by the query projection.

:result :sameGreatestLowerBound (:a :b :g1 :g2) .  
:result :sameGreatestLowerBound (:a :b :g2 :g1) .