helm/software/matita/library/didactic/exercises/natural_deduction.ma

   1 (* Esercizio 0
   2    ===========
   3
   4    Compilare i seguenti campi:
   5
   6    Nome1: ...
   7    Cognome1: ...
   8    Matricola1: ...
   9    Account1: ...
  10
  11    Nome2: ...
  12    Cognome2: ...
  13    Matricola2: ...
  14    Account2: ...
  15
  16 *)
  17
  18
  19 include "didactic/support/natural_deduction.ma".
  20
  21
  22
  23 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
  24 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
  25 apply rule (⇒_i [H] (¬A ∨ ¬B));
  26 apply rule (RAA [K] (⊥));
  27 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
  28         [ apply rule (discharge [K]).
  29         | apply rule (∨_i_l (¬A));
  30         ]