Relation DISTRIBUTES

• Defined in theory: Abstract-algebra
• Source code: abstract-algebra.lisp

Slots on this relation:

Instance-Of: Relation

Arity: 3

Equivalence Axioms:

(<=> (Distributes ?Op ?G ?Domain)
     (And (Binary-Operator-On ?Op ?Domain)
          (Binary-Operator-On ?G ?Domain)
          (Forall (?X ?Y ?Z)
                  (=> (Instance-Of ?X ?Domain)
                      (Instance-Of ?Y ?Domain)
                      (Instance-Of ?Z ?Domain)
                      (= (Value ?Op (Value ?G ?X ?Y) ?Z)
                         (Value ?G
                                (Value ?Op ?X ?Z)
                                (Value ?Op ?Y ?Z)))))))

Other Related Axioms:

(<=> (Distributes ?Op ?G ?Domain)
     (And (Binary-Operator-On ?Op ?Domain)
          (Binary-Operator-On ?G ?Domain)
          (Forall (?X ?Y ?Z)
                  (=> (Instance-Of ?X ?Domain)
                      (Instance-Of ?Y ?Domain)
                      (Instance-Of ?Z ?Domain)
                      (= (Value ?Op (Value ?G ?X ?Y) ?Z)
                         (Value ?G
                                (Value ?Op ?X ?Z)
                                (Value ?Op ?Y ?Z)))))))

(<=> (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
          (Semigroup ?Domain ?Mult-Op ?One-Id)
          (Distributes ?Mult-Op ?Plus-Op ?Domain)))

(<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
          (Abelian-Semigroup ?Domain ?Mult-Op ?One-Id)
          (Distributes ?Mult-Op ?Plus-Op ?Domain)))