SHARE
TWEET

Untitled

a guest Nov 13th, 2019 92 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Theorem “A7.1.1 no”: ¬ (∃ x : ℤ • ∀ y : ℤ • y + 2 < 3 · x )
  2. Proof:
  3.   Using “Generalised De Morgan”:
  4.     Subproof for `(∀ x : ℤ • ∃ y : ℤ • ¬ (y + 2 < 3 · x) )`:
  5.       For any `x : ℤ`:
  6.           ∃ y : ℤ • ¬ (y + 2 < 3 · x)
  7.         ⇐ ⟨“∃-Introduction”⟩
  8.           (¬ (y + 2 < 3 · x))[y ≔ 3 · x]
  9.         = ⟨ Substitution⟩
  10.           (¬ (3 · x + 2 < 3 · x))
  11.         = ⟨ “Identity of +”⟩
  12.           (¬ (3 · x + 2 < 3 · x + 0))
  13.         = ⟨ “<-Isotonicity of +”⟩
  14.           (¬ (2 < 0))
  15.         ≡ ⟨ Fact `2 < 0 ≡ false`⟩
  16.           (¬ false)
  17.         ≡ ⟨ “Negation of `false`”⟩
  18.           true
  19.  
  20.  
  21.  
  22.  
  23. Theorem “A7.1.2 yes”: (∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)
  24. Proof:
  25.     (∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)
  26.   =⟨ Subproof for `(∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)`:
  27.           For any `x`:
  28.               For any `y`:
  29.                   ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5
  30.                 ⇐⟨“∃-Introduction”⟩
  31.                   (y + 2 · z ≤ z + 3 · x + 5)[z ≔ 3 · x + 5 - y]
  32.                 =⟨ Substitution⟩
  33.                   (y + 2 · (3 · x + 5 - y) ≤ 3 · x + 5 - y + 3 · x + 5)
  34.                 =⟨ “Subtraction”⟩
  35.                   (y + 2 · (3 · x + 5 + - y) ≤ 3 · x + 5 + - y + 3 · x + 5)
  36.                 =⟨ “Distributivity of · over +”⟩
  37.                   (y + 2 · 3 · x + 2 · 5 + 2 · (- y) ≤ (3 + 3)· x + 5 + - y + 5)
  38.                 =⟨ Evaluation⟩
  39.                   (y + 6· x + 10 + 2 · (- y) ≤ 6 · x + - y + 10)
  40.                 =⟨ Evaluation⟩
  41.                   (y + 6· x + 10 + 2 · (- y) ≤ 6 · x +  - y + 10)
  42.                 =⟨ (15.21)⟩
  43.                   (y + 6· x + 10 + (- 2) · y ≤ 6 · x  + - y + 10)
  44.                 =⟨ “Identity of ·”, “Distributivity of · over +”⟩
  45.                   (6· x + 10 + (1 + (- 2)) · y ≤ 6 · x  + - y + 10)
  46.                 =⟨ “Subtraction”, Fact `1 - 2 = - 1`⟩
  47.                   (6· x + 10 + (- 1) · y ≤ 6 · x - y + 10)
  48.                 =⟨ (15.20) ⟩
  49.                   (6· x + 10 + (- y) ≤ 6 · x - y + 10)
  50.                 =⟨ “Symmetry of +” ⟩
  51.                   (6· x  + (- y) + 10 ≤ 6 · x - y + 10)
  52.                 =⟨ “Subtraction” ⟩
  53.                   (6· x - y + 10 ≤ 6 · x - y + 10)
  54.                 =⟨ “Reflexivity of ≤” ⟩
  55.                    true
  56.      ⟩
  57.      true
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top