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[, ctx, auto_fresh])	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.
`choose`(pf)	Convert a theorem of the form `\|= forall xs, exists y0 y1.
`compose`(ab, bc)	Compose two implications.
`decl_occurs`(f, body)	Check if symbol f appears in body.
`declare`(name, *sorts)	Reserve a name.
`define`(name, args, body)	Define a non recursive definition.
`define_fix`(name, args, retsort, fix_lam)	Define a recursive definition.
`define_simple`(name, args, body)	A simple non recursive definition is a conservative extension https://en.wikipedia.org/wiki/Conservative_extension
`ext`(domain, range_)
`forget`(ts, thm)	"Forget" a term using existentials.
`free_vars`(e)	Get an overapproximation of free variables in a term.
`fresh_const`(q[, prefixes])	Generate fresh constants of same sort as quantifier.
`generalize`(vs, pf)	Generalize a theorem with respect to a list of schema variables.
`herb`(thm[, prefixes])	Herbrandize a theorem.
`induct_inductive`(x, P)	Build a basic induction principle for an algebraic datatype
`instan`(ts, pf)	Instantiate a universally quantified formula.
`is_declared`(e)
`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)
`make_unfolding`(pf)	Take an axiom of the form \|= forall x0 x1 ..., xn, f(x0, x1, ..., xn) = body and return a Defn object for f. Unfolding judgments can be used with unfold_defns.
`modus`(ab, a)	Modus ponens for implies and equality.
`obtain`(thm)	Skolemize an existential quantifier.
`open_binder`(lam)	Open a quantifier with fresh variables.
`prove`(thm[, by, admit, timeout, dump, solver])	Prove a theorem using a list of previously proved lemmas.
`register_definition`(defn)	Can register other unfoldings besides those generated by define.
`rename_vars2`(pf, vs[, patterns, no_patterns])	Rename bound variables and also attach triggers
`specialize`(ts, thm)	Instantiate a universally quantified formula forall xs, P(xs) -> P(ts) This is forall elimination
`subst`(t, eqs)	Substitute using equality proofs
`trigger`(pf[, patterns, no_patterns])	Add e-matching triggers to a quantified proof.
`unfold`(e, decls)	Unfold function definitions in an expression.
`unfold_defns`(e, defns)	Unfold definitions in an expression.

Classes

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

Exceptions

LemmaError

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, ctx=None, auto_fresh=False) → Datatype

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

>>> Nat = Inductive("Nat909")
>>> 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(note, /): Add a note to the exception

args

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

class kdrag.kernel.Unfolding(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. It’s more a recognition of a fact in unfoldable form

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.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.choose(pf: Proof) → tuple[list[FuncDeclRef], Proof]

Convert a theorem of the form |= forall xs, exists y0 y1… , P(xs, y0, y1, …) to |= forall xs, P(xs, f0(xs), f1(xs), …).

>>> x,y,z = smt.Ints("x y z")
>>> pf = kd.prove(smt.ForAll([x], smt.Exists([y], y >= x)))
>>> choose(pf)
([f!...], |= ForAll(x!..., f!...(x!...) >= x!...))

Parameters:: pf (Proof)
Return type:: tuple[list[FuncDeclRef], 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.decl_occurs(f: FuncDeclRef, body: ExprRef) → bool

Check if symbol f appears in body.

>>> x = smt.Int("x")
>>> y = smt.Bool("y")
>>> f = smt.Function("f", smt.IntSort(), smt.BoolSort(), smt.IntSort())
>>> assert decl_occurs(f, 1 + f(x, y))
>>> assert not decl_occurs(f, x + y + 1)

Parameters:

f (FuncDeclRef)
body (ExprRef)

Return type:

bool

kdrag.kernel.declare(name: str, *sorts: SortRef) → FuncDeclRef

Reserve a name. This helps avoid accidental clashing of axioms over the same symbol. It also make serialization possible and easier.

>>> declare("reserved_example", smt.IntSort())
reserved_example
>>> declare("reserved_example", smt.IntSort())
Traceback (most recent call last):
    ...
ValueError: ('Declaration name already reserved: reserved_example', 'with sorts', [], Int)

Parameters:

name (str)
sorts (SortRef)

Return type:

FuncDeclRef

kdrag.kernel.define(name: str, args: list[ExprRef], body: ExprRef) → 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.define_simple(name: str, args: list[ExprRef], body: ExprRef) → FuncDeclRef

A simple non recursive definition is a conservative extension https://en.wikipedia.org/wiki/Conservative_extension

>>> x = smt.Int("x")
>>> define_simple("mysucc9034", [x], x + 1)
mysucc9034
>>> f = smt.Function("f102", smt.IntSort(), smt.IntSort())
>>> define_simple("f102", [x], f(x))
Traceback (most recent call last):
    ...
ValueError: ('Symbol appears in it's own definition. This is not a simple definition and requires further checks for consistency', f102, f102(x))

Parameters:

name (str)
args (list[ExprRef])
body (ExprRef)

Return type:

FuncDeclRef

kdrag.kernel.defns: dict[FuncDeclRef, Unfolding] = {(Array (Array Sierpinski Bool) Bool).finite: Unfolding(name='(Array (Array Sierpinski Bool) Bool).finite', decl=(Array (Array Sierpinski Bool) Bool).finite, args=[], body=Exists(finwit!981, ForAll(x!980, A!982[x!980] == Contains(finwit!981, Unit(x!980)))), ax=|= ForAll(A, (Array (Array Sierpinski Bool) Bool).finite(A) == (Exists(finwit!981, ForAll(x!980, A[x!980] == Contains(finwit!981, Unit(x!980)))))), _subst_fun_body=Exists(finwit!981, ForAll(x!980, Var(2)[x!980] == Contains(finwit!981, Unit(x!980))))), (Array Bool Bool).choose: Unfolding(name='(Array Bool Bool).choose', decl=(Array Bool Bool).choose, args=[], body=If(P!207[True], True, False), ax=|= ForAll(P, (Array Bool Bool).choose(P) == If(P[True], True, False)), _subst_fun_body=If(Var(0)[True], True, False)), (Array Bool Bool).finite: Unfolding(name='(Array Bool Bool).finite', decl=(Array Bool Bool).finite, args=[], body=Exists(finwit!99, ForAll(x!98, A!100[x!98] == Contains(finwit!99, Unit(x!98)))), ax=|= ForAll(A, (Array Bool Bool).finite(A) == (Exists(finwit!99, ForAll(x!98, A[x!98] == Contains(finwit!99, Unit(x!98)))))), _subst_fun_body=Exists(finwit!99, ForAll(x!98, Var(2)[x!98] == Contains(finwit!99, Unit(x!98))))), (Array EReal Bool).finite: Unfolding(name='(Array EReal Bool).finite', decl=(Array EReal Bool).finite, args=[], body=Exists(finwit!1248, ForAll(x!1247, A!1249[x!1247] == Contains(finwit!1248, Unit(x!1247)))), ax=|= ForAll(A, (Array EReal Bool).finite(A) == (Exists(finwit!1248, ForAll(x!1247, A[x!1247] == Contains(finwit!1248, Unit(x!1247)))))), _subst_fun_body=Exists(finwit!1248, ForAll(x!1247, Var(2)[x!1247] == Contains(finwit!1248, Unit(x!1247))))), (Array Int Bool).choose: Unfolding(name='(Array Int Bool).choose', decl=(Array Int Bool).choose, args=[], body=search(P!326, 0), ax=|= ForAll(P, (Array Int Bool).choose(P) == search(P, 0)), _subst_fun_body=search(Var(0), 0)), (Array Int Bool).finite: Unfolding(name='(Array Int Bool).finite', decl=(Array Int Bool).finite, args=[], body=Exists(finwit!61, ForAll(x!60, A!62[x!60] == Contains(finwit!61, Unit(x!60)))), ax=|= ForAll(A, (Array Int Bool).finite(A) == (Exists(finwit!61, ForAll(x!60, A[x!60] == Contains(finwit!61, Unit(x!60)))))), _subst_fun_body=Exists(finwit!61, ForAll(x!60, Var(2)[x!60] == Contains(finwit!61, Unit(x!60))))), (Array Int Real).add: Unfolding(name='(Array Int Real).add', decl=(Array Int Real).add, args=[], body=Lambda(i, a!1446[i] + b!1447[i]), ax=|= ForAll([a, b], (Array Int Real).add(a, b) == (Lambda(i, a[i] + b[i]))), _subst_fun_body=Lambda(i, Var(1)[i] + Var(2)[i])), (Array Int Real).div_: Unfolding(name='(Array Int Real).div_', decl=(Array Int Real).div_, args=[], body=Lambda(i, a!1456[i]/b!1457[i]), ax=|= ForAll([a, b], (Array Int Real).div_(a, b) == (Lambda(i, a[i]/b[i]))), _subst_fun_body=Lambda(i, Var(1)[i]/Var(2)[i])), (Array Int Real).mul: Unfolding(name='(Array Int Real).mul', decl=(Array Int Real).mul, args=[], body=Lambda(i, a!1454[i]*b!1455[i]), ax=|= ForAll([a, b], (Array Int Real).mul(a, b) == (Lambda(i, a[i]*b[i]))), _subst_fun_body=Lambda(i, Var(1)[i]*Var(2)[i])), (Array Int Real).neg: Unfolding(name='(Array Int Real).neg', decl=(Array Int Real).neg, args=[], body=Lambda(i, -a!1458[i]), ax=|= ForAll(a, (Array Int Real).neg(a) == (Lambda(i, -a[i]))), _subst_fun_body=Lambda(i, -Var(1)[i])), (Array Int Real).sub: Unfolding(name='(Array Int Real).sub', decl=(Array Int Real).sub, args=[], body=Lambda(i, a!1452[i] - b!1453[i]), ax=|= ForAll([a, b], (Array Int Real).sub(a, b) == (Lambda(i, a[i] - b[i]))), _subst_fun_body=Lambda(i, Var(1)[i] - Var(2)[i])), (Array Real Bool).finite: Unfolding(name='(Array Real Bool).finite', decl=(Array Real Bool).finite, args=[], body=Exists(finwit!23, ForAll(x!22, A!24[x!22] == Contains(finwit!23, Unit(x!22)))), ax=|= ForAll(A, (Array Real Bool).finite(A) == (Exists(finwit!23, ForAll(x!22, A[x!22] == Contains(finwit!23, Unit(x!22)))))), _subst_fun_body=Exists(finwit!23, ForAll(x!22, Var(2)[x!22] == Contains(finwit!23, Unit(x!22))))), (Array Real Real).add: Unfolding(name='(Array Real Real).add', decl=(Array Real Real).add, args=[], body=Lambda(x, f!400[x] + g!401[x]), ax=|= ForAll([f, g], (Array Real Real).add(f, g) == (Lambda(x, f[x] + g[x]))), _subst_fun_body=Lambda(x, Var(1)[x] + Var(2)[x])), (Array Real Real).div_: Unfolding(name='(Array Real Real).div_', decl=(Array Real Real).div_, args=[], body=Lambda(x, f!406[x]/g!407[x]), ax=|= ForAll([f, g], (Array Real Real).div_(f, g) == (Lambda(x, f[x]/g[x]))), _subst_fun_body=Lambda(x, Var(1)[x]/Var(2)[x])), (Array Real Real).mul: Unfolding(name='(Array Real Real).mul', decl=(Array Real Real).mul, args=[], body=Lambda(x, f!404[x]*g!405[x]), ax=|= ForAll([f, g], (Array Real Real).mul(f, g) == (Lambda(x, f[x]*g[x]))), _subst_fun_body=Lambda(x, Var(1)[x]*Var(2)[x])), (Array Real Real).sub: Unfolding(name='(Array Real Real).sub', decl=(Array Real Real).sub, args=[], body=Lambda(x, f!402[x] - g!403[x]), ax=|= ForAll([f, g], (Array Real Real).sub(f, g) == (Lambda(x, f[x] - g[x]))), _subst_fun_body=Lambda(x, Var(1)[x] - Var(2)[x])), (Array Sierpinski Bool).finite: Unfolding(name='(Array Sierpinski Bool).finite', decl=(Array Sierpinski Bool).finite, args=[], body=Exists(finwit!925, ForAll(x!924, A!926[x!924] == Contains(finwit!925, Unit(x!924)))), ax=|= ForAll(A, (Array Sierpinski Bool).finite(A) == (Exists(finwit!925, ForAll(x!924, A[x!924] == Contains(finwit!925, Unit(x!924)))))), _subst_fun_body=Exists(finwit!925, ForAll(x!924, Var(2)[x!924] == Contains(finwit!925, Unit(x!924))))), (Array Sierpinski Bool).open: Unfolding(name='(Array Sierpinski Bool).open', decl=(Array Sierpinski Bool).open, args=[], body=Or(A!1010 == K(Sierpinski, False), A!1010 == K(Sierpinski, True), A!1010 == Store(K(Sierpinski, False), S1, True)), ax=|= ForAll(A, (Array Sierpinski Bool).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))), (Array Vec2 Bool).finite: Unfolding(name='(Array Vec2 Bool).finite', decl=(Array Vec2 Bool).finite, args=[], body=Exists(finwit!1357, ForAll(x!1356, A!1358[x!1356] == Contains(finwit!1357, Unit(x!1356)))), ax=|= ForAll(A, (Array Vec2 Bool).finite(A) == (Exists(finwit!1357, ForAll(x!1356, A[x!1356] == Contains(finwit!1357, Unit(x!1356)))))), _subst_fun_body=Exists(finwit!1357, ForAll(x!1356, Var(2)[x!1356] == Contains(finwit!1357, Unit(x!1356))))), Atom.fresh: Unfolding(name='Atom.fresh', decl=Atom.fresh, args=[], body=a!1073 != x!1072, ax=|= ForAll([x, a], Atom.fresh(x, a) == a != x), _subst_fun_body=Var(1) != Var(0)), Atom.swap: Unfolding(name='Atom.swap', decl=Atom.swap, args=[], body=If(x!1074 == a!1075, b!1076, If(x!1074 == b!1076, a!1075, x!1074)), ax=|= ForAll([x, a, b], Atom.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)))), BitVecN.to_int: Unfolding(name='BitVecN.to_int', decl=BitVecN.to_int, args=[], body=If(Length(val(x!188)) == 0, 0, BV2Int(Nth(val(x!188), 0)) + 2* BitVecN.to_int(BitVecN(seq.extract(val(x!188), 1, Length(val(x!188)) - 1)))), ax=|= ForAll(x, BitVecN.to_int(x) == If(Length(val(x)) == 0, 0, BV2Int(Nth(val(x), 0)) + 2* BitVecN.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* BitVecN.to_int(BitVecN(seq.extract(val(Var(0)), 1, Length(val(Var(0))) - 1))))), C.add: Unfolding(name='C.add', decl=C.add, args=[], body=C(re(z1!0) + re(z2!1), im(z1!0) + im(z2!1)), ax=|= ForAll([z1, z2], C.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)))), C.div_: Unfolding(name='C.div_', decl=C.div_, args=[], body=C((re(z1!4)*re(z2!5) + im(z1!4)*im(z2!5))/ (re(z2!5)**2 + im(z2!5)**2), (im(z1!4)*re(z2!5) - re(z1!4)*im(z2!5))/ (re(z2!5)**2 + im(z2!5)**2)), ax=|= ForAll([z1, z2], C.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))), C.mul: Unfolding(name='C.mul', decl=C.mul, args=[], body=C(re(z1!2)*re(z2!3) - im(z1!2)*im(z2!3), re(z1!2)*im(z2!3) + im(z1!2)*re(z2!3)), ax=|= ForAll([z1, z2], C.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)))), C.norm2: Unfolding(name='C.norm2', decl=C.norm2, args=[], body=C.mul(z!1185, conj(z!1185)), ax=|= ForAll(z, C.norm2(z) == C.mul(z, conj(z))), _subst_fun_body=C.mul(Var(0), conj(Var(0)))), EPosReal.wf: Unfolding(name='EPosReal.wf', decl=EPosReal.wf, args=[], body=Implies(is(real, x!1281), val(x!1281) >= 0), ax=|= ForAll(x, EPosReal.wf(x) == Implies(is(real, x), val(x) >= 0)), _subst_fun_body=Implies(is(real, Var(0)), val(Var(0)) >= 0)), EReal.add: Unfolding(name='EReal.add', decl=EReal.add, args=[], body=If(And(is(Real, x!1208), is(Real, y!1209)), Real(val(x!1208) + val(y!1209)), If(And(is(Inf, x!1208), Not(is(NegInf, y!1209))), Inf, If(And(Not(is(NegInf, x!1208)), is(Inf, y!1209)), Inf, If(And(is(NegInf, x!1208), Not(is(Inf, y!1209))), NegInf, If(And(Not(is(Inf, x!1208)), is(NegInf, y!1209)), NegInf, add_undef(x!1208, y!1209)))))), ax=|= ForAll([x, y], EReal.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)))))))), EReal.le: Unfolding(name='EReal.le', decl=EReal.le, args=[], body=If(x!1198 == y!1199, True, If(is(NegInf, x!1198), True, If(is(Inf, y!1199), True, If(is(NegInf, y!1199), False, If(is(Inf, x!1198), False, If(And(is(Real, x!1198), is(Real, y!1199)), val(x!1198) <= val(y!1199), unreachable!1197)))))), ax=|= ForAll([x, y], EReal.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!1197))))))), _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!1197))))))), Interval.add: Unfolding(name='Interval.add', decl=Interval.add, args=[], body=Interval(lo(i!1406) + lo(j!1407), hi(i!1406) + hi(j!1407)), ax=|= ForAll([i, j], Interval.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)))), Interval.mul: Unfolding(name='Interval.mul', decl=Interval.mul, args=[], body=Interval(If(And(hi(I!1420)*hi(J!1421) <= lo(I!1420)*lo(J!1421), hi(I!1420)*hi(J!1421) <= hi(I!1420)*lo(J!1421), hi(I!1420)*hi(J!1421) <= lo(I!1420)*hi(J!1421)), hi(I!1420)*hi(J!1421), If(And(lo(I!1420)*lo(J!1421) <= hi(I!1420)*lo(J!1421), lo(I!1420)*lo(J!1421) <= lo(I!1420)*hi(J!1421)), lo(I!1420)*lo(J!1421), If(And(hi(I!1420)*lo(J!1421) <= lo(I!1420)*hi(J!1421)), hi(I!1420)*lo(J!1421), lo(I!1420)*hi(J!1421)))), If(And(hi(I!1420)*hi(J!1421) >= lo(I!1420)*lo(J!1421), hi(I!1420)*hi(J!1421) >= hi(I!1420)*lo(J!1421), hi(I!1420)*hi(J!1421) >= lo(I!1420)*hi(J!1421)), hi(I!1420)*hi(J!1421), If(And(lo(I!1420)*lo(J!1421) <= hi(I!1420)*lo(J!1421), lo(I!1420)*lo(J!1421) <= lo(I!1420)*hi(J!1421)), lo(I!1420)*lo(J!1421), If(And(hi(I!1420)*lo(J!1421) <= lo(I!1420)*hi(J!1421)), hi(I!1420)*lo(J!1421), lo(I!1420)*hi(J!1421))))), ax=|= ForAll([I, J], Interval.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))))))), Interval.setof: Unfolding(name='Interval.setof', decl=Interval.setof, args=[], body=Lambda(x, And(lo(i!1387) <= x, x <= hi(i!1387))), ax=|= ForAll(i, Interval.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))))), Interval.sub: Unfolding(name='Interval.sub', decl=Interval.sub, args=[], body=Interval(lo(i!1413) - hi(j!1414), hi(i!1413) - lo(j!1414)), ax=|= ForAll([i, j], Interval.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)))), KnownBits_1.and_: Unfolding(name='KnownBits_1.and_', decl=KnownBits_1.and_, args=[], body=KnownBits_1(ones(x!698) & ones(y!699), ~(~unknowns(x!698) & ~ones(x!698) | ~unknowns(y!699) & ~ones(y!699) | ones(x!698) & ones(y!699))), ax=|= ForAll([x, y], KnownBits_1.and_(x, y) == KnownBits_1(ones(x) & ones(y), ~(~unknowns(x) & ~ones(x) | ~unknowns(y) & ~ones(y) | ones(x) & ones(y)))), _subst_fun_body=KnownBits_1(ones(Var(0)) & ones(Var(1)), ~(~unknowns(Var(0)) & ~ones(Var(0)) | ~unknowns(Var(1)) & ~ones(Var(1)) | ones(Var(0)) & ones(Var(1))))), KnownBits_1.const: Unfolding(name='KnownBits_1.const', decl=KnownBits_1.const, args=[], body=KnownBits_1(a!665, 0), ax=|= ForAll(a, KnownBits_1.const(a) == KnownBits_1(a, 0)), _subst_fun_body=KnownBits_1(Var(0), 0)), KnownBits_1.invert: Unfolding(name='KnownBits_1.invert', decl=KnownBits_1.invert, args=[], body=KnownBits_1(~unknowns(x!689) & ~ones(x!689), unknowns(x!689)), ax=|= ForAll(x, KnownBits_1.invert(x) == KnownBits_1(~unknowns(x) & ~ones(x), unknowns(x))), _subst_fun_body=KnownBits_1(~unknowns(Var(0)) & ~ones(Var(0)), unknowns(Var(0)))), KnownBits_1.is_const: Unfolding(name='KnownBits_1.is_const', decl=KnownBits_1.is_const, args=[], body=unknowns(x!666) == 0, ax=|= ForAll(x, KnownBits_1.is_const(x) == (unknowns(x) == 0)), _subst_fun_body=unknowns(Var(0)) == 0), KnownBits_1.or_: Unfolding(name='KnownBits_1.or_', decl=KnownBits_1.or_, args=[], body=KnownBits_1(ones(x!716) | ones(y!717), ~(ones(x!716) | ones(y!717) | ~unknowns(x!716) & ~ones(x!716) & ~unknowns(y!717) & ~ones(y!717))), ax=|= ForAll([x, y], KnownBits_1.or_(x, y) == KnownBits_1(ones(x) | ones(y), ~(ones(x) | ones(y) | ~unknowns(x) & ~ones(x) & ~unknowns(y) & ~ones(y)))), _subst_fun_body=KnownBits_1(ones(Var(0)) | ones(Var(1)), ~(ones(Var(0)) | ones(Var(1)) | ~unknowns(Var(0)) & ~ones(Var(0)) & ~unknowns(Var(1)) & ~ones(Var(1))))), KnownBits_1.setof: Unfolding(name='KnownBits_1.setof', decl=KnownBits_1.setof, args=[], body=Lambda(a, ~unknowns(x!663) & a == ones(x!663)), ax=|= ForAll(x, KnownBits_1.setof(x) == (Lambda(a, ~unknowns(x) & a == ones(x)))), _subst_fun_body=Lambda(a, ~unknowns(Var(1)) & a == ones(Var(1)))), KnownBits_1.wf: Unfolding(name='KnownBits_1.wf', decl=KnownBits_1.wf, args=[], body=ones(x!664) & unknowns(x!664) == 0, ax=|= ForAll(x, KnownBits_1.wf(x) == (ones(x) & unknowns(x) == 0)), _subst_fun_body=ones(Var(0)) & unknowns(Var(0)) == 0), KnownBits_1.zeros: Unfolding(name='KnownBits_1.zeros', decl=KnownBits_1.zeros, args=[], body=~unknowns(x!688) & ~ones(x!688), ax=|= ForAll(x, KnownBits_1.zeros(x) == ~unknowns(x) & ~ones(x)), _subst_fun_body=~unknowns(Var(0)) & ~ones(Var(0))), NDArray.add: Unfolding(name='NDArray.add', decl=NDArray.add, args=[], body=If(shape(u!1844) == shape(v!1845), NDArray(shape(u!1844), Lambda(k, data(u!1844)[k] + data(v!1845)[k])), add_undef(u!1844, v!1845)), ax=|= ForAll([u, v], NDArray.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)))), Nat.add: Unfolding(name='Nat.add', decl=Nat.add, args=[], body=If(is(Z, x!364), y!365, S(Nat.add(pred(x!364), y!365))), ax=|= ForAll([x, y], Nat.add(x, y) == If(is(Z, x), y, S(Nat.add(pred(x), y)))), _subst_fun_body=If(is(Z, Var(0)), Var(1), S(Nat.add(pred(Var(0)), Var(1))))), R.add: Unfolding(name='R.add', decl=R.add, args=[], body=x!408 + y!409, ax=|= ForAll([x, y], R.add(x, y) == x + y), _subst_fun_body=Var(0) + Var(1)), R.dist: Unfolding(name='R.dist', decl=R.dist, args=[], body=absR(x!1166 - y!1167), ax=|= ForAll([x!1144, y!1145], R.dist(x!1144, y!1145) == absR(x!1144 - y!1145)), _subst_fun_body=absR(Var(0) - Var(1))), R.max: Unfolding(name='R.max', decl=R.max, args=[], body=If(x!498 >= y!499, x!498, y!499), ax=|= ForAll([x, y], R.max(x, y) == If(x >= y, x, y)), _subst_fun_body=If(Var(0) >= Var(1), Var(0), Var(1))), R.sqr: Unfolding(name='R.sqr', decl=R.sqr, args=[], body=x!585*x!585, ax=|= ForAll(x, R.sqr(x) == x*x), _subst_fun_body=Var(0)*Var(0)), R.zero: Unfolding(name='R.zero', decl=R.zero, args=[], body=0, ax=|= R.zero == 0, _subst_fun_body=0), RFun.const: Unfolding(name='RFun.const', decl=RFun.const, args=[], body=K(Real, x!646), ax=|= ForAll(x, RFun.const(x) == K(Real, x)), _subst_fun_body=K(Real, Var(0))), RFun.ident: Unfolding(name='RFun.ident', decl=RFun.ident, args=[], body=Lambda(x, x), ax=|= RFun.ident == (Lambda(x, x)), _subst_fun_body=Lambda(x, x)), RFun.smul: Unfolding(name='RFun.smul', decl=RFun.smul, args=[], body=Lambda(x, mul(c!1282, f!1283[x])), ax=|= ForAll([c, f], RFun.smul(c, f) == (Lambda(x, mul(c, f[x])))), _subst_fun_body=Lambda(x, mul(Var(1), Var(2)[x]))), RSeq.const: Unfolding(name='RSeq.const', decl=RSeq.const, args=[], body=Lambda(i, x!1425), ax=|= ForAll(x, RSeq.const(x) == (Lambda(i, x))), _subst_fun_body=Lambda(i, Var(1))), RSeq.id: Unfolding(name='RSeq.id', decl=RSeq.id, args=[], body=Lambda(i, ToReal(i)), ax=|= RSeq.id == (Lambda(i, ToReal(i))), _subst_fun_body=Lambda(i, ToReal(i))), RSeq.rev: Unfolding(name='RSeq.rev', decl=RSeq.rev, args=[], body=Lambda(i, a!1433[-i]), ax=|= ForAll(a, RSeq.rev(a) == (Lambda(i, a[-i]))), _subst_fun_body=Lambda(i, Var(1)[-i])), RSeq.shift: Unfolding(name='RSeq.shift', decl=RSeq.shift, args=[], body=Lambda(i, a!1430[i - n!1431]), ax=|= ForAll([a, n], RSeq.shift(a, n) == (Lambda(i, a[i - n]))), _subst_fun_body=Lambda(i, Var(1)[i - Var(2)])), RSeq.smul: Unfolding(name='RSeq.smul', decl=RSeq.smul, args=[], body=Lambda(n, x!1459*a!1460[n]), ax=|= ForAll([x, a], RSeq.smul(x, a) == (Lambda(n, x*a[n]))), _subst_fun_body=Lambda(n, Var(1)*Var(2)[n])), RSeq.zero: Unfolding(name='RSeq.zero', decl=RSeq.zero, args=[], body=K(Int, 0), ax=|= RSeq.zero == K(Int, 0), _subst_fun_body=K(Int, 0)), RSet.has_lb: Unfolding(name='RSet.has_lb', decl=RSet.has_lb, args=[], body=ForAll(x, Implies(A!1875[x], M!1876 <= x)), ax=|= ForAll([A, M], RSet.has_lb(A, M) == (ForAll(x, Implies(A[x], M <= x)))), _subst_fun_body=ForAll(x, Implies(Var(1)[x], Var(2) <= x))), RSet.inf: Unfolding(name='RSet.inf', decl=RSet.inf, args=[], body=RSet.sup(Lambda(x, RSet.has_lb(A!1877, x))), ax=|= ForAll(A, RSet.inf(A) == RSet.sup(Lambda(x, RSet.has_lb(A, x)))), _subst_fun_body=RSet.sup(Lambda(x, RSet.has_lb(Var(1), x)))), RSet.is_ub: Unfolding(name='RSet.is_ub', decl=RSet.is_ub, args=[], body=Exists(M, has_ub(A!1854, M)), ax=|= ForAll(A, RSet.is_ub(A) == (Exists(M, has_ub(A, M)))), _subst_fun_body=Exists(M, has_ub(Var(1), M))), RSet.sing: Unfolding(name='RSet.sing', decl=RSet.sing, args=[], body=Lambda(x, x == c!1873), ax=|= ForAll(c, RSet.sing(c) == (Lambda(x, x == c))), _subst_fun_body=Lambda(x, x == Var(1))), T_Int.add: Unfolding(name='T_Int.add', decl=T_Int.add, args=[], body=T_Int(Lambda(t, val(x!1077)[t] + val(y!1078)[t])), ax=|= ForAll([x, y], T_Int.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]))), T_Int.ge: Unfolding(name='T_Int.ge', decl=T_Int.ge, args=[], body=T_Bool(Lambda(t, val(x!1081)[t] >= val(y!1082)[t])), ax=|= ForAll([x, y], T_Int.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]))), T_Int.le: Unfolding(name='T_Int.le', decl=T_Int.le, args=[], body=T_Bool(Lambda(t, val(x!1083)[t] <= val(y!1084)[t])), ax=|= ForAll([x, y], T_Int.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]))), T_Real.add: Unfolding(name='T_Real.add', decl=T_Real.add, args=[], body=T_Real(Lambda(t, val(x!1079)[t] + val(y!1080)[t])), ax=|= ForAll([x, y], T_Real.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]))), Vec2.add: Unfolding(name='Vec2.add', decl=Vec2.add, args=[], body=Vec2(x(u!1313) + x(v!1314), y(u!1313) + y(v!1314)), ax=|= ForAll([u, v], Vec2.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)))), Vec2.dist: Unfolding(name='Vec2.dist', decl=Vec2.dist, args=[], body=sqrt(Vec2.norm2(Vec2.sub(u!1326, v!1327))), ax=|= ForAll([u, v], Vec2.dist(u, v) == sqrt(Vec2.norm2(Vec2.sub(u, v)))), _subst_fun_body=sqrt(Vec2.norm2(Vec2.sub(Var(0), Var(1))))), Vec2.dot: Unfolding(name='Vec2.dot', decl=Vec2.dot, args=[], body=x(u!1318)*x(v!1319) + y(u!1318)*y(v!1319), ax=|= ForAll([u, v], Vec2.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))), Vec2.neg: Unfolding(name='Vec2.neg', decl=Vec2.neg, args=[], body=Vec2(-x(u!1317), -y(u!1317)), ax=|= ForAll(u, Vec2.neg(u) == Vec2(-x(u), -y(u))), _subst_fun_body=Vec2(-x(Var(0)), -y(Var(0)))), Vec2.norm: Unfolding(name='Vec2.norm', decl=Vec2.norm, args=[], body=sqrt(Vec2.dot(u!1321, u!1321)), ax=|= ForAll(u, Vec2.norm(u) == sqrt(Vec2.dot(u, u))), _subst_fun_body=sqrt(Vec2.dot(Var(0), Var(0)))), Vec2.norm2: Unfolding(name='Vec2.norm2', decl=Vec2.norm2, args=[], body=Vec2.dot(u!1320, u!1320), ax=|= ForAll(u, Vec2.norm2(u) == Vec2.dot(u, u)), _subst_fun_body=Vec2.dot(Var(0), Var(0))), Vec2.sub: Unfolding(name='Vec2.sub', decl=Vec2.sub, args=[], body=Vec2(x(u!1315) - x(v!1316), y(u!1315) - y(v!1316)), ax=|= ForAll([u, v], Vec2.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)))), Vec3.add: Unfolding(name='Vec3.add', decl=Vec3.add, args=[], body=Vec3(x(u!1894) + x(v!1895), y(u!1894) + y(v!1895), z(u!1894) + z(v!1895)), ax=|= ForAll([u, v], Vec3.add(u, v) == Vec3(x(u) + x(v), y(u) + y(v), z(u) + z(v))), _subst_fun_body=Vec3(x(Var(0)) + x(Var(1)), y(Var(0)) + y(Var(1)), z(Var(0)) + z(Var(1)))), Vec3.dist: Unfolding(name='Vec3.dist', decl=Vec3.dist, args=[], body=sqrt(Vec3.norm2(Vec3.sub(u!1929, v!1930))), ax=|= ForAll([u, v], Vec3.dist(u, v) == sqrt(Vec3.norm2(Vec3.sub(u, v)))), _subst_fun_body=sqrt(Vec3.norm2(Vec3.sub(Var(0), Var(1))))), Vec3.dot: Unfolding(name='Vec3.dot', decl=Vec3.dot, args=[], body=x(u!1911)*x(v!1912) + y(u!1911)*y(v!1912) + z(u!1911)*z(v!1912), ax=|= ForAll([u, v], Vec3.dot(u, v) == x(u)*x(v) + y(u)*y(v) + z(u)*z(v)), _subst_fun_body=x(Var(0))*x(Var(1)) + y(Var(0))*y(Var(1)) + z(Var(0))*z(Var(1))), Vec3.neg: Unfolding(name='Vec3.neg', decl=Vec3.neg, args=[], body=Vec3(-x(u!1900), -y(u!1900), -z(u!1900)), ax=|= ForAll(u, Vec3.neg(u) == Vec3(-x(u), -y(u), -z(u))), _subst_fun_body=Vec3(-x(Var(0)), -y(Var(0)), -z(Var(0)))), Vec3.norm: Unfolding(name='Vec3.norm', decl=Vec3.norm, args=[], body=sqrt(Vec3.norm2(u!1924)), ax=|= ForAll(u, Vec3.norm(u) == sqrt(Vec3.norm2(u))), _subst_fun_body=sqrt(Vec3.norm2(Var(0)))), Vec3.norm2: Unfolding(name='Vec3.norm2', decl=Vec3.norm2, args=[], body=Vec3.dot(u!1920, u!1920), ax=|= ForAll(u, Vec3.norm2(u) == Vec3.dot(u, u)), _subst_fun_body=Vec3.dot(Var(0), Var(0))), Vec3.smul: Unfolding(name='Vec3.smul', decl=Vec3.smul, args=[], body=Vec3(a!1901*x(u!1902), a!1901*y(u!1902), a!1901*z(u!1902)), ax=|= ForAll([a, u], Vec3.smul(a, u) == Vec3(a*x(u), a*y(u), a*z(u))), _subst_fun_body=Vec3(Var(0)*x(Var(1)), Var(0)*y(Var(1)), Var(0)*z(Var(1)))), Vec3.sub: Unfolding(name='Vec3.sub', decl=Vec3.sub, args=[], body=Vec3(x(u!1898) - x(v!1899), y(u!1898) - y(v!1899), z(u!1898) - z(v!1899)), ax=|= ForAll([u, v], Vec3.sub(u, v) == Vec3(x(u) - x(v), y(u) - y(v), z(u) - z(v))), _subst_fun_body=Vec3(x(Var(0)) - x(Var(1)), y(Var(0)) - y(Var(1)), z(Var(0)) - z(Var(1)))), ZF.elts: Unfolding(name='ZF.elts', decl=ZF.elts, args=[], body=Lambda(x, ∈(x, A!1960)), ax=|= ForAll(A, ZF.elts(A) == (Lambda(x, ∈(x, A)))), _subst_fun_body=Lambda(x, ∈(x, Var(1)))), ZF.sing: Unfolding(name='ZF.sing', decl=ZF.sing, args=[], body=upair(x!2049, x!2049), ax=|= ForAll(x, ZF.sing(x) == upair(x, x)), _subst_fun_body=upair(Var(0), Var(0))), ZFSet.le: Unfolding(name='ZFSet.le', decl=ZFSet.le, args=[], body=ForAll(x, Implies(∈(x, A!1965), ∈(x, B!1966))), ax=|= ForAll([A, B], ZFSet.le(A, B) == (ForAll(x, Implies(∈(x, A), ∈(x, B))))), _subst_fun_body=ForAll(x, Implies(∈(x, Var(1)), ∈(x, Var(2))))), ZFSet.sub: Unfolding(name='ZFSet.sub', decl=ZFSet.sub, args=[], body=sep(A!2328, Lambda(x, Not(∈(x, B!2329)))), ax=|= ForAll([A, B], ZFSet.sub(A, B) == sep(A, Lambda(x, Not(∈(x, B))))), _subst_fun_body=sep(Var(0), Lambda(x, Not(∈(x, Var(2)))))), ZSet.finite: Unfolding(name='ZSet.finite', decl=ZSet.finite, args=[], body=And(ZSet.is_ub(A!339), ZSet.is_lb(A!339)), ax=|= ForAll(A, ZSet.finite(A) == And(ZSet.is_ub(A), ZSet.is_lb(A))), _subst_fun_body=And(ZSet.is_ub(Var(0)), ZSet.is_lb(Var(0)))), ZSet.has_lb: Unfolding(name='ZSet.has_lb', decl=ZSet.has_lb, args=[], body=ForAll(x, Implies(A!336[x], y!337 <= x)), ax=|= ForAll([A, y], ZSet.has_lb(A, y) == (ForAll(x, Implies(A[x], y <= x)))), _subst_fun_body=ForAll(x, Implies(Var(1)[x], Var(2) <= x))), ZSet.has_ub: Unfolding(name='ZSet.has_ub', decl=ZSet.has_ub, args=[], body=ForAll(x, Implies(A!333[x], x <= y!334)), ax=|= ForAll([A, y], ZSet.has_ub(A, y) == (ForAll(x, Implies(A[x], x <= y)))), _subst_fun_body=ForAll(x, Implies(Var(1)[x], x <= Var(2)))), ZSet.is_lb: Unfolding(name='ZSet.is_lb', decl=ZSet.is_lb, args=[], body=Exists(x, ZSet.has_lb(A!338, x)), ax=|= ForAll(A, ZSet.is_lb(A) == (Exists(x, ZSet.has_lb(A, x)))), _subst_fun_body=Exists(x, ZSet.has_lb(Var(1), x))), ZSet.is_ub: Unfolding(name='ZSet.is_ub', decl=ZSet.is_ub, args=[], body=Exists(x, ZSet.has_ub(A!335, x)), ax=|= ForAll(A, ZSet.is_ub(A) == (Exists(x, ZSet.has_ub(A, x)))), _subst_fun_body=Exists(x, ZSet.has_ub(Var(1), x))), abelian: Unfolding(name='abelian', decl=abelian, args=[], body=ForAll([x!734, y!735], mul(x!734, y!735) == mul(y!735, x!734)), ax=|= abelian == (ForAll([x!734, y!735], mul(x!734, y!735) == mul(y!735, x!734))), _subst_fun_body=ForAll([x!734, y!735], mul(x!734, y!735) == mul(y!735, x!734))), abs: Unfolding(name='abs', decl=abs, args=[], body=Map(absR, a!1570), ax=|= ForAll(a, abs(a) == Map(absR, a)), _subst_fun_body=Map(absR, Var(0))), absR: Unfolding(name='absR', decl=absR, args=[], body=If(x!431 >= 0, x!431, -x!431), ax=|= ForAll(x, absR(x) == If(x >= 0, x, -x)), _subst_fun_body=If(Var(0) >= 0, Var(0), -Var(0))), add_defined: Unfolding(name='add_defined', decl=add_defined, args=[], body=Or(And(is(Real, x!1210), is(Real, y!1211)), And(is(Inf, x!1210), Not(is(NegInf, y!1211))), And(Not(is(NegInf, x!1210)), is(Inf, y!1211)), And(is(NegInf, x!1210), Not(is(Inf, y!1211))), And(Not(is(Inf, x!1210)), is(NegInf, y!1211))), 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))))), aeq: Unfolding(name='aeq', decl=aeq, args=[], body=If(x!474 - y!475 > 0, x!474 - y!475, -(x!474 - y!475)) <= eps!476, ax=|= ForAll([x, y, eps], aeq(x, y, eps) == (If(x - y > 0, x - y, -(x - y)) <= eps)), _subst_fun_body=If(Var(0) - Var(1) > 0, Var(0) - Var(1), -(Var(0) - Var(1))) <= Var(2)), always: Unfolding(name='always', decl=always, args=[], body=T_Bool(Lambda(t!1099, ForAll(dt!1100, Implies(dt!1100 >= 0, val(p!1101)[t!1099 + dt!1100])))), ax=|= ForAll(p, always(p) == T_Bool(Lambda(t!1099, ForAll(dt!1100, Implies(dt!1100 >= 0, val(p)[t!1099 + dt!1100]))))), _subst_fun_body=T_Bool(Lambda(t!1099, ForAll(dt!1100, Implies(dt!1100 >= 0, val(Var(2))[t!1099 + dt!1100]))))), ball: Unfolding(name='ball', decl=ball, args=[], body=Lambda(y!1148, absR(y!1148 - x!1149) < r!1150), ax=|= ForAll([x!1144, r!1147], ball(x!1144, r!1147) == (Lambda(y!1148, absR(y!1148 - x!1144) < r!1147))), _subst_fun_body=Lambda(y!1148, absR(y!1148 - Var(1)) < Var(2))), bchoose: Unfolding(name='bchoose', decl=bchoose, args=[], body=downsearch(P!329, N!330), ax=|= ForAll([P, N], bchoose(P, N) == downsearch(P, N)), _subst_fun_body=downsearch(Var(0), Var(1))), beq: Unfolding(name='beq', decl=beq, args=[], body=T_Bool(Lambda(t!1104, val(p!1105)[t!1104] == val(q!1106)[t!1104])), ax=|= ForAll([p, q], beq(p, q) == T_Bool(Lambda(t!1104, val(p)[t!1104] == val(q)[t!1104]))), _subst_fun_body=T_Bool(Lambda(t!1104, val(Var(1))[t!1104] == val(Var(2))[t!1104]))), bexist: Unfolding(name='bexist', decl=bexist, args=[], body=If(n!1026 < 0, False, Or(A!1025[n!1026], bexists(A!1025, n!1026 - 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)))), bexists: Unfolding(name='bexists', decl=bexists, args=[], body=P!331[bchoose(P!331, N!332)], ax=|= ForAll([P, N], bexists(P, N) == P[bchoose(P, N)]), _subst_fun_body=Var(0)[bchoose(Var(0), Var(1))]), bforall: Unfolding(name='bforall', decl=bforall, args=[], body=If(n!1028 < 0, True, And(A!1027[n!1028], bforall(A!1027, n!1028 - 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: Unfolding(name='biginter', decl=biginter, args=[], body=sep(pick(a!2166), Lambda(x, ForAll(b!1956, Implies(∈(b!1956, a!2166), ∈(x, b!1956))))), ax=|= ForAll(a!1955, biginter(a!1955) == sep(pick(a!1955), Lambda(x, ForAll(b!1956, Implies(∈(b!1956, a!1955), ∈(x, b!1956)))))), _subst_fun_body=sep(pick(Var(0)), Lambda(x, ForAll(b!1956, Implies(∈(b!1956, Var(2)), ∈(x, b!1956)))))), cauchy_mod: Unfolding(name='cauchy_mod', decl=cauchy_mod, args=[], body=ForAll(eps, Implies(eps > 0, ForAll([m, k], Implies(And(m > mod!1611[eps], k > mod!1611[eps]), absR(a!1610[m] - a!1610[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))))), ceil: Unfolding(name='ceil', decl=ceil, args=[], body=-floor(-x!563), ax=|= ForAll(x, ceil(x) == -floor(-x)), _subst_fun_body=-floor(-Var(0))), cinter: Unfolding(name='cinter', decl=cinter, args=[], body=Lambda(x, ForAll(n, An!1891[n][x])), ax=|= ForAll(An, cinter(An) == (Lambda(x, ForAll(n, An[n][x])))), _subst_fun_body=Lambda(x, ForAll(n, Var(2)[n][x]))), circle: Unfolding(name='circle', decl=circle, args=[], body=Lambda(p, Vec2.norm2(Vec2.sub(p, c!1328)) == r!1329*r!1329), ax=|= ForAll([c, r], circle(c, r) == (Lambda(p, Vec2.norm2(Vec2.sub(p, c)) == r*r))), _subst_fun_body=Lambda(p, Vec2.norm2(Vec2.sub(p, Var(1))) == Var(2)*Var(2))), closed: Unfolding(name='closed', decl=closed, args=[], body=(Array Sierpinski Bool).open(complement(A!1022)), ax=|= ForAll(A, closed(A) == (Array Sierpinski Bool).open(complement(A))), _subst_fun_body=(Array Sierpinski Bool).open(complement(Var(0)))), closed_int: Unfolding(name='closed_int', decl=closed_int, args=[], body=Lambda(z, And(x!1869 <= z, z <= y!1870)), ax=|= ForAll([x, y], closed_int(x, y) == (Lambda(z, And(x <= z, z <= y)))), _subst_fun_body=Lambda(z, And(Var(1) <= z, z <= Var(2)))), comp: Unfolding(name='comp', decl=comp, args=[], body=Lambda(x, f!644[g!645[x]]), ax=|= ForAll([f, g], comp(f, g) == (Lambda(x, f[g[x]]))), _subst_fun_body=Lambda(x, Var(1)[Var(2)[x]])), conj: Unfolding(name='conj', decl=conj, args=[], body=C(re(z!1175), -im(z!1175)), ax=|= ForAll(z, conj(z) == C(re(z), -im(z))), _subst_fun_body=C(re(Var(0)), -im(Var(0)))), cont_at: Unfolding(name='cont_at', decl=cont_at, args=[], body=ForAll(eps, Implies(eps > 0, Exists(delta, And(delta > 0, ForAll(y, Implies(absR(x!653 - y) < delta, absR(f!652[x!653] - f!652[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: Unfolding(name='cos', decl=cos, args=[], body=Map(cos, a!1569), ax=|= ForAll(a, cos(a) == Map(cos, a)), _subst_fun_body=Map(cos, Var(0))), cross: Unfolding(name='cross', decl=cross, args=[], body=Vec3(y(u!1933)*z(v!1934) - z(u!1933)*y(v!1934), z(u!1933)*x(v!1934) - x(u!1933)*z(v!1934), x(u!1933)*y(v!1934) - y(u!1933)*x(v!1934)), ax=|= ForAll([u, v], cross(u, v) == Vec3(y(u)*z(v) - z(u)*y(v), z(u)*x(v) - x(u)*z(v), x(u)*y(v) - y(u)*x(v))), _subst_fun_body=Vec3(y(Var(0))*z(Var(1)) - z(Var(0))*y(Var(1)), z(Var(0))*x(Var(1)) - x(Var(0))*z(Var(1)), x(Var(0))*y(Var(1)) - y(Var(0))*x(Var(1)))), cumsum: Unfolding(name='cumsum', decl=cumsum, args=[], body=Lambda(i, If(i == 0, a!1470[0], If(i > 0, cumsum(a!1470)[i - 1] + a!1470[i], -cumsum(a!1470)[i + 1] - a!1470[i + 1]))), 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 + 1]))))), _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 + 1])))), cunion: Unfolding(name='cunion', decl=cunion, args=[], body=Lambda(x, Exists(n, An!1892[n][x])), ax=|= ForAll(An, cunion(An) == (Lambda(x, Exists(n, An[n][x])))), _subst_fun_body=Lambda(x, Exists(n, Var(2)[n][x]))), decimate: Unfolding(name='decimate', decl=decimate, args=[], body=Lambda(i, a!1436[i*n!1437]), ax=|= ForAll([a, n], decimate(a, n) == (Lambda(i, a[i*n]))), _subst_fun_body=Lambda(i, Var(1)[i*Var(2)])), delay: Unfolding(name='delay', decl=delay, args=[], body=RSeq.shift(a!1432, 1), ax=|= ForAll(a, delay(a) == RSeq.shift(a, 1)), _subst_fun_body=RSeq.shift(Var(0), 1)), diff: Unfolding(name='diff', decl=diff, args=[], body=Lambda(i, a!1445[i + 1] - a!1445[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: Unfolding(name='diff_at', decl=diff_at, args=[], body=Exists(y, has_diff_at(f!650, x!651, 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: Unfolding(name='dilate', decl=dilate, args=[], body=Lambda(i, a!1434[i/n!1435]), ax=|= ForAll([a, n], dilate(a, n) == (Lambda(i, a[i/n]))), _subst_fun_body=Lambda(i, Var(1)[i/Var(2)])), dom: Unfolding(name='dom', decl=dom, args=[], body=sep(bigunion(bigunion(R!2494)), Lambda(x, Exists(y, ∈(pair(x, y), R!2494)))), ax=|= ForAll(R, dom(R) == sep(bigunion(bigunion(R)), Lambda(x, Exists(y, ∈(pair(x, y), R))))), _subst_fun_body=sep(bigunion(bigunion(Var(0))), Lambda(x, Exists(y, ∈(pair(x, y), Var(2)))))), dommap: Unfolding(name='dommap', decl=dommap, args=[], body=Lambda(i, a!1429[F!1428[i]]), ax=|= ForAll([F, a], dommap(F, a) == (Lambda(i, a[F[i]]))), _subst_fun_body=Lambda(i, Var(2)[Var(1)[i]])), double: Unfolding(name='double', decl=double, args=[], body=If(is(Z, n!363), Z, S(S(double(pred(n!363))))), 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))))))), downsearch: Unfolding(name='downsearch', decl=downsearch, args=[], body=If(P!327[n!328], n!328, If(n!328 < 0, 0, downsearch(P!327, n!328 - 1))), ax=|= ForAll([P, n!301], downsearch(P, n!301) == If(P[n!301], n!301, If(n!301 < 0, 0, downsearch(P, n!301 - 1)))), _subst_fun_body=If(Var(0)[Var(1)], Var(1), If(Var(1) < 0, 0, downsearch(Var(0), Var(1) - 1)))), dvd: Unfolding(name='dvd', decl=dvd, args=[], body=Exists(p, m!299 == n!298*p), ax=|= ForAll([n, m], dvd(n, m) == (Exists(p, m == n*p))), _subst_fun_body=Exists(p, Var(2) == Var(1)*p)), empty: Unfolding(name='empty', decl=empty, args=[], body=Interval(1, 0), ax=|= empty == Interval(1, 0), _subst_fun_body=Interval(1, 0)), even: Unfolding(name='even', decl=even, args=[], body=Exists(y, x!271 == 2*y), ax=|= ForAll(x, even(x) == (Exists(y, x == 2*y))), _subst_fun_body=Exists(y, Var(1) == 2*y)), eventually: Unfolding(name='eventually', decl=eventually, args=[], body=T_Bool(Lambda(t!1096, Exists(dt!1097, And(dt!1097 >= 0, val(p!1098)[t!1096 + dt!1097])))), ax=|= ForAll(p, eventually(p) == T_Bool(Lambda(t!1096, Exists(dt!1097, And(dt!1097 >= 0, val(p)[t!1096 + dt!1097]))))), _subst_fun_body=T_Bool(Lambda(t!1096, Exists(dt!1097, And(dt!1097 >= 0, val(Var(2))[t!1096 + dt!1097]))))), expi: Unfolding(name='expi', decl=expi, args=[], body=C(cos(t!1186), sin(t!1186)), ax=|= ForAll(t, expi(t) == C(cos(t), sin(t))), _subst_fun_body=C(cos(Var(0)), sin(Var(0)))), fact: Unfolding(name='fact', decl=fact, args=[], body=If(n!300 <= 0, 1, n!300*fact(n!300 - 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))), finsum: Unfolding(name='finsum', decl=finsum, args=[], body=cumsum(a!1566)[n!1567], ax=|= ForAll([a, n], finsum(a, n) == cumsum(a)[n]), _subst_fun_body=cumsum(Var(0))[Var(1)]), floor: Unfolding(name='floor', decl=floor, args=[], body=ToReal(ToInt(x!546)), ax=|= ForAll(x, floor(x) == ToReal(ToInt(x))), _subst_fun_body=ToReal(ToInt(Var(0)))), from_int: Unfolding(name='from_int', decl=from_int, args=[], body=If(a!341 <= 0, Z, S(from_int(a!341 - 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: Unfolding(name='fst', decl=fst, args=[], body=pick(biginter(p!2366)), ax=|= ForAll(p!1959, fst(p!1959) == pick(biginter(p!1959))), _subst_fun_body=pick(biginter(Var(0)))), geom: Unfolding(name='geom', decl=geom, args=[], body=Lambda(i, pownat(x!1426, i)), ax=|= ForAll(x, geom(x) == (Lambda(i, pownat(x, i)))), _subst_fun_body=Lambda(i, pownat(Var(1), i))), has_bound: Unfolding(name='has_bound', decl=has_bound, args=[], body=ForAll(n, absR(a!1604[n]) <= M!1605), ax=|= ForAll([a, M], has_bound(a, M) == (ForAll(n, absR(a[n]) <= M))), _subst_fun_body=ForAll(n, absR(Var(1)[n]) <= Var(2))), has_lim: Unfolding(name='has_lim', decl=has_lim, args=[], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(a!1612[n] - y!1613) < 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: Unfolding(name='has_lim_at', decl=has_lim_at, args=[], body=ForAll(eps, Implies(0 < eps, Exists(delta, And(delta > 0, ForAll(x, Implies(And(0 < absR(x - p!648), absR(x - p!648) < delta), absR(f!647[x] - L!649) < 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_max: Unfolding(name='has_max', decl=has_max, args=[], body=And(A!1865[x!1866], RSet.sup(A!1865) == x!1866), ax=|= ForAll([A, x], has_max(A, x) == And(A[x], RSet.sup(A) == x)), _subst_fun_body=And(Var(0)[Var(1)], RSet.sup(Var(0)) == Var(1))), has_sum: Unfolding(name='has_sum', decl=has_sum, args=[], body=has_lim(cumsum(a!1652), y!1653), ax=|= ForAll([a, y], has_sum(a, y) == has_lim(cumsum(a), y)), _subst_fun_body=has_lim(cumsum(Var(0)), Var(1))), has_ub: Unfolding(name='has_ub', decl=has_ub, args=[], body=ForAll(x, Implies(A!1852[x], x <= M!1853)), ax=|= ForAll([A, M], has_ub(A, M) == (ForAll(x, Implies(A[x], x <= M)))), _subst_fun_body=ForAll(x, Implies(Var(1)[x], x <= Var(2)))), iand: Unfolding(name='iand', decl=iand, args=[], body=Prop(Lambda(w, And(val(a!1032)[w], val(b!1033)[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])))), ieq: Unfolding(name='ieq', decl=ieq, args=[], body=T_Bool(Lambda(t!1131, val(x!1132)[t!1131] == val(y!1133)[t!1131])), ax=|= ForAll([x, y], ieq(x, y) == T_Bool(Lambda(t!1131, val(x)[t!1131] == val(y)[t!1131]))), _subst_fun_body=T_Bool(Lambda(t!1131, val(Var(1))[t!1131] == val(Var(2))[t!1131]))), if_int: Unfolding(name='if_int', decl=if_int, args=[], body=T_Int(Lambda(t!1139, If(val(p!1140)[t!1139], val(x!1141)[t!1139], val(y!1142)[t!1139]))), ax=|= ForAll([p, x, y], if_int(p, x, y) == T_Int(Lambda(t!1139, If(val(p)[t!1139], val(x)[t!1139], val(y)[t!1139])))), _subst_fun_body=T_Int(Lambda(t!1139, If(val(Var(1))[t!1139], val(Var(2))[t!1139], val(Var(3))[t!1139])))), iimpl: Unfolding(name='iimpl', decl=iimpl, args=[], body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a!1036)[u], val(b!1037)[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])))))), ind: Unfolding(name='ind', decl=ind, args=[], body=Lambda(i, If(S!1427[i], 1, 0)), ax=|= ForAll(S, ind(S) == (Lambda(i, If(S[i], 1, 0)))), _subst_fun_body=Lambda(i, If(Var(1)[i], 1, 0))), ineq: Unfolding(name='ineq', decl=ineq, args=[], body=T_Bool(Lambda(t!1134, val(x!1135)[t!1134] != val(y!1136)[t!1134])), ax=|= ForAll([x, y], ineq(x, y) == T_Bool(Lambda(t!1134, val(x)[t!1134] != val(y)[t!1134]))), _subst_fun_body=T_Bool(Lambda(t!1134, val(Var(1))[t!1134] != val(Var(2))[t!1134]))), inext: Unfolding(name='inext', decl=inext, args=[], body=T_Int(Lambda(t!1137, val(x!1138)[t!1137 + 1])), ax=|= ForAll(x, inext(x) == T_Int(Lambda(t!1137, val(x)[t!1137 + 1]))), _subst_fun_body=T_Int(Lambda(t!1137, val(Var(1))[t!1137 + 1]))), inot: Unfolding(name='inot', decl=inot, args=[], body=Prop(Lambda(w, ForAll(u, Implies(acc(w, u), Implies(val(a!1038)[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: Unfolding(name='inter', decl=inter, args=[], body=sep(A!2184, Lambda(x, ∈(x, B!2185))), ax=|= ForAll([A, B], inter(A, B) == sep(A, Lambda(x, ∈(x, B)))), _subst_fun_body=sep(Var(0), Lambda(x, ∈(x, Var(2))))), ior: Unfolding(name='ior', decl=ior, args=[], body=Prop(Lambda(w, Or(val(a!1034)[w], val(b!1035)[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_bounded: Unfolding(name='is_bounded', decl=is_bounded, args=[], body=Exists(M, has_bound(a!1606, M)), ax=|= ForAll(a, is_bounded(a) == (Exists(M, has_bound(a, M)))), _subst_fun_body=Exists(M, has_bound(Var(1), M))), is_cauchy: Unfolding(name='is_cauchy', decl=is_cauchy, args=[], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll([m, k], Implies(And(m > N, k > N), absR(a!1609[m] - a!1609[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: Unfolding(name='is_circle', decl=is_circle, args=[], body=Exists([c, r], circle(c, r) == A!1386), 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: Unfolding(name='is_cont', decl=is_cont, args=[], body=ForAll(x, cont_at(f!658, 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: Unfolding(name='is_conv', decl=is_conv, args=[], body=Exists(y, has_lim(a!1614, 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: Unfolding(name='is_diff', decl=is_diff, args=[], body=ForAll(x, diff_at(f!657, 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: Unfolding(name='is_empty', decl=is_empty, args=[], body=hi(i) > lo(i), ax=|= ForAll(I, is_empty(I) == (hi(i) > lo(i))), _subst_fun_body=hi(i) > lo(i)), is_idem: Unfolding(name='is_idem', decl=is_idem, args=[], body=mul(A!897, A!897) == A!897, ax=|= ForAll(A, is_idem(A) == (mul(A, A) == A)), _subst_fun_body=mul(Var(0), Var(0)) == Var(0)), is_linear: Unfolding(name='is_linear', decl=is_linear, args=[], body=And(ForAll([x, y], f!1284[R.add(x, y)] == R.add(f!1284[x], f!1284[y])), ForAll([x, c], f!1284[mul(c, x)] == mul(c, f!1284[x]))), ax=|= ForAll(f, is_linear(f) == And(ForAll([x, y], f[R.add(x, y)] == R.add(f[x], f[y])), ForAll([x, c], f[mul(c, x)] == mul(c, f[x])))), _subst_fun_body=And(ForAll([x, y], Var(2)[R.add(x, y)] == R.add(Var(2)[x], Var(2)[y])), ForAll([x, c], Var(2)[mul(c, x)] == mul(c, Var(2)[x])))), is_lub: Unfolding(name='is_lub', decl=is_lub, args=[], body=And(upper_bound(A!1279, x!1280), ForAll(y, Implies(upper_bound(A!1279, y), EReal.le(x!1280, y)))), ax=|= ForAll([A, x], is_lub(A, x) == And(upper_bound(A, x), ForAll(y, Implies(upper_bound(A, y), EReal.le(x, y))))), _subst_fun_body=And(upper_bound(Var(0), Var(1)), ForAll(y, Implies(upper_bound(Var(1), y), EReal.le(Var(2), y))))), is_monotone: Unfolding(name='is_monotone', decl=is_monotone, args=[], body=ForAll([n, m], Implies(n <= m, a!1607[n] <= a!1607[m])), ax=|= ForAll(a, is_monotone(a) == (ForAll([n, m], Implies(n <= m, a[n] <= a[m])))), _subst_fun_body=ForAll([n, m], Implies(n <= m, Var(2)[n] <= Var(2)[m]))), is_nonneg: Unfolding(name='is_nonneg', decl=is_nonneg, args=[], body=ForAll(n, a!1608[n] >= 0), ax=|= ForAll(a, is_nonneg(a) == (ForAll(n, a[n] >= 0))), _subst_fun_body=ForAll(n, Var(1)[n] >= 0)), is_open: Unfolding(name='is_open', decl=is_open, args=[], body=ForAll(x!1144, Implies(S!1151[x!1144], Exists(r!1147, And(0 < r!1147, subset(ball(x!1144, r!1147), S!1151))))), ax=|= ForAll(S, is_open(S) == (ForAll(x!1144, Implies(S[x!1144], Exists(r!1147, And(0 < r!1147, subset(ball(x!1144, r!1147), S))))))), _subst_fun_body=ForAll(x!1144, Implies(Var(1)[x!1144], Exists(r!1147, And(0 < r!1147, subset(ball(x!1144, r!1147), Var(2))))))), is_orth: Unfolding(name='is_orth', decl=is_orth, args=[], body=mul(A!896, trans(A!896)) == I, ax=|= ForAll(A, is_orth(A) == (mul(A, trans(A)) == I)), _subst_fun_body=mul(Var(0), trans(Var(0))) == I), is_pair: Unfolding(name='is_pair', decl=is_pair, args=[], body=Exists([a!1955, b!1956], pair(a!1955, b!1956) == c!2365), ax=|= ForAll(c!1957, is_pair(c!1957) == (Exists([a!1955, b!1956], pair(a!1955, b!1956) == c!1957))), _subst_fun_body=Exists([a!1955, b!1956], pair(a!1955, b!1956) == Var(2))), is_rel: Unfolding(name='is_rel', decl=is_rel, args=[], body=ForAll(p!1959, Implies(∈(p!1959, R!2493), is_pair(p!1959))), ax=|= ForAll(R, is_rel(R) == (ForAll(p!1959, Implies(∈(p!1959, R), is_pair(p!1959))))), _subst_fun_body=ForAll(p!1959, Implies(∈(p!1959, Var(1)), is_pair(p!1959)))), is_set: Unfolding(name='is_set', decl=is_set, args=[], body=Exists(A, reflects(P!1963, A)), ax=|= ForAll(P, is_set(P) == (Exists(A, reflects(P, A)))), _subst_fun_body=Exists(A, reflects(Var(1), A))), is_summable: Unfolding(name='is_summable', decl=is_summable, args=[], body=Exists(y, has_sum(a!1654, 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: Unfolding(name='is_symm', decl=is_symm, args=[], body=trans(A!895) == A!895, ax=|= ForAll(A, is_symm(A) == (trans(A) == A)), _subst_fun_body=trans(Var(0)) == Var(0)), iterate: Unfolding(name='iterate', decl=iterate, args=[], body=Lambda(i, If(i <= 0, x!1439, f!1438[iterate(f!1438, x!1439)[ToReal(i - 1)]])), ax=|= ForAll([f, x], iterate(f, x) == (Lambda(i, If(i <= 0, x, f[iterate(f, x)[ToReal(i - 1)]])))), _subst_fun_body=Lambda(i, If(i <= 0, Var(2), Var(1)[iterate(Var(1), Var(2))[ToReal(i - 1)]]))), join: Unfolding(name='join', decl=join, args=[], body=Interval(min(lo(i!1397), lo(j!1398)), R.max(hi(i!1397), hi(j!1398))), ax=|= ForAll([i, j], join(i, j) == Interval(min(lo(i), lo(j)), R.max(hi(i), hi(j)))), _subst_fun_body=Interval(min(lo(Var(0)), lo(Var(1))), R.max(hi(Var(0)), hi(Var(1))))), krondelta: Unfolding(name='krondelta', decl=krondelta, args=[], body=Lambda(i, If(i == n!1443, 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))), lim: Unfolding(name='lim', decl=lim, args=[], body=f!1615(A!1616), ax=|= ForAll(A!1422, lim(A!1422) == f!1615(A!1422)), _subst_fun_body=f!1615(Var(0))), max: Unfolding(name='max', decl=max, args=[], body=Lambda(i, If(i == 0, a!1521[0], If(i > 0, R.max(max(a!1521)[i - 1], a!1521[i]), R.max(max(a!1521)[i + 1], a!1521[i])))), ax=|= ForAll(a, max(a) == (Lambda(i, If(i == 0, a[0], If(i > 0, R.max(max(a)[i - 1], a[i]), R.max(max(a)[i + 1], a[i])))))), _subst_fun_body=Lambda(i, If(i == 0, Var(1)[0], If(i > 0, R.max(max(Var(1))[i - 1], Var(1)[i]), R.max(max(Var(1))[i + 1], Var(1)[i]))))), meet: Unfolding(name='meet', decl=meet, args=[], body=Interval(R.max(lo(i!1388), lo(j!1389)), min(hi(i!1388), hi(j!1389))), ax=|= ForAll([i, j], meet(i, j) == Interval(R.max(lo(i), lo(j)), min(hi(i), hi(j)))), _subst_fun_body=Interval(R.max(lo(Var(0)), lo(Var(1))), min(hi(Var(0)), hi(Var(1))))), mid: Unfolding(name='mid', decl=mid, args=[], body=(lo(i!1405) + hi(i!1405))/2, ax=|= ForAll(i, mid(i) == (lo(i) + hi(i))/2), _subst_fun_body=(lo(Var(0)) + hi(Var(0)))/2), min: Unfolding(name='min', decl=min, args=[], body=If(x!517 <= y!518, x!517, y!518), 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: Unfolding(name='mu', decl=mu, args=[], body=mu_iter(A!1031, 0), ax=|= ForAll(A, mu(A) == mu_iter(A, 0)), _subst_fun_body=mu_iter(Var(0), 0)), mu_iter: Unfolding(name='mu_iter', decl=mu_iter, args=[], body=If(A!1029[n!1030], n!1030, mu_iter(A!1029, n!1030 + 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: Unfolding(name='mul', decl=mul, args=[], body=x!419*y!420, ax=|= ForAll([x, y], mul(x, y) == x*y), _subst_fun_body=Var(0)*Var(1)), nested: Unfolding(name='nested', decl=nested, args=[], body=ForAll(n, subset(An!1893[n + 1], An!1893[n])), ax=|= ForAll(An, nested(An) == (ForAll(n, subset(An[n + 1], An[n])))), _subst_fun_body=ForAll(n, subset(Var(1)[n + 1], Var(1)[n]))), next: Unfolding(name='next', decl=next, args=[], body=T_Bool(Lambda(t!1102, val(p!1103)[t!1102 + 1])), ax=|= ForAll(p, next(p) == T_Bool(Lambda(t!1102, val(p)[t!1102 + 1]))), _subst_fun_body=T_Bool(Lambda(t!1102, val(Var(1))[t!1102 + 1]))), nonneg: Unfolding(name='nonneg', decl=nonneg, args=[], body=absR(x!495) == x!495, ax=|= ForAll(x, nonneg(x) == (absR(x) == x)), _subst_fun_body=absR(Var(0)) == Var(0)), odd: Unfolding(name='odd', decl=odd, args=[], body=Exists(y, x!272 == 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: Unfolding(name='one', decl=one, args=[], body=1, ax=|= one == 1, _subst_fun_body=1), ones: Unfolding(name='ones', decl=ones, args=[], body=NDArray(Unit(n!1843), 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_int: Unfolding(name='open_int', decl=open_int, args=[], body=Lambda(z, And(x!1867 < z, z < y!1868)), ax=|= ForAll([x, y], open_int(x, y) == (Lambda(z, And(x < z, z < y)))), _subst_fun_body=Lambda(z, And(Var(1) < z, z < Var(2)))), pair: Unfolding(name='pair', decl=pair, args=[], body=upair(ZF.sing(a!2363), upair(a!2363, b!2364)), ax=|= ForAll([a!1955, b!1956], pair(a!1955, b!1956) == upair(ZF.sing(a!1955), upair(a!1955, b!1956))), _subst_fun_body=upair(ZF.sing(Var(0)), upair(Var(0), Var(1)))), perp: Unfolding(name='perp', decl=perp, args=[], body=Vec3.dot(u!1931, v!1932) == 0, ax=|= ForAll([u, v], perp(u, v) == (Vec3.dot(u, v) == 0)), _subst_fun_body=Vec3.dot(Var(0), Var(1)) == 0), pick: Unfolding(name='pick', decl=pick, args=[], body=f!1979(a!1980), ax=|= ForAll(a!1955, pick(a!1955) == f!1979(a!1955)), _subst_fun_body=f!1979(Var(0))), pos: Unfolding(name='pos', decl=pos, args=[], body=Lambda(i, If(i >= 0, a!1444[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: Unfolding(name='pow', decl=pow, args=[], body=x!569**y!570, ax=|= ForAll([x, y], pow(x, y) == x**y), _subst_fun_body=Var(0)**Var(1)), powers: Unfolding(name='powers', decl=powers, args=[], body=Lambda(i, If(i == 0, 1, If(i < 0, powers(x!1655)[i + 1]/x!1655, x!1655*powers(x!1655)[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])))), pownat: Unfolding(name='pownat', decl=pownat, args=[], body=If(n!579 == 0, 1, If(n!579 > 0, x!578*pownat(x!578, n!579 - 1), pownat(x!578, n!579 + 1)/x!578)), ax=|= ForAll([x, n], pownat(x, n) == If(n == 0, 1, If(n > 0, x*pownat(x, n - 1), pownat(x, n + 1)/x))), _subst_fun_body=If(Var(1) == 0, 1, If(Var(1) > 0, Var(0)*pownat(Var(0), Var(1) - 1), pownat(Var(0), Var(1) + 1)/Var(0)))), prime: Unfolding(name='prime', decl=prime, args=[], body=And(n!297 > 1, Not(Exists([p, q], And(p > 1, q > 1, n!297 == 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))))), prod: Unfolding(name='prod', decl=prod, args=[], body=sep(pow(pow(union(A!2420, B!2421))), Lambda(p!1959, Exists([x, y], And(And(∈(x, A!2420), ∈(y, B!2421)), p!1959 == pair(x, y))))), ax=|= ForAll([A, B], prod(A, B) == sep(pow(pow(union(A, B))), Lambda(p!1959, Exists([x, y], And(And(∈(x, A), ∈(y, B)), p!1959 == pair(x, y)))))), _subst_fun_body=sep(pow(pow(union(Var(0), Var(1)))), Lambda(p!1959, Exists([x, y], And(And(∈(x, Var(3)), ∈(y, Var(4))), p!1959 == pair(x, y)))))), ran: Unfolding(name='ran', decl=ran, args=[], body=sep(bigunion(bigunion(R!2495)), Lambda(y, Exists(x, ∈(pair(x, y), R!2495)))), ax=|= ForAll(R, ran(R) == sep(bigunion(bigunion(R)), Lambda(y, Exists(x, ∈(pair(x, y), R))))), _subst_fun_body=sep(bigunion(bigunion(Var(0))), Lambda(y, Exists(x, ∈(pair(x, y), Var(2)))))), reflects: Unfolding(name='reflects', decl=reflects, args=[], body=ForAll(x, ∈(x, A!1962) == P!1961[x]), ax=|= ForAll([P, A], reflects(P, A) == (ForAll(x, ∈(x, A) == P[x]))), _subst_fun_body=ForAll(x, ∈(x, Var(2)) == Var(1)[x])), safe_pred: Unfolding(name='safe_pred', decl=safe_pred, args=[], body=If(is(Z, n!340), Z, pred(n!340)), 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)))), search: Unfolding(name='search', decl=search, args=[], body=If(P!324[n!325], n!325, If(P!324[-n!325], -n!325, If(P!324[n!325 + 1], 1, 0))), ax=|= ForAll([P, n!301], search(P, n!301) == If(P[n!301], n!301, If(P[-n!301], -n!301, If(P[n!301 + 1], 1, 0)))), _subst_fun_body=If(Var(0)[Var(1)], Var(1), If(Var(0)[-Var(1)], -Var(1), If(Var(0)[Var(1) + 1], 1, 0)))), sgn: Unfolding(name='sgn', decl=sgn, args=[], body=If(x!432 > 0, 1, If(x!432 < 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: Unfolding(name='shift', decl=shift, args=[], body=Lambda(x, A!1871[x - c!1872]), ax=|= ForAll([A, c], shift(A, c) == (Lambda(x, A[x - c]))), _subst_fun_body=Lambda(x, Var(1)[x - Var(2)])), sin: Unfolding(name='sin', decl=sin, args=[], body=Map(sin, a!1568), ax=|= ForAll(a, sin(a) == Map(sin, a)), _subst_fun_body=Map(sin, Var(0))), snd: Unfolding(name='snd', decl=snd, args=[], body=If(ZF.sing(ZF.sing(fst(p!2367))) == p!2367, fst(p!2367), pick(ZFSet.sub(bigunion(p!2367), ZF.sing(fst(p!2367))))), ax=|= ForAll(p!1959, snd(p!1959) == If(ZF.sing(ZF.sing(fst(p!1959))) == p!1959, fst(p!1959), pick(ZFSet.sub(bigunion(p!1959), ZF.sing(fst(p!1959)))))), _subst_fun_body=If(ZF.sing(ZF.sing(fst(Var(0)))) == Var(0), fst(Var(0)), pick(ZFSet.sub(bigunion(Var(0)), ZF.sing(fst(Var(0))))))), sqrt: Unfolding(name='sqrt', decl=sqrt, args=[], body=x!588**(1/2), ax=|= ForAll(x, sqrt(x) == x**(1/2)), _subst_fun_body=Var(0)**(1/2)), sub: Unfolding(name='sub', decl=sub, args=[], body=x!415 - y!416, ax=|= ForAll([x, y], sub(x, y) == x - y), _subst_fun_body=Var(0) - Var(1)), tan: Unfolding(name='tan', decl=tan, args=[], body=sin(x!643)/cos(x!643), ax=|= ForAll(x, tan(x) == sin(x)/cos(x)), _subst_fun_body=sin(Var(0))/cos(Var(0))), tand: Unfolding(name='tand', decl=tand, args=[], body=T_Bool(Lambda(t!1087, And(val(p!1088)[t!1087], val(q!1089)[t!1087]))), ax=|= ForAll([p, q], tand(p, q) == T_Bool(Lambda(t!1087, And(val(p)[t!1087], val(q)[t!1087])))), _subst_fun_body=T_Bool(Lambda(t!1087, And(val(Var(1))[t!1087], val(Var(2))[t!1087])))), temp.valid: Unfolding(name='temp.valid', decl=temp.valid, args=[], body=val(p!1107)[0], ax=|= ForAll(p, temp.valid(p) == val(p)[0]), _subst_fun_body=val(Var(0))[0]), timpl: Unfolding(name='timpl', decl=timpl, args=[], body=T_Bool(Lambda(t!1093, Implies(val(p!1094)[t!1093], val(q!1095)[t!1093]))), ax=|= ForAll([p, q], timpl(p, q) == T_Bool(Lambda(t!1093, Implies(val(p)[t!1093], val(q)[t!1093])))), _subst_fun_body=T_Bool(Lambda(t!1093, Implies(val(Var(1))[t!1093], val(Var(2))[t!1093])))), tint: Unfolding(name='tint', decl=tint, args=[], body=T_Int(K(Int, x!1143)), ax=|= ForAll(x, tint(x) == T_Int(K(Int, x))), _subst_fun_body=T_Int(K(Int, Var(0)))), tnot: Unfolding(name='tnot', decl=tnot, args=[], body=T_Bool(Lambda(t!1085, Not(val(p!1086)[t!1085]))), ax=|= ForAll(p, tnot(p) == T_Bool(Lambda(t!1085, Not(val(p)[t!1085])))), _subst_fun_body=T_Bool(Lambda(t!1085, Not(val(Var(1))[t!1085])))), to_int: Unfolding(name='to_int', decl=to_int, args=[], body=If(is(Z, n!342), 0, 1 + to_int(pred(n!342))), 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: Unfolding(name='tor', decl=tor, args=[], body=T_Bool(Lambda(t!1090, Or(val(p!1091)[t!1090], val(q!1092)[t!1090]))), ax=|= ForAll([p, q], tor(p, q) == T_Bool(Lambda(t!1090, Or(val(p)[t!1090], val(q)[t!1090])))), _subst_fun_body=T_Bool(Lambda(t!1090, Or(val(Var(1))[t!1090], val(Var(2))[t!1090])))), union: Unfolding(name='union', decl=union, args=[], body=bigunion(upair(A!2072, B!2073)), ax=|= ForAll([A, B], union(A, B) == bigunion(upair(A, B))), _subst_fun_body=bigunion(upair(Var(0), Var(1)))), upper_bound: Unfolding(name='upper_bound', decl=upper_bound, args=[], body=ForAll(y, Implies(A!1277[y], EReal.le(y, x!1278))), ax=|= ForAll([A, x], upper_bound(A, x) == (ForAll(y, Implies(A[y], EReal.le(y, x))))), _subst_fun_body=ForAll(y, Implies(Var(1)[y], EReal.le(y, Var(2))))), valid: Unfolding(name='valid', decl=valid, args=[], body=ForAll(w, val(a!1039)[w]), ax=|= ForAll(a, valid(a) == (ForAll(w, val(a)[w]))), _subst_fun_body=ForAll(w, val(Var(1))[w])), where: Unfolding(name='where', decl=where, args=[], body=Lambda(i, If(mask!1440[i], a!1441[i], b!1442[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: Unfolding(name='width', decl=width, args=[], body=hi(i!1404) - lo(i!1404), ax=|= ForAll(i, width(i) == hi(i) - lo(i)), _subst_fun_body=hi(Var(0)) - lo(Var(0))), zero: Unfolding(name='zero', decl=zero, args=[], body=NDArray(Unit(n!1842), K(Int, 0)), ax=|= ForAll(n, zero(n) == NDArray(Unit(n), K(Int, 0))), _subst_fun_body=NDArray(Unit(Var(0)), 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.free_vars(e: ExprRef) → set[ExprRef]

Get an overapproximation of free variables in a term. This is used for skolemization.

>>> x,y = smt.Ints("x y")
>>> z = FreshVar("z", smt.IntSort())
>>> assert z in free_vars(x + y + z)

Parameters:: e (ExprRef)
Return type:: set[ExprRef]

kdrag.kernel.fresh_const(q: QuantifierRef, prefixes=None) → list[ExprRef]

Generate fresh constants of same sort as quantifier.

Parameters:: q (QuantifierRef)
Return type:: list[ExprRef]

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, prefixes=None) → 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.is_declared(e: ExprRef | FuncDeclRef) → bool

Parameters:: e (ExprRef | FuncDeclRef)
Return type:: bool

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.make_unfolding(pf: Proof) → Unfolding

Take an axiom of the form |= forall x0 x1 …, xn, f(x0, x1, …, xn) = body and return a Defn object for f. Unfolding judgments can be used with unfold_defns.

>>> x,y,z = smt.Ints("x y z")
>>> pf = kd.prove(smt.ForAll([x,y], x + y == y + x + 0)) # has shape of definition, but not "definitional"
>>> defn = make_unfolding(pf)
>>> unfold_defns(z + 42, [defn])
(42 + z + 0, |= z + 42 == 42 + z + 0)

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

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.open_binder(lam: QuantifierRef) → tuple[list[ExprRef], ExprRef]

Open a quantifier with fresh variables. This achieves the locally nameless representation https://chargueraud.org/research/2009/ln/main.pdf where it is harder to go wrong.

The variables are schema variables which when used in a proof may be generalized

>>> x = smt.Int("x")
>>> open_binder(smt.ForAll([x], x > 0))
([x!...], x!... > 0)

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

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.register_definition(defn: Unfolding)

Can register other unfoldings besides those generated by define. This may be useful to get unfolding for objects constructed in roundabout ays.

Parameters:: defn (Unfolding)

kdrag.kernel.rename_vars2(pf: Proof, vs: list[ExprRef], patterns=[], no_patterns=[]) → Proof

Rename bound variables and also attach triggers

>>> x,y = smt.Ints("x y")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> rename_vars2(kd.prove(smt.ForAll([x, y], x + 1 > x)), [y,x], patterns=[x+y])
|= ForAll([y, x], y + 1 > y)
>>> rename_vars2(kd.prove(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:

pf (Proof)
vs (list[ExprRef])

Return type:

Proof

kdrag.kernel.specialize(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.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.trigger(pf: Proof, patterns: list[ExprRef] = [], no_patterns: list[ExprRef] = []) → Proof

Add e-matching triggers to a quantified proof. Logically speaking, does nothing.

>>> x,y = smt.Ints("x y")
>>> p = kd.prove(smt.ForAll([x,y], y > 0, x + y > x))
>>> p.thm.num_patterns()
0
>>> p2 = trigger(p, patterns=[x + y])
>>> p2
|= ForAll([x, y], Implies(y > 0, x + y > x))
>>> p2.thm.pattern(0)
Var(1) + Var(0)

Parameters:

pf (Proof)
patterns (list[ExprRef])
no_patterns (list[ExprRef])

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]

kdrag.kernel.unfold_defns(e: ExprRef, defns: Sequence[Unfolding]) → tuple[ExprRef, Proof]

Unfold definitions in an expression.

Parameters:

e (ExprRef)
defns (Sequence[Unfolding])

Return type:

tuple[ExprRef, Proof]