distributes | BinaryFunction | BinaryFunction | trichotomizingOn | 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 | (=> (distributes ?FUNCTION1 ?FUNCTION2) (forall (?INST1 ?INST2 ?INST3) (=> (and (instance ?INST1 (DomainFn ?FUNCTION1)) (instance ?INST2 (DomainFn ?FUNCTION1)) (instance ?INST3 (DomainFn ?FUNCTION1)) (instance ?INST1 (DomainFn ?FUNCTION2)) (instance ?INST2 (DomainFn ?FUNCTION2)) (instance ?INST3 (DomainFn ?FUNCTION2))) (equal (AssignmentFn ?FUNCTION1 ?INST1 (AssignmentFn ?FUNCTION2 ?INST2 ?INST3)) (AssignmentFn ?FUNCTION2 (AssignmentFn ?FUNCTION1 ?INST1 ?INST2) (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))
| | BinaryRelation |