FUNC s = Slider2(a, b, c) IS 
      (E y :: b = (s, y) REL (a, c)) 
END;

PRED Slider(a, f, c, s) IS 
      Slider2(a, f, c) = s 
END;

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

PRED OnLine(a, b, c, t) IS 
      b = (t, 0) REL (a, c) 
END;

(* "pt" is the point at parametric 
   location "t" on the Bezier curve "a", 
   "b", "c", "d". *)

PRED CurvePt(t, a, b, c, d, pt) IS 
      (E e ~ (0.5, 0) REL (a, b)
       , f ~ (0.5, 0) REL (b, c)
       , g ~ (0.5, 0) REL (c, d)
       , h ~ (0.5, 0) REL (e, f)
       , i ~ (0.5, 0) REL (f, g)
       , pt ~ (0.5, 0) REL (h, i) :: 
        OnLine(a, e, b, t) 
    AND OnLine(b, f, c, t) 
    AND OnLine(c, g, d, t) 
    AND OnLine(e, h, f, t) 
    AND OnLine(f, i, g, t) 
    AND OnLine(h, pt, i, t)) 
END;

(* The points "k", "l", and "m" compose 
   a slider, the points "a", "b", "c", 
   and "d" are the control points of a 
   Bezier curve, and "pt" is the point 
   at parametric loca- tion "t" on the 
   curve, where "t" is the slider value 
   of "k", "l", and "m" (i.e., the ratio 
   "Dist(k,l2)/Dist(k,m)", where "l2" is 
   the projection of "l" onto the 
   segment "km"). *)

PRED SliderCurvePt(k, l, m, a, b, c, d, 
                   pt) IS 
      (E t :: 
        t = Slider2(k, l, m) 
    AND CurvePt(t, a, b, c, d, pt)) 
END;

PROC SliderBg(a, b) IS 
    IF c 
     = (0.06804, -0.035581) REL (a, b)
     , d ~ (0.93196, 0.035581) REL (a, b)
     , e 
     ~ (0.423529, -0.494118) REL (a, c)
     , f 
     ~ (0.576471, 0.494118) REL (a, c)
     , g 
     ~ (0.576471, 0.494118) REL (b, d)
     , h 
     ~ (0.423529, -0.494118) REL (b, d) 
    :: a HOR f 
   AND e HOR c 
   AND d HOR h 
   AND g HOR b 
   AND a VER e 
   AND f VER c 
   AND d VER g 
   AND h VER b 
   AND (a, e) CONG (b, h) 
   AND (a, f) CONG (b, g) 
    -> Shape.Rect(a, b)
     ; PS.Stroke()
     ; Shape.Rect(c, d)
     ; PS.Fill() 
    FI 
END;