see

Composition of injective functions is injective.

Insight

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

Selected conclusions:

• :result :sameInputByCompositeInjectivity (:h :b :a) .
• :result :sameInputByCompositeInjectivity (:h :a :b) .

Explanation

The generated JavaScript starts from 12 compiled source fact(s), applies 8 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 :inX true, then (?x ?x) :sameTerm true. This produced (:a :a) :sameTerm true .
  • Premises used:
    • :a :inX true . (source fact)
• Rule 1: if ?x :inX true, then (?x ?x) :sameTerm true. This produced (:b :b) :sameTerm true .
  • Premises used:
    • :b :inX true . (source fact)
• Rule 2: if ?y :inY true, then (?y ?y) :sameTerm true. This produced (:p :p) :sameTerm true .
  • Premises used:
    • :p :inY true . (source fact)
• Rule 2: if ?y :inY true, then (?y ?y) :sameTerm true. This produced (:q :q) :sameTerm true .
  • Premises used:
    • :q :inY true . (source fact)
• Rule 3: if ?z :inZ true, then (?z ?z) :sameTerm true. This produced (:r :r) :sameTerm true .
  • Premises used:
    • :r :inZ true . (source fact)
• Rule 6: if ?f :injective true; (?f ?x) :app ?u; (?f ?y) :app ?v; (?u ?v) :sameTerm true, then (?x ?y) :sameTerm true. This produced (:p :q) :sameTerm true .
  • Premises used:
    • :g :injective true . (source fact)
    • (:g :p) :app :r . (source fact)
    • (:g :q) :app :r . (source fact)
    • (:r :r) :sameTerm true . (derived fact)
• Rule 6: if ?f :injective true; (?f ?x) :app ?u; (?f ?y) :app ?v; (?u ?v) :sameTerm true, then (?x ?y) :sameTerm true. This produced (:q :p) :sameTerm true .
  • Premises used:
    • :g :injective true . (source fact)
    • (:g :q) :app :r . (source fact)
    • (:g :p) :app :r . (source fact)
    • (:r :r) :sameTerm true . (derived fact)
• Rule 7: if ?h :compositeOf (?g ?f); (?f ?x) :app ?y; (?g ?y) :app ?z, then (?h ?x) :app ?z. This produced (:h :a) :app :r .
  • Premises used:
    • :h :compositeOf (:g :f) . (source fact)
    • (:f :a) :app :p . (source fact)
    • (:g :p) :app :r . (source fact)

Evidence

These are the facts selected by the query projection.

:result :sameInputByCompositeInjectivity (:h :a :b) .  
:result :sameInputByCompositeInjectivity (:h :b :a) .