remove-weak-inequalities

Included Books

other

(in-package "ACL2")

other

(table acl2-defaults-table :state-ok t)

include-book

(include-book "building-blocks")

present-in-goalfunction

(defun present-in-goal
  (term goal)
  (cond ((endp goal) nil)
    ((equal term (car goal)) 'positive)
    ((and (eq (fn-symb (car goal)) 'not)
       (equal term (fargn (car goal) 1))) 'negative)
    (t (present-in-goal term (cdr goal)))))

remove-weak-inequalities-one-fnfunction

(defun remove-weak-inequalities-one-fn
  (x y mfc state)
  (if (eq (present-in-goal `(< ,Y ,X) (mfc-clause mfc)) 'positive)
    (let ((contradictionp (mfc-ap `(< ,Y ,X) mfc state)))
      (if (equal (length (access poly contradictionp :parents)) 1)
        t
        nil))
    nil))

remove-weak-inequalities-onetheorem

(defthm remove-weak-inequalities-one
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (remove-weak-inequalities-one-fn x y mfc state))
      (<= x y))
    (<= x y)))

remove-weak-inequalities-two-fnfunction

(defun remove-weak-inequalities-two-fn
  (x y mfc state)
  (if (eq (present-in-goal `(< ,X ,Y) (mfc-clause mfc)) 'negative)
    (let ((contradictionp (mfc-ap `(not (< ,X ,Y)) mfc state)))
      (if (equal (length (access poly contradictionp :parents)) 1)
        t
        nil))
    nil))

remove-weak-inequalities-twotheorem

(defthm remove-weak-inequalities-two
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (remove-weak-inequalities-two-fn x y mfc state))
      (< x y))
    (< x y)))