distributes (distributes)

A BinaryFunction function1 is distributive over another BinaryFunction function2 just in case (function1 inst1 (function2 inst2 inst3)) is equal to (function2 (function1 inst1 inst2) (function1 inst1 inst3)), for all inst1, inst2, and inst3.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

varga

inheritable relation

dvi-lakshana
is instance of

varga

inheritable relation

dvi-aadhaarI sambandha
is instance of

distributes

Coordinate term(s)

arc weight authors before or equal causes causes subclass citizen closed on connected contains information cooccur copy date decreases likelihood developmental form disjoint documentation duration earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element in list in scope of interest increases likelihood independent probability inhabits inhibits initial list instance inverse irreflexive on larger less than less than or equal to material measure meets temporally modal attribute overlaps temporally parent partial ordering on partly located path length possesses precondition prevents property publishes range range subclass refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph sub list sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure temporal part time total ordering on trichotomizing on uses valence version

Type restrictions

distributes(dvi-aadhaary prakaarya, dvi-aadhaary prakaarya)

Axioms (1)

agar function1 is distributive over function2,
to sab-kuch inst1,inst2,inst3 ke lie hai, ki: agar the number argument of function1 is an instance of class1 aur inst1 is an instance of class1 aur inst2 is an instance of class1 aur inst3 is an instance of class1 aur the number argument of function2 is an instance of class2 aur inst1 is an instance of class2 aur inst2 is an instance of class2 aur inst3 is an instance of class2, to "function1(inst1,"function2(inst2,inst3)")" is equal to "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))