|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- gabriela.lua - Gabriela Avila's calculator for quantified
-- expressions, Lua version
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 2012mar30
-- Licence: GPL3
--
-- The latest upstream version of this can be found at:
-- http://angg.twu.net/dednat5/gabriela.lua
-- http://angg.twu.net/dednat5/gabriela.lua.html
-- (find-dn5 "gabriela.lua")
-- Quick index:
-- «.intro» (to "intro")
-- «.infix-algorithm» (to "infix-algorithm")
-- «.eoo.lua» (to "eoo.lua")
-- «.Expr» (to "Expr")
-- «.expr:infix» (to "expr:infix")
-- «.constructors» (to "constructors")
-- «.expr:tolisp» (to "expr:tolisp")
-- «.expr:eval» (to "expr:eval")
-- «.eval-quantifiers» (to "eval-quantifiers")
-- «.expr:print» (to "expr:print")
-- «.expr:Dbg» (to "expr:Dbg")
-- «.Rect» (to "Rect")
-- «.Rect-test» (to "Rect-test")
-- «.test-infix» (to "test-infix")
-- «.test-context» (to "test-context")
-- «intro» (to ".intro")
-- Consider a quantified expression, like this one (and note that to
-- keep everything in ascii we write "Fa" for "for all" and "Ex" for
-- "exists"):
--
-- Fa x in {2, 3, 4}. Ex y in {3, 4, 5}. 2*x <= y+3
--
-- using the constructors defined in this library we can create a
-- tree-ish repreresentation of that expression in memory with:
--
-- x = Var "x"
-- y = Var "y"
-- _2, _3, _4, _5 = Num(2), Num(3), Num(4), Num(5)
-- comparison = Le(_2*x, y+_3)
-- ex_expression = Ex(y, Set(_3, _4, _5), comparison)
-- fa_expression = Fa(x, Set(_2, _3, _4), ex_expression)
--
-- All the subexpressions of "fa_expression", i.e., the ones marked
-- below (even numbers!),
--
-- Fa x in {2, 3, 4}. Ex y in {3, 4, 5}. 2*x <= y+3
-- - - - - - - - - - - - -
-- \-------/ \-------/ \-/ \-/
-- \--------/
-- \---------------------------/
-- \----------------------------------------------/
--
-- are represented internally as objects of the class "Expr", and so
-- they know how to respond to all the methods for Expr objects - most
-- importantly, they have a special "__tostring" that prints them in
-- infix notation using only the parentheses that are essential, and
-- they have an "eval". Here is a quick test:
--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "gabriela.lua"
x = Var "x"
y = Var "y"
_2, _3, _4, _5 = Num(2), Num(3), Num(4), Num(5)
comparison = Le(_2*x, y+_3)
ex_expression = Ex(y, Set(_3, _4, _5), comparison)
fa_expression = Fa(x, Set(_2, _3, _4), ex_expression)
ex_expression:print() --> Ex y in {3, 4, 5}. 2*x <= y+3
fa_expression:print() --> Fa x in {2, 3, 4}. Ex y in {3, 4, 5}. 2*x <= y+3
fa_expression:eval():print() --> T
x:Whens(Set(_2, _3, _4), ex_expression)
--]]
--[[
-- «infix-algorithm» (to ".infix-algorithm")
--
-- The algorith for displaying infix expressions
-- =============================================
-- The code for displaying expressions in infix notation was inspired
-- by something that I learned in the code for Andrej Bauer's PLZoo:
--
-- (find-es "ml" "plzoo")
-- (find-es "ml" "levy")
-- (find-levyfile "syntax.ml" "string_of_expr")
-- http://andrej.com/plzoo/
-- http://andrej.com/plzoo/html/miniml.html
-- ^ look for "string_of_expr"
--
-- The basic idea is that each fully parenthesised expression like
--
-- 22 + (33 * ((44 - 55) - (66 - 77)))
--
-- has a unique representation with minimal parenthesisation, which in
-- the case of the expression above is:
--
-- 22 + 33 * (44 - 55 - (66 - 77))
--
-- to discover where those essential parentheses are, let's mark them
-- in the edges of the representation of the expression as a tree:
--
-- +
-- / \
-- 22 *
-- / \()
-- 33 -
-- / \()
-- - -
-- / \ / \
-- 44 55 66 77
--
-- If we write certain numbers at the top and the bottom of each
-- connective, the rule becomes evident. Each edge connects a bottom
-- number (above) to a top number (below). When b >= t, use
-- parentheses.
-- ___
-- / 7 \
-- / + \
-- |_6___7_|
-- / \
-- 22 ___
-- / 8 \
-- / * \
-- |_7___8_|
-- / \()
-- 33 ___
-- / 7 \
-- / - \
-- |_6___7_|
-- / \()
-- ___ ___
-- / 7 \ / 7 \
-- / - \ / - \
-- |_6___7_| |_6___7_|
-- / \ / \
-- 44 55 66 77
--]]
-- «eoo.lua» (to ".eoo.lua")
-- dofile "eoo.lua" -- (find-dn5 "eoo.lua")
-- Just the relevant definitions from eoo.lua, to make this self-contained.
-- The documentation is at:
-- (find-dn5 "eoo.lua" "test-eoo")
-- (find-dn5 "eoo.lua" "box-diagram")
Class = {
type = "Class",
__call = function (class, o) return setmetatable(o, class) end,
}
setmetatable(Class, Class)
otype = function (o) -- works like type, except on my "objects"
local mt = getmetatable(o)
return mt and mt.type or type(o)
end
-- end of eoo.lua
--
-- And here's "mapconcat", from my init file:
-- (find-angg "LUA/lua50init.lua" "map" "mapconcat")
-- (find-lua51manualw3m "#pdf-table.concat")
map = function (f, A, i, j)
local B = {}
for k=(i or 1),(j or #A) do table.insert(B, (f(A[k]))) end
return B
end
mapconcat = function (f, A, sep, i, j)
return table.concat(map(f, A, i, j), sep)
end
id = function (...) return ... end
sorted = function (T, lt) table.sort(T, lt); return T end
keys = function (T)
local ks = {}
for k,_ in pairs(T) do table.insert(ks, k) end
return ks
end
min = function (a, b) return a < b and a or b end
max = function (a, b) return a < b and b or a end
-- end of mapconcat
-- «Expr» (to ".Expr")
-- «expr:infix» (to ".expr:infix")
Expr = Class {
type = "Expr",
__index = {
infix = function (e, b)
local op, e1, e2, e3 = e[0], e[1], e[2], e[3]
local t, str
if op == "v" then t, str = 200, e[1]
elseif op == "n" then t, str = 200, tostring(e[1])
elseif op == "b" then t, str = 200, e[1] and "T" or "F"
elseif op == "u-" then t, str = 9, "-"..e1:infix(100)
elseif op == "*" then t, str = 8, e1:infix(7).."*"..e2:infix(8)
elseif op == "/" then t, str = 8, e1:infix(7).."*"..e2:infix(8)
elseif op == "+" then t, str = 7, e1:infix(6).."+"..e2:infix(7)
elseif op == "-" then t, str = 7, e1:infix(6).."-"..e2:infix(7)
elseif op == "==" then t, str = 6, e1:infix(6).." == "..e2:infix(6)
elseif op == "<=" then t, str = 6, e1:infix(6).." <= "..e2:infix(6)
elseif op == ">=" then t, str = 6, e1:infix(6).." >= "..e2:infix(6)
elseif op == "<" then t, str = 6, e1:infix(6).." < " ..e2:infix(6)
elseif op == ">" then t, str = 6, e1:infix(6).." > " ..e2:infix(6)
elseif op == "!=" then t, str = 6, e1:infix(6).." != "..e2:infix(6)
elseif op == "nt" then t, str = 5, "not "..e1:infix(4)
elseif op == "&" then t, str = 4, e1:infix(3).." & " ..e2:infix(4)
elseif op == "|" then t, str = 3, e1:infix(2).." | " ..e2:infix(3)
elseif op == "->" then t, str = 2, e1:infix(2).." -> "..e2:infix(2)
elseif op == "()" then t, str = 200, "("..e:infixs()..")"
elseif op == "{}" then t, str = 200, "{"..e:infixs().."}"
elseif op == "Fa" then t, str = 1, "Fa "..e1:infix().." in "..
e2:infix()..". "..e3:infix()
elseif op == "Ex" then t, str = 1, "Ex "..e1:infix().." in "..
e2:infix()..". "..e3:infix()
elseif op == "Dg" then str, t = e1:infix()
else str, t = e:infix_other(b) -- all extensions
end
if b and t <= b then str = "("..str..")" end
return str, t
end,
infixs = function (e, sep, i, j)
return mapconcat(e.infix, e, (sep or ", "), i, j)
end,
},
__tostring = function (e) return (e:infix()) end,
__add = function (e1, e2) return Expr {[0]="+", e1, e2} end,
__sub = function (e1, e2) return Expr {[0]="-", e1, e2} end,
__mul = function (e1, e2) return Expr {[0]="*", e1, e2} end,
__div = function (e1, e2) return Expr {[0]="/", e1, e2} end,
__unm = function (e1) return Expr {[0]="u-", e1} end,
}
-- Constructors
-- «constructors» (to ".constructors")
Num = function (n) return Expr {[0]="n", n} end
Var = function (s) return Expr {[0]="v", s} end
Bool = function (b) return Expr {[0]="b", b} end
True = Bool(true)
False = Bool(false)
Unm = function (e1) return - e1 end
Mul = function (e1, e2) return e1 * e2 end
Div = function (e1, e2) return e1 / e2 end
Add = function (e1, e2) return e1 + e2 end
Sub = function (e1, e2) return e1 - e2 end
Eq = function (e1, e2) return Expr {[0]="==", e1, e2} end
Lt = function (e1, e2) return Expr {[0]="<", e1, e2} end
Le = function (e1, e2) return Expr {[0]="<=", e1, e2} end
Ge = function (e1, e2) return Expr {[0]=">=", e1, e2} end
Gt = function (e1, e2) return Expr {[0]="<", e1, e2} end
Neq = function (e1, e2) return Expr {[0]="!=", e1, e2} end
Not = function (e1) return Expr {[0]="nt", e1} end
And = function (e1, e2) return Expr {[0]="&", e1, e2} end
Or = function (e1, e2) return Expr {[0]="|", e1, e2} end
Imp = function (e1, e2) return Expr {[0]="->", e1, e2} end
Tuple = function (...) return Expr {[0]="()", ...} end
Set = function (...) return Expr {[0]="{}", ...} end
Fa = function (e1, e2, e3) return Expr {[0]="Fa", e1, e2, e3} end
Ex = function (e1, e2, e3) return Expr {[0]="Ex", e1, e2, e3} end
-- «expr:tolisp» (to ".expr:tolisp")
-- A Lisp-ish representation.
-- Note that our Exprs use 0-based arrays, not cons cells.
-- (find-elnode "Cons Cell Type")
-- (find-elnode "Box Diagrams")
tolisp = function (e)
if type(e) == "number" then return e
elseif type(e) == "string" then return "\""..e.."\""
elseif otype(e) == "Expr" then
return "("..tolisp(e[0]).." "..mapconcat(tolisp, e, " ")..")"
else return "<"..tostring(e)..">"
end
end
Expr.__index.tolisp = function (e) return tolisp(e) end
-- «expr:eval» (to ".expr:eval")
-- Evaluation.
-- To avoid making the code above too big we inject new methods into
-- Expr, using a low-level syntax for that:
-- Expr.__index.newmethod = function (e, a, b, c) ... end
etype = function (e) return otype(e) == "Expr" and e[0] end
Expr.__index.neval = function (e)
local ee = e:eval()
if etype(ee) == "n" then return ee[1] end
error("Not a number: "..tostring(ee))
end
Expr.__index.beval = function (e)
local ee = e:eval()
if etype(ee) == "b" then return ee[1] end
error("Not a boolean: "..tostring(ee))
end
Expr.__index.seval = function (e)
local ee = e:eval()
if etype(ee) == "{}" then return ee end
error("Not a set: "..tostring(ee))
end
Expr.__index.eval_components = function (e)
local A = map(e.eval, e)
A[0] = e[0]
return Expr(A)
end
_and = function (P, Q) return P and Q end
_or = function (P, Q) return P or Q end
_imp = function (P, Q) return (not P) or Q end
context = {}
Expr.__index.eval = function (e)
local op, e1, e2, e3 = e[0], e[1], e[2], e[3]
if op == "n" then return e
elseif op == "b" then return e
elseif op == "v" then return context[e1] or error("Undef: "..e1)
elseif op == "u-" then return Num(- e1:neval())
elseif op == "*" then return Num(e1:neval() * e2:neval())
elseif op == "/" then return Num(e1:neval() / e2:neval())
elseif op == "+" then return Num(e1:neval() + e2:neval())
elseif op == "-" then return Num(e1:neval() - e2:neval())
elseif op == "==" then return Bool(e1:neval() == e2:neval())
elseif op == "<=" then return Bool(e1:neval() <= e2:neval())
elseif op == ">=" then return Bool(e1:neval() >= e2:neval())
elseif op == "<" then return Bool(e1:neval() < e2:neval())
elseif op == ">" then return Bool(e1:neval() > e2:neval())
elseif op == "!=" then return Bool(e1:neval() ~= e2:neval())
elseif op == "nt" then return Bool(not e1:beval())
elseif op == "&" then return Bool(_and(e1:beval(), e2:beval()))
elseif op == "|" then return Bool(_or (e1:beval(), e2:beval()))
elseif op == "->" then return Bool(_imp(e1:beval(), e2:beval()))
elseif op == "{}" then return e:eval_components()
elseif op == "()" then return e:eval_components()
elseif op == "Fa" then return Bool(e1:_fold(true, _and, _beval, e2, e3))
elseif op == "Ex" then return Bool(e1:_fold(false, _or, _beval, e2, e3))
elseif op == "Dg" then return e1:DbgEval() -- defined elsewhere
else return e:eval_other() -- all extensions
end
end
-- «eval-quantifiers» (to ".eval-quantifiers")
-- The evaluation code for "Fa" and "Ex" calls "_fold" and "_beval",
-- that are defined below.
Expr.__index.varname = function (e)
if etype(e) == "v" then return e[1] end
error("Not a variable: "..tostring(ee))
end
Expr.__index.as = function (var, value, expr)
local vname = var:varname()
local oldvalue = context[vname]
context[vname] = value
local result = expr:eval()
context[vname] = oldvalue
return result
end
Expr.__index._fold = function (var, r, op, normalize, set, expr)
for _,value in ipairs(set) do
r = op(r, normalize(var:as(value, expr)))
end
return r
end
_beval = function (e) return e:beval() end
-- «expr:print» (to ".expr:print")
-- Some methods for printing
Expr.__index.print = function (e) print(e); return e end
Expr.__index.lprint = function (e) print(e:tolisp()); return e end
Expr.__index.rprint = function (e) print(e:torect()); return e end
Expr.__index.peval = function (e)
local result = e:eval()
print(tostring(e).." --> "..tostring(result))
return result
end
Expr.__index.preval = function (e)
print(tostring(e))
print(torect(e))
print()
local result = e:eval()
print(" --> "..tostring(result))
print()
return result
end
-- Obsolete?
Expr.__index.When = function (var, value, expr)
return "When " ..tostring(var)..
"=" ..tostring(value)..
": " ..tostring(expr)..
" --> "..tostring(var:as(value, expr))
end
Expr.__index.Whens = function (var, set, expr)
for _,value in ipairs(set) do
print(var:When(value, expr))
end
end
-- «expr:Dbg» (to ".expr:Dbg")
-- Support for debugging (verbose subexpressions)
Expr.__index.Dbg = function (e1) return Expr {[0]="Dg", e1} end
Expr.__index.DbgEval = function (expr)
local result = expr:eval()
print(contextstring()..tostring(expr).." --> "..tostring(result))
return result
end
contextstring = function ()
local sk = sorted(keys(context))
local f = function (name) return name.."="..tostring(context[name]) end
return "["..mapconcat(f, sk, " ").."] "
end
-- Convenience: some expressions (variables and numeric constants)
-- that I use in tests
_0 = Num(0)
_1 = Num(1)
_2 = Num(2)
_3 = Num(3)
_4 = Num(4)
_5 = Num(5)
a = Var "a"
b = Var "b"
c = Var "c"
d = Var "d"
x = Var "x"
y = Var "y"
-- «Rect» (to ".Rect")
-- Rectangles (for trees)
-- (find-luamanualw3m "#pdf-string.rep")
strrep = function (str, n) return string.rep(str, max(0, n)) end
strpad = function (str, n, char) return str..strrep(char or " ", n-#str) end
torect = function (o)
if otype(o) == "Rect" then return o end
if otype(o) == "Expr" then return o:torect() end
o = tostring(o)
return Rect {w=#o, o}
end
copy = function (A)
local B = {}
for k,v in pairs(A) do B[k] = v end
setmetatable(B, getmetatable(A))
return B
end
Rect = Class {
type = "Rect",
__index = {
copy = function (rect) return copy(rect) end,
get = function (rect, y) return rect[y] or "" end,
getp = function (rect, y, c) return strpad(rect:get(y), rect.w, c) end,
adjw = function (rect, y) rect.w = max(rect.w, #rect:get(y)) end,
set = function (rect, y, str, fill)
for i=#rect+1,y-1 do rect[i] = fill or "" end
rect[y] = str
rect:adjw(y)
return rect
end,
lower = function (rect, n, ...)
for i=1,(n or 1) do table.insert(rect, 1, "") end
for y,str in ipairs({...}) do rect:set(y, str) end
return rect
end,
under = function (rect, str) return rect:copy():lower(2, str, "|") end,
under_ = function (rect, str, n)
return rect:under(strpad(str, rect.w+(n or 2), "_"))
end,
},
__tostring = function (rect) return mapconcat(id, rect, "\n") end,
__concat = function (r1, r2)
r1 = torect(r1)
r2 = torect(r2)
r3 = Rect {w=0}
for y=1,max(#r1, #r2) do r3:set(y, r1:getp(y, " ")..r2:get(y)) end
return r3
end,
}
rectconcat = function (op, rects)
if #rects == 1 then return torect(rects[1]):under(op) end
local out = torect(rects[1]):under_(op)
for i=2,#rects-1 do out = out..torect(rects[i]):under_(".") end
return out..torect(rects[#rects]):under(".")
end
Expr.__index.torect = function (e)
local op, e1 = e[0], e[1]
if op == "n" then return torect(e1) end
if op == "v" then return torect(e1) end
if op == "b" then return torect(e:infix()) end
-- local subrects = map(Expr.__index.torect, e)
local subrects = map(torect, e)
return rectconcat (op, subrects)
end
--[[
-- Low-level tests for Rect
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "gabriela.lua"
r = Rect {w=3, "a", "ab", "abc"}
= r
= r..r
= r.."foo"
= "--"..r
= rectconcat("+", {2, 3})
= rectconcat("+", {2, 34, 5})
= r:under_("Fa")..r:under(".")
= r:under_("Fa")
= r:under(".")
-- «Rect-test» (to ".Rect-test")
-- High-level tests for Rect
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "gabriela.lua"
= (_2 * _3 + _4 * - _5):torect()
comparison = Le(_2*x, y+_3)
ex_expression = Ex(y, Set(_3, _4, _5), comparison)
fa_expression = Fa(x, Set(_2, _3, _4), ex_expression)
= fa_expression
= tolisp(fa_expression)
PP(fa_expression)
= fa_expression:torect()
e = fa_expression
= "eval( "..e:torect().." ) --> "..e:eval():torect()
-- Output:
-- eval( Fa_.________. ) --> T
-- | | |
-- x {}_.__. Ex_.________.
-- | | | | | |
-- 2 3 4 y {}_.__. <=____.
-- | | | | |
-- 3 4 5 *__. +__.
-- | | | |
-- 2 x y 3
--]]
--[[
-- Tests
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
-- Some ways of printing an expression and its result
dofile "gabriela.lua"
A = Set(_2, _3, _5)
B = Set(_2, _3)
expr = Le(a*a, Num(10))
a:Whens(A, expr)
a:Whens(B, expr)
Fa(a, A, expr):peval()
Fa(a, B, expr):peval()
= _2 * _3 + _4 * _5
(_2 * _3 + _4 * _5):peval()
= (_2 * _3):Dbg() + (_4 * _5):Dbg()
((_2 * _3):Dbg() + (_4 * _5):Dbg()):peval()
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
-- The internal representation vs. the infix representation
dofile "gabriela.lua"
PP(2)
PP(_2, otype(_2))
= _2 + _3
PP(_2 + _3)
(_2 + _3):lprint()
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
-- Basic evaluation
dofile "gabriela.lua"
= _2 + _3
= (_2 + _3):eval()
= (_2 + - _3):eval()
PP((_2 + - _3):eval())
= Le(_2, _3)
= Le(_2, _3):eval()
= Ge(_2, _3):eval()
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "gabriela.lua"
= Ge(a+(b*(c-d)), a)
= Ge(a, a+(b*(c-d)))
PP(Ge(a, a+(b*(c-d))))
(Ge(a, a+(b*(c-d)))):lprint()
= Set(a*a, b, c, Tuple(a, b))
(Set(a*a, b, c, Tuple(a, b))):lprint()
= Fa(a, Set(b, c), Le(a, d))
(Fa(a, Set(b, c), Le(a, d))):lprint()
e = Le(_2*a, b+_3)
ee = Ex(b, Set(_3, _4, _5), e)
eee = Fa(a, Set(_2, _3, _4), ee)
= And(ee, ee)
= And(e, eee)
= _2:eval()
= _2 + _3
= (_2 + _3):eval()
= (_2 * - _3):eval()
PP(_2)
PP(- _3)
PP( _3 :neval())
PP((- _3):neval())
-- «test-infix» (to ".test-infix")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
-- Tests for the parenthesisation algorithm (using "pyramids")
dofile "gabriela.lua"
= And(And(a, b), And(c, d))
= Or (Or (a, b), Or (c, d))
= Imp(Imp(a, b), Imp(c, d))
pyr = function (F) print(F(F(a, b), F(c, d))) end
pyr2 = function (F, G) print(F(G(a, b), G(c, d)), G(F(a, b), F(c, d))) end
pyrs = function (T)
for i=1,#T-1 do pyr(T[i]); pyr2(T[i], T[i+1]) end
pyr(T[#T])
end
pyr(And)
pyr(Or)
pyr(Imp)
pyr2(And, Or)
pyr2(And, Not)
pyrs {
Unm, Mul, Div, Add, Sub,
Eq, Lt, Le, Ge, Gt,
Not, And, Or, Imp,
}
-- «test-context» (to ".test-context")
-- This is obsolete, see:
-- (find-dn5 "gabriela-app.lua")
-- (find-dn5 "gabriela-app.lua" "contexts-test")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
-- Printing the context
dofile "gabriela.lua"
comparison = Le(_2*x, y+_3)
comparison = Le(_2*x, y+_3):Dbg()
ex_expression = Ex(y, Set(_3, _4, _5), comparison)
ex_expression = Ex(y, Set(_3, _4, _5), comparison):Dbg()
fa_expression = Fa(x, Set(_2, _3, _4), ex_expression)
fa_expression:peval()
-- [x=2 y=3] 2*x <= y+3 --> T
-- [x=2 y=4] 2*x <= y+3 --> T
-- [x=2 y=5] 2*x <= y+3 --> T
-- [x=2] Ex y in {3, 4, 5}. 2*x <= y+3 --> T
-- [x=3 y=3] 2*x <= y+3 --> T
-- [x=3 y=4] 2*x <= y+3 --> T
-- [x=3 y=5] 2*x <= y+3 --> T
-- [x=3] Ex y in {3, 4, 5}. 2*x <= y+3 --> T
-- [x=4 y=3] 2*x <= y+3 --> F
-- [x=4 y=4] 2*x <= y+3 --> F
-- [x=4 y=5] 2*x <= y+3 --> T
-- [x=4] Ex y in {3, 4, 5}. 2*x <= y+3 --> T
-- Fa x in {2, 3, 4}. Ex y in {3, 4, 5}. 2*x <= y+3 --> T
--]]
-- Local Variables:
-- coding: raw-text-unix
-- ee-anchor-format: "«%s»"
-- End: