kdrag.kernel

The kernel hold core proof datatypes and core inference rules. By and large, all proofs must flow through this module.

Module Attributes

defns

defn holds definitional axioms for function symbols.

Functions

`FreshVar`(prefix, sort)	Generate a fresh variable.
`Inductive`(name)	Declare datatypes with auto generated induction principles.
`andI`(pfs)	Prove an and from two kd.Proofs of its conjuncts.
`axiom`(thm[, by])	Assert an axiom.
`compose`(ab, bc)	Compose two implications.
`consider`(x)	The purpose of this is to seed the solver with interesting terms.
`define`(name, args, body[, lift_lambda])	Define a non recursive definition.
`define_fix`(name, args, retsort, fix_lam)	Define a recursive definition.
`einstan`(thm)	Skolemize an existential quantifier.
`forget`(ts, pf)	"Forget" a term using existentials.
`forget2`(ts, thm)	"Forget" a term using existentials.
`free_in`(vs, t)	Returns True if none of the variables in vs exist unbound in t.
`fresh_const`(q)	Generate fresh constants of same sort as quantifier.
`generalize`(vs, pf)	Generalize a theorem with respect to a list of schema variables.
`herb`(thm)	Herbrandize a theorem.
`induct_inductive`(x, P)	Build a basic induction principle for an algebraic datatype
`instan`(ts, pf)	Instantiate a universally quantified formula.
`instan2`(ts, thm)	Instantiate a universally quantified formula forall xs, P(xs) -> P(ts) This is forall elimination
`is_defined`(x)	Determined if expression head is in definitions.
`is_fresh_var`(v)	Check if a variable is a schema variable.
`is_proof`(p)
`modus`(ab, a)	Modus ponens for implies and equality.
`prove`(thm[, by, admit, timeout, dump, solver])	Prove a theorem using a list of previously proved lemmas.
`rename_vars`(t, vs)
`skolem`(pf)	Skolemize an existential quantifier.
`subst`(t, eqs)	Substitute using equality proofs
`substitute_fresh_vars`(pf, *subst)	Substitute schematic variables in a theorem.
`unfold`(e, decls)	Unfold function definitions in an expression.

Classes

`Defn`(name, args, body, ax, subst_funs_body)	A record storing definition.
`Judgement`()	Judgements should be constructed by smart constructors.
`Proof`(thm, reason[, admit])	It is unlikely that users should be accessing the Proof constructor directly.

Exceptions

LemmaError

class kdrag.kernel.Defn(name: str, args: list[ExprRef], body: ExprRef, ax: Proof, subst_funs_body: ExprRef)

Bases: object

A record storing definition. It is useful to record definitions as special axioms because we often must unfold them.

Parameters:

name (str)
args (list[ExprRef])
body (ExprRef)
ax (Proof)
subst_funs_body (ExprRef)

args: list[ExprRef]

ax: Proof

body: ExprRef

name: str

subst_funs_body: ExprRef

kdrag.kernel.FreshVar(prefix: str, sort: SortRef) → ExprRef

Generate a fresh variable. This is distinguished from FreshConst by the fact that it has freshness evidence. This is intended to be used for constants that represent arbitrary terms (implicitly universally quantified). For example, axioms like c_fresh = t should never be asserted about bare FreshVars as they imply a probably inconsistent axiom, whereas asserting such an axiom about FreshConst is ok, effectively defining a new rigid constant.

>>> FreshVar("x", smt.IntSort()).fresh_evidence
_FreshVarEvidence(v=x!...)

Parameters:

prefix (str)
sort (SortRef)

Return type:

ExprRef

kdrag.kernel.Inductive(name: str) → Datatype

Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype

>>> Nat = Inductive("Nat")
>>> Nat.declare("zero")
>>> Nat.declare("succ", ("pred", Nat))
>>> Nat = Nat.create()
>>> Nat.succ(Nat.zero)
succ(zero)

Parameters:: name (str)
Return type:: Datatype

class kdrag.kernel.Judgement

Bases: object

Judgements should be constructed by smart constructors. Having an object of supertype judgement represents having shown some kind of truth. Judgements are the things that go above and below inference lines in a proof system. Don’t worry about it. It is just nice to have a name for the concept.

See: - https://en.wikipedia.org/wiki/Judgment_(mathematical_logic) - https://mathoverflow.net/questions/254518/what-exactly-is-a-judgement - https://ncatlab.org/nlab/show/judgment

exception kdrag.kernel.LemmaError

Bases: Exception

add_note(object, /): Exception.add_note(note) – add a note to the exception

args

with_traceback(object, /): Exception.with_traceback(tb) – set self.__traceback__ to tb and return self.

class kdrag.kernel.Proof(thm: BoolRef, reason: list[Any], admit: bool = False)

Bases: Judgement

It is unlikely that users should be accessing the Proof constructor directly. This is not ironclad. If you really want the Proof constructor, I can’t stop you.

Parameters:

thm (BoolRef)
reason (list[Any])
admit (bool)

__call__(*args: ExprRef | Proof)

>>> x,y = smt.Ints("x y")
>>> p = prove(smt.ForAll([y], smt.ForAll([x], x >= x - 1)))
>>> p(x)
|= ForAll(x, x >= x - 1)
>>> p(x, smt.IntVal(7))
|= 7 >= 7 - 1

>>> a,b,c = smt.Bools("a b c")
>>> ab = prove(smt.Implies(a,smt.Implies(a, a)))
>>> a = axiom(a)
>>> ab(a)
|= Implies(a, a)
>>> ab(a,a)
|= a

Parameters:: args (ExprRef | Proof)

admit: bool = False

forall(fresh_vars: list[ExprRef]) → Proof

Generalize a proof involved schematic variables generated by FreshVar

>>> x = FreshVar("x", smt.IntSort())
>>> prove(x + 1 > x).forall([x])
|= ForAll(x!..., x!... + 1 > x!...)

Parameters:: fresh_vars (list[ExprRef])
Return type:: Proof

reason: list[Any]

thm: BoolRef

kdrag.kernel.andI(pfs: Sequence[Proof]) → Proof

Prove an and from two kd.Proofs of its conjuncts.

>>> a, b = smt.Bools("a b")
>>> pa = kd.axiom(smt.Implies(True, a))
>>> pb = kd.axiom(smt.Implies(True, b))
>>> andI([pa, pb, pb])
|= Implies(True, And(a, b, b))

Parameters:: pfs (Sequence[Proof])
Return type:: Proof

kdrag.kernel.axiom(thm: BoolRef, by=['axiom']) → Proof

Assert an axiom.

Axioms are necessary and useful. But you must use great care.

Parameters:

thm (BoolRef) – The axiom to assert.
by – A python object explaining why the axiom should exist. Often a string explaining the axiom.

Return type:

Proof

kdrag.kernel.compose(ab: Proof, bc: Proof) → Proof

Compose two implications. Useful for chaining implications.

>>> a,b,c = smt.Bools("a b c")
>>> ab = axiom(smt.Implies(a, b))
>>> bc = axiom(smt.Implies(b, c))
>>> compose(ab, bc)
|= Implies(a, c)

Parameters:

ab (Proof)
bc (Proof)

Return type:

Proof

kdrag.kernel.consider(x: ExprRef) → Proof

The purpose of this is to seed the solver with interesting terms. Axiom schema. We may give a fresh name to any constant. An “anonymous” form of define. Pointing out the interesting terms is sometimes the essence of a proof.

Parameters:: x (ExprRef)
Return type:: Proof

kdrag.kernel.define(name: str, args: list[ExprRef], body: ExprRef, lift_lambda=False) → FuncDeclRef

Define a non recursive definition. Useful for shorthand and abstraction. Does not currently defend against ill formed definitions. TODO: Check for bad circularity, record dependencies

Parameters:

name (str) – The name of the term to define.
args (list[ExprRef]) – The arguments of the term.
defn – The definition of the term.
body (ExprRef)

Returns:

A tuple of the defined term and the proof of the definition.

Return type:

tuple[smt.FuncDeclRef, Proof]

kdrag.kernel.define_fix(name: str, args: list[ExprRef], retsort, fix_lam) → FuncDeclRef

Define a recursive definition.

Parameters:

name (str)
args (list[ExprRef])

Return type:

FuncDeclRef

kdrag.kernel.defns: dict[FuncDeclRef, Defn] = {abelian: Defn(name='abelian', args=[], body=ForAll([x!478, y!479], mul(x!478, y!479) == mul(y!479, x!478)), ax=|= abelian == (ForAll([x!478, y!479], mul(x!478, y!479) == mul(y!479, x!478))), subst_funs_body=ForAll([x!478, y!479], mul(x!478, y!479) == mul(y!479, x!478))), absR: Defn(name='absR', args=[x], body=If(x >= 0, x, -x), ax=|= ForAll(x, absR(x) == If(x >= 0, x, -x)), subst_funs_body=If(Var(0) >= 0, Var(0), -Var(0))), add: Defn(name='add', args=[x, y], body=If(is(Z, x), y, S(add(pred(x), y))), ax=|= ForAll([x, y], add(x, y) == If(is(Z, x), y, S(add(pred(x), y)))), subst_funs_body=If(is(Z, Var(0)), Var(1), S(add(pred(Var(0)), Var(1))))), add: Defn(name='add', args=[f, g], body=Lambda(x, f[x] + g[x]), ax=|= ForAll([f, g], add(f, g) == (Lambda(x, f[x] + g[x]))), subst_funs_body=Lambda(x, Var(1)[x] + Var(2)[x])), add: Defn(name='add', args=[a, b], body=Lambda(i, a[i] + b[i]), ax=|= ForAll([a, b], add(a, b) == (Lambda(i, a[i] + b[i]))), subst_funs_body=Lambda(i, Var(1)[i] + Var(2)[i])), add: Defn(name='add', args=[x, y], body=x + y, ax=|= ForAll([x, y], add(x, y) == x + y), subst_funs_body=Var(0) + Var(1)), add: Defn(name='add', args=[z1, z2], body=C(re(z1) + re(z2), im(z1) + im(z2)), ax=|= ForAll([z1, z2], add(z1, z2) == C(re(z1) + re(z2), im(z1) + im(z2))), subst_funs_body=C(re(Var(0)) + re(Var(1)), im(Var(0)) + im(Var(1)))), add: Defn(name='add', args=[x, y], body=If(And(is(Real, x), is(Real, y)), Real(val(x) + val(y)), If(And(is(Inf, x), Not(is(NegInf, y))), Inf, If(And(Not(is(NegInf, x)), is(Inf, y)), Inf, If(And(is(NegInf, x), Not(is(Inf, y))), NegInf, If(And(Not(is(Inf, x)), is(NegInf, y)), NegInf, add_undef(x, y)))))), ax=|= ForAll([x, y], add(x, y) == If(And(is(Real, x), is(Real, y)), Real(val(x) + val(y)), If(And(is(Inf, x), Not(is(NegInf, y))), Inf, If(And(Not(is(NegInf, x)), is(Inf, y)), Inf, If(And(is(NegInf, x), Not(is(Inf, y))), NegInf, If(And(Not(is(Inf, x)), is(NegInf, y)), NegInf, add_undef(x, y))))))), subst_funs_body=If(And(is(Real, Var(0)), is(Real, Var(1))), Real(val(Var(0)) + val(Var(1))), If(And(is(Inf, Var(0)), Not(is(NegInf, Var(1)))), Inf, If(And(Not(is(NegInf, Var(0))), is(Inf, Var(1))), Inf, If(And(is(NegInf, Var(0)), Not(is(Inf, Var(1)))), NegInf, If(And(Not(is(Inf, Var(0))), is(NegInf, Var(1))), NegInf, add_undef(Var(0), Var(1)))))))), add: Defn(name='add', args=[u, v], body=Vec2(x(u) + x(v), y(u) + y(v)), ax=|= ForAll([u, v], add(u, v) == Vec2(x(u) + x(v), y(u) + y(v))), subst_funs_body=Vec2(x(Var(0)) + x(Var(1)), y(Var(0)) + y(Var(1)))), add: Defn(name='add', args=[u, v], body=Vec3(x0(u) + x0(v), x1(u) + x1(v), x2(u) + x2(v)), ax=|= ForAll([u, v], add(u, v) == Vec3(x0(u) + x0(v), x1(u) + x1(v), x2(u) + x2(v))), subst_funs_body=Vec3(x0(Var(0)) + x0(Var(1)), x1(Var(0)) + x1(Var(1)), x2(Var(0)) + x2(Var(1)))), add: Defn(name='add', args=[i, j], body=Interval(lo(i) + lo(j), hi(i) + hi(j)), ax=|= ForAll([i, j], add(i, j) == Interval(lo(i) + lo(j), hi(i) + hi(j))), subst_funs_body=Interval(lo(Var(0)) + lo(Var(1)), hi(Var(0)) + hi(Var(1)))), add: Defn(name='add', args=[u, v], body=If(shape(u) == shape(v), NDArray(shape(u), Lambda(k, data(u)[k] + data(v)[k])), add_undef(u, v)), ax=|= ForAll([u, v], add(u, v) == If(shape(u) == shape(v), NDArray(shape(u), Lambda(k, data(u)[k] + data(v)[k])), add_undef(u, v))), subst_funs_body=If(shape(Var(0)) == shape(Var(1)), NDArray(shape(Var(0)), Lambda(k, data(Var(1))[k] + data(Var(2))[k])), add_undef(Var(0), Var(1)))), add_defined: Defn(name='add_defined', args=[x, y], body=Or(And(is(Real, x), is(Real, y)), And(is(Inf, x), Not(is(NegInf, y))), And(Not(is(NegInf, x)), is(Inf, y)), And(is(NegInf, x), Not(is(Inf, y))), And(Not(is(Inf, x)), is(NegInf, y))), ax=|= ForAll([x, y], add_defined(x, y) == Or(And(is(Real, x), is(Real, y)), And(is(Inf, x), Not(is(NegInf, y))), And(Not(is(NegInf, x)), is(Inf, y)), And(is(NegInf, x), Not(is(Inf, y))), And(Not(is(Inf, x)), is(NegInf, y)))), subst_funs_body=Or(And(is(Real, Var(0)), is(Real, Var(1))), And(is(Inf, Var(0)), Not(is(NegInf, Var(1)))), And(Not(is(NegInf, Var(0))), is(Inf, Var(1))), And(is(NegInf, Var(0)), Not(is(Inf, Var(1)))), And(Not(is(Inf, Var(0))), is(NegInf, Var(1))))), ball: Defn(name='ball', args=[x!706, r!709], body=Lambda(y!710, absR(y!710 - x!706) < r!709), ax=|= ForAll([x!706, r!709], ball(x!706, r!709) == (Lambda(y!710, absR(y!710 - x!706) < r!709))), subst_funs_body=Lambda(y!710, absR(y!710 - Var(1)) < Var(2))), cauchy_mod: Defn(name='cauchy_mod', args=[a, mod], body=ForAll(eps, Implies(eps > 0, ForAll([m, k], Implies(And(m > mod[eps], k > mod[eps]), absR(a[m] - a[k]) < eps)))), ax=|= ForAll([a, mod], cauchy_mod(a, mod) == (ForAll(eps, Implies(eps > 0, ForAll([m, k], Implies(And(m > mod[eps], k > mod[eps]), absR(a[m] - a[k]) < eps)))))), subst_funs_body=ForAll(eps, Implies(eps > 0, ForAll([m, k], Implies(And(m > Var(4)[eps], k > Var(4)[eps]), absR(Var(3)[m] - Var(3)[k]) < eps))))), circle: Defn(name='circle', args=[c, r], body=Lambda(p, norm2(sub(p, c)) == r*r), ax=|= ForAll([c, r], circle(c, r) == (Lambda(p, norm2(sub(p, c)) == r*r))), subst_funs_body=Lambda(p, norm2(sub(p, Var(1))) == Var(2)*Var(2))), closed: Defn(name='closed', args=[A], body=open(complement(A)), ax=|= ForAll(A, closed(A) == open(complement(A))), subst_funs_body=open(complement(Var(0)))), comp: Defn(name='comp', args=[f, g], body=Lambda(x, f[g[x]]), ax=|= ForAll([f, g], comp(f, g) == (Lambda(x, f[g[x]]))), subst_funs_body=Lambda(x, Var(1)[Var(2)[x]])), conj: Defn(name='conj', args=[z], body=C(re(z), -im(z)), ax=|= ForAll(z, conj(z) == C(re(z), -im(z))), subst_funs_body=C(re(Var(0)), -im(Var(0)))), const: Defn(name='const', args=[x], body=K(Real, x), ax=|= ForAll(x, const(x) == K(Real, x)), subst_funs_body=K(Real, Var(0))), cont_at: Defn(name='cont_at', args=[f, x], body=ForAll(eps, Implies(eps > 0, Exists(delta, And(delta > 0, ForAll(y, Implies(absR(x - y) < delta, absR(f[x] - f[y]) < eps)))))), ax=|= ForAll([f, x], cont_at(f, x) == (ForAll(eps, Implies(eps > 0, Exists(delta, And(delta > 0, ForAll(y, Implies(absR(x - y) < delta, absR(f[x] - f[y]) < eps)))))))), subst_funs_body=ForAll(eps, Implies(eps > 0, Exists(delta, And(delta > 0, ForAll(y, Implies(absR(Var(4) - y) < delta, absR(Var(3)[Var(4)] - Var(3)[y]) < eps))))))), cross: Defn(name='cross', args=[u, v], body=Vec3(x1(u)*x2(v) - x2(u)*x1(v), x2(u)*x0(v) - x0(u)*x2(v), x0(u)*x1(v) - x1(u)*x0(v)), ax=|= ForAll([u, v], cross(u, v) == Vec3(x1(u)*x2(v) - x2(u)*x1(v), x2(u)*x0(v) - x0(u)*x2(v), x0(u)*x1(v) - x1(u)*x0(v))), subst_funs_body=Vec3(x1(Var(0))*x2(Var(1)) - x2(Var(0))*x1(Var(1)), x2(Var(0))*x0(Var(1)) - x0(Var(0))*x2(Var(1)), x0(Var(0))*x1(Var(1)) - x1(Var(0))*x0(Var(1)))), delta: Defn(name='delta', args=[n, x], body=Lambda(n, If(n == 0, x, 0)), ax=|= ForAll([n, x], delta(n, x) == (Lambda(n, If(n == 0, x, 0)))), subst_funs_body=Lambda(n, If(n == 0, Var(2), 0))), diff_at: Defn(name='diff_at', args=[f, x], body=Exists(y, has_diff_at(f, x, y)), ax=|= ForAll([f, x], diff_at(f, x) == (Exists(y, has_diff_at(f, x, y)))), subst_funs_body=Exists(y, has_diff_at(Var(1), Var(2), y))), dist: Defn(name='dist', args=[x!706, y!707], body=absR(x!706 - y!707), ax=|= ForAll([x!706, y!707], dist(x!706, y!707) == absR(x!706 - y!707)), subst_funs_body=absR(Var(0) - Var(1))), dist: Defn(name='dist', args=[u, v], body=sqrt(norm2(sub(u, v))), ax=|= ForAll([u, v], dist(u, v) == sqrt(norm2(sub(u, v)))), subst_funs_body=sqrt(norm2(sub(Var(0), Var(1))))), div_: Defn(name='div_', args=[f, g], body=Lambda(x, f[x]/g[x]), ax=|= ForAll([f, g], div_(f, g) == (Lambda(x, f[x]/g[x]))), subst_funs_body=Lambda(x, Var(1)[x]/Var(2)[x])), div_: Defn(name='div_', args=[a, b], body=Lambda(i, a[i]/b[i]), ax=|= ForAll([a, b], div_(a, b) == (Lambda(i, a[i]/b[i]))), subst_funs_body=Lambda(i, Var(1)[i]/Var(2)[i])), div_: Defn(name='div_', args=[z1, z2], body=C((re(z1)*re(z2) + im(z1)*im(z2))/(re(z2)**2 + im(z2)**2), (im(z1)*re(z2) - re(z1)*im(z2))/(re(z2)**2 + im(z2)**2)), ax=|= ForAll([z1, z2], div_(z1, z2) == C((re(z1)*re(z2) + im(z1)*im(z2))/ (re(z2)**2 + im(z2)**2), (im(z1)*re(z2) - re(z1)*im(z2))/ (re(z2)**2 + im(z2)**2))), subst_funs_body=C((re(Var(0))*re(Var(1)) + im(Var(0))*im(Var(1)))/ (re(Var(1))**2 + im(Var(1))**2), (im(Var(0))*re(Var(1)) - re(Var(0))*im(Var(1)))/ (re(Var(1))**2 + im(Var(1))**2))), div_: Defn(name='div_', args=[u, v], body=Vec3(x0(u)/x0(v), x1(u)/x1(v), x2(u)/x2(v)), ax=|= ForAll([u, v], div_(u, v) == Vec3(x0(u)/x0(v), x1(u)/x1(v), x2(u)/x2(v))), subst_funs_body=Vec3(x0(Var(0))/x0(Var(1)), x1(Var(0))/x1(Var(1)), x2(Var(0))/x2(Var(1)))), dot: Defn(name='dot', args=[u, v], body=x(u)*x(v) + y(u)*y(v), ax=|= ForAll([u, v], dot(u, v) == x(u)*x(v) + y(u)*y(v)), subst_funs_body=x(Var(0))*x(Var(1)) + y(Var(0))*y(Var(1))), dot: Defn(name='dot', args=[u, v], body=0 + x0(u)*x0(v) + x1(u)*x1(v) + x2(u)*x2(v), ax=|= ForAll([u, v], dot(u, v) == 0 + x0(u)*x0(v) + x1(u)*x1(v) + x2(u)*x2(v)), subst_funs_body=0 + x0(Var(0))*x0(Var(1)) + x1(Var(0))*x1(Var(1)) + x2(Var(0))*x2(Var(1))), double: Defn(name='double', args=[n], body=If(is(Z, n), Z, S(S(double(pred(n))))), ax=|= ForAll(n, double(n) == If(is(Z, n), Z, S(S(double(pred(n)))))), subst_funs_body=If(is(Z, Var(0)), Z, S(S(double(pred(Var(0))))))), even: Defn(name='even', args=[x], body=Exists(y, x == 2*y), ax=|= ForAll(x, even(x) == (Exists(y, x == 2*y))), subst_funs_body=Exists(y, Var(1) == 2*y)), expi: Defn(name='expi', args=[t], body=C(cos(t), sin(t)), ax=|= ForAll(t, expi(t) == C(cos(t), sin(t))), subst_funs_body=C(cos(Var(0)), sin(Var(0)))), finite: Defn(name='finite', args=[A], body=Exists(finwit!303, ForAll(x!302, A[x!302] == Contains(finwit!303, Unit(x!302)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!303, ForAll(x!302, A[x!302] == Contains(finwit!303, Unit(x!302)))))), subst_funs_body=Exists(finwit!303, ForAll(x!302, Var(2)[x!302] == Contains(finwit!303, Unit(x!302))))), finite: Defn(name='finite', args=[A], body=Exists(finwit!608, ForAll(x!607, A[x!607] == Contains(finwit!608, Unit(x!607)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!608, ForAll(x!607, A[x!607] == Contains(finwit!608, Unit(x!607)))))), subst_funs_body=Exists(finwit!608, ForAll(x!607, Var(2)[x!607] == Contains(finwit!608, Unit(x!607))))), finite: Defn(name='finite', args=[A], body=Exists(finwit!663, ForAll(x!662, A[x!662] == Contains(finwit!663, Unit(x!662)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!663, ForAll(x!662, A[x!662] == Contains(finwit!663, Unit(x!662)))))), subst_funs_body=Exists(finwit!663, ForAll(x!662, Var(2)[x!662] == Contains(finwit!663, Unit(x!662))))), finite: Defn(name='finite', args=[A], body=Exists(finwit!821, ForAll(x!820, A[x!820] == Contains(finwit!821, Unit(x!820)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!821, ForAll(x!820, A[x!820] == Contains(finwit!821, Unit(x!820)))))), subst_funs_body=Exists(finwit!821, ForAll(x!820, Var(2)[x!820] == Contains(finwit!821, Unit(x!820))))), floor: Defn(name='floor', args=[x], body=ToReal(ToInt(x)), ax=|= ForAll(x, floor(x) == ToReal(ToInt(x))), subst_funs_body=ToReal(ToInt(Var(0)))), from_int: Defn(name='from_int', args=[a], body=If(a <= 0, Z, S(from_int(a - 1))), ax=|= ForAll(a, from_int(a) == If(a <= 0, Z, S(from_int(a - 1)))), subst_funs_body=If(Var(0) <= 0, Z, S(from_int(Var(0) - 1)))), has_lim_at: Defn(name='has_lim_at', args=[f, p, L], body=ForAll(eps, Implies(0 < eps, Exists(delta, And(delta > 0, ForAll(x, Implies(And(0 < absR(x - p), absR(x - p) < delta), absR(f[x] - L) < eps)))))), ax=|= ForAll([f, p, L], has_lim_at(f, p, L) == (ForAll(eps, Implies(0 < eps, Exists(delta, And(delta > 0, ForAll(x, Implies(And(0 < absR(x - p), absR(x - p) < delta), absR(f[x] - L) < eps)))))))), subst_funs_body=ForAll(eps, Implies(0 < eps, Exists(delta, And(delta > 0, ForAll(x, Implies(And(0 < absR(x - Var(4)), absR(x - Var(4)) < delta), absR(Var(3)[x] - Var(5)) < eps))))))), ident: Defn(name='ident', args=[], body=Lambda(x, x), ax=|= ident == (Lambda(x, x)), subst_funs_body=Lambda(x, x)), is_cauchy: Defn(name='is_cauchy', args=[a], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll([m, k], Implies(And(m > N, k > N), absR(a[m] - a[k]) < eps))))), ax=|= ForAll(a, is_cauchy(a) == (ForAll(eps, Implies(eps > 0, Exists(N, ForAll([m, k], Implies(And(m > N, k > N), absR(a[m] - a[k]) < eps))))))), subst_funs_body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll([m, k], Implies(And(m > N, k > N), absR(Var(4)[m] - Var(4)[k]) < eps)))))), is_circle: Defn(name='is_circle', args=[A], body=Exists([c, r], circle(c, r) == A), ax=|= ForAll(A, is_circle(A) == (Exists([c, r], circle(c, r) == A))), subst_funs_body=Exists([c, r], circle(c, r) == Var(2))), is_cont: Defn(name='is_cont', args=[f], body=ForAll(x, cont_at(f, x)), ax=|= ForAll(f, is_cont(f) == (ForAll(x, cont_at(f, x)))), subst_funs_body=ForAll(x, cont_at(Var(1), x))), is_convergent: Defn(name='is_convergent', args=[a], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(m, Implies(m > N, Exists(x, absR(a[m] - x) < eps)))))), ax=|= ForAll(a, is_convergent(a) == (ForAll(eps, Implies(eps > 0, Exists(N, ForAll(m, Implies(m > N, Exists(x, absR(a[m] - x) < eps)))))))), subst_funs_body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(m, Implies(m > N, Exists(x, absR(Var(4)[m] - x) < eps))))))), is_diff: Defn(name='is_diff', args=[f], body=ForAll(x, diff_at(f, x)), ax=|= ForAll(f, is_diff(f) == (ForAll(x, diff_at(f, x)))), subst_funs_body=ForAll(x, diff_at(Var(1), x))), is_idem: Defn(name='is_idem', args=[A], body=mul(A, A) == A, ax=|= ForAll(A, is_idem(A) == (mul(A, A) == A)), subst_funs_body=mul(Var(0), Var(0)) == Var(0)), is_open: Defn(name='is_open', args=[S], body=ForAll(x!706, Implies(S[x!706], Exists(r!709, And(0 < r!709, subset(ball(x!706, r!709), S))))), ax=|= ForAll(S, is_open(S) == (ForAll(x!706, Implies(S[x!706], Exists(r!709, And(0 < r!709, subset(ball(x!706, r!709), S))))))), subst_funs_body=ForAll(x!706, Implies(Var(1)[x!706], Exists(r!709, And(0 < r!709, subset(ball(x!706, r!709), Var(2))))))), is_orth: Defn(name='is_orth', args=[A], body=mul(A, trans(A)) == I, ax=|= ForAll(A, is_orth(A) == (mul(A, trans(A)) == I)), subst_funs_body=mul(Var(0), trans(Var(0))) == I), is_symm: Defn(name='is_symm', args=[A], body=trans(A) == A, ax=|= ForAll(A, is_symm(A) == (trans(A) == A)), subst_funs_body=trans(Var(0)) == Var(0)), join: Defn(name='join', args=[i, j], body=Interval(min(lo(i), lo(j)), max(hi(i), hi(j))), ax=|= ForAll([i, j], join(i, j) == Interval(min(lo(i), lo(j)), max(hi(i), hi(j)))), subst_funs_body=Interval(min(lo(Var(0)), lo(Var(1))), max(hi(Var(0)), hi(Var(1))))), le: Defn(name='le', args=[x, y], body=If(x == y, True, If(is(NegInf, x), True, If(is(Inf, y), True, If(is(NegInf, y), False, If(is(Inf, x), False, If(And(is(Real, x), is(Real, y)), val(x) <= val(y), unreachable!771)))))), ax=|= ForAll([x, y], le(x, y) == If(x == y, True, If(is(NegInf, x), True, If(is(Inf, y), True, If(is(NegInf, y), False, If(is(Inf, x), False, If(And(is(Real, x), is(Real, y)), val(x) <= val(y), unreachable!771))))))), subst_funs_body=If(Var(0) == Var(1), True, If(is(NegInf, Var(0)), True, If(is(Inf, Var(1)), True, If(is(NegInf, Var(1)), False, If(is(Inf, Var(0)), False, If(And(is(Real, Var(0)), is(Real, Var(1))), val(Var(0)) <= val(Var(1)), unreachable!771))))))), max: Defn(name='max', args=[x, y], body=If(x >= y, x, y), ax=|= ForAll([x, y], max(x, y) == If(x >= y, x, y)), subst_funs_body=If(Var(0) >= Var(1), Var(0), Var(1))), meet: Defn(name='meet', args=[i, j], body=Interval(max(lo(i), lo(j)), min(hi(i), hi(j))), ax=|= ForAll([i, j], meet(i, j) == Interval(max(lo(i), lo(j)), min(hi(i), hi(j)))), subst_funs_body=Interval(max(lo(Var(0)), lo(Var(1))), min(hi(Var(0)), hi(Var(1))))), mid: Defn(name='mid', args=[i], body=(lo(i) + hi(i))/2, ax=|= ForAll(i, mid(i) == (lo(i) + hi(i))/2), subst_funs_body=(lo(Var(0)) + hi(Var(0)))/2), min: Defn(name='min', args=[x, y], body=If(x <= y, x, y), ax=|= ForAll([x, y], min(x, y) == If(x <= y, x, y)), subst_funs_body=If(Var(0) <= Var(1), Var(0), Var(1))), mul: Defn(name='mul', args=[f, g], body=Lambda(x, f[x]*g[x]), ax=|= ForAll([f, g], mul(f, g) == (Lambda(x, f[x]*g[x]))), subst_funs_body=Lambda(x, Var(1)[x]*Var(2)[x])), mul: Defn(name='mul', args=[a, b], body=Lambda(i, a[i]*b[i]), ax=|= ForAll([a, b], mul(a, b) == (Lambda(i, a[i]*b[i]))), subst_funs_body=Lambda(i, Var(1)[i]*Var(2)[i])), mul: Defn(name='mul', args=[x, y], body=x*y, ax=|= ForAll([x, y], mul(x, y) == x*y), subst_funs_body=Var(0)*Var(1)), mul: Defn(name='mul', args=[z1, z2], body=C(re(z1)*re(z2) - im(z1)*im(z2), re(z1)*im(z2) + im(z1)*re(z2)), ax=|= ForAll([z1, z2], mul(z1, z2) == C(re(z1)*re(z2) - im(z1)*im(z2), re(z1)*im(z2) + im(z1)*re(z2))), subst_funs_body=C(re(Var(0))*re(Var(1)) - im(Var(0))*im(Var(1)), re(Var(0))*im(Var(1)) + im(Var(0))*re(Var(1)))), mul: Defn(name='mul', args=[u, v], body=Vec3(x0(u)*x0(v), x1(u)*x1(v), x2(u)*x2(v)), ax=|= ForAll([u, v], mul(u, v) == Vec3(x0(u)*x0(v), x1(u)*x1(v), x2(u)*x2(v))), subst_funs_body=Vec3(x0(Var(0))*x0(Var(1)), x1(Var(0))*x1(Var(1)), x2(Var(0))*x2(Var(1)))), neg: Defn(name='neg', args=[u], body=Vec2(-x(u), -y(u)), ax=|= ForAll(u, neg(u) == Vec2(-x(u), -y(u))), subst_funs_body=Vec2(-x(Var(0)), -y(Var(0)))), neg: Defn(name='neg', args=[u], body=Vec3(-x0(u), -x1(u), -x2(u)), ax=|= ForAll(u, neg(u) == Vec3(-x0(u), -x1(u), -x2(u))), subst_funs_body=Vec3(-x0(Var(0)), -x1(Var(0)), -x2(Var(0)))), nonneg: Defn(name='nonneg', args=[x], body=absR(x) == x, ax=|= ForAll(x, nonneg(x) == (absR(x) == x)), subst_funs_body=absR(Var(0)) == Var(0)), norm2: Defn(name='norm2', args=[z], body=mul(z, conj(z)), ax=|= ForAll(z, norm2(z) == mul(z, conj(z))), subst_funs_body=mul(Var(0), conj(Var(0)))), norm2: Defn(name='norm2', args=[u], body=dot(u, u), ax=|= ForAll(u, norm2(u) == dot(u, u)), subst_funs_body=dot(Var(0), Var(0))), norm2: Defn(name='norm2', args=[u], body=x0(u)*x0(u) + x1(u)*x1(u) + x2(u)*x2(u), ax=|= ForAll(u, norm2(u) == x0(u)*x0(u) + x1(u)*x1(u) + x2(u)*x2(u)), subst_funs_body=x0(Var(0))*x0(Var(0)) + x1(Var(0))*x1(Var(0)) + x2(Var(0))*x2(Var(0))), odd: Defn(name='odd', args=[x], body=Exists(y, x == 2*y + 1), ax=|= ForAll(x, odd(x) == (Exists(y, x == 2*y + 1))), subst_funs_body=Exists(y, Var(1) == 2*y + 1)), one: Defn(name='one', args=[], body=1, ax=|= one == 1, subst_funs_body=1), ones: Defn(name='ones', args=[n], body=NDArray(Unit(n), K(Int, 1)), ax=|= ForAll(n, ones(n) == NDArray(Unit(n), K(Int, 1))), subst_funs_body=NDArray(Unit(Var(0)), K(Int, 1))), open: Defn(name='open', args=[A], body=Or(A == K(Sierpinski, False), A == K(Sierpinski, True), A == Store(K(Sierpinski, False), S1, True)), ax=|= ForAll(A, open(A) == Or(A == K(Sierpinski, False), A == K(Sierpinski, True), A == Store(K(Sierpinski, False), S1, True))), subst_funs_body=Or(Var(0) == K(Sierpinski, False), Var(0) == K(Sierpinski, True), Var(0) == Store(K(Sierpinski, False), S1, True))), pow: Defn(name='pow', args=[x, y], body=x**y, ax=|= ForAll([x, y], pow(x, y) == x**y), subst_funs_body=Var(0)**Var(1)), safe_pred: Defn(name='safe_pred', args=[n], body=If(is(Z, n), Z, pred(n)), ax=|= ForAll(n, safe_pred(n) == If(is(Z, n), Z, pred(n))), subst_funs_body=If(is(Z, Var(0)), Z, pred(Var(0)))), select_16_be: Defn(name='select_16_be', args=[a, addr], body=Concat(a[addr + 0], a[addr + 1]), ax=|= ForAll([a, addr], select_16_be(a, addr) == Concat(a[addr + 0], a[addr + 1])), subst_funs_body=Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1])), select_16_be: Defn(name='select_16_be', args=[a, addr], body=Concat(a[addr + 0], a[addr + 1]), ax=|= ForAll([a, addr], select_16_be(a, addr) == Concat(a[addr + 0], a[addr + 1])), subst_funs_body=Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1])), select_16_le: Defn(name='select_16_le', args=[a, addr], body=Concat(a[addr + 2 - 0 - 1], a[addr + 2 - 1 - 1]), ax=|= ForAll([a, addr], select_16_le(a, addr) == Concat(a[addr + 2 - 0 - 1], a[addr + 2 - 1 - 1])), subst_funs_body=Concat(Var(0)[Var(1) + 2 - 0 - 1], Var(0)[Var(1) + 2 - 1 - 1])), select_16_le: Defn(name='select_16_le', args=[a, addr], body=Concat(a[addr + 2 - 0 - 1], a[addr + 2 - 1 - 1]), ax=|= ForAll([a, addr], select_16_le(a, addr) == Concat(a[addr + 2 - 0 - 1], a[addr + 2 - 1 - 1])), subst_funs_body=Concat(Var(0)[Var(1) + 2 - 0 - 1], Var(0)[Var(1) + 2 - 1 - 1])), select_32_be: Defn(name='select_32_be', args=[a, addr], body=Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), ax=|= ForAll([a, addr], select_32_be(a, addr) == Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3])), subst_funs_body=Concat(Concat(Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1]), Var(0)[Var(1) + 2]), Var(0)[Var(1) + 3])), select_32_be: Defn(name='select_32_be', args=[a, addr], body=Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), ax=|= ForAll([a, addr], select_32_be(a, addr) == Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3])), subst_funs_body=Concat(Concat(Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1]), Var(0)[Var(1) + 2]), Var(0)[Var(1) + 3])), select_32_le: Defn(name='select_32_le', args=[a, addr], body=Concat(Concat(Concat(a[addr + 4 - 0 - 1], a[addr + 4 - 1 - 1]), a[addr + 4 - 2 - 1]), a[addr + 4 - 3 - 1]), ax=|= ForAll([a, addr], select_32_le(a, addr) == Concat(Concat(Concat(a[addr + 4 - 0 - 1], a[addr + 4 - 1 - 1]), a[addr + 4 - 2 - 1]), a[addr + 4 - 3 - 1])), subst_funs_body=Concat(Concat(Concat(Var(0)[Var(1) + 4 - 0 - 1], Var(0)[Var(1) + 4 - 1 - 1]), Var(0)[Var(1) + 4 - 2 - 1]), Var(0)[Var(1) + 4 - 3 - 1])), select_32_le: Defn(name='select_32_le', args=[a, addr], body=Concat(Concat(Concat(a[addr + 4 - 0 - 1], a[addr + 4 - 1 - 1]), a[addr + 4 - 2 - 1]), a[addr + 4 - 3 - 1]), ax=|= ForAll([a, addr], select_32_le(a, addr) == Concat(Concat(Concat(a[addr + 4 - 0 - 1], a[addr + 4 - 1 - 1]), a[addr + 4 - 2 - 1]), a[addr + 4 - 3 - 1])), subst_funs_body=Concat(Concat(Concat(Var(0)[Var(1) + 4 - 0 - 1], Var(0)[Var(1) + 4 - 1 - 1]), Var(0)[Var(1) + 4 - 2 - 1]), Var(0)[Var(1) + 4 - 3 - 1])), select_64_be: Defn(name='select_64_be', args=[a, addr], body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), a[addr + 4]), a[addr + 5]), a[addr + 6]), a[addr + 7]), ax=|= ForAll([a, addr], select_64_be(a, addr) == Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), a[addr + 4]), a[addr + 5]), a[addr + 6]), a[addr + 7])), subst_funs_body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1]), Var(0)[Var(1) + 2]), Var(0)[Var(1) + 3]), Var(0)[Var(1) + 4]), Var(0)[Var(1) + 5]), Var(0)[Var(1) + 6]), Var(0)[Var(1) + 7])), select_64_be: Defn(name='select_64_be', args=[a, addr], body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), a[addr + 4]), a[addr + 5]), a[addr + 6]), a[addr + 7]), ax=|= ForAll([a, addr], select_64_be(a, addr) == Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 0], a[addr + 1]), a[addr + 2]), a[addr + 3]), a[addr + 4]), a[addr + 5]), a[addr + 6]), a[addr + 7])), subst_funs_body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1]), Var(0)[Var(1) + 2]), Var(0)[Var(1) + 3]), Var(0)[Var(1) + 4]), Var(0)[Var(1) + 5]), Var(0)[Var(1) + 6]), Var(0)[Var(1) + 7])), select_64_le: Defn(name='select_64_le', args=[a, addr], body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 8 - 0 - 1], a[addr + 8 - 1 - 1]), a[addr + 8 - 2 - 1]), a[addr + 8 - 3 - 1]), a[addr + 8 - 4 - 1]), a[addr + 8 - 5 - 1]), a[addr + 8 - 6 - 1]), a[addr + 8 - 7 - 1]), ax=|= ForAll([a, addr], select_64_le(a, addr) == Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 8 - 0 - 1], a[addr + 8 - 1 - 1]), a[addr + 8 - 2 - 1]), a[addr + 8 - 3 - 1]), a[addr + 8 - 4 - 1]), a[addr + 8 - 5 - 1]), a[addr + 8 - 6 - 1]), a[addr + 8 - 7 - 1])), subst_funs_body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(Var(0)[Var(1) + 8 - 0 - 1], Var(0)[Var(1) + 8 - 1 - 1]), Var(0)[Var(1) + 8 - 2 - 1]), Var(0)[Var(1) + 8 - 3 - 1]), Var(0)[Var(1) + 8 - 4 - 1]), Var(0)[Var(1) + 8 - 5 - 1]), Var(0)[Var(1) + 8 - 6 - 1]), Var(0)[Var(1) + 8 - 7 - 1])), select_64_le: Defn(name='select_64_le', args=[a, addr], body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 8 - 0 - 1], a[addr + 8 - 1 - 1]), a[addr + 8 - 2 - 1]), a[addr + 8 - 3 - 1]), a[addr + 8 - 4 - 1]), a[addr + 8 - 5 - 1]), a[addr + 8 - 6 - 1]), a[addr + 8 - 7 - 1]), ax=|= ForAll([a, addr], select_64_le(a, addr) == Concat(Concat(Concat(Concat(Concat(Concat(Concat(a[addr + 8 - 0 - 1], a[addr + 8 - 1 - 1]), a[addr + 8 - 2 - 1]), a[addr + 8 - 3 - 1]), a[addr + 8 - 4 - 1]), a[addr + 8 - 5 - 1]), a[addr + 8 - 6 - 1]), a[addr + 8 - 7 - 1])), subst_funs_body=Concat(Concat(Concat(Concat(Concat(Concat(Concat(Var(0)[Var(1) + 8 - 0 - 1], Var(0)[Var(1) + 8 - 1 - 1]), Var(0)[Var(1) + 8 - 2 - 1]), Var(0)[Var(1) + 8 - 3 - 1]), Var(0)[Var(1) + 8 - 4 - 1]), Var(0)[Var(1) + 8 - 5 - 1]), Var(0)[Var(1) + 8 - 6 - 1]), Var(0)[Var(1) + 8 - 7 - 1])), seqlim: Defn(name='seqlim', args=[a, y], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(a[n] - y) < eps))))), ax=|= ForAll([a, y], seqlim(a, y) == (ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(a[n] - y) < eps))))))), subst_funs_body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(Var(3)[n] - Var(4)) < eps)))))), setof: Defn(name='setof', args=[i], body=Lambda(x, And(lo(i) <= x, x <= hi(i))), ax=|= ForAll(i, setof(i) == (Lambda(x, And(lo(i) <= x, x <= hi(i))))), subst_funs_body=Lambda(x, And(lo(Var(1)) <= x, x <= hi(Var(1))))), sgn: Defn(name='sgn', args=[x], body=If(x > 0, 1, If(x < 0, -1, 0)), ax=|= ForAll(x, sgn(x) == If(x > 0, 1, If(x < 0, -1, 0))), subst_funs_body=If(Var(0) > 0, 1, If(Var(0) < 0, -1, 0))), sqr: Defn(name='sqr', args=[x], body=x*x, ax=|= ForAll(x, sqr(x) == x*x), subst_funs_body=Var(0)*Var(0)), sqrt: Defn(name='sqrt', args=[x], body=x**(1/2), ax=|= ForAll(x, sqrt(x) == x**(1/2)), subst_funs_body=Var(0)**(1/2)), sub: Defn(name='sub', args=[f, g], body=Lambda(x, f[x] - g[x]), ax=|= ForAll([f, g], sub(f, g) == (Lambda(x, f[x] - g[x]))), subst_funs_body=Lambda(x, Var(1)[x] - Var(2)[x])), sub: Defn(name='sub', args=[a, b], body=Lambda(i, a[i] - b[i]), ax=|= ForAll([a, b], sub(a, b) == (Lambda(i, a[i] - b[i]))), subst_funs_body=Lambda(i, Var(1)[i] - Var(2)[i])), sub: Defn(name='sub', args=[x, y], body=x - y, ax=|= ForAll([x, y], sub(x, y) == x - y), subst_funs_body=Var(0) - Var(1)), sub: Defn(name='sub', args=[u, v], body=Vec2(x(u) - x(v), y(u) - y(v)), ax=|= ForAll([u, v], sub(u, v) == Vec2(x(u) - x(v), y(u) - y(v))), subst_funs_body=Vec2(x(Var(0)) - x(Var(1)), y(Var(0)) - y(Var(1)))), sub: Defn(name='sub', args=[u, v], body=Vec3(x0(u) - x0(v), x1(u) - x1(v), x2(u) - x2(v)), ax=|= ForAll([u, v], sub(u, v) == Vec3(x0(u) - x0(v), x1(u) - x1(v), x2(u) - x2(v))), subst_funs_body=Vec3(x0(Var(0)) - x0(Var(1)), x1(Var(0)) - x1(Var(1)), x2(Var(0)) - x2(Var(1)))), sub: Defn(name='sub', args=[i, j], body=Interval(lo(i) - hi(j), hi(i) - lo(j)), ax=|= ForAll([i, j], sub(i, j) == Interval(lo(i) - hi(j), hi(i) - lo(j))), subst_funs_body=Interval(lo(Var(0)) - hi(Var(1)), hi(Var(0)) - lo(Var(1)))), tan: Defn(name='tan', args=[x], body=sin(x)/cos(x), ax=|= ForAll(x, tan(x) == sin(x)/cos(x)), subst_funs_body=sin(Var(0))/cos(Var(0))), to_int: Defn(name='to_int', args=[x], body=If(Length(val(x)) == 0, 0, BV2Int(Nth(val(x), 0)) + 2* to_int(BitVecN(seq.extract(val(x), 1, Length(val(x)) - 1)))), ax=|= ForAll(x, to_int(x) == If(Length(val(x)) == 0, 0, BV2Int(Nth(val(x), 0)) + 2* to_int(BitVecN(seq.extract(val(x), 1, Length(val(x)) - 1))))), subst_funs_body=If(Length(val(Var(0))) == 0, 0, BV2Int(Nth(val(Var(0)), 0)) + 2* to_int(BitVecN(seq.extract(val(Var(0)), 1, Length(val(Var(0))) - 1))))), to_int: Defn(name='to_int', args=[n], body=If(is(Z, n), 0, 1 + to_int(pred(n))), ax=|= ForAll(n, to_int(n) == If(is(Z, n), 0, 1 + to_int(pred(n)))), subst_funs_body=If(is(Z, Var(0)), 0, 1 + to_int(pred(Var(0))))), wf: Defn(name='wf', args=[x], body=Implies(is(real, x), val(x) >= 0), ax=|= ForAll(x, wf(x) == Implies(is(real, x), val(x) >= 0)), subst_funs_body=Implies(is(real, Var(0)), val(Var(0)) >= 0)), width: Defn(name='width', args=[i], body=hi(i) - lo(i), ax=|= ForAll(i, width(i) == hi(i) - lo(i)), subst_funs_body=hi(Var(0)) - lo(Var(0))), zero: Defn(name='zero', args=[], body=0, ax=|= zero == 0, subst_funs_body=0), zero: Defn(name='zero', args=[n], body=NDArray(Unit(n), K(Int, 0)), ax=|= ForAll(n, zero(n) == NDArray(Unit(n), K(Int, 0))), subst_funs_body=NDArray(Unit(Var(0)), K(Int, 0)))}: defn holds definitional axioms for function symbols.

kdrag.kernel.einstan(thm: QuantifierRef) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier. exists xs, P(xs) -> P(cs) for fresh cs https://en.wikipedia.org/wiki/Existential_instantiation

Parameters:: thm (QuantifierRef)
Return type:: tuple[list[ExprRef], Proof]

kdrag.kernel.forget(ts: Iterable[ExprRef], pf: Proof) → Proof

“Forget” a term using existentials. This is existential introduction. This could be derived from forget2

Parameters:

ts (Iterable[ExprRef])
pf (Proof)

Return type:

Proof

kdrag.kernel.forget2(ts: Sequence[ExprRef], thm: QuantifierRef) → Proof

“Forget” a term using existentials. This is existential introduction. P(ts) -> exists xs, P(xs) thm is an existential formula, and ts are terms to substitute those variables with. forget easily follows. https://en.wikipedia.org/wiki/Existential_generalization

Parameters:

ts (Sequence[ExprRef])
thm (QuantifierRef)

Return type:

Proof

kdrag.kernel.free_in(vs: list[ExprRef], t: ExprRef) → bool

Returns True if none of the variables in vs exist unbound in t. Distinct from occurs in that vs have to be constants, not general terms.

>>> x,y,z = smt.Ints("x y z")
>>> assert not free_in([x], x + y + z)
>>> assert free_in([x], y + z)
>>> assert free_in([x], smt.Lambda([x], x + y + z))

Parameters:

vs (list[ExprRef])
t (ExprRef)

Return type:

bool

kdrag.kernel.fresh_const(q: QuantifierRef)

Generate fresh constants of same sort as quantifier.

Parameters:: q (QuantifierRef)

kdrag.kernel.generalize(vs: list[ExprRef], pf: Proof) → Proof

Generalize a theorem with respect to a list of schema variables. This introduces a universal quantifier for schema variables.

>>> x = FreshVar("x", smt.IntSort())
>>> y = FreshVar("y", smt.IntSort())
>>> generalize([x, y], prove(x == x))
|= ForAll([x!..., y!...], x!... == x!...)

Parameters:

vs (list[ExprRef])
pf (Proof)

Return type:

Proof

kdrag.kernel.herb(thm: QuantifierRef) → tuple[list[ExprRef], Proof]

Herbrandize a theorem. It is sufficient to prove a theorem for fresh consts to prove a universal. Note: Perhaps lambdaized form is better? Return vars and lamda that could receive |= P[vars]

Parameters:: thm (QuantifierRef)
Return type:: tuple[list[ExprRef], Proof]

kdrag.kernel.induct_inductive(x: DatatypeRef, P: QuantifierRef) → Proof

Build a basic induction principle for an algebraic datatype

Parameters:

x (DatatypeRef)
P (QuantifierRef)

Return type:

Proof

kdrag.kernel.instan(ts: Sequence[ExprRef], pf: Proof) → Proof

Instantiate a universally quantified formula. This is forall elimination

Parameters:

ts (Sequence[ExprRef])
pf (Proof)

Return type:

Proof

kdrag.kernel.instan2(ts: Sequence[ExprRef], thm: BoolRef) → Proof

Instantiate a universally quantified formula forall xs, P(xs) -> P(ts) This is forall elimination

Parameters:

ts (Sequence[ExprRef])
thm (BoolRef)

Return type:

Proof

kdrag.kernel.is_defined(x: ExprRef) → bool

Determined if expression head is in definitions.

Parameters:: x (ExprRef)
Return type:: bool

kdrag.kernel.is_fresh_var(v: ExprRef) → bool

Check if a variable is a schema variable. Schema variables are generated by FreshVar and have a _FreshVarEvidence attribute.

>>> is_fresh_var(FreshVar("x", smt.IntSort()))
True

Parameters:: v (ExprRef)
Return type:: bool

kdrag.kernel.is_proof(p: Proof) → bool

Parameters:: p (Proof)
Return type:: bool

kdrag.kernel.modus(ab: Proof, a: Proof) → Proof

Modus ponens for implies and equality.

>>> a,b = smt.Bools("a b")
>>> ab = axiom(smt.Implies(a, b))
>>> a = axiom(a)
>>> modus(ab, a)
|= b
>>> ab1 = axiom(smt.Eq(a.thm, b))
>>> modus(ab1, a)
|= b

Parameters:

ab (Proof)
a (Proof)

Return type:

Proof

kdrag.kernel.prove(thm: BoolRef, by: Proof | Iterable[Proof] = [], admit=False, timeout=1000, dump=False, solver=None) → Proof

Prove a theorem using a list of previously proved lemmas.

In essence prove(Implies(by, thm)).

Parameters:

thm (smt.BoolRef) – The theorem to prove.
thm – The theorem to prove.
by (list[Proof]) – A list of previously proved lemmas.
admit (bool) – If True, admit the theorem without proof.

Returns:

A proof object of thm

Return type:

Proof

>>> prove(smt.BoolVal(True))
|= True
>>> prove(smt.RealVal(1) >= smt.RealVal(0))
|= 1 >= 0

kdrag.kernel.rename_vars(t: QuantifierRef, vs: list[ExprRef]) → tuple[QuantifierRef, Proof]

>>> x,y = smt.Ints("x y")
>>> rename_vars(smt.ForAll([x, y], x + 1 > y), [y,x])
(ForAll([y, x], y + 1 > x), |= (ForAll([x, y], x + 1 > y)) == (ForAll([y, x], y + 1 > x)))
>>> rename_vars(smt.Exists([x], x + 1 > y), [y])
Traceback (most recent call last):
    ...
ValueError: ('Cannot rename vars to ones that already occur in term', [y], Exists(x, x + 1 > y))

Parameters:

t (QuantifierRef)
vs (list[ExprRef])

Return type:

tuple[QuantifierRef, Proof]

kdrag.kernel.skolem(pf: Proof) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier.

Parameters:: pf (Proof)
Return type:: tuple[list[ExprRef], Proof]

kdrag.kernel.subst(t: ExprRef, eqs: Sequence[Proof]) → tuple[ExprRef, Proof]

Substitute using equality proofs

>>> x, y = smt.Ints("x y")
>>> eq = kd.prove(x == ((x + 1) - 1))
>>> subst(x + 3, [eq])
(x + 1 - 1 + 3, |= x + 3 == x + 1 - 1 + 3)

Parameters:

t (ExprRef)
eqs (Sequence[Proof])

Return type:

tuple[ExprRef, Proof]

kdrag.kernel.substitute_fresh_vars(pf: Proof, *subst) → Proof

Substitute schematic variables in a theorem. This is is single step instead of generalizing to a Forall and then eliminating it.

>>> x = FreshVar("x", smt.IntSort())
>>> y = FreshVar("y", smt.IntSort())
>>> substitute_fresh_vars(prove(x == x), (x, smt.IntVal(42)), (y, smt.IntVal(43)))
|= 42 == 42

Parameters:: pf (Proof)
Return type:: Proof

kdrag.kernel.unfold(e: ExprRef, decls: Sequence[FuncDeclRef]) → tuple[ExprRef, Proof]

Unfold function definitions in an expression.

>>> x,y = smt.Ints("x y")
>>> f = define("f", [x,y], x + 2*y)
>>> g = define("g", [x,y], f(x,y) + 1)
>>> unfold(f(42,13) + g(7,8), [f])
(42 + 2*13 + g(7, 8), |= f(42, 13) + g(7, 8) == 42 + 2*13 + g(7, 8))
>>> unfold(f(42,13) + g(7,8), [f,g])
(42 + 2*13 + f(7, 8) + 1, |= f(42, 13) + g(7, 8) == 42 + 2*13 + f(7, 8) + 1)

Parameters:

e (ExprRef)
decls (Sequence[FuncDeclRef])

Return type:

tuple[ExprRef, Proof]