Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }|instance 1 of a Gentzen proof system}}
{{TableauLine | n    = 1
              | f    = \neg p, p, q
              | rlnk = Definition:Gentzen Proof System/Instance 1#Axioms
              | rtxt = Axiom
}}
{{TableauLine | n    = 2
              | f    = \neg p, p \lor q
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \lor$
              | dep  = 1
}}
{{TableauLine | n    = 3
              | f    = \neg p, p, r
              | rlnk = Definition:Gentzen Proof System/Instance 1#Axioms
              | rtxt = Axiom
}}
{{TableauLine | n    = 4
              | f    = \neg p, p \lor r
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \lor$
              | dep  = 3
}}
{{TableauLine | n    = 5
              | f    = \neg p, \paren {p \lor q} \land \paren {p \lor r}
              | rlnk = Definition:Gentzen Proof System/Instance 1/Alpha-Rule
              | rtxt = $\alpha$-Rule: $\alpha \land$
              | dep  = 2, 4
}}
{{TableauLine | n    = 6
              | f    = \neg q, \neg r, p, q
              | rlnk = Definition:Gentzen Proof System/Instance 1#Axioms
              | rtxt = Axiom
}}
{{TableauLine | n    = 7
              | f    = \neg q, \neg r, p \lor q
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \lor$
              | dep  = 6
}}
{{TableauLine | n    = 8
              | f    = \neg q, \neg r, p, r
              | rlnk = Definition:Gentzen Proof System/Instance 1#Axioms
              | rtxt = Axiom
}}
{{TableauLine | n    = 9
              | f    = \neg q, \neg r, p \lor r
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \lor$
              | dep  = 8
}}
{{TableauLine | n    = 10
              | f    = \neg q, \neg r, \paren {p \lor q} \land \paren {p \lor r}
              | rlnk = Definition:Gentzen Proof System/Instance 1/Alpha-Rule
              | rtxt = $\alpha$-Rule: $\alpha \land$
              | dep  = 7, 9
}}
{{TableauLine | n    = 11
              | f    = \neg \paren {q \land r}, \paren {p \lor q} \land \paren {p \lor r}
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \land$
              | dep  = 10
}}
{{TableauLine | n    = 12
              | f    = \neg \paren {p \lor \paren {q \land r} }, \paren {p \lor q} \land \paren {p \lor r}
              | rlnk = Definition:Gentzen Proof System/Instance 1/Alpha-Rule
              | rtxt = $\alpha$-Rule: $\alpha \land$
              | dep  = 5, 11
}}
{{TableauLine | n    = 13
              | f    = \paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }
              | rlnk = Definition:Gentzen Proof System/Instance 1/Beta-Rule
              | rtxt = $\beta$-Rule: $\beta \implies$
              | dep  = 12
}}
{{EndTableau}}
{{qed}}