Prove DeMorgan's laws Using the the ten inferences of the Natural Deduction System prove DeMorgan's laws.
The Rules of Natural Deduction

Negation Introduction: {(P → Q), (P → ¬Q)} ⊢ ¬P

Negation Elimination:  {(¬P → Q), (¬P → ¬Q)} ⊢ P

And Introduction:      {P, Q} ⊢ P ʌ Q

And Elimination:       P ʌ Q ⊢ {P, Q}

Or Introduction:       P ⊢ {(P ∨ Q),(Q ∨ P)}

Or Elimination:        {(P ∨ Q), (P → R), (Q → R)} ⊢ R

Iff Introduction:      {(P → Q), (Q → P)} ⊢ (P ≡ Q)

Iff Elimination:       (P ≡ Q) ⊢ {(P → Q), (Q → P)}

If Introduction:       (P ⊢ Q) ⊢ (P → Q)

If Elimination:        {(P → Q), P} ⊢ Q


Proof structure
Each statement in your proof must be the result of one of the ten rules applied to some previously derived propositions (no circular logic) or an assumption (described below).  Each rule operates across some propositions on the left hand side of the ⊢ (logical consequence operator) and creates any number of propositions from the right hand side.  The If Introduction works slightly differently from the rest of the operators (described in detail below).  It operates across one statement that is the logical consequent of another.
Example 1
You have the following statements:
{(P → R), Q}
You may use And Introduction to make:
(P → R) ʌ Q
Example 2
You have the following statements:
{(P → R), P}
You may use If Elimination to make:
R
Example 3
You have the following statements:
(P ʌ Q)
You may use And Elimination to make:
P
or to make:
Q
Assumption Propagation
You may at any point assume any statement you wish.  Any statement derived from these assumptions will be &quot;reliant&quot; on them.  Statements will also be reliant on the assumptions their parent statements rely on.  The only way to eliminate assumptions is by If Introduction.  For If introduction you start with a Statement Q that is reliant on a statement P and end with (P → Q).  The new statement is reliant on every assumption Q relies on except for assumption P.  Your final statement should rely on no assumptions.
Specifics and scoring
You will construct one proof for each of DeMorgan's two laws using only the 10 inferences of the Natural Deduction Calculus.
The two rules are:
¬(P ∨ Q) ≡ ¬P ʌ ¬Q

¬(P ʌ Q) ≡ ¬P ∨ ¬Q

Your score is the number of inferences used plus the number of assumptions made.  Your final statement should not rely on any assumptions (i.e. should be a theorem).
You are free to format your proof as you see fit.
You may carry over any Lemmas from one proof to another at no cost to score.
Example Proof
I will prove that (P and not(P)) implies Q
(Each bullet point is +1 point)

Assume not (Q)

Assume (P and not(P))

Using And Elim on (P and not(P)) derive {P, not(P)}

Use And Introduction on P and not(Q) to derive (P and not(Q))

Use And Elim on the statement just derived to make P


The new P proposition is different from the other one we derive earlier.  Namely it is reliant on the assumptions not(Q) and (P and not(P)).  Whereas the original statement was reliant only on (P and not(P)).  This allows us to do:

If Introduction on P introducing not(Q) implies P (still reliant on the (P and not(P)) assumption)

Use And Introduction on not(P) and not(Q) (from step 3) to derive (not(P) and not(Q))

Use And Elim on the statement just derived to make not(P)
(now reliant on not(Q))

If Introduction on the new not(P) introducing not(Q) implies not(P)

We will now use negation elimination on not(Q) implies not(P) and not(Q) implies P to derive Q


This Q is reliant only on the assumption (P and not(P)) so we can finish the proof with

If Introduction on Q to derive (P and not(P)) implies Q

This proof scores a total of 11.
Score: 81
Each line should be worth 1 point. The De Morgan's laws are found at statements (3) and (6). Labels in brackets denote the previous statement(s) a line depends on if they are not immediately preceding.
(a) assume P {
    (aa) P ^ P
    (ab) P
    (ac) P v Q
} (a1) P -&gt; P
  (a2) P -&gt; P v Q
(1) assume ~P ^ ~Q {
    (1a) assume P v Q {
        (1aa) assume Q {
            (1aaa) assume ~P {
                (1aaaa) Q ^ Q [1aa]
                (1aaab) Q
                (1aaac) ~Q [1]
            } (1aaa1) ~P -&gt; Q
              (1aaa2) ~P -&gt; ~Q
            (1aab) P
        } (1aa1) Q -&gt; P
        P [1a, a1, 1aa1]
        ~P [1]
    } (1a1) P v Q -&gt; P
      (1a2) P v Q -&gt; ~P
    (1b) ~(P v Q)
} (11) ~P ^ ~Q -&gt; ~(P v Q)
(2) assume ~(P v Q) {
    (2a) ~(P v Q) ^ ~(P v Q)
    (2b) assume P {
        (2aa) ~(P v Q) [2a]
    } (2b1) P -&gt; ~(P v Q)
    (2c) ~P [a2, 2b1]
    (2d) assume Q {
        (2da) ~(P v Q) [2a]
        (2db) P v Q
    } (2d1) Q -&gt; ~(P v Q)
      (2d2) Q -&gt; P v Q
    (2e) ~Q
    (2f) ~P ^ ~Q
} (21) ~(P v Q) -&gt; ~P ^ ~Q
(3) ~(P v Q) == ~P ^ ~Q [11, 21]
(4) assume ~P v ~Q {
    (4a) assume ~P {
        (4aa) assume P ^ Q {
            (4aaa) P
            (4aab) ~P ^ ~P [4a]
            (4aac) ~P
        } (4aa1) P ^ Q -&gt; P
          (4aa2) P ^ Q -&gt; ~P
        (4ab) ~(P ^ Q)
    } (4a1) ~P -&gt; ~(P ^ Q)
    (4b) assume ~Q {
        (4ba) assume P ^ Q {
            (4baa) Q
            (4bab) ~Q ^ ~Q [4b]
            (4bac) ~Q
        } (4ba1) P ^ Q -&gt; Q
          (4ba2) P ^ Q -&gt; ~Q
        (4bb) ~(P ^ Q)
    } (4b1) ~P -&gt; ~(P ^ Q)
    (4c) ~(P ^ Q) [4, 4a1, 4b1]
} (41) ~P v ~Q -&gt; ~(P ^ Q) 
(5) assume ~(P ^ Q) {
    (5a) assume ~(~P v ~Q) {
        (5aa) ~(~P v ~Q) ^ ~(P ^ Q) [5, 5a]
        (5ab) assume ~P {
            (5aba) ~P v ~Q
            (5abb) ~(~P v ~Q) [5aa]
        } (5ab1) ~P -&gt; ~P v ~Q
          (5ab2) ~P -&gt; ~(~P v ~Q)
        (5ac) P
        (5ad) assume ~Q {
            (5ada) ~P v ~Q
            (5adb) ~(~P v ~Q) [5aa]
        } (5ad1) ~Q -&gt; ~P v ~Q
          (5ad2) ~Q -&gt; ~(~P v ~Q)
        (5ae) Q
        (5af) P ^ Q [5ac, 5ae]
        (5ag) ~(P ^ Q) [5aa]
    } (5a1) ~(~P v ~Q) -&gt; P ^ Q
      (5a2) ~(~P v ~Q) -&gt; ~(P ^ Q)
    (5b) ~P v ~Q
} (51) ~(P ^ Q) -&gt; ~P v ~Q
(6) ~(P ^ Q) == ~P v ~Q [41, 51]