kdrag.theories.logic.axioms.ext

kdrag.theories.logic.axioms.ext(*sorts: 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:

sorts (SortRef)

Return type:

Proof