[Spam] [SCL] question about composite terms in relation/function position

[Robert E. Kent]

This expression with universal quantifiers is nonsense. What I should have
used was a lambda operator for binding the arguments of relations.  For example,

((lambda (x y) (less-than (square-root x) (times x y))) 4 1)

But such would not conform to SCL.

> was not successful because it contains free variables and it is unclear
how to bind the arguments in the proper order. This can be done with
equations

> (forall (x y) (and (less-than (square-root x) (times x y)) (= x 4) (= y 1)))

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20040318/1aa5635a/attachment.html