Skip to content

Instantly share code, notes, and snippets.

@sphynx
Created August 10, 2013 20:21
Show Gist options
  • Save sphynx/6201976 to your computer and use it in GitHub Desktop.
Save sphynx/6201976 to your computer and use it in GitHub Desktop.
(define l_y1 :: int)
(define l_y2 :: int)
(define l_y3 :: int)
(define l_x1 :: int)
(define l_x2 :: int)
(define l_x3 :: int)
(define l_x4 :: int)
(assert (<= l_x1 3))
(assert (>= l_x1 0))
(assert (<= l_x2 3))
(assert (>= l_x2 0))
(assert (<= l_x3 3))
(assert (>= l_x3 0))
(assert (<= l_x4 3))
(assert (>= l_x4 0))
(assert (<= l_y1 3))
(assert (>= l_y1 1))
(assert (<= l_y2 3))
(assert (>= l_y2 1))
(assert (<= l_y3 3))
(assert (>= l_y3 1))
; L(y_i) = L(y_j) => y_i = y_j (each line number has only one component)
(assert (/= l_y1 l_y2))
(assert (/= l_y1 l_y3))
(assert (/= l_y2 l_y3))
; l_x1 < l_y1, l_x2 < l_y2, l_x3 < l_y3, l_x4 < l_y4
(assert (< l_x1 l_y1))
(assert (< l_x2 l_y2))
(assert (< l_x3 l_y3))
(assert (< l_x4 l_y3))
(check)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment