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[, fvs, 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, ...])	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.
`weaken`(pf, fvs)

Classes

`Judgement`()	Judgements should be constructed by smart constructors.
`Proof`(fvs, 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(fvs: frozenset[ExprRef], 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:

fvs (frozenset[ExprRef])
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

fvs: frozenset[ExprRef]

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, fvs=frozenset({}), 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=[A!982], 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=[P!207], 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=[A!100], 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=[A!1249], 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=[P!326], 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=[A!62], 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=[a!1448, b!1449], body=Lambda(i, a!1448[i] + b!1449[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=[a!1473, b!1474], body=Lambda(i, a!1473[i]/b!1474[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=[a!1460, b!1461], body=Lambda(i, a!1460[i]*b!1461[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=[a!1475], body=Lambda(i, -a!1475[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=[a!1458, b!1459], body=Lambda(i, a!1458[i] - b!1459[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=[A!24], 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=[f!400, g!401], 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=[f!406, g!407], 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=[f!404, g!405], 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=[f!402, g!403], 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=[A!926], 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=[A!1010], 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=[A!1358], 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=[x!1072, a!1073], 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=[x!1074, a!1075, b!1076], 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=[x!188], 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=[z1!0, z2!1], 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=[z1!4, z2!5], 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=[z1!2, z2!3], 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=[z!1185], 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=[x!1281], 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=[x!1208, y!1209], 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=[x!1198, y!1199], 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=[i!1406, j!1407], 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=[I!1420, J!1421], 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=[i!1387], 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=[i!1413, j!1414], 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=[x!698, y!699], 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=[a!665], 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=[x!689], 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=[x!666], 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=[x!716, y!717], 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=[x!663], 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=[x!664], 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=[x!688], 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=[u!1989, v!1990], body=If(shape(u!1989) == shape(v!1990), NDArray(shape(u!1989), Lambda(k, data(u!1989)[k] + data(v!1990)[k])), add_undef(u!1989, v!1990)), 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=[x!364, y!365], 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))))), PosEReal0.add: Unfolding(name='PosEReal0.add', decl=PosEReal0.add, args=[x!1932, y!1933], body=If(Or(is(Inf, x!1932), is(Inf, y!1933)), Inf, Fin(fin(x!1932) + fin(y!1933))), ax=|= ForAll([x, y], PosEReal0.add(x, y) == If(Or(is(Inf, x), is(Inf, y)), Inf, Fin(fin(x) + fin(y)))), _subst_fun_body=If(Or(is(Inf, Var(0)), is(Inf, Var(1))), Inf, Fin(fin(Var(0)) + fin(Var(1))))), PosEReal0.le: Unfolding(name='PosEReal0.le', decl=PosEReal0.le, args=[x!1944, y!1945], body=If(is(Inf, y!1945), True, If(is(Inf, x!1944), False, fin(x!1944) <= fin(y!1945))), ax=|= ForAll([x, y], PosEReal0.le(x, y) == If(is(Inf, y), True, If(is(Inf, x), False, fin(x) <= fin(y)))), _subst_fun_body=If(is(Inf, Var(1)), True, If(is(Inf, Var(0)), False, fin(Var(0)) <= fin(Var(1))))), PosEReal0.mul: Unfolding(name='PosEReal0.mul', decl=PosEReal0.mul, args=[x!1954, y!1955], body=If(Or(is(Inf, x!1954), is(Inf, y!1955)), Inf, Fin(fin(x!1954)*fin(y!1955))), ax=|= ForAll([x, y], PosEReal0.mul(x, y) == If(Or(is(Inf, x), is(Inf, y)), Inf, Fin(fin(x)*fin(y)))), _subst_fun_body=If(Or(is(Inf, Var(0)), is(Inf, Var(1))), Inf, Fin(fin(Var(0))*fin(Var(1))))), R.add: Unfolding(name='R.add', decl=R.add, args=[x!408, y!409], 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=[x!1166, y!1167], 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=[x!498, y!499], 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=[x!585], 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=[x!646], 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=[c!1282, f!1283], 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=[x!1425], 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=[a!1433], 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=[a!1430, n!1431], 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=[x!1476, a!1477], body=Lambda(n, x!1476*a!1477[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=[A!1913, M!1914], body=ForAll(x, Implies(A!1913[x], M!1914 <= 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=[A!1915], body=RSet.sup(Lambda(x, RSet.has_lb(A!1915, 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=[A!1892], body=Exists(M, has_ub(A!1892, 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=[c!1911], body=Lambda(x, x == c!1911), ax=|= ForAll(c, RSet.sing(c) == (Lambda(x, x == c))), _subst_fun_body=Lambda(x, x == Var(1))), Real.sqrt: Unfolding(name='Real.sqrt', decl=Real.sqrt, args=[x!588], body=x!588**(1/2), ax=|= ForAll(x, Real.sqrt(x) == x**(1/2)), _subst_fun_body=Var(0)**(1/2)), T_Int.add: Unfolding(name='T_Int.add', decl=T_Int.add, args=[x!1077, y!1078], 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=[x!1081, y!1082], 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=[x!1083, y!1084], 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=[x!1079, y!1080], 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=[u!1313, v!1314], 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=[u!1326, v!1327], body=Real.sqrt(Vec2.norm2(Vec2.sub(u!1326, v!1327))), ax=|= ForAll([u, v], Vec2.dist(u, v) == Real.sqrt(Vec2.norm2(Vec2.sub(u, v)))), _subst_fun_body=Real.sqrt(Vec2.norm2(Vec2.sub(Var(0), Var(1))))), Vec2.dot: Unfolding(name='Vec2.dot', decl=Vec2.dot, args=[u!1318, v!1319], 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=[u!1317], 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=[u!1321], body=Real.sqrt(Vec2.dot(u!1321, u!1321)), ax=|= ForAll(u, Vec2.norm(u) == Real.sqrt(Vec2.dot(u, u))), _subst_fun_body=Real.sqrt(Vec2.dot(Var(0), Var(0)))), Vec2.norm2: Unfolding(name='Vec2.norm2', decl=Vec2.norm2, args=[u!1320], 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=[u!1315, v!1316], 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=[u!1997, v!1998], body=Vec3(x(u!1997) + x(v!1998), y(u!1997) + y(v!1998), z(u!1997) + z(v!1998)), 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=[u!2032, v!2033], body=Real.sqrt(Vec3.norm2(Vec3.sub(u!2032, v!2033))), ax=|= ForAll([u, v], Vec3.dist(u, v) == Real.sqrt(Vec3.norm2(Vec3.sub(u, v)))), _subst_fun_body=Real.sqrt(Vec3.norm2(Vec3.sub(Var(0), Var(1))))), Vec3.dot: Unfolding(name='Vec3.dot', decl=Vec3.dot, args=[u!2014, v!2015], body=x(u!2014)*x(v!2015) + y(u!2014)*y(v!2015) + z(u!2014)*z(v!2015), 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=[u!2003], body=Vec3(-x(u!2003), -y(u!2003), -z(u!2003)), 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=[u!2027], body=Real.sqrt(Vec3.norm2(u!2027)), ax=|= ForAll(u, Vec3.norm(u) == Real.sqrt(Vec3.norm2(u))), _subst_fun_body=Real.sqrt(Vec3.norm2(Var(0)))), Vec3.norm2: Unfolding(name='Vec3.norm2', decl=Vec3.norm2, args=[u!2023], body=Vec3.dot(u!2023, u!2023), 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=[a!2004, u!2005], body=Vec3(a!2004*x(u!2005), a!2004*y(u!2005), a!2004*z(u!2005)), 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=[u!2001, v!2002], body=Vec3(x(u!2001) - x(v!2002), y(u!2001) - y(v!2002), z(u!2001) - z(v!2002)), 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=[A!2063], body=Lambda(x, ∈(x, A!2063)), 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=[x!2136], body=upair(x!2136, x!2136), 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=[A!2068, B!2069], body=ForAll(x, Implies(∈(x, A!2068), ∈(x, B!2069))), 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=[A!2418, B!2419], body=sep(A!2418, Lambda(x, Not(∈(x, B!2419)))), 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=[A!339], 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=[A!336, y!337], 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=[A!333, y!334], 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=[A!338], 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=[A!335], 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))), absR: Unfolding(name='absR', decl=absR, args=[x!431], 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=[x!1210, y!1211], 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=[x!474, y!475, eps!476], 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=[p!1101], 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=[x!1149, r!1150], 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=[P!329, N!330], 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=[p!1105, q!1106], 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=[A!1025, n!1026], 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=[P!331, N!332], 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=[A!1027, n!1028], 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=[a!2253], body=sep(pick(a!2253), Lambda(x, ForAll(b!2059, Implies(∈(b!2059, a!2253), ∈(x, b!2059))))), ax=|= ForAll(a!2058, biginter(a!2058) == sep(pick(a!2058), Lambda(x, ForAll(b!2059, Implies(∈(b!2059, a!2058), ∈(x, b!2059)))))), _subst_fun_body=sep(pick(Var(0)), Lambda(x, ForAll(b!2059, Implies(∈(b!2059, Var(2)), ∈(x, b!2059)))))), cauchy_mod: Unfolding(name='cauchy_mod', decl=cauchy_mod, args=[a!1677, mod!1678], body=ForAll(eps, Implies(eps > 0, ForAll([m, k], Implies(And(m > mod!1678[eps], k > mod!1678[eps]), absR(a!1677[m] - a!1677[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=[x!563], body=-floor(-x!563), ax=|= ForAll(x, ceil(x) == -floor(-x)), _subst_fun_body=-floor(-Var(0))), cinter: Unfolding(name='cinter', decl=cinter, args=[An!1929], body=Lambda(x, ForAll(n, An!1929[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=[c!1328, r!1329], 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=[A!1022], 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=[x!1907, y!1908], body=Lambda(z, And(x!1907 <= z, z <= y!1908)), 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=[f!644, g!645], 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=[z!1175], 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=[f!652, x!653], 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))))))), cross: Unfolding(name='cross', decl=cross, args=[u!2036, v!2037], body=Vec3(y(u!2036)*z(v!2037) - z(u!2036)*y(v!2037), z(u!2036)*x(v!2037) - x(u!2036)*z(v!2037), x(u!2036)*y(v!2037) - y(u!2036)*x(v!2037)), 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=[a!1492], body=Lambda(i, If(i == 0, a!1492[0], If(i > 0, cumsum(a!1492)[i - 1] + a!1492[i], -cumsum(a!1492)[i + 1] - a!1492[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=[An!1930], body=Lambda(x, Exists(n, An!1930[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=[a!1436, n!1437], 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=[a!1432], 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=[a!1447], body=Lambda(i, a!1447[i + 1] - a!1447[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=[f!650, x!651], 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=[a!1434, n!1435], 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=[R!2584], body=sep(bigunion(bigunion(R!2584)), Lambda(x, Exists(y, ∈(pair(x, y), R!2584)))), 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=[F!1428, a!1429], 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=[n!363], 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=[P!327, n!328], 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=[n!298, m!299], 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=[x!271], 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=[p!1098], 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=[t!1186], body=C(Real.cos(t!1186), Real.sin(t!1186)), ax=|= ForAll(t, expi(t) == C(Real.cos(t), Real.sin(t))), _subst_fun_body=C(Real.cos(Var(0)), Real.sin(Var(0)))), eye: Unfolding(name='eye', decl=eye, args=[n!1634], body=Lambda([i, j], If(i == j, 1, 0)), ax=|= ForAll(n, eye(n) == (Lambda([i, j], If(i == j, 1, 0)))), _subst_fun_body=Lambda([i, j], If(i == j, 1, 0))), fact: Unfolding(name='fact', decl=fact, args=[n!300], 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=[a!1588, n!1589], body=cumsum(a!1588)[n!1589], 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=[x!546], 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=[a!341], 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=[p!2456], body=pick(biginter(p!2456)), ax=|= ForAll(p!2062, fst(p!2062) == pick(biginter(p!2062))), _subst_fun_body=pick(biginter(Var(0)))), geom: Unfolding(name='geom', decl=geom, args=[x!1426], 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=[a!1671, M!1672], body=ForAll(n, absR(a!1671[n]) <= M!1672), 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=[a!1679, y!1680], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll(n, Implies(n > N, absR(a!1679[n] - y!1680) < 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=[f!647, p!648, L!649], 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=[A!1903, x!1904], body=And(A!1903[x!1904], RSet.sup(A!1903) == x!1904), 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=[a!1719, y!1720], body=has_lim(cumsum(a!1719), y!1720), 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=[A!1890, M!1891], body=ForAll(x, Implies(A!1890[x], x <= M!1891)), 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=[a!1032, b!1033], 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=[x!1132, y!1133], 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=[p!1140, x!1141, y!1142], 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=[a!1036, b!1037], 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=[S!1427], 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=[x!1135, y!1136], 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=[x!1138], 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=[a!1038], 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=[A!2271, B!2272], body=sep(A!2271, Lambda(x, ∈(x, B!2272))), 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=[a!1034, b!1035], 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=[a!1673], body=Exists(M, has_bound(a!1673, 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=[a!1676], body=ForAll(eps, Implies(eps > 0, Exists(N, ForAll([m, k], Implies(And(m > N, k > N), absR(a!1676[m] - a!1676[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=[A!1386], 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=[f!658], 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=[a!1681], body=Exists(y, has_lim(a!1681, 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=[f!657], 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=[I!1403], 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=[A!897], 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=[f!1284], 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=[A!1279, x!1280], 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=[a!1674], body=ForAll([n, m], Implies(n <= m, a!1674[n] <= a!1674[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=[a!1675], body=ForAll(n, a!1675[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=[S!1151], 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=[A!896], 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=[c!2455], body=Exists([a!2058, b!2059], pair(a!2058, b!2059) == c!2455), ax=|= ForAll(c!2060, is_pair(c!2060) == (Exists([a!2058, b!2059], pair(a!2058, b!2059) == c!2060))), _subst_fun_body=Exists([a!2058, b!2059], pair(a!2058, b!2059) == Var(2))), is_rel: Unfolding(name='is_rel', decl=is_rel, args=[R!2583], body=ForAll(p!2062, Implies(∈(p!2062, R!2583), is_pair(p!2062))), ax=|= ForAll(R, is_rel(R) == (ForAll(p!2062, Implies(∈(p!2062, R), is_pair(p!2062))))), _subst_fun_body=ForAll(p!2062, Implies(∈(p!2062, Var(1)), is_pair(p!2062)))), is_set: Unfolding(name='is_set', decl=is_set, args=[P!2066], body=Exists(A, reflects(P!2066, 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=[a!1721], body=Exists(y, has_sum(a!1721, 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=[A!895], 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=[f!1438, x!1439], 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=[i!1397, j!1398], 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=[n!1443], 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=[A!1683], body=f!1682(A!1683), ax=|= ForAll(A!1422, lim(A!1422) == f!1682(A!1422)), _subst_fun_body=f!1682(Var(0))), max: Unfolding(name='max', decl=max, args=[a!1543], body=Lambda(i, If(i == 0, a!1543[0], If(i > 0, R.max(max(a!1543)[i - 1], a!1543[i]), R.max(max(a!1543)[i + 1], a!1543[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=[i!1388, j!1389], 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=[i!1405], 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=[x!517, y!518], 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=[A!1031], 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=[A!1029, n!1030], 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=[x!419, y!420], 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=[An!1931], body=ForAll(n, subset(An!1931[n + 1], An!1931[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=[p!1103], 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=[x!495], 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=[x!272], 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=[n!1988], body=NDArray(Unit(n!1988), 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=[x!1905, y!1906], body=Lambda(z, And(x!1905 < z, z < y!1906)), 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=[a!2453, b!2454], body=upair(ZF.sing(a!2453), upair(a!2453, b!2454)), ax=|= ForAll([a!2058, b!2059], pair(a!2058, b!2059) == upair(ZF.sing(a!2058), upair(a!2058, b!2059))), _subst_fun_body=upair(ZF.sing(Var(0)), upair(Var(0), Var(1)))), perp: Unfolding(name='perp', decl=perp, args=[u!2034, v!2035], body=Vec3.dot(u!2034, v!2035) == 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=[a!2083], body=f!2082(a!2083), ax=|= ForAll(a!2058, pick(a!2058) == f!2082(a!2058)), _subst_fun_body=f!2082(Var(0))), pos: Unfolding(name='pos', decl=pos, args=[a!1446], body=Lambda(i, If(i >= 0, a!1446[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=[x!569, y!570], 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=[x!1722], body=Lambda(i, If(i == 0, 1, If(i < 0, powers(x!1722)[i + 1]/x!1722, x!1722*powers(x!1722)[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=[x!578, n!579], 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=[n!297], 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=[A!2510, B!2511], body=sep(pow(pow(union(A!2510, B!2511))), Lambda(p!2062, Exists([x, y], And(And(∈(x, A!2510), ∈(y, B!2511)), p!2062 == pair(x, y))))), ax=|= ForAll([A, B], prod(A, B) == sep(pow(pow(union(A, B))), Lambda(p!2062, Exists([x, y], And(And(∈(x, A), ∈(y, B)), p!2062 == pair(x, y)))))), _subst_fun_body=sep(pow(pow(union(Var(0), Var(1)))), Lambda(p!2062, Exists([x, y], And(And(∈(x, Var(3)), ∈(y, Var(4))), p!2062 == pair(x, y)))))), ran: Unfolding(name='ran', decl=ran, args=[R!2585], body=sep(bigunion(bigunion(R!2585)), Lambda(y, Exists(x, ∈(pair(x, y), R!2585)))), 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=[P!2064, A!2065], body=ForAll(x, ∈(x, A!2065) == P!2064[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])), rseq.abs: Unfolding(name='rseq.abs', decl=rseq.abs, args=[a!1637], body=Map(absR, a!1637), ax=|= ForAll(a, rseq.abs(a) == Map(absR, a)), _subst_fun_body=Map(absR, Var(0))), rseq.cos: Unfolding(name='rseq.cos', decl=rseq.cos, args=[a!1636], body=Map(Real.cos, a!1636), ax=|= ForAll(a, rseq.cos(a) == Map(Real.cos, a)), _subst_fun_body=Map(Real.cos, Var(0))), rseq.dot: Unfolding(name='rseq.dot', decl=rseq.dot, args=[n!1602, a!1603, b!1604], body=finsum((Array Int Real).mul(a!1603, b!1604), n!1602), ax=|= ForAll([n, a, b], rseq.dot(n, a, b) == finsum((Array Int Real).mul(a, b), n)), _subst_fun_body=finsum((Array Int Real).mul(Var(1), Var(2)), Var(0))), rseq.outer: Unfolding(name='rseq.outer', decl=rseq.outer, args=[a!1632, b!1633], body=Lambda([i, j], a!1632[i]*b!1633[j]), ax=|= ForAll([a, b], rseq.outer(a, b) == (Lambda([i, j], a[i]*b[j]))), _subst_fun_body=Lambda([i, j], Var(2)[i]*Var(3)[j])), rseq.sin: Unfolding(name='rseq.sin', decl=rseq.sin, args=[a!1635], body=Map(Real.sin, a!1635), ax=|= ForAll(a, rseq.sin(a) == Map(Real.sin, a)), _subst_fun_body=Map(Real.sin, Var(0))), safe_pred: Unfolding(name='safe_pred', decl=safe_pred, args=[n!340], 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=[P!324, n!325], 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=[x!432], 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=[A!1909, c!1910], body=Lambda(x, A!1909[x - c!1910]), ax=|= ForAll([A, c], shift(A, c) == (Lambda(x, A[x - c]))), _subst_fun_body=Lambda(x, Var(1)[x - Var(2)])), snd: Unfolding(name='snd', decl=snd, args=[p!2457], body=If(ZF.sing(ZF.sing(fst(p!2457))) == p!2457, fst(p!2457), pick(ZFSet.sub(bigunion(p!2457), ZF.sing(fst(p!2457))))), ax=|= ForAll(p!2062, snd(p!2062) == If(ZF.sing(ZF.sing(fst(p!2062))) == p!2062, fst(p!2062), pick(ZFSet.sub(bigunion(p!2062), ZF.sing(fst(p!2062)))))), _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))))))), sub: Unfolding(name='sub', decl=sub, args=[x!415, y!416], 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=[x!643], body=Real.sin(x!643)/Real.cos(x!643), ax=|= ForAll(x, tan(x) == Real.sin(x)/Real.cos(x)), _subst_fun_body=Real.sin(Var(0))/Real.cos(Var(0))), tand: Unfolding(name='tand', decl=tand, args=[p!1088, q!1089], 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=[p!1107], 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=[p!1094, q!1095], 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=[x!1143], 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=[p!1086], 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=[n!342], 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=[p!1091, q!1092], 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=[A!2159, B!2160], body=bigunion(upair(A!2159, B!2160)), 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=[A!1277, x!1278], 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=[a!1039], 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=[mask!1440, a!1441, b!1442], 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=[i!1404], 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=[n!1987], body=NDArray(Unit(n!1987), 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, fvs=frozenset({})) → 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]

kdrag.kernel.weaken(pf: Proof, fvs: Sequence[ExprRef]) → Proof

Parameters:

pf (Proof)
fvs (Sequence[ExprRef])

Return type:

Proof