kdrag.kernel.choose

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]