====================================================
DATE: 09-20-2003
TIME: 16:45:48
Theorem: DM 1          42          Conclusion: (AvB)<->~(~A&~B)
* 1.  AvB                                                   Assumption
** 2.  ~A&~B                                                Assumption
** 3.  ~A                                                   &ELIM/L  2
** 4.  ~B                                                   &ELIM/R  2
** 5.  B                                                    v ELIM  1  3
* 6.  ~(~A&~B)                                              ~INTRO  2 4 5
 7.  (AvB)->~(~A&~B)                                        -> INTRO  1  6
* 8.  ~(~A&~B)                                              Assumption
** 9.  ~(AvB)                                               Assumption
*** 10.  A                                                  Assumption
*** 11.  AvB                                                vINTRO  10
** 12.  ~A                                                  ~INTRO  10 11 9
*** 13.  B                                                  Assumption
*** 14.  AvB                                                vINTRO  13
** 15.  ~B                                                  ~INTRO  13 14 9
** 16.  ~A&~B                                               &INTRO  12  15
* 17.  AvB                                                  ~ELIM  9  16 8
 18.  ~(~A&~B)->(AvB)                                       -> INTRO  8  17
 19.  (AvB)<->~(~A&~B)                                      <->INTRO  7 18

DEDUCTION IS COMPLETE


Minor ~INTRO error: Cited sentence and its negation in wrong order.
====================================================
DATE: 09-20-2003
TIME: 16:57:10
Theorem: DM 2          43          Conclusion: (A&B)<->~(~Av~B)
* 1.  A&B                                                   Assumption
* 2.  A                                                     &ELIM/L  1
* 3.  B                                                     &ELIM/R  1
** 4.  ~Av~B                                                Assumption
** 5.  ~~A                                                  DN INTRO  2
** 6.  ~B                                                   v ELIM  4  5
* 7.  ~(~Av~B)                                              ~INTRO  4 3 6
 8.  (A&B)->~(~Av~B)                                        -> INTRO  1  7
* 9.  ~(~Av~B)                                              Assumption
** 10.  ~(A&B)                                              Assumption
*** 11.  ~A                                                 Assumption
*** 12.  ~Av~B                                              vINTRO  11
** 13.  A                                                   ~ELIM  11  12 9
*** 14.  ~B                                                 Assumption
*** 15.  ~Av~B                                              vINTRO  14
** 16.  B                                                   ~ELIM  14  15 9
** 17.  A&B                                                 &INTRO  13  16
* 18.  A&B                                                  ~ELIM  10  17 10
 19.  ~(~Av~B)->(A&B)                                       -> INTRO  9  18
 20.  (A&B)<->~(~Av~B)                                      <->INTRO  8 19

DEDUCTION IS COMPLETE

==================
Observe that the assumption in line 10 was superfluous, since A&B can be derived,
without using line 10, as it was on line 17.  (We can see that line 10 was not cited
until line 18.)  Thus, line 10 and line 18 were superfluous, and the deduction could have 
been done in 18 steps.