GNU Aris Manual: dt

Next: eq, Previous: id, Up: Equivalence Rules [Contents]

6.2.6 Distribution

P ^ (Q0 v Q1 v ... v Qn) <=> (P ^ Q0) v (P ^ Q1) v (P ^ Q2) v ... v (P ^ Qn)
P v (Q0 v Q1 ^ ... ^ Qn) <=> (P v Q0) ^ (P v Q1) ^ (P v Q2) ^ ... ^ (P v Qn)
3x(P(x) v Q(x)) <=> 3x(P(x)) v 3x(Q(x))
Vx(P(x) ^ Q(x)) <=> Vx(P(x)) ^ Vx(Q(x))