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.
`define`(name, args, body[, lift_lambda])	Define a non recursive definition.
`define_fix`(name, args, retsort, fix_lam)	Define a recursive definition.
`ext`(domain, range_)
`forget`(ts, thm)	"Forget" a term using existentials.
`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.
`obtain`(thm)	Skolemize an existential quantifier.
`prove`(thm[, by, admit, timeout, dump, solver])	Prove a theorem using a list of previously proved lemmas.
`subst`(t, eqs)	Substitute using equality proofs
`unfold`(e, decls)	Unfold function definitions in an expression.

Classes

`Defn`(name, decl, args, body, ax, _subst_fun_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, decl: FuncDeclRef, args: list[ExprRef], body: ExprRef, ax: Proof, _subst_fun_body: ExprRef)

Bases: Judgement

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

Parameters:

name (str)
decl (FuncDeclRef)
args (list[ExprRef])
body (ExprRef)
ax (Proof)
_subst_fun_body (ExprRef)

args: list[ExprRef]

ax: Proof

body: ExprRef

decl: FuncDeclRef

name: str

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, 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.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', decl=abelian, args=[], body=ForAll([x!501, y!502], mul(x!501, y!502) == mul(y!502, x!501)), ax=|= abelian == (ForAll([x!501, y!502], mul(x!501, y!502) == mul(y!502, x!501))), _subst_fun_body=ForAll([x!501, y!502], mul(x!501, y!502) == mul(y!502, x!501))), absR: Defn(name='absR', decl=absR, args=[x], body=If(x >= 0, x, -x), ax=|= ForAll(x, absR(x) == If(x >= 0, x, -x)), _subst_fun_body=If(Var(0) >= 0, Var(0), -Var(0))), add: Defn(name='add', decl=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_fun_body=If(is(Z, Var(0)), Var(1), S(add(pred(Var(0)), Var(1))))), add: Defn(name='add', decl=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_fun_body=Lambda(x, Var(1)[x] + Var(2)[x])), add: Defn(name='add', decl=add, args=[x, y], body=x + y, ax=|= ForAll([x, y], add(x, y) == x + y), _subst_fun_body=Var(0) + Var(1)), add: Defn(name='add', decl=add, args=[x, y], body=T_Int(Lambda(t, val(x)[t] + val(y)[t])), ax=|= ForAll([x, y], add(x, y) == T_Int(Lambda(t, val(x)[t] + val(y)[t]))), _subst_fun_body=T_Int(Lambda(t, val(Var(1))[t] + val(Var(2))[t]))), add: Defn(name='add', decl=add, args=[x, y], body=T_Real(Lambda(t, val(x)[t] + val(y)[t])), ax=|= ForAll([x, y], add(x, y) == T_Real(Lambda(t, val(x)[t] + val(y)[t]))), _subst_fun_body=T_Real(Lambda(t, val(Var(1))[t] + val(Var(2))[t]))), add: Defn(name='add', decl=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_fun_body=C(re(Var(0)) + re(Var(1)), im(Var(0)) + im(Var(1)))), add: Defn(name='add', decl=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_fun_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', decl=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_fun_body=Vec2(x(Var(0)) + x(Var(1)), y(Var(0)) + y(Var(1)))), add: Defn(name='add', decl=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_fun_body=Vec3(x0(Var(0)) + x0(Var(1)), x1(Var(0)) + x1(Var(1)), x2(Var(0)) + x2(Var(1)))), add: Defn(name='add', decl=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_fun_body=Interval(lo(Var(0)) + lo(Var(1)), hi(Var(0)) + hi(Var(1)))), add: Defn(name='add', decl=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_fun_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: Defn(name='add', decl=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_fun_body=Lambda(i, Var(1)[i] + Var(2)[i])), add_defined: Defn(name='add_defined', decl=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_fun_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))))), always: Defn(name='always', decl=always, args=[p], body=T_Bool(Lambda(t!765, ForAll(dt!766, Implies(dt!766 >= 0, val(p)[t!765 + dt!766])))), ax=|= ForAll(p, always(p) == T_Bool(Lambda(t!765, ForAll(dt!766, Implies(dt!766 >= 0, val(p)[t!765 + dt!766]))))), _subst_fun_body=T_Bool(Lambda(t!765, ForAll(dt!766, Implies(dt!766 >= 0, val(Var(2))[t!765 + dt!766]))))), ball: Defn(name='ball', decl=ball, args=[x!1226, r!1229], body=Lambda(y!1230, absR(y!1230 - x!1226) < r!1229), ax=|= ForAll([x!1226, r!1229], ball(x!1226, r!1229) == (Lambda(y!1230, absR(y!1230 - x!1226) < r!1229))), _subst_fun_body=Lambda(y!1230, absR(y!1230 - Var(1)) < Var(2))), beq: Defn(name='beq', decl=beq, args=[p, q], body=T_Bool(Lambda(t!768, val(p)[t!768] == val(q)[t!768])), ax=|= ForAll([p, q], beq(p, q) == T_Bool(Lambda(t!768, val(p)[t!768] == val(q)[t!768]))), _subst_fun_body=T_Bool(Lambda(t!768, val(Var(1))[t!768] == val(Var(2))[t!768]))), bexist: Defn(name='bexist', decl=bexist, args=[A, n], body=If(n < 0, False, Or(A[n], bexists(A, n - 1))), ax=|= ForAll([A, n], bexist(A, n) == If(n < 0, False, Or(A[n], bexists(A, n - 1)))), _subst_fun_body=If(Var(1) < 0, False, Or(Var(0)[Var(1)], bexists(Var(0), Var(1) - 1)))), bforall: Defn(name='bforall', decl=bforall, args=[A, n], body=If(n < 0, True, And(A[n], bforall(A, n - 1))), ax=|= ForAll([A, n], bforall(A, n) == If(n < 0, True, And(A[n], bforall(A, n - 1)))), _subst_fun_body=If(Var(1) < 0, True, And(Var(0)[Var(1)], bforall(Var(0), Var(1) - 1)))), biginter: Defn(name='biginter', decl=biginter, args=[a!796], body=sep(pick(a!796), Lambda(x, ForAll(b!797, Implies(elem(b!797, a!796), elem(x, b!797))))), ax=|= ForAll(a!796, biginter(a!796) == sep(pick(a!796), Lambda(x, ForAll(b!797, Implies(elem(b!797, a!796), elem(x, b!797)))))), _subst_fun_body=sep(pick(Var(0)), Lambda(x, ForAll(b!797, Implies(elem(b!797, Var(2)), elem(x, b!797)))))), cauchy_mod: Defn(name='cauchy_mod', decl=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_fun_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', decl=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_fun_body=Lambda(p, norm2(sub(p, Var(1))) == Var(2)*Var(2))), closed: Defn(name='closed', decl=closed, args=[A], body=open(complement(A)), ax=|= ForAll(A, closed(A) == open(complement(A))), _subst_fun_body=open(complement(Var(0)))), comp: Defn(name='comp', decl=comp, args=[f, g], body=Lambda(x, f[g[x]]), ax=|= ForAll([f, g], comp(f, g) == (Lambda(x, f[g[x]]))), _subst_fun_body=Lambda(x, Var(1)[Var(2)[x]])), conj: Defn(name='conj', decl=conj, args=[z], body=C(re(z), -im(z)), ax=|= ForAll(z, conj(z) == C(re(z), -im(z))), _subst_fun_body=C(re(Var(0)), -im(Var(0)))), const: Defn(name='const', decl=const, args=[x], body=K(Real, x), ax=|= ForAll(x, const(x) == K(Real, x)), _subst_fun_body=K(Real, Var(0))), const: Defn(name='const', decl=const, args=[x], body=Lambda(i, x), ax=|= ForAll(x, const(x) == (Lambda(i, x))), _subst_fun_body=Lambda(i, Var(1))), cont_at: Defn(name='cont_at', decl=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_fun_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))))))), cos: Defn(name='cos', decl=cos, args=[a], body=Map(cos, a), ax=|= ForAll(a, cos(a) == Map(cos, a)), _subst_fun_body=Map(cos, Var(0))), cross: Defn(name='cross', decl=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_fun_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)))), cumsum: Defn(name='cumsum', decl=cumsum, args=[a], body=Lambda(i, If(i == 0, a[0], If(i > 0, cumsum(a)[i - 1] + a[i], -cumsum(a)[i + 1] - a[i]))), ax=|= ForAll(a, cumsum(a) == (Lambda(i, If(i == 0, a[0], If(i > 0, cumsum(a)[i - 1] + a[i], -cumsum(a)[i + 1] - a[i]))))), _subst_fun_body=Lambda(i, If(i == 0, Var(1)[0], If(i > 0, cumsum(Var(1))[i - 1] + Var(1)[i], -cumsum(Var(1))[i + 1] - Var(1)[i])))), decimate: Defn(name='decimate', decl=decimate, args=[a, n], body=Lambda(i, a[i*n]), ax=|= ForAll([a, n], decimate(a, n) == (Lambda(i, a[i*n]))), _subst_fun_body=Lambda(i, Var(1)[i*Var(2)])), delay: Defn(name='delay', decl=delay, args=[a], body=shift(a, 1), ax=|= ForAll(a, delay(a) == shift(a, 1)), _subst_fun_body=shift(Var(0), 1)), diff: Defn(name='diff', decl=diff, args=[a], body=Lambda(i, a[i + 1] - a[i]), ax=|= ForAll(a, diff(a) == (Lambda(i, a[i + 1] - a[i]))), _subst_fun_body=Lambda(i, Var(1)[i + 1] - Var(1)[i])), diff_at: Defn(name='diff_at', decl=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_fun_body=Exists(y, has_diff_at(Var(1), Var(2), y))), dilate: Defn(name='dilate', decl=dilate, args=[a, n], body=Lambda(i, a[i/n]), ax=|= ForAll([a, n], dilate(a, n) == (Lambda(i, a[i/n]))), _subst_fun_body=Lambda(i, Var(1)[i/Var(2)])), dist: Defn(name='dist', decl=dist, args=[x!1226, y!1227], body=absR(x!1226 - y!1227), ax=|= ForAll([x!1226, y!1227], dist(x!1226, y!1227) == absR(x!1226 - y!1227)), _subst_fun_body=absR(Var(0) - Var(1))), dist: Defn(name='dist', decl=dist, args=[u, v], body=sqrt(norm2(sub(u, v))), ax=|= ForAll([u, v], dist(u, v) == sqrt(norm2(sub(u, v)))), _subst_fun_body=sqrt(norm2(sub(Var(0), Var(1))))), div_: Defn(name='div_', decl=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_fun_body=Lambda(x, Var(1)[x]/Var(2)[x])), div_: Defn(name='div_', decl=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_fun_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_', decl=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_fun_body=Vec3(x0(Var(0))/x0(Var(1)), x1(Var(0))/x1(Var(1)), x2(Var(0))/x2(Var(1)))), div_: Defn(name='div_', decl=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_fun_body=Lambda(i, Var(1)[i]/Var(2)[i])), dot: Defn(name='dot', decl=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_fun_body=x(Var(0))*x(Var(1)) + y(Var(0))*y(Var(1))), dot: Defn(name='dot', decl=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_fun_body=0 + x0(Var(0))*x0(Var(1)) + x1(Var(0))*x1(Var(1)) + x2(Var(0))*x2(Var(1))), double: Defn(name='double', decl=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_fun_body=If(is(Z, Var(0)), Z, S(S(double(pred(Var(0))))))), dvd: Defn(name='dvd', decl=dvd, args=[n, m], body=Exists(p, m == n*p), ax=|= ForAll([n, m], dvd(n, m) == (Exists(p, m == n*p))), _subst_fun_body=Exists(p, Var(2) == Var(1)*p)), elts: Defn(name='elts', decl=elts, args=[A], body=Lambda(x, elem(x, A)), ax=|= ForAll(A, elts(A) == (Lambda(x, elem(x, A)))), _subst_fun_body=Lambda(x, elem(x, Var(1)))), empty: Defn(name='empty', decl=empty, args=[], body=Interval(1, 0), ax=|= empty == Interval(1, 0), _subst_fun_body=Interval(1, 0)), even: Defn(name='even', decl=even, args=[x], body=Exists(y, x == 2*y), ax=|= ForAll(x, even(x) == (Exists(y, x == 2*y))), _subst_fun_body=Exists(y, Var(1) == 2*y)), eventually: Defn(name='eventually', decl=eventually, args=[p], body=T_Bool(Lambda(t!763, Exists(dt!764, And(dt!764 >= 0, val(p)[t!763 + dt!764])))), ax=|= ForAll(p, eventually(p) == T_Bool(Lambda(t!763, Exists(dt!764, And(dt!764 >= 0, val(p)[t!763 + dt!764]))))), _subst_fun_body=T_Bool(Lambda(t!763, Exists(dt!764, And(dt!764 >= 0, val(Var(2))[t!763 + dt!764]))))), expi: Defn(name='expi', decl=expi, args=[t], body=C(cos(t), sin(t)), ax=|= ForAll(t, expi(t) == C(cos(t), sin(t))), _subst_fun_body=C(cos(Var(0)), sin(Var(0)))), fact: Defn(name='fact', decl=fact, args=[n], body=If(n <= 0, 1, n*fact(n - 1)), ax=|= ForAll(n, fact(n) == If(n <= 0, 1, n*fact(n - 1))), _subst_fun_body=If(Var(0) <= 0, 1, Var(0)*fact(Var(0) - 1))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!17, ForAll(x!16, A[x!16] == Contains(finwit!17, Unit(x!16)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!17, ForAll(x!16, A[x!16] == Contains(finwit!17, Unit(x!16)))))), _subst_fun_body=Exists(finwit!17, ForAll(x!16, Var(2)[x!16] == Contains(finwit!17, Unit(x!16))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!54, ForAll(x!53, A[x!53] == Contains(finwit!54, Unit(x!53)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!54, ForAll(x!53, A[x!53] == Contains(finwit!54, Unit(x!53)))))), _subst_fun_body=Exists(finwit!54, ForAll(x!53, Var(2)[x!53] == Contains(finwit!54, Unit(x!53))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!91, ForAll(x!90, A[x!90] == Contains(finwit!91, Unit(x!90)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!91, ForAll(x!90, A[x!90] == Contains(finwit!91, Unit(x!90)))))), _subst_fun_body=Exists(finwit!91, ForAll(x!90, Var(2)[x!90] == Contains(finwit!91, Unit(x!90))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!631, ForAll(x!630, A[x!630] == Contains(finwit!631, Unit(x!630)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!631, ForAll(x!630, A[x!630] == Contains(finwit!631, Unit(x!630)))))), _subst_fun_body=Exists(finwit!631, ForAll(x!630, Var(2)[x!630] == Contains(finwit!631, Unit(x!630))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!686, ForAll(x!685, A[x!685] == Contains(finwit!686, Unit(x!685)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!686, ForAll(x!685, A[x!685] == Contains(finwit!686, Unit(x!685)))))), _subst_fun_body=Exists(finwit!686, ForAll(x!685, Var(2)[x!685] == Contains(finwit!686, Unit(x!685))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!1315, ForAll(x!1314, A[x!1314] == Contains(finwit!1315, Unit(x!1314)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!1315, ForAll(x!1314, A[x!1314] == Contains(finwit!1315, Unit(x!1314)))))), _subst_fun_body=Exists(finwit!1315, ForAll(x!1314, Var(2)[x!1314] == Contains(finwit!1315, Unit(x!1314))))), finite: Defn(name='finite', decl=finite, args=[A], body=Exists(finwit!1375, ForAll(x!1374, A[x!1374] == Contains(finwit!1375, Unit(x!1374)))), ax=|= ForAll(A, finite(A) == (Exists(finwit!1375, ForAll(x!1374, A[x!1374] == Contains(finwit!1375, Unit(x!1374)))))), _subst_fun_body=Exists(finwit!1375, ForAll(x!1374, Var(2)[x!1374] == Contains(finwit!1375, Unit(x!1374))))), finsum: Defn(name='finsum', decl=finsum, args=[a, n], body=cumsum(a)[n], ax=|= ForAll([a, n], finsum(a, n) == cumsum(a)[n]), _subst_fun_body=cumsum(Var(0))[Var(1)]), floor: Defn(name='floor', decl=floor, args=[x], body=ToReal(ToInt(x)), ax=|= ForAll(x, floor(x) == ToReal(ToInt(x))), _subst_fun_body=ToReal(ToInt(Var(0)))), fresh: Defn(name='fresh', decl=fresh, args=[x, a], body=a != x, ax=|= ForAll([x, a], fresh(x, a) == a != x), _subst_fun_body=Var(1) != Var(0)), from_int: Defn(name='from_int', decl=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_fun_body=If(Var(0) <= 0, Z, S(from_int(Var(0) - 1)))), fst: Defn(name='fst', decl=fst, args=[p!800], body=pick(biginter(p!800)), ax=|= ForAll(p!800, fst(p!800) == pick(biginter(p!800))), _subst_fun_body=pick(biginter(Var(0)))), ge: Defn(name='ge', decl=ge, args=[x, y], body=T_Bool(Lambda(t, val(x)[t] >= val(y)[t])), ax=|= ForAll([x, y], ge(x, y) == T_Bool(Lambda(t, val(x)[t] >= val(y)[t]))), _subst_fun_body=T_Bool(Lambda(t, val(Var(1))[t] >= val(Var(2))[t]))), has_lim: Defn(name='has_lim', decl=has_lim, 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], has_lim(a, y) == (ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(a[n] - y) < eps))))))), _subst_fun_body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(Var(3)[n] - Var(4)) < eps)))))), has_lim_at: Defn(name='has_lim_at', decl=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_fun_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))))))), has_sum: Defn(name='has_sum', decl=has_sum, args=[a, y], body=has_lim(cumsum(a), y), ax=|= ForAll([a, y], has_sum(a, y) == has_lim(cumsum(a), y)), _subst_fun_body=has_lim(cumsum(Var(0)), Var(1))), iand: Defn(name='iand', decl=iand, args=[a, b], body=Prop(Lambda(w, And(val(a)[w], val(b)[w]))), ax=|= ForAll([a, b], iand(a, b) == Prop(Lambda(w, And(val(a)[w], val(b)[w])))), _subst_fun_body=Prop(Lambda(w, And(val(Var(1))[w], val(Var(2))[w])))), id: Defn(name='id', decl=id, args=[], body=Lambda(i, ToReal(i)), ax=|= id == (Lambda(i, ToReal(i))), _subst_fun_body=Lambda(i, ToReal(i))), ident: Defn(name='ident', decl=ident, args=[], body=Lambda(x, x), ax=|= ident == (Lambda(x, x)), _subst_fun_body=Lambda(x, x)), ieq: Defn(name='ieq', decl=ieq, args=[x, y], body=T_Bool(Lambda(t!792, val(x)[t!792] == val(y)[t!792])), ax=|= ForAll([x, y], ieq(x, y) == T_Bool(Lambda(t!792, val(x)[t!792] == val(y)[t!792]))), _subst_fun_body=T_Bool(Lambda(t!792, val(Var(1))[t!792] == val(Var(2))[t!792]))), if_int: Defn(name='if_int', decl=if_int, args=[p, x, y], body=T_Int(Lambda(t!795, If(val(p)[t!795], val(x)[t!795], val(y)[t!795]))), ax=|= ForAll([p, x, y], if_int(p, x, y) == T_Int(Lambda(t!795, If(val(p)[t!795], val(x)[t!795], val(y)[t!795])))), _subst_fun_body=T_Int(Lambda(t!795, If(val(Var(1))[t!795], val(Var(2))[t!795], val(Var(3))[t!795])))), iimpl: Defn(name='iimpl', decl=iimpl, args=[a, b], body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a)[u], val(b)[u]))))), ax=|= ForAll([a, b], iimpl(a, b) == Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a)[u], val(b)[u])))))), _subst_fun_body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(Var(2))[u], val(Var(3))[u])))))), ineq: Defn(name='ineq', decl=ineq, args=[x, y], body=T_Bool(Lambda(t!793, val(x)[t!793] != val(y)[t!793])), ax=|= ForAll([x, y], ineq(x, y) == T_Bool(Lambda(t!793, val(x)[t!793] != val(y)[t!793]))), _subst_fun_body=T_Bool(Lambda(t!793, val(Var(1))[t!793] != val(Var(2))[t!793]))), inext: Defn(name='inext', decl=inext, args=[x], body=T_Int(Lambda(t!794, val(x)[t!794 + 1])), ax=|= ForAll(x, inext(x) == T_Int(Lambda(t!794, val(x)[t!794 + 1]))), _subst_fun_body=T_Int(Lambda(t!794, val(Var(1))[t!794 + 1]))), inot: Defn(name='inot', decl=inot, args=[a], body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a)[u], val(Prop(K(World, False)))[u]))))), ax=|= ForAll(a, inot(a) == Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a)[u], val(Prop(K(World, False)))[u])))))), _subst_fun_body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(Var(2))[u], val(Prop(K(World, False)))[u])))))), inter: Defn(name='inter', decl=inter, args=[A, B], body=sep(A, Lambda(x, elem(x, B))), ax=|= ForAll([A, B], inter(A, B) == sep(A, Lambda(x, elem(x, B)))), _subst_fun_body=sep(Var(0), Lambda(x, elem(x, Var(2))))), ior: Defn(name='ior', decl=ior, args=[a, b], body=Prop(Lambda(w, Or(val(a)[w], val(b)[w]))), ax=|= ForAll([a, b], ior(a, b) == Prop(Lambda(w, Or(val(a)[w], val(b)[w])))), _subst_fun_body=Prop(Lambda(w, Or(val(Var(1))[w], val(Var(2))[w])))), is_cauchy: Defn(name='is_cauchy', decl=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_fun_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', decl=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_fun_body=Exists([c, r], circle(c, r) == Var(2))), is_cont: Defn(name='is_cont', decl=is_cont, args=[f], body=ForAll(x, cont_at(f, x)), ax=|= ForAll(f, is_cont(f) == (ForAll(x, cont_at(f, x)))), _subst_fun_body=ForAll(x, cont_at(Var(1), x))), is_conv: Defn(name='is_conv', decl=is_conv, args=[a], body=Exists(y, has_lim(a, y)), ax=|= ForAll(a, is_conv(a) == (Exists(y, has_lim(a, y)))), _subst_fun_body=Exists(y, has_lim(Var(1), y))), is_diff: Defn(name='is_diff', decl=is_diff, args=[f], body=ForAll(x, diff_at(f, x)), ax=|= ForAll(f, is_diff(f) == (ForAll(x, diff_at(f, x)))), _subst_fun_body=ForAll(x, diff_at(Var(1), x))), is_empty: Defn(name='is_empty', decl=is_empty, args=[I], body=hi(i) > lo(i), ax=|= ForAll(I, is_empty(I) == (hi(i) > lo(i))), _subst_fun_body=hi(i) > lo(i)), is_idem: Defn(name='is_idem', decl=is_idem, args=[A], body=mul(A, A) == A, ax=|= ForAll(A, is_idem(A) == (mul(A, A) == A)), _subst_fun_body=mul(Var(0), Var(0)) == Var(0)), is_lub: Defn(name='is_lub', decl=is_lub, args=[A, x], body=And(upper_bound(A, x), ForAll(y, Implies(upper_bound(A, y), le(x, y)))), ax=|= ForAll([A, x], is_lub(A, x) == And(upper_bound(A, x), ForAll(y, Implies(upper_bound(A, y), le(x, y))))), _subst_fun_body=And(upper_bound(Var(0), Var(1)), ForAll(y, Implies(upper_bound(Var(1), y), le(Var(2), y))))), is_open: Defn(name='is_open', decl=is_open, args=[S], body=ForAll(x!1226, Implies(S[x!1226], Exists(r!1229, And(0 < r!1229, subset(ball(x!1226, r!1229), S))))), ax=|= ForAll(S, is_open(S) == (ForAll(x!1226, Implies(S[x!1226], Exists(r!1229, And(0 < r!1229, subset(ball(x!1226, r!1229), S))))))), _subst_fun_body=ForAll(x!1226, Implies(Var(1)[x!1226], Exists(r!1229, And(0 < r!1229, subset(ball(x!1226, r!1229), Var(2))))))), is_orth: Defn(name='is_orth', decl=is_orth, args=[A], body=mul(A, trans(A)) == I, ax=|= ForAll(A, is_orth(A) == (mul(A, trans(A)) == I)), _subst_fun_body=mul(Var(0), trans(Var(0))) == I), is_pair: Defn(name='is_pair', decl=is_pair, args=[c!798], body=Exists([a!796, b!797], pair(a!796, b!797) == c!798), ax=|= ForAll(c!798, is_pair(c!798) == (Exists([a!796, b!797], pair(a!796, b!797) == c!798))), _subst_fun_body=Exists([a!796, b!797], pair(a!796, b!797) == Var(2))), is_set: Defn(name='is_set', decl=is_set, args=[P], body=Exists(A, reflects(P, A)), ax=|= ForAll(P, is_set(P) == (Exists(A, reflects(P, A)))), _subst_fun_body=Exists(A, reflects(Var(1), A))), is_summable: Defn(name='is_summable', decl=is_summable, args=[a], body=Exists(y, has_sum(a, y)), ax=|= ForAll(a, is_summable(a) == (Exists(y, has_sum(a, y)))), _subst_fun_body=Exists(y, has_sum(Var(1), y))), is_symm: Defn(name='is_symm', decl=is_symm, args=[A], body=trans(A) == A, ax=|= ForAll(A, is_symm(A) == (trans(A) == A)), _subst_fun_body=trans(Var(0)) == Var(0)), join: Defn(name='join', decl=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_fun_body=Interval(min(lo(Var(0)), lo(Var(1))), max(hi(Var(0)), hi(Var(1))))), krondelta: Defn(name='krondelta', decl=krondelta, args=[n], body=Lambda(i, If(i == n, 1, 0)), ax=|= ForAll(n, krondelta(n) == (Lambda(i, If(i == n, 1, 0)))), _subst_fun_body=Lambda(i, If(i == Var(1), 1, 0))), le: Defn(name='le', decl=le, args=[x, y], body=T_Bool(Lambda(t, val(x)[t] <= val(y)[t])), ax=|= ForAll([x, y], le(x, y) == T_Bool(Lambda(t, val(x)[t] <= val(y)[t]))), _subst_fun_body=T_Bool(Lambda(t, val(Var(1))[t] <= val(Var(2))[t]))), le: Defn(name='le', decl=le, args=[A, B], body=ForAll(x, Implies(elem(x, A), elem(x, B))), ax=|= ForAll([A, B], le(A, B) == (ForAll(x, Implies(elem(x, A), elem(x, B))))), _subst_fun_body=ForAll(x, Implies(elem(x, Var(1)), elem(x, Var(2))))), le: Defn(name='le', decl=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!1270)))))), 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!1270))))))), _subst_fun_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!1270))))))), lim: Defn(name='lim', decl=lim, args=[A!1449], body=f!1465(A!1449), ax=|= ForAll(A!1449, lim(A!1449) == f!1465(A!1449)), _subst_fun_body=f!1465(Var(0))), max: Defn(name='max', decl=max, args=[x, y], body=If(x >= y, x, y), ax=|= ForAll([x, y], max(x, y) == If(x >= y, x, y)), _subst_fun_body=If(Var(0) >= Var(1), Var(0), Var(1))), meet: Defn(name='meet', decl=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_fun_body=Interval(max(lo(Var(0)), lo(Var(1))), min(hi(Var(0)), hi(Var(1))))), mid: Defn(name='mid', decl=mid, args=[i], body=(lo(i) + hi(i))/2, ax=|= ForAll(i, mid(i) == (lo(i) + hi(i))/2), _subst_fun_body=(lo(Var(0)) + hi(Var(0)))/2), min: Defn(name='min', decl=min, args=[x, y], body=If(x <= y, x, y), ax=|= ForAll([x, y], min(x, y) == If(x <= y, x, y)), _subst_fun_body=If(Var(0) <= Var(1), Var(0), Var(1))), mu: Defn(name='mu', decl=mu, args=[A], body=mu_iter(A, 0), ax=|= ForAll(A, mu(A) == mu_iter(A, 0)), _subst_fun_body=mu_iter(Var(0), 0)), mu_iter: Defn(name='mu_iter', decl=mu_iter, args=[A, n], body=If(A[n], n, mu_iter(A, n + 1)), ax=|= ForAll([A, n], mu_iter(A, n) == If(A[n], n, mu_iter(A, n + 1))), _subst_fun_body=If(Var(0)[Var(1)], Var(1), mu_iter(Var(0), Var(1) + 1))), mul: Defn(name='mul', decl=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_fun_body=Lambda(x, Var(1)[x]*Var(2)[x])), mul: Defn(name='mul', decl=mul, args=[x, y], body=x*y, ax=|= ForAll([x, y], mul(x, y) == x*y), _subst_fun_body=Var(0)*Var(1)), mul: Defn(name='mul', decl=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_fun_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', decl=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_fun_body=Vec3(x0(Var(0))*x0(Var(1)), x1(Var(0))*x1(Var(1)), x2(Var(0))*x2(Var(1)))), mul: Defn(name='mul', decl=mul, args=[I, J], body=Interval(If(And(hi(I)*hi(J) <= lo(I)*lo(J), hi(I)*hi(J) <= hi(I)*lo(J), hi(I)*hi(J) <= lo(I)*hi(J)), hi(I)*hi(J), If(And(lo(I)*lo(J) <= hi(I)*lo(J), lo(I)*lo(J) <= lo(I)*hi(J)), lo(I)*lo(J), If(And(hi(I)*lo(J) <= lo(I)*hi(J)), hi(I)*lo(J), lo(I)*hi(J)))), If(And(hi(I)*hi(J) >= lo(I)*lo(J), hi(I)*hi(J) >= hi(I)*lo(J), hi(I)*hi(J) >= lo(I)*hi(J)), hi(I)*hi(J), If(And(lo(I)*lo(J) <= hi(I)*lo(J), lo(I)*lo(J) <= lo(I)*hi(J)), lo(I)*lo(J), If(And(hi(I)*lo(J) <= lo(I)*hi(J)), hi(I)*lo(J), lo(I)*hi(J))))), ax=|= ForAll([I, J], mul(I, J) == Interval(If(And(hi(I)*hi(J) <= lo(I)*lo(J), hi(I)*hi(J) <= hi(I)*lo(J), hi(I)*hi(J) <= lo(I)*hi(J)), hi(I)*hi(J), If(And(lo(I)*lo(J) <= hi(I)*lo(J), lo(I)*lo(J) <= lo(I)*hi(J)), lo(I)*lo(J), If(And(hi(I)*lo(J) <= lo(I)*hi(J)), hi(I)*lo(J), lo(I)*hi(J)))), If(And(hi(I)*hi(J) >= lo(I)*lo(J), hi(I)*hi(J) >= hi(I)*lo(J), hi(I)*hi(J) >= lo(I)*hi(J)), hi(I)*hi(J), If(And(lo(I)*lo(J) <= hi(I)*lo(J), lo(I)*lo(J) <= lo(I)*hi(J)), lo(I)*lo(J), If(And(hi(I)*lo(J) <= lo(I)*hi(J)), hi(I)*lo(J), lo(I)*hi(J)))))), _subst_fun_body=Interval(If(And(hi(Var(0))*hi(Var(1)) <= lo(Var(0))*lo(Var(1)), hi(Var(0))*hi(Var(1)) <= hi(Var(0))*lo(Var(1)), hi(Var(0))*hi(Var(1)) <= lo(Var(0))*hi(Var(1))), hi(Var(0))*hi(Var(1)), If(And(lo(Var(0))*lo(Var(1)) <= hi(Var(0))*lo(Var(1)), lo(Var(0))*lo(Var(1)) <= lo(Var(0))*hi(Var(1))), lo(Var(0))*lo(Var(1)), If(And(hi(Var(0))*lo(Var(1)) <= lo(Var(0))*hi(Var(1))), hi(Var(0))*lo(Var(1)), lo(Var(0))*hi(Var(1))))), If(And(hi(Var(0))*hi(Var(1)) >= lo(Var(0))*lo(Var(1)), hi(Var(0))*hi(Var(1)) >= hi(Var(0))*lo(Var(1)), hi(Var(0))*hi(Var(1)) >= lo(Var(0))*hi(Var(1))), hi(Var(0))*hi(Var(1)), If(And(lo(Var(0))*lo(Var(1)) <= hi(Var(0))*lo(Var(1)), lo(Var(0))*lo(Var(1)) <= lo(Var(0))*hi(Var(1))), lo(Var(0))*lo(Var(1)), If(And(hi(Var(0))*lo(Var(1)) <= lo(Var(0))*hi(Var(1))), hi(Var(0))*lo(Var(1)), lo(Var(0))*hi(Var(1))))))), mul: Defn(name='mul', decl=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_fun_body=Lambda(i, Var(1)[i]*Var(2)[i])), neg: Defn(name='neg', decl=neg, args=[u], body=Vec2(-x(u), -y(u)), ax=|= ForAll(u, neg(u) == Vec2(-x(u), -y(u))), _subst_fun_body=Vec2(-x(Var(0)), -y(Var(0)))), neg: Defn(name='neg', decl=neg, args=[u], body=Vec3(-x0(u), -x1(u), -x2(u)), ax=|= ForAll(u, neg(u) == Vec3(-x0(u), -x1(u), -x2(u))), _subst_fun_body=Vec3(-x0(Var(0)), -x1(Var(0)), -x2(Var(0)))), neg: Defn(name='neg', decl=neg, args=[a], body=Lambda(i, -a[i]), ax=|= ForAll(a, neg(a) == (Lambda(i, -a[i]))), _subst_fun_body=Lambda(i, -Var(1)[i])), next: Defn(name='next', decl=next, args=[p], body=T_Bool(Lambda(t!767, val(p)[t!767 + 1])), ax=|= ForAll(p, next(p) == T_Bool(Lambda(t!767, val(p)[t!767 + 1]))), _subst_fun_body=T_Bool(Lambda(t!767, val(Var(1))[t!767 + 1]))), nonneg: Defn(name='nonneg', decl=nonneg, args=[x], body=absR(x) == x, ax=|= ForAll(x, nonneg(x) == (absR(x) == x)), _subst_fun_body=absR(Var(0)) == Var(0)), norm2: Defn(name='norm2', decl=norm2, args=[z], body=mul(z, conj(z)), ax=|= ForAll(z, norm2(z) == mul(z, conj(z))), _subst_fun_body=mul(Var(0), conj(Var(0)))), norm2: Defn(name='norm2', decl=norm2, args=[u], body=dot(u, u), ax=|= ForAll(u, norm2(u) == dot(u, u)), _subst_fun_body=dot(Var(0), Var(0))), norm2: Defn(name='norm2', decl=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_fun_body=x0(Var(0))*x0(Var(0)) + x1(Var(0))*x1(Var(0)) + x2(Var(0))*x2(Var(0))), odd: Defn(name='odd', decl=odd, args=[x], body=Exists(y, x == 2*y + 1), ax=|= ForAll(x, odd(x) == (Exists(y, x == 2*y + 1))), _subst_fun_body=Exists(y, Var(1) == 2*y + 1)), one: Defn(name='one', decl=one, args=[], body=1, ax=|= one == 1, _subst_fun_body=1), ones: Defn(name='ones', decl=ones, args=[n], body=NDArray(Unit(n), K(Int, 1)), ax=|= ForAll(n, ones(n) == NDArray(Unit(n), K(Int, 1))), _subst_fun_body=NDArray(Unit(Var(0)), K(Int, 1))), open: Defn(name='open', decl=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_fun_body=Or(Var(0) == K(Sierpinski, False), Var(0) == K(Sierpinski, True), Var(0) == Store(K(Sierpinski, False), S1, True))), pair: Defn(name='pair', decl=pair, args=[a!796, b!797], body=upair(sing(a!796), upair(a!796, b!797)), ax=|= ForAll([a!796, b!797], pair(a!796, b!797) == upair(sing(a!796), upair(a!796, b!797))), _subst_fun_body=upair(sing(Var(0)), upair(Var(0), Var(1)))), pick: Defn(name='pick', decl=pick, args=[a!796], body=f!814(a!796), ax=|= ForAll(a!796, pick(a!796) == f!814(a!796)), _subst_fun_body=f!814(Var(0))), pos: Defn(name='pos', decl=pos, args=[a], body=Lambda(i, If(i >= 0, a[i], 0)), ax=|= ForAll(a, pos(a) == (Lambda(i, If(i >= 0, a[i], 0)))), _subst_fun_body=Lambda(i, If(i >= 0, Var(1)[i], 0))), pow: Defn(name='pow', decl=pow, args=[x, y], body=x**y, ax=|= ForAll([x, y], pow(x, y) == x**y), _subst_fun_body=Var(0)**Var(1)), powers: Defn(name='powers', decl=powers, args=[x], body=Lambda(i, If(i == 0, 1, If(i < 0, powers(x)[i + 1]/x, x*powers(x)[i - 1]))), ax=|= ForAll(x, powers(x) == (Lambda(i, If(i == 0, 1, If(i < 0, powers(x)[i + 1]/x, x*powers(x)[i - 1]))))), _subst_fun_body=Lambda(i, If(i == 0, 1, If(i < 0, powers(Var(1))[i + 1]/Var(1), Var(1)*powers(Var(1))[i - 1])))), prime: Defn(name='prime', decl=prime, args=[n], body=And(n > 1, Not(Exists([p, q], And(p > 1, q > 1, n == p*q)))), ax=|= ForAll(n, prime(n) == And(n > 1, Not(Exists([p, q], And(p > 1, q > 1, n == p*q))))), _subst_fun_body=And(Var(0) > 1, Not(Exists([p, q], And(p > 1, q > 1, Var(2) == p*q))))), reflects: Defn(name='reflects', decl=reflects, args=[P, A], body=ForAll(x, elem(x, A) == P[x]), ax=|= ForAll([P, A], reflects(P, A) == (ForAll(x, elem(x, A) == P[x]))), _subst_fun_body=ForAll(x, elem(x, Var(2)) == Var(1)[x])), rev: Defn(name='rev', decl=rev, args=[a], body=Lambda(i, a[-i]), ax=|= ForAll(a, rev(a) == (Lambda(i, a[-i]))), _subst_fun_body=Lambda(i, Var(1)[-i])), safe_pred: Defn(name='safe_pred', decl=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_fun_body=If(is(Z, Var(0)), Z, pred(Var(0)))), select_16_be: Defn(name='select_16_be', decl=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_fun_body=Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1])), select_16_be: Defn(name='select_16_be', decl=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_fun_body=Concat(Var(0)[Var(1) + 0], Var(0)[Var(1) + 1])), select_16_le: Defn(name='select_16_le', decl=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_fun_body=Concat(Var(0)[Var(1) + 2 - 0 - 1], Var(0)[Var(1) + 2 - 1 - 1])), select_16_le: Defn(name='select_16_le', decl=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_fun_body=Concat(Var(0)[Var(1) + 2 - 0 - 1], Var(0)[Var(1) + 2 - 1 - 1])), select_32_be: Defn(name='select_32_be', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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', decl=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_fun_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])), setof: Defn(name='setof', decl=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_fun_body=Lambda(x, And(lo(Var(1)) <= x, x <= hi(Var(1))))), sgn: Defn(name='sgn', decl=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_fun_body=If(Var(0) > 0, 1, If(Var(0) < 0, -1, 0))), shift: Defn(name='shift', decl=shift, args=[a, n], body=Lambda(i, a[i - n]), ax=|= ForAll([a, n], shift(a, n) == (Lambda(i, a[i - n]))), _subst_fun_body=Lambda(i, Var(1)[i - Var(2)])), sin: Defn(name='sin', decl=sin, args=[a], body=Map(sin, a), ax=|= ForAll(a, sin(a) == Map(sin, a)), _subst_fun_body=Map(sin, Var(0))), sing: Defn(name='sing', decl=sing, args=[x], body=upair(x, x), ax=|= ForAll(x, sing(x) == upair(x, x)), _subst_fun_body=upair(Var(0), Var(0))), snd: Defn(name='snd', decl=snd, args=[p!800], body=If(sing(sing(fst(p!800))) == p!800, fst(p!800), pick(sub(bigunion(p!800), sing(fst(p!800))))), ax=|= ForAll(p!800, snd(p!800) == If(sing(sing(fst(p!800))) == p!800, fst(p!800), pick(sub(bigunion(p!800), sing(fst(p!800)))))), _subst_fun_body=If(sing(sing(fst(Var(0)))) == Var(0), fst(Var(0)), pick(sub(bigunion(Var(0)), sing(fst(Var(0))))))), sqr: Defn(name='sqr', decl=sqr, args=[x], body=x*x, ax=|= ForAll(x, sqr(x) == x*x), _subst_fun_body=Var(0)*Var(0)), sqrt: Defn(name='sqrt', decl=sqrt, args=[x], body=x**(1/2), ax=|= ForAll(x, sqrt(x) == x**(1/2)), _subst_fun_body=Var(0)**(1/2)), sub: Defn(name='sub', decl=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_fun_body=Lambda(x, Var(1)[x] - Var(2)[x])), sub: Defn(name='sub', decl=sub, args=[x, y], body=x - y, ax=|= ForAll([x, y], sub(x, y) == x - y), _subst_fun_body=Var(0) - Var(1)), sub: Defn(name='sub', decl=sub, args=[A, B], body=sep(A, Lambda(x, Not(elem(x, B)))), ax=|= ForAll([A, B], sub(A, B) == sep(A, Lambda(x, Not(elem(x, B))))), _subst_fun_body=sep(Var(0), Lambda(x, Not(elem(x, Var(2)))))), sub: Defn(name='sub', decl=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_fun_body=Vec2(x(Var(0)) - x(Var(1)), y(Var(0)) - y(Var(1)))), sub: Defn(name='sub', decl=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_fun_body=Vec3(x0(Var(0)) - x0(Var(1)), x1(Var(0)) - x1(Var(1)), x2(Var(0)) - x2(Var(1)))), sub: Defn(name='sub', decl=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_fun_body=Interval(lo(Var(0)) - hi(Var(1)), hi(Var(0)) - lo(Var(1)))), sub: Defn(name='sub', decl=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_fun_body=Lambda(i, Var(1)[i] - Var(2)[i])), swap: Defn(name='swap', decl=swap, args=[x, a, b], body=If(x == a, b, If(x == b, a, x)), ax=|= ForAll([x, a, b], swap(x, a, b) == If(x == a, b, If(x == b, a, x))), _subst_fun_body=If(Var(0) == Var(1), Var(2), If(Var(0) == Var(2), Var(1), Var(0)))), tan: Defn(name='tan', decl=tan, args=[x], body=sin(x)/cos(x), ax=|= ForAll(x, tan(x) == sin(x)/cos(x)), _subst_fun_body=sin(Var(0))/cos(Var(0))), tand: Defn(name='tand', decl=tand, args=[p, q], body=T_Bool(Lambda(t!760, And(val(p)[t!760], val(q)[t!760]))), ax=|= ForAll([p, q], tand(p, q) == T_Bool(Lambda(t!760, And(val(p)[t!760], val(q)[t!760])))), _subst_fun_body=T_Bool(Lambda(t!760, And(val(Var(1))[t!760], val(Var(2))[t!760])))), timpl: Defn(name='timpl', decl=timpl, args=[p, q], body=T_Bool(Lambda(t!762, Implies(val(p)[t!762], val(q)[t!762]))), ax=|= ForAll([p, q], timpl(p, q) == T_Bool(Lambda(t!762, Implies(val(p)[t!762], val(q)[t!762])))), _subst_fun_body=T_Bool(Lambda(t!762, Implies(val(Var(1))[t!762], val(Var(2))[t!762])))), tint: Defn(name='tint', decl=tint, args=[x], body=T_Int(K(Int, x)), ax=|= ForAll(x, tint(x) == T_Int(K(Int, x))), _subst_fun_body=T_Int(K(Int, Var(0)))), tnot: Defn(name='tnot', decl=tnot, args=[p], body=T_Bool(Lambda(t!759, Not(val(p)[t!759]))), ax=|= ForAll(p, tnot(p) == T_Bool(Lambda(t!759, Not(val(p)[t!759])))), _subst_fun_body=T_Bool(Lambda(t!759, Not(val(Var(1))[t!759])))), to_int: Defn(name='to_int', decl=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_fun_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', decl=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_fun_body=If(is(Z, Var(0)), 0, 1 + to_int(pred(Var(0))))), tor: Defn(name='tor', decl=tor, args=[p, q], body=T_Bool(Lambda(t!761, Or(val(p)[t!761], val(q)[t!761]))), ax=|= ForAll([p, q], tor(p, q) == T_Bool(Lambda(t!761, Or(val(p)[t!761], val(q)[t!761])))), _subst_fun_body=T_Bool(Lambda(t!761, Or(val(Var(1))[t!761], val(Var(2))[t!761])))), union: Defn(name='union', decl=union, args=[A, B], body=bigunion(upair(A, B)), ax=|= ForAll([A, B], union(A, B) == bigunion(upair(A, B))), _subst_fun_body=bigunion(upair(Var(0), Var(1)))), upper_bound: Defn(name='upper_bound', decl=upper_bound, args=[A, x], body=ForAll(y, Implies(A[y], le(y, x))), ax=|= ForAll([A, x], upper_bound(A, x) == (ForAll(y, Implies(A[y], le(y, x))))), _subst_fun_body=ForAll(y, Implies(Var(1)[y], le(y, Var(2))))), valid: Defn(name='valid', decl=valid, args=[a], body=ForAll(w, val(a)[w]), ax=|= ForAll(a, valid(a) == (ForAll(w, val(a)[w]))), _subst_fun_body=ForAll(w, val(Var(1))[w])), valid: Defn(name='valid', decl=valid, args=[p], body=val(p)[0], ax=|= ForAll(p, valid(p) == val(p)[0]), _subst_fun_body=val(Var(0))[0]), wf: Defn(name='wf', decl=wf, args=[x], body=Implies(is(real, x), val(x) >= 0), ax=|= ForAll(x, wf(x) == Implies(is(real, x), val(x) >= 0)), _subst_fun_body=Implies(is(real, Var(0)), val(Var(0)) >= 0)), where: Defn(name='where', decl=where, args=[mask, a, b], body=Lambda(i, If(mask[i], a[i], b[i])), ax=|= ForAll([mask, a, b], where(mask, a, b) == (Lambda(i, If(mask[i], a[i], b[i])))), _subst_fun_body=Lambda(i, If(Var(1)[i], Var(2)[i], Var(3)[i]))), width: Defn(name='width', decl=width, args=[i], body=hi(i) - lo(i), ax=|= ForAll(i, width(i) == hi(i) - lo(i)), _subst_fun_body=hi(Var(0)) - lo(Var(0))), zero: Defn(name='zero', decl=zero, args=[], body=0, ax=|= zero == 0, _subst_fun_body=0), zero: Defn(name='zero', decl=zero, args=[n], body=NDArray(Unit(n), K(Int, 0)), ax=|= ForAll(n, zero(n) == NDArray(Unit(n), K(Int, 0))), _subst_fun_body=NDArray(Unit(Var(0)), K(Int, 0))), zero: Defn(name='zero', decl=zero, args=[], body=K(Int, 0), ax=|= zero == K(Int, 0), _subst_fun_body=K(Int, 0))}: defn holds definitional axioms for function symbols.

kdrag.kernel.ext(domain: Sequence[SortRef], range_: SortRef) → Proof

>>> ext([smt.IntSort()], smt.IntSort())
|= ForAll([f, g], (f == g) == (ForAll(x0, f[x0] == g[x0])))
>>> ext([smt.IntSort(), smt.RealSort()], smt.IntSort())
|= ForAll([f, g],
       (f == g) ==
       (ForAll([x0, x1],
               Select(f, x0, x1) == Select(g, x0, x1))))

Parameters:

domain (Sequence[SortRef])
range_ (SortRef)

Return type:

Proof

kdrag.kernel.forget(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.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]

>>> x = smt.Int("x")
>>> herb(smt.ForAll([x], x >= x))
([x!...], |=  Implies(x!... >= x!..., ForAll(x, x >= x)))

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.obtain(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

>>> x = smt.Int("x")
>>> obtain(smt.Exists([x], x >= 0))
([x!...], |=  Implies(Exists(x, x >= 0), x!... >= 0))
>>> y = FreshVar("y", smt.IntSort())
>>> obtain(smt.Exists([x], x >= y))
([f!...(y!...)], |=  Implies(Exists(x, x >= y!...), f!...(y!...) >= y!...))

Parameters:: thm (QuantifierRef)
Return type:: tuple[list[ExprRef], 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.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.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]