		Search-engine friendly clone of the ACL2 documentation.

Unambiguity

Expr-unambp-of-operation-on-expr-unambp

Preservation of unambiguity by certain operations on expressions.

Definitions and Theorems

Theorem: expr-unambp-of-apply-pre-inc/dec-ops

(defthm expr-unambp-of-apply-pre-inc/dec-ops
  (implies (expr-unambp expr)
           (expr-unambp (apply-pre-inc/dec-ops inc/dec expr))))

Theorem: expr-unambp-of-apply-post-inc/dec-ops

(defthm expr-unambp-of-apply-post-inc/dec-ops
  (implies (expr-unambp expr)
           (expr-unambp (apply-post-inc/dec-ops expr inc/dec))))

Theorem: expr-list-unambp-of-expr-to-asg-expr-list

(defthm expr-list-unambp-of-expr-to-asg-expr-list
  (implies (expr-unambp expr)
           (expr-list-unambp (expr-to-asg-expr-list expr))))

Theorem: expr-unambp-of-check-expr-mul

(defthm expr-unambp-of-check-expr-mul
  (b* (((mv yes/no arg1 arg2)
        (check-expr-mul expr)))
    (implies (and (expr-unambp expr) yes/no)
             (and (expr-unambp arg1)
                  (expr-unambp arg2)))))

Theorem: expr-unambp-of-check-expr-binary

(defthm expr-unambp-of-check-expr-binary
  (b* (((mv yes/no & arg1 arg2)
        (check-expr-binary expr)))
    (implies (and (expr-unambp expr) yes/no)
             (and (expr-unambp arg1)
                  (expr-unambp arg2)))))