Searched defs:isIntLHS (Results 1 – 6 of 6) sorted by relevance
818 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local1730 Theorem isIntLHS(isIntegerThm(theIneq[0])); in projectInequalities() local3276 Theorem isIntLHS(isIntegerThm(theIneq[0])); in rewrite() local3314 Theorem isIntLHS(isIntegerThm(theIneq[0])); in rewrite() local
838 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local1362 Theorem isIntLHS(isIntegerThm(theIneq[0])); in projectInequalities() local
2086 const Theorem& isIntLHS, in lessThanToLE()3153 const Theorem& isIntLHS, in lessThanToLERewrite()
2044 const Theorem& isIntLHS, in lessThanToLE()3104 const Theorem& isIntLHS, in lessThanToLERewrite()
2246 const Theorem& isIntLHS, in lessThanToLE()3417 const Theorem& isIntLHS, in lessThanToLERewrite()
594 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local