kdrag.theories.logic.axioms.neg_ext

kdrag.theories.logic.axioms.neg_ext(*sorts: SortRef) → Proof

>>> neg_ext(smt.IntSort(), smt.IntSort())
|= ForAll([f, g], f != g == (Exists(x0, f[x0] != g[x0])))
>>> neg_ext(smt.IntSort(), smt.RealSort(), smt.IntSort())
|= ForAll([f, g],
       f != g ==
       (Exists([x0, x1],
               Select(f, x0, x1) != Select(g, x0, x1))))

Parameters:

sorts (SortRef)

Return type:

Proof