Don't like ads? PRO users don't see any ads ;-)
Public Pastes
Guest

Untitled

By: a guest on Mar 6th, 2010  |  syntax: Prolog  |  size: 0.25 KB  |  hits: 474  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. trans : ∀ x y w -> x ≡ y -> y ≡ w -> x ≡ w
  2. trans z z z x≡y y≡w = triv
  3. trans z z (s y) x≡y ()
  4. trans z (s y) w () y≡w
  5. trans (s y) z w () y≡w
  6. trans (s y) (s y') z x≡y ()
  7. trans (s x) (s y) (s w) x≡y y≡w = trans x y w x≡y y≡w
create a new version of this paste RAW Paste Data