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!1135], body=Exists(finwit!1134,        ForAll(x!1133,               A!1135[x!1133] ==               Contains(finwit!1134, Unit(x!1133)))), ax=|= ForAll(A,        (Array (Array Sierpinski Bool) Bool).finite(A) ==        (Exists(finwit!1134,                ForAll(x!1133,                       A[x!1133] ==                       Contains(finwit!1134, Unit(x!1133)))))), _subst_fun_body=Exists(finwit!1134,        ForAll(x!1133,               Var(2)[x!1133] ==               Contains(finwit!1134, Unit(x!1133))))), (Array (Array Sierpinski!1 Bool) Bool).finite: Unfolding(name='(Array (Array Sierpinski!1 Bool) Bool).finite', decl=(Array (Array Sierpinski!1 Bool) Bool).finite, args=[A!2973], body=Exists(finwit!2972,        ForAll(x!2971,               A!2973[x!2971] ==               Contains(finwit!2972, Unit(x!2971)))), ax=|= ForAll(A,        (Array (Array Sierpinski!1 Bool) Bool).finite(A) ==        (Exists(finwit!2972,                ForAll(x!2971,                       A[x!2971] ==                       Contains(finwit!2972, Unit(x!2971)))))), _subst_fun_body=Exists(finwit!2972,        ForAll(x!2971,               Var(2)[x!2971] ==               Contains(finwit!2972, Unit(x!2971))))), (Array Bool Bool).choose: Unfolding(name='(Array Bool Bool).choose', decl=(Array Bool Bool).choose, args=[P!288], body=If(P!288[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!128], body=Exists(finwit!127,        ForAll(x!126,               A!128[x!126] ==               Contains(finwit!127, Unit(x!126)))), ax=|= ForAll(A,        (Array Bool Bool).finite(A) ==        (Exists(finwit!127,                ForAll(x!126,                       A[x!126] ==                       Contains(finwit!127, Unit(x!126)))))), _subst_fun_body=Exists(finwit!127,        ForAll(x!126,               Var(2)[x!126] ==               Contains(finwit!127, Unit(x!126))))), (Array EReal Bool).finite: Unfolding(name='(Array EReal Bool).finite', decl=(Array EReal Bool).finite, args=[A!1491], body=Exists(finwit!1490,        ForAll(x!1489,               A!1491[x!1489] ==               Contains(finwit!1490, Unit(x!1489)))), ax=|= ForAll(A,        (Array EReal Bool).finite(A) ==        (Exists(finwit!1490,                ForAll(x!1489,                       A[x!1489] ==                       Contains(finwit!1490, Unit(x!1489)))))), _subst_fun_body=Exists(finwit!1490,        ForAll(x!1489,               Var(2)[x!1489] ==               Contains(finwit!1490, Unit(x!1489))))), (Array Int Bool).choose: Unfolding(name='(Array Int Bool).choose', decl=(Array Int Bool).choose, args=[P!419], body=search(P!419, 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!72], body=Exists(finwit!71,        ForAll(x!70,               A!72[x!70] == Contains(finwit!71, Unit(x!70)))), ax=|= ForAll(A,        (Array Int Bool).finite(A) ==        (Exists(finwit!71,                ForAll(x!70,                       A[x!70] ==                       Contains(finwit!71, Unit(x!70)))))), _subst_fun_body=Exists(finwit!71,        ForAll(x!70,               Var(2)[x!70] ==               Contains(finwit!71, Unit(x!70))))), (Array Int Real).add: Unfolding(name='(Array Int Real).add', decl=(Array Int Real).add, args=[a!3233, b!3234], body=Lambda(i, a!3233[i] + b!3234[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!3250, b!3251], body=Lambda(i, a!3250[i]/b!3251[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!3241, b!3242], body=Lambda(i, a!3241[i]*b!3242[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!3252], body=Lambda(i, -a!3252[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!3239, b!3240], body=Lambda(i, a!3239[i] - b!3240[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!524, g!525], body=Lambda(x, f!524[x] + g!525[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!530, g!531], body=Lambda(x, f!530[x]/g!531[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!528, g!529], body=Lambda(x, f!528[x]*g!529[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!526, g!527], body=Lambda(x, f!526[x] - g!527[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!1079], body=Exists(finwit!1078,        ForAll(x!1077,               A!1079[x!1077] ==               Contains(finwit!1078, Unit(x!1077)))), ax=|= ForAll(A,        (Array Sierpinski Bool).finite(A) ==        (Exists(finwit!1078,                ForAll(x!1077,                       A[x!1077] ==                       Contains(finwit!1078, Unit(x!1077)))))), _subst_fun_body=Exists(finwit!1078,        ForAll(x!1077,               Var(2)[x!1077] ==               Contains(finwit!1078, Unit(x!1077))))), (Array Sierpinski Bool).open: Unfolding(name='(Array Sierpinski Bool).open', decl=(Array Sierpinski Bool).open, args=[A!1163], body=Or(A!1163 == K(Sierpinski, False),    A!1163 == K(Sierpinski, True),    A!1163 == 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 Sierpinski!1 Bool).finite: Unfolding(name='(Array Sierpinski!1 Bool).finite', decl=(Array Sierpinski!1 Bool).finite, args=[A!2917], body=Exists(finwit!2916,        ForAll(x!2915,               A!2917[x!2915] ==               Contains(finwit!2916, Unit(x!2915)))), ax=|= ForAll(A,        (Array Sierpinski!1 Bool).finite(A) ==        (Exists(finwit!2916,                ForAll(x!2915,                       A[x!2915] ==                       Contains(finwit!2916, Unit(x!2915)))))), _subst_fun_body=Exists(finwit!2916,        ForAll(x!2915,               Var(2)[x!2915] ==               Contains(finwit!2916, Unit(x!2915))))), (Array Sierpinski!1 Bool).open: Unfolding(name='(Array Sierpinski!1 Bool).open', decl=(Array Sierpinski!1 Bool).open, args=[A!3001], body=Or(A!3001 == K(Sierpinski!1, False),    A!3001 == K(Sierpinski!1, True),    A!3001 == Store(K(Sierpinski!1, False), S1, True)), ax=|= ForAll(A,        (Array Sierpinski!1 Bool).open(A) ==        Or(A == K(Sierpinski!1, False),           A == K(Sierpinski!1, True),           A == Store(K(Sierpinski!1, False), S1, True))), _subst_fun_body=Or(Var(0) == K(Sierpinski!1, False),    Var(0) == K(Sierpinski!1, True),    Var(0) == Store(K(Sierpinski!1, False), S1, True))), (Array Vec2 Bool).finite: Unfolding(name='(Array Vec2 Bool).finite', decl=(Array Vec2 Bool).finite, args=[A!1603], body=Exists(finwit!1602,        ForAll(x!1601,               A!1603[x!1601] ==               Contains(finwit!1602, Unit(x!1601)))), ax=|= ForAll(A,        (Array Vec2 Bool).finite(A) ==        (Exists(finwit!1602,                ForAll(x!1601,                       A[x!1601] ==                       Contains(finwit!1602, Unit(x!1601)))))), _subst_fun_body=Exists(finwit!1602,        ForAll(x!1601,               Var(2)[x!1601] ==               Contains(finwit!1602, Unit(x!1601))))), Atom.fresh: Unfolding(name='Atom.fresh', decl=Atom.fresh, args=[x!1224, a!1225], body=a!1225 != x!1224, 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!1226, a!1227, b!1228], body=If(x!1226 == a!1227,    b!1228,    If(x!1226 == b!1228, a!1227, x!1226)), 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!259], body=If(Length(val(x!259)) == 0,    0,    BV2Int(Nth(val(x!259), 0)) +    2*    BitVecN.to_int(BitVecN(seq.extract(val(x!259),                                       1,                                       Length(val(x!259)) - 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!1332], body=C.mul(z!1332, conj(z!1332)), 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!1523], body=Implies(is(real, x!1523), val(x!1523) >= 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!1450, y!1451], body=If(And(is(Real, x!1450), is(Real, y!1451)),    Real(val(x!1450) + val(y!1451)),    If(And(is(Inf, x!1450), Not(is(NegInf, y!1451))),       Inf,       If(And(Not(is(NegInf, x!1450)), is(Inf, y!1451)),          Inf,          If(And(is(NegInf, x!1450), Not(is(Inf, y!1451))),             NegInf,             If(And(Not(is(Inf, x!1450)), is(NegInf, y!1451)),                NegInf,                add_undef(x!1450, y!1451)))))), 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!1440, y!1441], body=If(x!1440 == y!1441,    True,    If(is(NegInf, x!1440),       True,       If(is(Inf, y!1441),          True,          If(is(NegInf, y!1441),             False,             If(is(Inf, x!1440),                False,                If(And(is(Real, x!1440), is(Real, y!1441)),                   val(x!1440) <= val(y!1441),                   unreachable!1439)))))), 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!1439))))))), _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!1439))))))), Interval.add: Unfolding(name='Interval.add', decl=Interval.add, args=[i!1726, j!1727], body=Interval(lo(i!1726) + lo(j!1727), hi(i!1726) + hi(j!1727)), 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!1740, J!1741], body=Interval(If(And(hi(I!1740)*hi(J!1741) <=                 lo(I!1740)*lo(J!1741),                 hi(I!1740)*hi(J!1741) <=                 hi(I!1740)*lo(J!1741),                 hi(I!1740)*hi(J!1741) <=                 lo(I!1740)*hi(J!1741)),             hi(I!1740)*hi(J!1741),             If(And(lo(I!1740)*lo(J!1741) <=                    hi(I!1740)*lo(J!1741),                    lo(I!1740)*lo(J!1741) <=                    lo(I!1740)*hi(J!1741)),                lo(I!1740)*lo(J!1741),                If(And(hi(I!1740)*lo(J!1741) <=                       lo(I!1740)*hi(J!1741)),                   hi(I!1740)*lo(J!1741),                   lo(I!1740)*hi(J!1741)))),          If(And(hi(I!1740)*hi(J!1741) >=                 lo(I!1740)*lo(J!1741),                 hi(I!1740)*hi(J!1741) >=                 hi(I!1740)*lo(J!1741),                 hi(I!1740)*hi(J!1741) >=                 lo(I!1740)*hi(J!1741)),             hi(I!1740)*hi(J!1741),             If(And(lo(I!1740)*lo(J!1741) <=                    hi(I!1740)*lo(J!1741),                    lo(I!1740)*lo(J!1741) <=                    lo(I!1740)*hi(J!1741)),                lo(I!1740)*lo(J!1741),                If(And(hi(I!1740)*lo(J!1741) <=                       lo(I!1740)*hi(J!1741)),                   hi(I!1740)*lo(J!1741),                   lo(I!1740)*hi(J!1741))))), 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!1709], body=Lambda(x, And(lo(i!1709) <= x, x <= hi(i!1709))), 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!1733, j!1734], body=Interval(lo(i!1733) - hi(j!1734), hi(i!1733) - lo(j!1734)), 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!821, y!822], body=KnownBits_1(ones(x!821) & ones(y!822),             ~(~unknowns(x!821) & ~ones(x!821) |               ~unknowns(y!822) & ~ones(y!822) |               ones(x!821) & ones(y!822))), 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!788], body=KnownBits_1(a!788, 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!812], body=KnownBits_1(~unknowns(x!812) & ~ones(x!812),             unknowns(x!812)), 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!789], body=unknowns(x!789) == 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!839, y!840], body=KnownBits_1(ones(x!839) | ones(y!840),             ~(ones(x!839) |               ones(y!840) |               ~unknowns(x!839) &               ~ones(x!839) &               ~unknowns(y!840) &               ~ones(y!840))), 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!786], body=Lambda(a, ~unknowns(x!786) & a == ones(x!786)), 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!787], body=ones(x!787) & unknowns(x!787) == 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!811], body=~unknowns(x!811) & ~ones(x!811), 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!1936, v!1937], body=If(shape(u!1936) == shape(v!1937),    NDArray(shape(u!1936),            Lambda(k, data(u!1936)[k] + data(v!1937)[k])),    add_undef(u!1936, v!1937)), 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!488, y!489], body=If(is(Z, x!488), y!489, S(Nat.add(pred(x!488), y!489))), 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!1879, y!1880], body=If(Or(is(Inf, x!1879), is(Inf, y!1880)),    Inf,    Fin(fin(x!1879) + fin(y!1880))), 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!1891, y!1892], body=If(is(Inf, y!1892),    True,    If(is(Inf, x!1891), False, fin(x!1891) <= fin(y!1892))), 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!1901, y!1902], body=If(Or(is(Inf, x!1901), is(Inf, y!1902)),    Inf,    Fin(fin(x!1901)*fin(y!1902))), 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!532, y!533], body=x!532 + y!533, 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!1313, y!1314], body=absR(x!1313 - y!1314), ax=|= ForAll([x!1292, y!1293],        R.dist(x!1292, y!1293) == absR(x!1292 - y!1293)), _subst_fun_body=absR(Var(0) - Var(1))), R.max: Unfolding(name='R.max', decl=R.max, args=[x!622, y!623], body=If(x!622 >= y!623, x!622, y!623), 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!709], body=x!709*x!709, 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!770], body=K(Real, x!770), 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!1524, f!1525], body=Lambda(x, mul(c!1524, f!1525[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!3210], body=Lambda(i, x!3210), 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!3218], body=Lambda(i, a!3218[-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!3215, n!3216], body=Lambda(i, a!3215[i - n!3216]), 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!3253, a!3254], body=Lambda(n, x!3253*a!3254[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!1860, M!1861], body=ForAll(x, Implies(A!1860[x], M!1861 <= 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!1862], body=RSet.sup(Lambda(x, RSet.has_lb(A!1862, 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!1839], body=Exists(M, has_ub(A!1839, 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!1858], body=Lambda(x, x == c!1858), 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!712], body=x!712**(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!1229, y!1230], body=T_Int(Lambda(t, val(x!1229)[t] + val(y!1230)[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!1233, y!1234], body=T_Bool(Lambda(t, val(x!1233)[t] >= val(y!1234)[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!1235, y!1236], body=T_Bool(Lambda(t, val(x!1235)[t] <= val(y!1236)[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!1231, y!1232], body=T_Real(Lambda(t, val(x!1231)[t] + val(y!1232)[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!1555, v!1556], body=Vec2(x(u!1555) + x(v!1556), y(u!1555) + y(v!1556)), 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.cross: Unfolding(name='Vec2.cross', decl=Vec2.cross, args=[u!1572, v!1573], body=x(u!1572)*y(v!1573) - y(u!1572)*x(v!1573), ax=|= ForAll([u, v], Vec2.cross(u, v) == x(u)*y(v) - y(u)*x(v)), _subst_fun_body=x(Var(0))*y(Var(1)) - y(Var(0))*x(Var(1))), Vec2.dist: Unfolding(name='Vec2.dist', decl=Vec2.dist, args=[u!1570, v!1571], body=Real.sqrt(Vec2.norm2(Vec2.sub(u!1570, v!1571))), 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!1562, v!1563], body=x(u!1562)*x(v!1563) + y(u!1562)*y(v!1563), 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!1559], body=Vec2(-x(u!1559), -y(u!1559)), 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!1565], body=Real.sqrt(Vec2.dot(u!1565, u!1565)), 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!1564], body=Vec2.dot(u!1564, u!1564), ax=|= ForAll(u, Vec2.norm2(u) == Vec2.dot(u, u)), _subst_fun_body=Vec2.dot(Var(0), Var(0))), Vec2.smul: Unfolding(name='Vec2.smul', decl=Vec2.smul, args=[r!1560, u!1561], body=Vec2(r!1560*x(u!1561), r!1560*y(u!1561)), ax=|= ForAll([r, u], Vec2.smul(r, u) == Vec2(r*x(u), r*y(u))), _subst_fun_body=Vec2(Var(0)*x(Var(1)), Var(0)*y(Var(1)))), Vec2.sub: Unfolding(name='Vec2.sub', decl=Vec2.sub, args=[u!1557, v!1558], body=Vec2(x(u!1557) - x(v!1558), y(u!1557) - y(v!1558)), 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!2038, v!2039], body=Vec3(x(u!2038) + x(v!2039),      y(u!2038) + y(v!2039),      z(u!2038) + z(v!2039)), 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!2073, v!2074], body=Real.sqrt(Vec3.norm2(Vec3.sub(u!2073, v!2074))), 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!2055, v!2056], body=x(u!2055)*x(v!2056) + y(u!2055)*y(v!2056) + z(u!2055)*z(v!2056), 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!2044], body=Vec3(-x(u!2044), -y(u!2044), -z(u!2044)), 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!2068], body=Real.sqrt(Vec3.norm2(u!2068)), 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!2064], body=Vec3.dot(u!2064, u!2064), 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!2045, u!2046], body=Vec3(a!2045*x(u!2046), a!2045*y(u!2046), a!2045*z(u!2046)), 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!2042, v!2043], body=Vec3(x(u!2042) - x(v!2043),      y(u!2042) - y(v!2043),      z(u!2042) - z(v!2043)), 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!2104], body=Lambda(x, ∈(x, A!2104)), 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!2193], body=upair(x!2193, x!2193), 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!2109, B!2110], body=ForAll(x, Implies(∈(x, A!2109), ∈(x, B!2110))), 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!2472, B!2473], body=sep(A!2472, Lambda(x, Not(∈(x, B!2473)))), 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!432], body=And(ZSet.is_ub(A!432), ZSet.is_lb(A!432)), 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!429, y!430], body=ForAll(x, Implies(A!429[x], y!430 <= 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!426, y!427], body=ForAll(x, Implies(A!426[x], x <= y!427)), 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!431], body=Exists(x, ZSet.has_lb(A!431, 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!428], body=Exists(x, ZSet.has_ub(A!428, 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!887, y!888],        mul(x!887, y!888) == mul(y!888, x!887)), ax=|= abelian == (ForAll([x!887, y!888],         mul(x!887, y!888) == mul(y!888, x!887))), _subst_fun_body=ForAll([x!887, y!888],        mul(x!887, y!888) == mul(y!888, x!887))), absR: Unfolding(name='absR', decl=absR, args=[x!555], body=If(x!555 >= 0, x!555, -x!555), 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!1452, y!1453], body=Or(And(is(Real, x!1452), is(Real, y!1453)),    And(is(Inf, x!1452), Not(is(NegInf, y!1453))),    And(Not(is(NegInf, x!1452)), is(Inf, y!1453)),    And(is(NegInf, x!1452), Not(is(Inf, y!1453))),    And(Not(is(Inf, x!1452)), is(NegInf, y!1453))), 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!598, y!599, eps!600], body=If(x!598 - y!599 > 0, x!598 - y!599, -(x!598 - y!599)) <= eps!600, 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!1253], body=T_Bool(Lambda(t!1251,               ForAll(dt!1252,                      Implies(dt!1252 >= 0,                              val(p!1253)[t!1251 + dt!1252])))), ax=|= ForAll(p,        always(p) ==        T_Bool(Lambda(t!1251,                      ForAll(dt!1252,                             Implies(dt!1252 >= 0,                                     val(p)[t!1251 + dt!1252]))))), _subst_fun_body=T_Bool(Lambda(t!1251,               ForAll(dt!1252,                      Implies(dt!1252 >= 0,                              val(Var(2))[t!1251 + dt!1252]))))), and1: Unfolding(name='and1', decl=and1, args=[x!862, y!863], body=not1(nand1(x!862, y!863)), ax=|= ForAll([x, y], and1(x, y) == not1(nand1(x, y))), _subst_fun_body=not1(nand1(Var(0), Var(1)))), and2: Unfolding(name='and2', decl=and2, args=[x!877, y!878], body=Concat(and1(Extract(1, 1, x!877), Extract(1, 1, y!878)),        and1(Extract(0, 0, x!877), Extract(0, 0, y!878))), ax=|= ForAll([x, y],        and2(x, y) ==        Concat(and1(Extract(1, 1, x), Extract(1, 1, y)),               and1(Extract(0, 0, x), Extract(0, 0, y)))), _subst_fun_body=Concat(and1(Extract(1, 1, Var(0)), Extract(1, 1, Var(1))),        and1(Extract(0, 0, Var(0)), Extract(0, 0, Var(1))))), ball: Unfolding(name='ball', decl=ball, args=[x!1297, r!1298], body=Lambda(y!1296, absR(y!1296 - x!1297) < r!1298), ax=|= ForAll([x!1292, r!1295],        ball(x!1292, r!1295) ==        (Lambda(y!1296, absR(y!1296 - x!1292) < r!1295))), _subst_fun_body=Lambda(y!1296, absR(y!1296 - Var(1)) < Var(2))), bchoose: Unfolding(name='bchoose', decl=bchoose, args=[P!422, N!423], body=downsearch(P!422, N!423), 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!1257, q!1258], body=T_Bool(Lambda(t!1256,               val(p!1257)[t!1256] == val(q!1258)[t!1256])), ax=|= ForAll([p, q],        beq(p, q) ==        T_Bool(Lambda(t!1256,                      val(p)[t!1256] == val(q)[t!1256]))), _subst_fun_body=T_Bool(Lambda(t!1256,               val(Var(1))[t!1256] == val(Var(2))[t!1256]))), between: Unfolding(name='between', decl=between, args=[p!1676, q!1677, a!1678], body=And(collinear(p!1676, q!1677, a!1678),     Vec2.dot(Vec2.sub(q!1677, p!1676),              Vec2.sub(a!1678, p!1676)) >=     0,     Vec2.dot(Vec2.sub(p!1676, q!1677),              Vec2.sub(a!1678, q!1677)) >=     0), ax=|= ForAll([p, q, a],        between(p, q, a) ==        And(collinear(p, q, a),            Vec2.dot(Vec2.sub(q, p), Vec2.sub(a, p)) >= 0,            Vec2.dot(Vec2.sub(p, q), Vec2.sub(a, q)) >= 0)), _subst_fun_body=And(collinear(Var(0), Var(1), Var(2)),     Vec2.dot(Vec2.sub(Var(1), Var(0)),              Vec2.sub(Var(2), Var(0))) >=     0,     Vec2.dot(Vec2.sub(Var(0), Var(1)),              Vec2.sub(Var(2), Var(1))) >=     0)), bexist: Unfolding(name='bexist', decl=bexist, args=[A!1181, n!1182], body=If(n!1182 < 0,    False,    Or(A!1181[n!1182], bexists(A!1181, n!1182 - 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!424, N!425], body=P!424[bchoose(P!424, N!425)], 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!1183, n!1184], body=If(n!1184 < 0,    True,    And(A!1183[n!1184], bforall(A!1183, n!1184 - 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!2310], body=sep(pick(a!2310),     Lambda(x,            ForAll(b!2100,                   Implies(∈(b!2100, a!2310), ∈(x, b!2100))))), ax=|= ForAll(a!2099,        biginter(a!2099) ==        sep(pick(a!2099),            Lambda(x,                   ForAll(b!2100,                          Implies(∈(b!2100, a!2099),                                  ∈(x, b!2100)))))), _subst_fun_body=sep(pick(Var(0)),     Lambda(x,            ForAll(b!2100,                   Implies(∈(b!2100, Var(2)), ∈(x, b!2100)))))), ceil: Unfolding(name='ceil', decl=ceil, args=[x!687], body=-floor(-x!687), ax=|= ForAll(x, ceil(x) == -floor(-x)), _subst_fun_body=-floor(-Var(0))), cinter: Unfolding(name='cinter', decl=cinter, args=[An!1876], body=Lambda(x, ForAll(n, An!1876[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!1706, p!1707], body=Lambda(q,        Vec2.norm2(Vec2.sub(p!1707, c!1706)) ==        Vec2.norm2(Vec2.sub(q, c!1706))), ax=|= ForAll([c, p],        circle(c, p) ==        (Lambda(q,                Vec2.norm2(Vec2.sub(p, c)) ==                Vec2.norm2(Vec2.sub(q, c))))), _subst_fun_body=Lambda(q,        Vec2.norm2(Vec2.sub(Var(2), Var(1))) ==        Vec2.norm2(Vec2.sub(q, Var(1))))), closed_int: Unfolding(name='closed_int', decl=closed_int, args=[x!1854, y!1855], body=Lambda(z, And(x!1854 <= z, z <= y!1855)), 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)))), collinear: Unfolding(name='collinear', decl=collinear, args=[p!1671, q!1672, a!1673], body=Vec2.cross(Vec2.sub(q!1672, p!1671),            Vec2.sub(a!1673, p!1671)) == 0, ax=|= ForAll([p, q, a],        collinear(p, q, a) ==        (Vec2.cross(Vec2.sub(q, p), Vec2.sub(a, p)) == 0)), _subst_fun_body=Vec2.cross(Vec2.sub(Var(1), Var(0)),            Vec2.sub(Var(2), Var(0))) == 0), comp: Unfolding(name='comp', decl=comp, args=[f!768, g!769], body=Lambda(x, f!768[g!769[x]]), ax=|= ForAll([f, g], comp(f, g) == (Lambda(x, f[g[x]]))), _subst_fun_body=Lambda(x, Var(1)[Var(2)[x]])), cong_seg: Unfolding(name='cong_seg', decl=cong_seg, args=[p!1680, q!1681, a!1682, b!1683], body=Vec2.norm2(Vec2.sub(p!1680, q!1681)) == Vec2.norm2(Vec2.sub(a!1682, b!1683)), ax=|= ForAll([p, q, a, b],        cong_seg(p, q, a, b) ==        (Vec2.norm2(Vec2.sub(p, q)) ==         Vec2.norm2(Vec2.sub(a, b)))), _subst_fun_body=Vec2.norm2(Vec2.sub(Var(0), Var(1))) == Vec2.norm2(Vec2.sub(Var(2), Var(3)))), conj: Unfolding(name='conj', decl=conj, args=[z!1322], body=C(re(z!1322), -im(z!1322)), 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!776, x!777], body=ForAll(eps,        Implies(eps > 0,                Exists(delta,                       And(delta > 0,                           ForAll(y,                                  Implies(absR(x!777 - y) <                                         delta,                                         absR(f!776[x!777] -                                         f!776[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!2077, v!2078], body=Vec3(y(u!2077)*z(v!2078) - z(u!2077)*y(v!2078),      z(u!2077)*x(v!2078) - x(u!2077)*z(v!2078),      x(u!2077)*y(v!2078) - y(u!2077)*x(v!2078)), 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!3266], body=Lambda(i,        If(i == 0,           a!3266[0],           If(i > 0,              cumsum(a!3266)[i - 1] + a!3266[i],              -cumsum(a!3266)[i + 1] - a!3266[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!1877], body=Lambda(x, Exists(n, An!1877[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!3221, n!3222], body=Lambda(i, a!3221[i*n!3222]), 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!3217], body=RSeq.shift(a!3217, 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!3232], body=Lambda(i, a!3232[i + 1] - a!3232[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!774, x!775], body=Exists(y, has_diff_at(f!774, x!775, 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!3219, n!3220], body=Lambda(i, a!3219[i/n!3220]), ax=|= ForAll([a, n], dilate(a, n) == (Lambda(i, a[i/n]))), _subst_fun_body=Lambda(i, Var(1)[i/Var(2)])), dir: Unfolding(name='dir', decl=dir, args=[p!1692], body=ray(Vec2(ToReal(0), ToReal(0)), p!1692), ax=|= ForAll(p, dir(p) == ray(Vec2(ToReal(0), ToReal(0)), p)), _subst_fun_body=ray(Vec2(ToReal(0), ToReal(0)), Var(0))), dom: Unfolding(name='dom', decl=dom, args=[R!2637], body=sep(bigunion(bigunion(R!2637)),     Lambda(x, Exists(y, ∈(pair(x, y), R!2637)))), 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!3213, a!3214], body=Lambda(i, a!3214[F!3213[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!487], body=If(is(Z, n!487), Z, S(S(double(pred(n!487))))), 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!420, n!421], body=If(P!420[n!421],    n!421,    If(n!421 < 0, 0, downsearch(P!420, n!421 - 1))), ax=|= ForAll([P, n!394],        downsearch(P, n!394) ==        If(P[n!394],           n!394,           If(n!394 < 0, 0, downsearch(P, n!394 - 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!391, m!392], body=Exists(p, m!392 == n!391*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!364], body=Exists(y, x!364 == 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!1250], body=T_Bool(Lambda(t!1248,               Exists(dt!1249,                      And(dt!1249 >= 0,                          val(p!1250)[t!1248 + dt!1249])))), ax=|= ForAll(p,        eventually(p) ==        T_Bool(Lambda(t!1248,                      Exists(dt!1249,                             And(dt!1249 >= 0,                                 val(p)[t!1248 + dt!1249]))))), _subst_fun_body=T_Bool(Lambda(t!1248,               Exists(dt!1249,                      And(dt!1249 >= 0,                          val(Var(2))[t!1248 + dt!1249]))))), expi: Unfolding(name='expi', decl=expi, args=[t!1333], body=C(Real.cos(t!1333), Real.sin(t!1333)), ax=|= ForAll(t, expi(t) == C(Real.cos(t), Real.sin(t))), _subst_fun_body=C(Real.cos(Var(0)), Real.sin(Var(0)))), fact: Unfolding(name='fact', decl=fact, args=[n!393], body=If(n!393 <= 0, 1, n!393*fact(n!393 - 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))), floor: Unfolding(name='floor', decl=floor, args=[x!670], body=ToReal(ToInt(x!670)), 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!465], body=If(a!465 <= 0, Z, S(from_int(a!465 - 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)))), from_nat: Unfolding(name='from_nat', decl=from_nat, args=[n!434], body=If(n!434%2 == 0, n!434/2, -(n!434 + 1)/2), ax=|= ForAll(n!394,        from_nat(n!394) ==        If(n!394%2 == 0, n!394/2, -(n!394 + 1)/2)), _subst_fun_body=If(Var(0)%2 == 0, Var(0)/2, -(Var(0) + 1)/2)), fst: Unfolding(name='fst', decl=fst, args=[p!2509], body=pick(biginter(p!2509)), ax=|= ForAll(p!2103, fst(p!2103) == pick(biginter(p!2103))), _subst_fun_body=pick(biginter(Var(0)))), geom: Unfolding(name='geom', decl=geom, args=[x!3211], body=Lambda(i, pownat(x!3211, i)), ax=|= ForAll(x, geom(x) == (Lambda(i, pownat(x, i)))), _subst_fun_body=Lambda(i, pownat(Var(1), i))), has_lim_at: Unfolding(name='has_lim_at', decl=has_lim_at, args=[f!771, p!772, L!773], body=ForAll(eps,        Implies(0 < eps,                Exists(delta,                       And(delta > 0,                           ForAll(x,                                  Implies(And(0 <                                         absR(x - p!772),                                         absR(x - p!772) <                                         delta),                                         absR(f!771[x] -                                         L!773) <                                         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!1850, x!1851], body=And(A!1850[x!1851], RSet.sup(A!1850) == x!1851), 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_ub: Unfolding(name='has_ub', decl=has_ub, args=[A!1837, M!1838], body=ForAll(x, Implies(A!1837[x], x <= M!1838)), 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!1188, b!1189], body=Prop(Lambda(w, And(val(a!1188)[w], val(b!1189)[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!1280, y!1281], body=T_Bool(Lambda(t!1279,               val(x!1280)[t!1279] == val(y!1281)[t!1279])), ax=|= ForAll([x, y],        ieq(x, y) ==        T_Bool(Lambda(t!1279,                      val(x)[t!1279] == val(y)[t!1279]))), _subst_fun_body=T_Bool(Lambda(t!1279,               val(Var(1))[t!1279] == val(Var(2))[t!1279]))), if_int: Unfolding(name='if_int', decl=if_int, args=[p!1288, x!1289, y!1290], body=T_Int(Lambda(t!1287,              If(val(p!1288)[t!1287],                 val(x!1289)[t!1287],                 val(y!1290)[t!1287]))), ax=|= ForAll([p, x, y],        if_int(p, x, y) ==        T_Int(Lambda(t!1287,                     If(val(p)[t!1287],                        val(x)[t!1287],                        val(y)[t!1287])))), _subst_fun_body=T_Int(Lambda(t!1287,              If(val(Var(1))[t!1287],                 val(Var(2))[t!1287],                 val(Var(3))[t!1287])))), iimpl: Unfolding(name='iimpl', decl=iimpl, args=[a!1192, b!1193], body=Prop(Lambda(w,             ForAll(u,                    Implies(acc(w, u),                            Implies(val(a!1192)[u],                                    val(b!1193)[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!3212], body=Lambda(i, If(S!3212[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!1283, y!1284], body=T_Bool(Lambda(t!1282,               val(x!1283)[t!1282] != val(y!1284)[t!1282])), ax=|= ForAll([x, y],        ineq(x, y) ==        T_Bool(Lambda(t!1282,                      val(x)[t!1282] != val(y)[t!1282]))), _subst_fun_body=T_Bool(Lambda(t!1282,               val(Var(1))[t!1282] != val(Var(2))[t!1282]))), inext: Unfolding(name='inext', decl=inext, args=[x!1286], body=T_Int(Lambda(t!1285, val(x!1286)[t!1285 + 1])), ax=|= ForAll(x,        inext(x) == T_Int(Lambda(t!1285, val(x)[t!1285 + 1]))), _subst_fun_body=T_Int(Lambda(t!1285, val(Var(1))[t!1285 + 1]))), inot: Unfolding(name='inot', decl=inot, args=[a!1194], body=Prop(Lambda(w,             ForAll(u,                    Implies(acc(w, u),                            Implies(val(a!1194)[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!2327, B!2328], body=sep(A!2327, Lambda(x, ∈(x, B!2328))), 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!1190, b!1191], body=Prop(Lambda(w, Or(val(a!1190)[w], val(b!1191)[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_circle: Unfolding(name='is_circle', decl=is_circle, args=[A!1708], body=Exists([c, q], ForAll(p, circle(c, q)[p] == A!1708[p])), ax=|= ForAll(A,        is_circle(A) ==        (Exists([c, q], ForAll(p, circle(c, q)[p] == A[p])))), _subst_fun_body=Exists([c, q], ForAll(p, circle(c, q)[p] == Var(3)[p]))), is_cont: Unfolding(name='is_cont', decl=is_cont, args=[f!782], body=ForAll(x, cont_at(f!782, x)), ax=|= ForAll(f, is_cont(f) == (ForAll(x, cont_at(f, x)))), _subst_fun_body=ForAll(x, cont_at(Var(1), x))), is_diff: Unfolding(name='is_diff', decl=is_diff, args=[f!781], body=ForAll(x, diff_at(f!781, x)), ax=|= ForAll(f, is_diff(f) == (ForAll(x, diff_at(f, x)))), _subst_fun_body=ForAll(x, diff_at(Var(1), x))), is_dir: Unfolding(name='is_dir', decl=is_dir, args=[A!1693], body=Exists(p,        And(p != Vec2(ToReal(0), ToReal(0)),            Vec2.norm2(p) == 1,            dir(p) == A!1693)), ax=|= ForAll(A,        is_dir(A) ==        (Exists(p,                And(p != Vec2(ToReal(0), ToReal(0)),                    Vec2.norm2(p) == 1,                    dir(p) == A)))), _subst_fun_body=Exists(p,        And(p != Vec2(ToReal(0), ToReal(0)),            Vec2.norm2(p) == 1,            dir(p) == Var(1)))), is_empty: Unfolding(name='is_empty', decl=is_empty, args=[I!1723], 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!1050], body=mul(A!1050, A!1050) == A!1050, ax=|= ForAll(A, is_idem(A) == (mul(A, A) == A)), _subst_fun_body=mul(Var(0), Var(0)) == Var(0)), is_line: Unfolding(name='is_line', decl=is_line, args=[A!1635], body=Exists([p, q],        And(p != q, ForAll(a, line(p, q)[a] == A!1635[a]))), ax=|= ForAll(A,        is_line(A) ==        (Exists([p, q],                And(p != q, ForAll(a, line(p, q)[a] == A[a]))))), _subst_fun_body=Exists([p, q],        And(p != q, ForAll(a, line(p, q)[a] == Var(3)[a])))), is_linear: Unfolding(name='is_linear', decl=is_linear, args=[f!1526], body=And(ForAll([x, y],            f!1526[R.add(x, y)] ==            R.add(f!1526[x], f!1526[y])),     ForAll([x, c], f!1526[mul(c, x)] == mul(c, f!1526[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!1521, x!1522], body=And(upper_bound(A!1521, x!1522),     ForAll(y,            Implies(upper_bound(A!1521, y),                    EReal.le(x!1522, 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_open: Unfolding(name='is_open', decl=is_open, args=[S!1299], body=ForAll(x!1292,        Implies(S!1299[x!1292],                Exists(r!1295,                       And(0 < r!1295,                           subset(ball(x!1292, r!1295),                                  S!1299))))), ax=|= ForAll(S,        is_open(S) ==        (ForAll(x!1292,                Implies(S[x!1292],                        Exists(r!1295,                               And(0 < r!1295,                                   subset(ball(x!1292,                                         r!1295),                                         S))))))), _subst_fun_body=ForAll(x!1292,        Implies(Var(1)[x!1292],                Exists(r!1295,                       And(0 < r!1295,                           subset(ball(x!1292, r!1295),                                  Var(2))))))), is_orth: Unfolding(name='is_orth', decl=is_orth, args=[A!1049], body=mul(A!1049, trans(A!1049)) == 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!2508], body=Exists([a!2099, b!2100], pair(a!2099, b!2100) == c!2508), ax=|= ForAll(c!2101,        is_pair(c!2101) ==        (Exists([a!2099, b!2100],                pair(a!2099, b!2100) == c!2101))), _subst_fun_body=Exists([a!2099, b!2100], pair(a!2099, b!2100) == Var(2))), is_parallel: Unfolding(name='is_parallel', decl=is_parallel, args=[A!1667, B!1668], body=Vec2.cross(Vec2.sub(f!1663(A!1667), f!1664(A!1667)),            Vec2.sub(f!1663(B!1668), f!1664(B!1668))) == 0, ax=|= ForAll([A, B],        is_parallel(A, B) ==        (Vec2.cross(Vec2.sub(f!1663(A), f!1664(A)),                    Vec2.sub(f!1663(B), f!1664(B))) ==         0)), _subst_fun_body=Vec2.cross(Vec2.sub(f!1663(Var(0)), f!1664(Var(0))),            Vec2.sub(f!1663(Var(1)), f!1664(Var(1)))) == 0), is_perp: Unfolding(name='is_perp', decl=is_perp, args=[A!1665, B!1666], body=Vec2.dot(Vec2.sub(f!1663(A!1665), f!1664(A!1665)),          Vec2.sub(f!1663(B!1666), f!1664(B!1666))) == 0, ax=|= ForAll([A, B],        is_perp(A, B) ==        (Vec2.dot(Vec2.sub(f!1663(A), f!1664(A)),                  Vec2.sub(f!1663(B), f!1664(B))) ==         0)), _subst_fun_body=Vec2.dot(Vec2.sub(f!1663(Var(0)), f!1664(Var(0))),          Vec2.sub(f!1663(Var(1)), f!1664(Var(1)))) == 0), is_point: Unfolding(name='is_point', decl=is_point, args=[A!1632], body=Exists(p, point(p) == A!1632), ax=|= ForAll(A, is_point(A) == (Exists(p, point(p) == A))), _subst_fun_body=Exists(p, point(p) == Var(1))), is_rel: Unfolding(name='is_rel', decl=is_rel, args=[R!2636], body=ForAll(p!2103, Implies(∈(p!2103, R!2636), is_pair(p!2103))), ax=|= ForAll(R,        is_rel(R) ==        (ForAll(p!2103,                Implies(∈(p!2103, R), is_pair(p!2103))))), _subst_fun_body=ForAll(p!2103, Implies(∈(p!2103, Var(1)), is_pair(p!2103)))), is_set: Unfolding(name='is_set', decl=is_set, args=[P!2107], body=Exists(A, reflects(P!2107, A)), ax=|= ForAll(P, is_set(P) == (Exists(A, reflects(P, A)))), _subst_fun_body=Exists(A, reflects(Var(1), A))), is_symm: Unfolding(name='is_symm', decl=is_symm, args=[A!1048], body=trans(A!1048) == A!1048, 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!3223, x!3224], body=Lambda(i,        If(i <= 0,           x!3224,           f!3223[iterate(f!3223, x!3224)[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!1717, j!1718], body=Interval(min(lo(i!1717), lo(j!1718)),          R.max(hi(i!1717), hi(j!1718))), 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!3228], body=Lambda(i, If(i == n!3228, 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))), line: Unfolding(name='line', decl=line, args=[p!1633, q!1634], body=Lambda(a,        Vec2.cross(Vec2.sub(a, p!1633),                   Vec2.sub(q!1634, p!1633)) ==        0), ax=|= ForAll([p, q],        line(p, q) ==        (Lambda(a,                Vec2.cross(Vec2.sub(a, p), Vec2.sub(q, p)) ==                0))), _subst_fun_body=Lambda(a,        Vec2.cross(Vec2.sub(a, Var(1)),                   Vec2.sub(Var(2), Var(1))) ==        0)), meet: Unfolding(name='meet', decl=meet, args=[i!1710, j!1711], body=Interval(R.max(lo(i!1710), lo(j!1711)),          min(hi(i!1710), hi(j!1711))), 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!1725], body=(lo(i!1725) + hi(i!1725))/2, ax=|= ForAll(i, mid(i) == (lo(i) + hi(i))/2), _subst_fun_body=(lo(Var(0)) + hi(Var(0)))/2), midp: Unfolding(name='midp', decl=midp, args=[p!1669, q!1670], body=Vec2.smul(1/2, Vec2.add(p!1669, q!1670)), ax=|= ForAll([p, q], midp(p, q) == Vec2.smul(1/2, Vec2.add(p, q))), _subst_fun_body=Vec2.smul(1/2, Vec2.add(Var(0), Var(1)))), min: Unfolding(name='min', decl=min, args=[x!641, y!642], body=If(x!641 <= y!642, x!641, y!642), 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!1187], body=mu_iter(A!1187, 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!1185, n!1186], body=If(A!1185[n!1186], n!1186, mu_iter(A!1185, n!1186 + 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!543, y!544], body=x!543*y!544, ax=|= ForAll([x, y], mul(x, y) == x*y), _subst_fun_body=Var(0)*Var(1)), nand1: Unfolding(name='nand1', decl=nand1, args=[x!857, y!858], body=~(x!857 & y!858), ax=|= ForAll([x, y], nand1(x, y) == ~(x & y)), _subst_fun_body=~(Var(0) & Var(1))), nand2: Unfolding(name='nand2', decl=nand2, args=[x!872, y!873], body=Concat(nand1(Extract(1, 1, x!872), Extract(1, 1, y!873)),        nand1(Extract(0, 0, x!872), Extract(0, 0, y!873))), ax=|= ForAll([x, y],        nand2(x, y) ==        Concat(nand1(Extract(1, 1, x), Extract(1, 1, y)),               nand1(Extract(0, 0, x), Extract(0, 0, y)))), _subst_fun_body=Concat(nand1(Extract(1, 1, Var(0)), Extract(1, 1, Var(1))),        nand1(Extract(0, 0, Var(0)), Extract(0, 0, Var(1))))), nand2step: Unfolding(name='nand2step', decl=nand2step, args=[st!158], body=If(rom(st!158)[pc(st!158)] >> 15 == 0,    Nand2State(pc(st!158) + 1,               rom(st!158),               ram(st!158),               D(st!158),               rom(st!158)[pc(st!158)]),    Nand2State(If(If(rom(st!158)[pc(st!158)] & 7 == 0,                     False,                     If(rom(st!158)[pc(st!158)] & 7 == 1,                        If(rom(st!158)[pc(st!158)] >> 6 & 127 ==                           42,                           0,                           If(rom(st!158)[pc(st!158)] >> 6 &                              127 ==                              63,                              1,                              If(rom(st!158)[pc(st!158)] >> 6 &                                 127 ==                                 58,                                 65535,                                 If(rom(st!158)[pc(st!158)] >>                                    6 &                                    127 ==                                    12,                                    D(st!158),                                    If(rom(st!158)[pc(st!158)] >>                                       6 &                                       127 ==                                       48,                                       A(st!158),                                       If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         112,                                         rom(st!158)[A(st!158)],                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         13,                                         ~D(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         49,                                         ~A(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         113,                                         ~rom(st!158)[A(st!158)],                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         15,                                         -D(st!158),                                         If(...[...] >> 6 &                                         127 ==                                         51,                                         -A(st!158),                                         If(... >> ... & 127 ==                                         115,                                         -rom(...)[A(...)],                                         If(... & ... == 31,                                         D(...) + 1,                                         If(... == ...,                                         ... + ...,                                         If(..., ..., ...))))))))))))))) >                        0,                        If(rom(st!158)[pc(st!158)] & 7 == 2,                           If(rom(st!158)[pc(st!158)] >> 6 &                              127 ==                              42,                              0,                              If(rom(st!158)[pc(st!158)] >> 6 &                                 127 ==                                 63,                                 1,                                 If(rom(st!158)[pc(st!158)] >>                                    6 &                                    127 ==                                    58,                                    65535,                                    If(rom(st!158)[pc(st!158)] >>                                       6 &                                       127 ==                                       12,                                       D(st!158),                                       If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         48,                                         A(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         112,                                         rom(st!158)[A(st!158)],                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         13,                                         ~D(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         49,                                         ~A(st!158),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         113,                                         ~rom(st!158)[A(st!158)],                                         If(...[...] >> 6 &                                         127 ==                                         15,                                         -D(st!158),                                         If(... >> ... & 127 ==                                         51,                                         -A(st!158),                                         If(... & ... == 115,                                         -...[...],                                         If(... == ...,                                         ... + ...,                                         If(..., ..., ...)))))))))))))) ==                           0,                           If(rom(st!158)[pc(st!158)] & 7 ==                              3,                              If(rom(st!158)[pc(st!158)] >> 6 &                                 127 ==                                 42,                                 0,                                 If(rom(st!158)[pc(st!158)] >>                                    6 &                                    127 ==                                    63,                                    1,                                    If(rom(st!158)[pc(st!158)] >>                                       6 &                                       127 ==                                       58,                                       65535,                                       If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         12,                                         D(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         48,                                         A(st!158),                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         112,                                         rom(st!158)[A(st!158)],                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         13,                                         ~D(st!158),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         49,                                         ~A(st!158),                                         If(...[...] >> 6 &                                         127 ==                                         113,                                         ~rom(st!158)[A(st!158)],                                         If(... >> ... & 127 ==                                         15,                                         -D(st!158),                                         If(... & ... == 51,                                         -A(...),                                         If(... == ...,                                         -...,                                         If(..., ..., ...))))))))))))) >=                              0,                              If(rom(st!158)[pc(st!158)] & 7 ==                                 4,                                 If(rom(st!158)[pc(st!158)] >>                                    6 &                                    127 ==                                    42,                                    0,                                    If(rom(st!158)[pc(st!158)] >>                                       6 &                                       127 ==                                       63,                                       1,                                       If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         58,                                         65535,                                         If(rom(st!158)[pc(st!158)] >>                                         6 &                                         127 ==                                         12, ..., ax=|= ForAll(st,        nand2step(st) ==        If(rom(st)[pc(st)] >> 15 == 0,           Nand2State(pc(st) + 1,                      rom(st),                      ram(st),                      D(st),                      rom(st)[pc(st)]),           Nand2State(If(If(rom(st)[pc(st)] & 7 == 0,                            False,                            If(rom(st)[pc(st)] & 7 == 1,                               If(rom(st)[pc(st)] >> 6 & 127 ==                                  42,                                  0,                                  If(rom(st)[pc(st)] >> 6 &                                     127 ==                                     63,                                     1,                                     If(rom(st)[pc(st)] >> 6 &                                        127 ==                                        58,                                        65535,                                        If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         12,                                         D(st),                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         48,                                         A(st),                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         112,                                         rom(st)[A(st)],                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         13,                                         ~D(st),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         49,                                         ~A(st),                                         If(...[...] >> 6 &                                         127 ==                                         113,                                         ~rom(st)[A(st)],                                         If(... >> ... & 127 ==                                         15,                                         -D(st),                                         If(... & ... == 51,                                         -A(...),                                         If(... == ...,                                         -...,                                         If(..., ..., ...))))))))))))) >                               0,                               If(rom(st)[pc(st)] & 7 == 2,                                  If(rom(st)[pc(st)] >> 6 &                                     127 ==                                     42,                                     0,                                     If(rom(st)[pc(st)] >> 6 &                                        127 ==                                        63,                                        1,                                        If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         58,                                         65535,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         12,                                         D(st),                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         48,                                         A(st),                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         112,                                         rom(st)[A(st)],                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         13,                                         ~D(st),                                         If(...[...] >> 6 &                                         127 ==                                         49,                                         ~A(st),                                         If(... >> ... & 127 ==                                         113,                                         ~rom(...)[A(...)],                                         If(... & ... == 15,                                         -D(...),                                         If(... == ...,                                         -...,                                         If(..., ..., ...)))))))))))) ==                                  0,                                  If(rom(st)[pc(st)] & 7 == 3,                                     If(rom(st)[pc(st)] >> 6 &                                        127 ==                                        42,                                        0,                                        If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         63,                                         1,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         58,                                         65535,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         12,                                         D(st),                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         48,                                         A(st),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         112,                                         rom(st)[A(st)],                                         If(...[...] >> 6 &                                         127 ==                                         13,                                         ~D(st),                                         If(... >> ... & 127 ==                                         49,                                         ~A(st),                                         If(... & ... == 113,                                         ~...[...],                                         If(... == ...,                                         -...,                                         If(..., ..., ...))))))))))) >=                                     0,                                     If(rom(st)[pc(st)] & 7 ==                                        4,                                        If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         42,                                         0,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         63,                                         1,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         58,                                         65535,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         12,                                         D(st),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         48,                                         A(st),                                         If(...[...] >> 6 &                                         127 ==                                         112,                                         rom(st)[A(st)],                                         If(... >> ... & 127 ==                                         13,                                         ~D(st),                                         If(... & ... == 49,                                         ~A(...),                                         If(... == ...,                                         ~...,                                         If(..., ..., ...)))))))))) <                                        0,                                        If(rom(st)[pc(st)] &                                         7 ==                                         5,                                         If(rom(st)[pc(st)] >>                                         6 &                                         127 ==                                         42,                                         0,                                         If(rom(st)[pc(st)] >>                                         6 & ..., _subst_fun_body=If(rom(Var(0))[pc(Var(0))] >> 15 == 0,    Nand2State(pc(Var(0)) + 1,               rom(Var(0)),               ram(Var(0)),               D(Var(0)),               rom(Var(0))[pc(Var(0))]),    Nand2State(If(If(rom(Var(0))[pc(Var(0))] & 7 == 0,                     False,                     If(rom(Var(0))[pc(Var(0))] & 7 == 1,                        If(rom(Var(0))[pc(Var(0))] >> 6 & 127 ==                           42,                           0,                           If(rom(Var(0))[pc(Var(0))] >> 6 &                              127 ==                              63,                              1,                              If(rom(Var(0))[pc(Var(0))] >> 6 &                                 127 ==                                 58,                                 65535,                                 If(rom(Var(0))[pc(Var(0))] >>                                    6 &                                    127 ==                                    12,                                    D(Var(0)),                                    If(rom(Var(0))[pc(Var(0))] >>                                       6 &                                       127 ==                                       48,                                       A(Var(0)),                                       If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         112,                                         rom(Var(0))[A(Var(0))],                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         13,                                         ~D(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         49,                                         ~A(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         113,                                         ~rom(Var(0))[A(Var(0))],                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         15,                                         -D(Var(0)),                                         If(...[...] >> 6 &                                         127 ==                                         51,                                         -A(Var(0)),                                         If(... >> ... & 127 ==                                         115,                                         -rom(...)[A(...)],                                         If(... & ... == 31,                                         D(...) + 1,                                         If(... == ...,                                         ... + ...,                                         If(..., ..., ...))))))))))))))) >                        0,                        If(rom(Var(0))[pc(Var(0))] & 7 == 2,                           If(rom(Var(0))[pc(Var(0))] >> 6 &                              127 ==                              42,                              0,                              If(rom(Var(0))[pc(Var(0))] >> 6 &                                 127 ==                                 63,                                 1,                                 If(rom(Var(0))[pc(Var(0))] >>                                    6 &                                    127 ==                                    58,                                    65535,                                    If(rom(Var(0))[pc(Var(0))] >>                                       6 &                                       127 ==                                       12,                                       D(Var(0)),                                       If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         48,                                         A(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         112,                                         rom(Var(0))[A(Var(0))],                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         13,                                         ~D(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         49,                                         ~A(Var(0)),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         113,                                         ~rom(Var(0))[A(Var(0))],                                         If(...[...] >> 6 &                                         127 ==                                         15,                                         -D(Var(0)),                                         If(... >> ... & 127 ==                                         51,                                         -A(Var(0)),                                         If(... & ... == 115,                                         -...[...],                                         If(... == ...,                                         ... + ...,                                         If(..., ..., ...)))))))))))))) ==                           0,                           If(rom(Var(0))[pc(Var(0))] & 7 ==                              3,                              If(rom(Var(0))[pc(Var(0))] >> 6 &                                 127 ==                                 42,                                 0,                                 If(rom(Var(0))[pc(Var(0))] >>                                    6 &                                    127 ==                                    63,                                    1,                                    If(rom(Var(0))[pc(Var(0))] >>                                       6 &                                       127 ==                                       58,                                       65535,                                       If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         12,                                         D(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         48,                                         A(Var(0)),                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         112,                                         rom(Var(0))[A(Var(0))],                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         13,                                         ~D(Var(0)),                                         If(rom(...)[pc(...)] >>                                         6 &                                         127 ==                                         49,                                         ~A(Var(0)),                                         If(...[...] >> 6 &                                         127 ==                                         113,                                         ~rom(Var(0))[A(Var(0))],                                         If(... >> ... & 127 ==                                         15,                                         -D(Var(0)),                                         If(... & ... == 51,                                         -A(...),                                         If(... == ...,                                         -...,                                         If(..., ..., ...))))))))))))) >=                              0,                              If(rom(Var(0))[pc(Var(0))] & 7 ==                                 4,                                 If(rom(Var(0))[pc(Var(0))] >>                                    6 &                                    127 ==                                    42,                                    0,                                    If(rom(Var(0))[pc(Var(0))] >>                                       6 &                                       127 ==                                       63,                                       1,                                       If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         58,                                         65535,                                         If(rom(Var(0))[pc(Var(0))] >>                                         6 &                                         127 ==                                         12, ...), natpair: Unfolding(name='natpair', decl=natpair, args=[n!441, m!442], body=((n!441 + m!442)*(n!441 + m!442 + 1))/2 + m!442, ax=|= ForAll([n!394, m!404],        natpair(n!394, m!404) ==        ((n!394 + m!404)*(n!394 + m!404 + 1))/2 + m!404), _subst_fun_body=((Var(0) + Var(1))*(Var(0) + Var(1) + 1))/2 + Var(1)), natpair_to_tuple: Unfolding(name='natpair_to_tuple', decl=natpair_to_tuple, args=[k!451], body=If(k!451 < 0,    Tuple_Int_Int(-1, -1),    If(k!451 == 0,       Tuple_Int_Int(0, 0),       If(_0(natpair_to_tuple(k!451 - 1)) == 0,          Tuple_Int_Int(_1(natpair_to_tuple(k!451 - 1)) + 1,                        0),          Tuple_Int_Int(_0(natpair_to_tuple(k!451 - 1)) - 1,                        _1(natpair_to_tuple(k!451 - 1)) + 1)))), ax=|= ForAll(k!395,        natpair_to_tuple(k!395) ==        If(k!395 < 0,           Tuple_Int_Int(-1, -1),           If(k!395 == 0,              Tuple_Int_Int(0, 0),              If(_0(natpair_to_tuple(k!395 - 1)) == 0,                 Tuple_Int_Int(_1(natpair_to_tuple(k!395 - 1)) +                               1,                               0),                 Tuple_Int_Int(_0(natpair_to_tuple(k!395 - 1)) -                               1,                               _1(natpair_to_tuple(k!395 - 1)) +                               1))))), _subst_fun_body=If(Var(0) < 0,    Tuple_Int_Int(-1, -1),    If(Var(0) == 0,       Tuple_Int_Int(0, 0),       If(_0(natpair_to_tuple(Var(0) - 1)) == 0,          Tuple_Int_Int(_1(natpair_to_tuple(Var(0) - 1)) + 1,                        0),          Tuple_Int_Int(_0(natpair_to_tuple(Var(0) - 1)) - 1,                        _1(natpair_to_tuple(Var(0) - 1)) + 1))))), nested: Unfolding(name='nested', decl=nested, args=[An!1878], body=ForAll(n, subset(An!1878[n + 1], An!1878[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!1255], body=T_Bool(Lambda(t!1254, val(p!1255)[t!1254 + 1])), ax=|= ForAll(p,        next(p) == T_Bool(Lambda(t!1254, val(p)[t!1254 + 1]))), _subst_fun_body=T_Bool(Lambda(t!1254, val(Var(1))[t!1254 + 1]))), nonneg: Unfolding(name='nonneg', decl=nonneg, args=[x!619], body=absR(x!619) == x!619, ax=|= ForAll(x, nonneg(x) == (absR(x) == x)), _subst_fun_body=absR(Var(0)) == Var(0)), not1: Unfolding(name='not1', decl=not1, args=[x!859], body=nand1(x!859, x!859), ax=|= ForAll(x, not1(x) == nand1(x, x)), _subst_fun_body=nand1(Var(0), Var(0))), not2: Unfolding(name='not2', decl=not2, args=[x!874], body=Concat(not1(Extract(1, 1, x!874)),        not1(Extract(0, 0, x!874))), ax=|= ForAll(x,        not2(x) ==        Concat(not1(Extract(1, 1, x)),               not1(Extract(0, 0, x)))), _subst_fun_body=Concat(not1(Extract(1, 1, Var(0))),        not1(Extract(0, 0, Var(0))))), odd: Unfolding(name='odd', decl=odd, args=[x!365], body=Exists(y, x!365 == 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!1935], body=NDArray(Unit(n!1935), 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!1852, y!1853], body=Lambda(z, And(x!1852 < z, z < y!1853)), 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)))), or1: Unfolding(name='or1', decl=or1, args=[x!867, y!868], body=nand1(not1(x!867), not1(y!868)), ax=|= ForAll([x, y], or1(x, y) == nand1(not1(x), not1(y))), _subst_fun_body=nand1(not1(Var(0)), not1(Var(1)))), or2: Unfolding(name='or2', decl=or2, args=[x!882, y!883], body=Concat(or1(Extract(1, 1, x!882), Extract(1, 1, y!883)),        or1(Extract(0, 0, x!882), Extract(0, 0, y!883))), ax=|= ForAll([x, y],        or2(x, y) ==        Concat(or1(Extract(1, 1, x), Extract(1, 1, y)),               or1(Extract(0, 0, x), Extract(0, 0, y)))), _subst_fun_body=Concat(or1(Extract(1, 1, Var(0)), Extract(1, 1, Var(1))),        or1(Extract(0, 0, Var(0)), Extract(0, 0, Var(1))))), pair: Unfolding(name='pair', decl=pair, args=[n!463], body=from_nat(natpair(to_nat(n!463), to_nat(m!404))), ax=|= ForAll(n!394,        pair(n!394) ==        from_nat(natpair(to_nat(n!394), to_nat(m!404)))), _subst_fun_body=from_nat(natpair(to_nat(Var(0)), to_nat(m!404)))), pair: Unfolding(name='pair', decl=pair, args=[a!2506, b!2507], body=upair(ZF.sing(a!2506), upair(a!2506, b!2507)), ax=|= ForAll([a!2099, b!2100],        pair(a!2099, b!2100) ==        upair(ZF.sing(a!2099), upair(a!2099, b!2100))), _subst_fun_body=upair(ZF.sing(Var(0)), upair(Var(0), Var(1)))), perp: Unfolding(name='perp', decl=perp, args=[u!2075, v!2076], body=Vec3.dot(u!2075, v!2076) == 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!2124], body=f!2123(a!2124), ax=|= ForAll(a!2099, pick(a!2099) == f!2123(a!2099)), _subst_fun_body=f!2123(Var(0))), point: Unfolding(name='point', decl=point, args=[p!1631], body=Store(K(Vec2, False), p!1631, True), ax=|= ForAll(p, point(p) == Store(K(Vec2, False), p, True)), _subst_fun_body=Store(K(Vec2, False), Var(0), True)), pos: Unfolding(name='pos', decl=pos, args=[a!3231], body=Lambda(i, If(i >= 0, a!3231[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!693, y!694], body=x!693**y!694, ax=|= ForAll([x, y], pow(x, y) == x**y), _subst_fun_body=Var(0)**Var(1)), pownat: Unfolding(name='pownat', decl=pownat, args=[x!702, n!703], body=If(n!703 == 0,    1,    If(n!703 > 0,       x!702*pownat(x!702, n!703 - 1),       pownat(x!702, n!703 + 1)/x!702)), 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!390], body=And(n!390 > 1,     Not(Exists([p, q], And(p > 1, q > 1, n!390 == 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!2563, B!2564], body=sep(pow(pow(union(A!2563, B!2564))),     Lambda(p!2103,            Exists([x, y],                   And(And(∈(x, A!2563), ∈(y, B!2564)),                       p!2103 == pair(x, y))))), ax=|= ForAll([A, B],        prod(A, B) ==        sep(pow(pow(union(A, B))),            Lambda(p!2103,                   Exists([x, y],                          And(And(∈(x, A), ∈(y, B)),                              p!2103 == pair(x, y)))))), _subst_fun_body=sep(pow(pow(union(Var(0), Var(1)))),     Lambda(p!2103,            Exists([x, y],                   And(And(∈(x, Var(3)), ∈(y, Var(4))),                       p!2103 == pair(x, y)))))), ran: Unfolding(name='ran', decl=ran, args=[R!2638], body=sep(bigunion(bigunion(R!2638)),     Lambda(y, Exists(x, ∈(pair(x, y), R!2638)))), 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)))))), ray: Unfolding(name='ray', decl=ray, args=[p!1690, q!1691], body=Lambda(a,        And(collinear(p!1690, q!1691, a),            Vec2.dot(Vec2.sub(q!1691, p!1690),                     Vec2.sub(a, p!1690)) >=            0)), ax=|= ForAll([p, q],        ray(p, q) ==        (Lambda(a,                And(collinear(p, q, a),                    Vec2.dot(Vec2.sub(q, p), Vec2.sub(a, p)) >=                    0)))), _subst_fun_body=Lambda(a,        And(collinear(Var(1), Var(2), a),            Vec2.dot(Vec2.sub(Var(2), Var(1)),                     Vec2.sub(a, Var(1))) >=            0))), reflects: Unfolding(name='reflects', decl=reflects, args=[P!2105, A!2106], body=ForAll(x, ∈(x, A!2106) == P!2105[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=[n!464], body=If(is(Z, n!464), Z, pred(n!464)), 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!417, n!418], body=If(P!417[n!418],    n!418,    If(P!417[-n!418], -n!418, If(P!417[n!418 + 1], 1, 0))), ax=|= ForAll([P, n!394],        search(P, n!394) ==        If(P[n!394],           n!394,           If(P[-n!394], -n!394, If(P[n!394 + 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!556], body=If(x!556 > 0, 1, If(x!556 < 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!1856, c!1857], body=Lambda(x, A!1856[x - c!1857]), 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!2510], body=If(ZF.sing(ZF.sing(fst(p!2510))) == p!2510,    fst(p!2510),    pick(ZFSet.sub(bigunion(p!2510), ZF.sing(fst(p!2510))))), ax=|= ForAll(p!2103,        snd(p!2103) ==        If(ZF.sing(ZF.sing(fst(p!2103))) == p!2103,           fst(p!2103),           pick(ZFSet.sub(bigunion(p!2103),                          ZF.sing(fst(p!2103)))))), _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!539, y!540], body=x!539 - y!540, ax=|= ForAll([x, y], sub(x, y) == x - y), _subst_fun_body=Var(0) - Var(1)), tan: Unfolding(name='tan', decl=tan, args=[x!767], body=Real.sin(x!767)/Real.cos(x!767), 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!1240, q!1241], body=T_Bool(Lambda(t!1239,               And(val(p!1240)[t!1239], val(q!1241)[t!1239]))), ax=|= ForAll([p, q],        tand(p, q) ==        T_Bool(Lambda(t!1239,                      And(val(p)[t!1239], val(q)[t!1239])))), _subst_fun_body=T_Bool(Lambda(t!1239,               And(val(Var(1))[t!1239], val(Var(2))[t!1239])))), temp.valid: Unfolding(name='temp.valid', decl=temp.valid, args=[p!1259], body=val(p!1259)[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!1246, q!1247], body=T_Bool(Lambda(t!1245,               Implies(val(p!1246)[t!1245],                       val(q!1247)[t!1245]))), ax=|= ForAll([p, q],        timpl(p, q) ==        T_Bool(Lambda(t!1245,                      Implies(val(p)[t!1245], val(q)[t!1245])))), _subst_fun_body=T_Bool(Lambda(t!1245,               Implies(val(Var(1))[t!1245],                       val(Var(2))[t!1245])))), tint: Unfolding(name='tint', decl=tint, args=[x!1291], body=T_Int(K(Int, x!1291)), 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!1238], body=T_Bool(Lambda(t!1237, Not(val(p!1238)[t!1237]))), ax=|= ForAll(p,        tnot(p) ==        T_Bool(Lambda(t!1237, Not(val(p)[t!1237])))), _subst_fun_body=T_Bool(Lambda(t!1237, Not(val(Var(1))[t!1237])))), to_int: Unfolding(name='to_int', decl=to_int, args=[n!466], body=If(is(Z, n!466), 0, 1 + to_int(pred(n!466))), 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))))), to_nat: Unfolding(name='to_nat', decl=to_nat, args=[n!433], body=If(n!433 >= 0, n!433*2, n!433*-2 - 1), ax=|= ForAll(n!394,        to_nat(n!394) ==        If(n!394 >= 0, n!394*2, n!394*-2 - 1)), _subst_fun_body=If(Var(0) >= 0, Var(0)*2, Var(0)*-2 - 1)), tor: Unfolding(name='tor', decl=tor, args=[p!1243, q!1244], body=T_Bool(Lambda(t!1242,               Or(val(p!1243)[t!1242], val(q!1244)[t!1242]))), ax=|= ForAll([p, q],        tor(p, q) ==        T_Bool(Lambda(t!1242,                      Or(val(p)[t!1242], val(q)[t!1242])))), _subst_fun_body=T_Bool(Lambda(t!1242,               Or(val(Var(1))[t!1242], val(Var(2))[t!1242])))), union: Unfolding(name='union', decl=union, args=[A!2216, B!2217], body=bigunion(upair(A!2216, B!2217)), 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!1519, x!1520], body=ForAll(y, Implies(A!1519[y], EReal.le(y, x!1520))), 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!1195], body=ForAll(w, val(a!1195)[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!3225, a!3226, b!3227], body=Lambda(i, If(mask!3225[i], a!3226[i], b!3227[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!1724], body=hi(i!1724) - lo(i!1724), 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!1934], body=NDArray(Unit(n!1934), K(Int, 0)), ax=|= ForAll(n, zero(n) == NDArray(Unit(n), K(Int, 0))), _subst_fun_body=NDArray(Unit(Var(0)), K(Int, 0))), zf.false: Unfolding(name='zf.false', decl=zf.false, args=[], body=∅, ax=|= zf.false == ∅, _subst_fun_body=∅), zf.succ: Unfolding(name='zf.succ', decl=zf.succ, args=[x!2639], body=union(x!2639, ZF.sing(x!2639)), ax=|= ForAll(x, zf.succ(x) == union(x, ZF.sing(x))), _subst_fun_body=union(Var(0), ZF.sing(Var(0)))), zf.true: Unfolding(name='zf.true', decl=zf.true, args=[], body=ZF.sing(∅), ax=|= zf.true == ZF.sing(∅), _subst_fun_body=ZF.sing(∅)), zf.zero: Unfolding(name='zf.zero', decl=zf.zero, args=[], body=∅, ax=|= zf.zero == ∅, _subst_fun_body=∅)}

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