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: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
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)
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]
-- 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 {
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:
```