Sample proofs: Negation, Inequivalence, and False (3.8 to 3.19)

We can put in a few example proofs here of the sort we'd like Edsger to be able to check.

3.11

    -p === q === p === -q
  === < (3.9) >
    -(p === q) === p === -q
  === < (3.2) with q := -q >
    -(p === q) === -q === p
  === < (3.9) with p,q := q,p >
    -(p === q) === -(q === p)
  === < (3.2) >
    -(p === q) === -(p === q)
      -- Done by Reflexivity of === (3.5)

3.12

3.13

    -false === true
  === < (3.8) >
    --true === true
      -- Done by Double negation (3.12)

3.14

    (p -=== q) === -p === q
  === < (3.9) >
    (p -=== q) === -(p === q)
  === < (3.10) >
    (p -=== q) === (p -=== q)
      -- Done by Reflexivity of === (3.5)

3.15

    -p === p === false
  === < (3.9) with q := p >
    -(p === p) === false
  === < (3.3) with q := p >
    -true === false
      -- Done by (3.8)

3.16

    p -=== q
  === < (3.10) >
    -(p === q)
  === < (3.2) >
    -(q === p)
  === < (3.10) with p,q := q,p >
    q -=== p

3.17

    ((p -=== q) -=== r) === (p -=== (q -=== r))

3.18

    ((p -=== q) === r) === (p -=== (q === r))

3.19

    p -=== q === r === p === q -===r