PRED Mid(a, b, c) IS 
      b = (0.5, 0) REL (a, c) 
END;

PRED Perp(a, b, c) IS 
      (E y :: a = (0, y) REL (b, c)) 
END;

FUNC y = Square(x) IS x * x = y END;

FUNC y = Sqrt(x) IS 
      y ~ 1 AND y * y = x 
END;

PROC PlotSqrt(a, b) IS 
    x 
 :: { x := 0
    ; PS.MoveTo(a)
    ; DO x <= 10 
      -> y 
      :: { y = Sqrt(x) 
        -> PS.LineTo((x, y) REL (a, b)) 
          }
       ; x := x + 0.1 
      OD 
     } 
END;

PROC SqrtTest(a, b) IS 
    IF sq2 ~ 1 
    :: sq2 * sq2 = 2 
    -> PS.MoveTo((1, sq2) REL (a, b))
     ; PS.LineTo(b)
     ; PS.Stroke() 
    FI 
END;

PROC IntersectTest(a, b, c, d) IS 
    IF ax, ay, bx, by, cx, cy, dx, dy 
    :: a = (ax, ay) 
   AND b = (bx, by) 
   AND c = (cx, cy) 
   AND d = (dx, dy) 
    -> { px, py 
      :: (px - ax) * (cy - ay) 
       = (py - ay) * (cx - ax) 
     AND (px - bx) * (dy - by) 
       = (py - by) * (dx - bx) 
      -> PS.MoveTo((px, py))
       ; PS.LineTo(a)
       ; PS.Stroke() 
        } 
    FI 
END;