# Composition of injective functions is injective.
@prefix : <https://eyereasoner.github.io/eye/reasoning#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

{ ?x :inX true. } => { (?x ?x) :sameTerm true. }.
{ ?y :inY true. } => { (?y ?y) :sameTerm true. }.
{ ?z :inZ true. } => { (?z ?z) :sameTerm true. }.
{ (?a ?b) :sameTerm true. } => { (?b ?a) :sameTerm true. }.
{ (?f ?x) :app ?u. (?f ?x) :app ?v. } => { (?u ?v) :sameTerm true. }.
{ ?f :injective true. (?f ?x) :app ?u. (?f ?y) :app ?v. (?u ?v) :sameTerm true. } => { (?x ?y) :sameTerm true. }.
{ ?h :compositeOf (?g ?f). (?f ?x) :app ?y. (?g ?y) :app ?z. } => { (?h ?x) :app ?z. }.
{ ?h :compositeOf (?g ?f). ?f :injective true. ?g :injective true. (?f ?x) :app ?fx. (?f ?y) :app ?fy. (?g ?fx) :app ?u. (?g ?fy) :app ?v. (?u ?v) :sameTerm true. (?x ?y) :sameTerm true. } => { (?h ?x ?y) :sameInputUnderEqualCompositeOutput true. }.

:a :inX true.
:b :inX true.
:p :inY true.
:q :inY true.
:r :inZ true.
:f :injective true.
:g :injective true.
:h :compositeOf (:g :f).
(:f :a) :app :p.
(:f :b) :app :q.
(:g :p) :app :r.
(:g :q) :app :r.

{ (?h ?x ?y) :sameInputUnderEqualCompositeOutput true. ?x log:notEqualTo ?y. } log:query { :result :sameInputByCompositeInjectivity (?h ?x ?y). }.