		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-binary

Transform a binary expression.

Signature
(simpadd0-expr-binary op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg2 arg2-new arg2-events arg2-thm-name arg2-vartys info gin) → (mv expr gout)
Arguments: op — Guard (binopp op).; arg1 — Guard (exprp arg1).; arg1-new — Guard (exprp arg1-new).; arg1-events — Guard (pseudo-event-form-listp arg1-events).; arg1-thm-name — Guard (symbolp arg1-thm-name).; arg1-vartys — Guard (ident-type-mapp arg1-vartys).; arg2 — Guard (exprp arg2).; arg2-new — Guard (exprp arg2-new).; arg2-events — Guard (pseudo-event-form-listp arg2-events).; arg2-thm-name — Guard (symbolp arg2-thm-name).; arg2-vartys — Guard (ident-type-mapp arg2-vartys).; info — Guard (binary-infop info).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp gout).

The resulting expression is obtained by combining the binary operator with the possibly transformed argument expressions, unless the binary operator is + and the possibly transformed left argument is an int expression and the possibly transformed right argument is an int octal 0 without leading zeros, in which case the resulting expression is just that expression. This is the core of this simple transformation.

We generate a theorem only if theorems were generated for both argument expressions. We generate a theorem for pure strict and non-strict operators. We generate a theorem for simple assignment expressions whose left side is a variable of integer type and whose right side is a pure expression of the same integer type.

For pure (strict and non-strict) operators, we use and join the variable-type maps for the two argument expressions. For assignment expressions, instead we take the map from the validation table that annotates the expression. This is in general a supermap of the two maps (which we double-check here, throwing a hard error if not). In upcoming extensions, we will extend the generated theorem to say that all the variables in the map are preserved by the execution of the assignment expression, which is needed to compose proofs for sequential statements.

Definitions and Theorems

Function: simpadd0-expr-binary

(defun simpadd0-expr-binary
       (op arg1 arg1-new arg1-events arg1-thm-name
           arg1-vartys arg2 arg2-new arg2-events
           arg2-thm-name arg2-vartys info gin)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1)
                             (exprp arg1-new)
                             (pseudo-event-form-listp arg1-events)
                             (symbolp arg1-thm-name)
                             (ident-type-mapp arg1-vartys)
                             (exprp arg2)
                             (exprp arg2-new)
                             (pseudo-event-form-listp arg2-events)
                             (symbolp arg2-thm-name)
                             (ident-type-mapp arg2-vartys)
                             (binary-infop info)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (and (expr-unambp arg1)
                             (expr-unambp arg1-new)
                             (expr-unambp arg2)
                             (expr-unambp arg2-new))))
 (let ((__function__ 'simpadd0-expr-binary))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (expr (make-expr-binary :op op
                            :arg1 arg1
                            :arg2 arg2
                            :info info))
    (simpp (and (binop-case op :add)
                (type-case (expr-type arg1-new) :sint)
                (expr-zerop arg2-new)))
    (expr-new (if simpp (expr-fix arg1-new)
                (make-expr-binary :op op
                                  :arg1 arg1-new
                                  :arg2 arg2-new
                                  :info info)))
    (arg1-vartys (ident-type-map-fix arg1-vartys))
    (arg2-vartys (ident-type-map-fix arg2-vartys))
    (vartys (simpadd0-join-vartys arg1-vartys arg2-vartys))
    (gout-no-thm
        (make-simpadd0-gout :events (append arg1-events arg2-events)
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid
                            :vartys vartys))
    ((unless (and arg1-thm-name arg2-thm-name))
     (mv expr-new gout-no-thm)))
   (cond
    ((member-eq (binop-kind op)
                '(:mul :div
                       :rem :add
                       :sub :shl
                       :shr :lt
                       :gt :le
                       :ge :eq
                       :ne :bitand
                       :bitxor :bitior))
     (b*
      ((hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e ldm-expr)
               (:e c::iconst-length-none)
               (:e c::iconst-base-oct)
               (:e c::iconst)
               (:e c::const-int)
               (:e c::expr-const)
               (:e c::binop-kind)
               (:e c::binop-add)
               (:e c::binop-purep)
               (:e c::binop-strictp)
               (:e c::expr-binary)
               (:e c::type-nonchar-integerp)
               (:e c::promote-type)
               (:e c::uaconvert-types)
               (:e c::type-sint)
               (:e member-equal))
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                arg2-thm-name
                (cons
                 (cons
                  ':instance
                  (cons
                   'simpadd0-expr-binary-pure-strict-support-lemma
                   (cons
                    (cons
                      'op
                      (cons (cons 'quote (cons (ldm-binop op) 'nil))
                            'nil))
                    (cons
                     (cons
                      'old-arg1
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'old-arg2
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-arg1
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'new-arg2
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                              'ldm-expr
                              (cons
                                  (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                             'nil)))
                          'nil))
                        'nil)))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'simpadd0-expr-binary-pure-strict-error-support-lemma
                    (cons
                     (cons
                      'op
                      (cons (cons 'quote (cons (ldm-binop op) 'nil))
                            'nil))
                     (cons
                      (cons
                       'arg1
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'arg2
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       'nil)))))
                  (and
                   simpp
                   (cons
                    (cons
                     ':instance
                     (cons
                      'simpadd0-expr-binary-simp-support-lemma
                      (cons
                       (cons
                        'expr
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       'nil)))
                    'nil))))))
              'nil)))))
         'nil))
       ((mv thm-event thm-name thm-index)
        (simpadd0-gen-expr-pure-thm
             expr expr-new vartys
             gin.const-new gin.thm-index hints)))
      (mv expr-new
          (make-simpadd0-gout
               :events (append arg1-events
                               arg2-events (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid (cons thm-name gin.names-to-avoid)
               :vartys vartys))))
    ((member-eq (binop-kind op)
                '(:logand :logor))
     (b*
      ((hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e ldm-expr)
               (:e ldm-ident)
               (:e ident)
               (:e c::expr-binary)
               (:e c::binop-logand)
               (:e c::binop-logor)
               (:e c::type-sint)
               (:e c::type-nonchar-integerp))
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                arg2-thm-name
                (cons
                 (cons
                  ':instance
                  (cons
                   (case (binop-kind op)
                    (:logand
                     'simpadd0-expr-binary-logand-first-support-lemma)
                    (:logor
                     'simpadd0-expr-binary-logor-first-support-lemma))
                   (cons
                    (cons
                     'old-arg1
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'old-arg2
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'new-arg1
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                            'ldm-expr
                            (cons (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-arg2
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       'nil))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    (case (binop-kind op)
                     (:logand
                      'simpadd0-expr-binary-logand-second-support-lemma)
                     (:logor
                      'simpadd0-expr-binary-logor-second-support-lemma))
                    (cons
                     (cons
                      'old-arg1
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'old-arg2
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-arg1
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'new-arg2
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                              'ldm-expr
                              (cons
                                  (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                             'nil)))
                          'nil))
                        'nil))))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     (case (binop-kind op)
                      (:logand
                       'simpadd0-expr-binary-logand-first-error-support-lemma)
                      (:logor
                       'simpadd0-expr-binary-logor-first-error-support-lemma))
                     (cons
                      (cons
                       'arg1
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'arg2
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       'nil))))
                   (cons
                    (cons
                     ':instance
                     (cons
                      (case (binop-kind op)
                       (:logand
                        'simpadd0-expr-binary-logand-second-error-support-lemma)
                       (:logor
                        'simpadd0-expr-binary-logor-second-error-support-lemma))
                      (cons
                       (cons
                        'arg1
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'arg2
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                             'nil)))
                          'nil))
                        'nil))))
                    'nil))))))
              'nil)))))
         'nil))
       ((mv thm-event thm-name thm-index)
        (simpadd0-gen-expr-pure-thm
             expr expr-new vartys
             gin.const-new gin.thm-index hints)))
      (mv expr-new
          (make-simpadd0-gout
               :events (append arg1-events
                               arg2-events (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid (cons thm-name gin.names-to-avoid)
               :vartys vartys))))
    ((eq (binop-kind op) :asg)
     (b*
      (((unless (and (expr-case arg1 :ident)
                     (expr-purep arg2)
                     (equal (expr-type arg1)
                            (expr-type arg2))
                     (type-integerp (expr-type arg1))))
        (mv expr-new gout-no-thm))
       (vartys (simpadd0-vartys-from-valid-table
                    (c$::binary-info->table info)))
       ((unless (omap::submap arg1-vartys vartys))
        (raise
         "Internal error: ~
                    argument variables ~x0 are not a submap of ~
                    validation table variables ~x1."
         arg1-vartys vartys)
        (mv (irr-expr) (irr-simpadd0-gout)))
       ((unless (omap::submap arg2-vartys vartys))
        (raise
         "Internal error: ~
                    argument variables ~x0 are not a submap of ~
                    validation table variables ~x1."
         arg2-vartys vartys)
        (mv (irr-expr) (irr-simpadd0-gout)))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e ldm-expr)
               (:e ldm-ident)
               (:e ident)
               (:e c::expr-kind)
               (:e c::expr-ident)
               (:e c::expr-binary)
               (:e c::binop-asg)
               (:e c::ident)
               (:e c::type-nonchar-integerp)
               c::not-errorp-when-compustate-has-var-with-type-p
               c::type-of-value-when-compustate-has-var-with-type-p
               c::valuep-of-read-object-of-objdesign-of-var
               c::not-errorp-when-valuep)
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                arg2-thm-name
                (cons
                 (cons
                  ':instance
                  (cons
                   'simpadd0-expr-binary-asg-support-lemma
                   (cons
                    (cons
                     'old-arg
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'new-arg
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons
                            'ldm-expr
                            (cons (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'var
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                            'ldm-ident
                            (cons
                             (cons
                               'quote
                               (cons (expr-ident->ident arg1) 'nil))
                             'nil))
                           'nil)))
                        'nil))
                      'nil)))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'simpadd0-expr-binary-asg-error-support-lemma
                    (cons
                     (cons
                      'var
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons
                           'ldm-ident
                           (cons
                            (cons
                               'quote
                               (cons (expr-ident->ident arg1) 'nil))
                            'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'expr
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      '((fenv old-fenv))))))
                  'nil))))
              'nil)))))
         'nil))
       ((mv thm-event thm-name thm-index)
        (simpadd0-gen-expr-asg-thm
             expr expr-new vartys
             gin.const-new gin.thm-index hints)))
      (mv expr-new
          (make-simpadd0-gout
               :events (append arg1-events
                               arg2-events (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid (cons thm-name gin.names-to-avoid)
               :vartys vartys))))
    (t (mv expr-new gout-no-thm))))))

Theorem: exprp-of-simpadd0-expr-binary.expr

(defthm exprp-of-simpadd0-expr-binary.expr
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op
                             arg1 arg1-new arg1-events arg1-thm-name
                             arg1-vartys arg2 arg2-new arg2-events
                             arg2-thm-name arg2-vartys info gin)))
   (exprp expr))
 :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-expr-binary.gout

(defthm simpadd0-goutp-of-simpadd0-expr-binary.gout
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op
                             arg1 arg1-new arg1-events arg1-thm-name
                             arg1-vartys arg2 arg2-new arg2-events
                             arg2-thm-name arg2-vartys info gin)))
   (simpadd0-goutp gout))
 :rule-classes :rewrite)

Theorem: expr-unamp-of-simpadd0-expr-binary

(defthm expr-unamp-of-simpadd0-expr-binary
 (implies
   (and (expr-unambp arg1-new)
        (expr-unambp arg2-new))
   (b*
     (((mv ?expr ?gout)
       (simpadd0-expr-binary op
                             arg1 arg1-new arg1-events arg1-thm-name
                             arg1-vartys arg2 arg2-new arg2-events
                             arg2-thm-name arg2-vartys info gin)))
     (expr-unambp expr))))

Theorem: simpadd0-expr-binary-pure-strict-support-lemma

(defthm simpadd0-expr-binary-pure-strict-support-lemma
 (b* ((old (c::expr-binary op old-arg1 old-arg2))
      (new (c::expr-binary op new-arg1 new-arg2))
      (old-arg1-result (c::exec-expr-pure old-arg1 compst))
      (old-arg2-result (c::exec-expr-pure old-arg2 compst))
      (new-arg1-result (c::exec-expr-pure new-arg1 compst))
      (new-arg2-result (c::exec-expr-pure new-arg2 compst))
      (old-arg1-value (c::expr-value->value old-arg1-result))
      (old-arg2-value (c::expr-value->value old-arg2-result))
      (new-arg1-value (c::expr-value->value new-arg1-result))
      (new-arg2-value (c::expr-value->value new-arg2-result))
      (old-result (c::exec-expr-pure old compst))
      (new-result (c::exec-expr-pure new compst))
      (old-value (c::expr-value->value old-result))
      (new-value (c::expr-value->value new-result))
      (type1 (c::type-of-value old-arg1-value))
      (type2 (c::type-of-value old-arg2-value)))
  (implies (and (c::binop-purep op)
                (c::binop-strictp op)
                (not (c::errorp old-result))
                (not (c::errorp new-arg1-result))
                (not (c::errorp new-arg2-result))
                (equal old-arg1-value new-arg1-value)
                (equal old-arg2-value new-arg2-value)
                (c::type-nonchar-integerp type1)
                (c::type-nonchar-integerp type2))
           (and (not (c::errorp new-result))
                (equal old-value new-value)
                (equal (c::type-of-value old-value)
                       (cond ((member-equal (c::binop-kind op)
                                            '(:mul :div
                                                   :rem :add
                                                   :sub :bitand
                                                   :bitxor :bitior))
                              (c::uaconvert-types type1 type2))
                             ((member-equal (c::binop-kind op)
                                            '(:shl :shr))
                              (c::promote-type type1))
                             (t (c::type-sint))))))))

Theorem: simpadd0-expr-binary-pure-strict-error-support-lemma

(defthm simpadd0-expr-binary-pure-strict-error-support-lemma
  (implies
       (and (c::binop-strictp op)
            (or (c::errorp (c::exec-expr-pure arg1 compst))
                (c::errorp (c::exec-expr-pure arg2 compst))))
       (c::errorp (c::exec-expr-pure (c::expr-binary op arg1 arg2)
                                     compst))))

Theorem: simpadd0-expr-binary-simp-support-lemma

(defthm simpadd0-expr-binary-simp-support-lemma
 (b*
  ((zero
       (c::expr-const
            (c::const-int
                 (c::make-iconst :value 0
                                 :base (c::iconst-base-oct)
                                 :unsignedp nil
                                 :length (c::iconst-length-none)))))
   (expr+zero (c::expr-binary (c::binop-add)
                              expr zero))
   (expr-result (c::exec-expr-pure expr compst))
   (expr-value (c::expr-value->value expr-result))
   (expr+zero-result (c::exec-expr-pure expr+zero compst))
   (expr+zero-value (c::expr-value->value expr+zero-result)))
  (implies (and (not (c::errorp expr-result))
                (equal (c::type-of-value expr-value)
                       (c::type-sint)))
           (equal expr+zero-value expr-value))))

Theorem: simpadd0-expr-binary-logand-first-support-lemma

(defthm simpadd0-expr-binary-logand-first-support-lemma
  (b* ((old (c::expr-binary (c::binop-logand)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logand)
                            new-arg1 new-arg2))
       (old-arg1-result (c::exec-expr-pure old-arg1 compst))
       (new-arg1-result (c::exec-expr-pure new-arg1 compst))
       (old-arg1-value (c::expr-value->value old-arg1-result))
       (new-arg1-value (c::expr-value->value new-arg1-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type1 (c::type-of-value old-arg1-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-arg1-result))
                  (equal old-arg1-value new-arg1-value)
                  (c::type-nonchar-integerp type1)
                  (not (c::test-value old-arg1-value)))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         (c::type-sint))))))

Theorem: simpadd0-expr-binary-logand-second-support-lemma

(defthm simpadd0-expr-binary-logand-second-support-lemma
  (b* ((old (c::expr-binary (c::binop-logand)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logand)
                            new-arg1 new-arg2))
       (old-arg1-result (c::exec-expr-pure old-arg1 compst))
       (old-arg2-result (c::exec-expr-pure old-arg2 compst))
       (new-arg1-result (c::exec-expr-pure new-arg1 compst))
       (new-arg2-result (c::exec-expr-pure new-arg2 compst))
       (old-arg1-value (c::expr-value->value old-arg1-result))
       (old-arg2-value (c::expr-value->value old-arg2-result))
       (new-arg1-value (c::expr-value->value new-arg1-result))
       (new-arg2-value (c::expr-value->value new-arg2-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type1 (c::type-of-value old-arg1-value))
       (type2 (c::type-of-value old-arg2-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-arg1-result))
                  (not (c::errorp new-arg2-result))
                  (equal old-arg1-value new-arg1-value)
                  (equal old-arg2-value new-arg2-value)
                  (c::type-nonchar-integerp type1)
                  (c::type-nonchar-integerp type2)
                  (c::test-value old-arg1-value))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         (c::type-sint))))))

Theorem: simpadd0-expr-binary-logand-first-error-support-lemma

(defthm simpadd0-expr-binary-logand-first-error-support-lemma
 (implies
     (c::errorp (c::exec-expr-pure arg1 compst))
     (c::errorp (c::exec-expr-pure (c::expr-binary (c::binop-logand)
                                                   arg1 arg2)
                                   compst))))

Theorem: simpadd0-expr-binary-logand-second-error-support-lemma

(defthm simpadd0-expr-binary-logand-second-error-support-lemma
 (implies
  (and
   (not (c::errorp (c::exec-expr-pure arg1 compst)))
   (c::type-nonchar-integerp
       (c::type-of-value
            (c::expr-value->value (c::exec-expr-pure arg1 compst))))
   (c::test-value
        (c::expr-value->value (c::exec-expr-pure arg1 compst)))
   (c::errorp (c::exec-expr-pure arg2 compst)))
  (c::errorp (c::exec-expr-pure (c::expr-binary (c::binop-logand)
                                                arg1 arg2)
                                compst))))

Theorem: simpadd0-expr-binary-logor-first-support-lemma

(defthm simpadd0-expr-binary-logor-first-support-lemma
  (b* ((old (c::expr-binary (c::binop-logor)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logor)
                            new-arg1 new-arg2))
       (old-arg1-result (c::exec-expr-pure old-arg1 compst))
       (new-arg1-result (c::exec-expr-pure new-arg1 compst))
       (old-arg1-value (c::expr-value->value old-arg1-result))
       (new-arg1-value (c::expr-value->value new-arg1-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type1 (c::type-of-value old-arg1-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-arg1-result))
                  (equal old-arg1-value new-arg1-value)
                  (c::type-nonchar-integerp type1)
                  (c::test-value old-arg1-value))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         (c::type-sint))))))

Theorem: simpadd0-expr-binary-logor-second-support-lemma

(defthm simpadd0-expr-binary-logor-second-support-lemma
  (b* ((old (c::expr-binary (c::binop-logor)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logor)
                            new-arg1 new-arg2))
       (old-arg1-result (c::exec-expr-pure old-arg1 compst))
       (old-arg2-result (c::exec-expr-pure old-arg2 compst))
       (new-arg1-result (c::exec-expr-pure new-arg1 compst))
       (new-arg2-result (c::exec-expr-pure new-arg2 compst))
       (old-arg1-value (c::expr-value->value old-arg1-result))
       (old-arg2-value (c::expr-value->value old-arg2-result))
       (new-arg1-value (c::expr-value->value new-arg1-result))
       (new-arg2-value (c::expr-value->value new-arg2-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type1 (c::type-of-value old-arg1-value))
       (type2 (c::type-of-value old-arg2-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-arg1-result))
                  (not (c::errorp new-arg2-result))
                  (equal old-arg1-value new-arg1-value)
                  (equal old-arg2-value new-arg2-value)
                  (c::type-nonchar-integerp type1)
                  (c::type-nonchar-integerp type2)
                  (not (c::test-value old-arg1-value)))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         (c::type-sint))))))

Theorem: simpadd0-expr-binary-logor-first-error-support-lemma

(defthm simpadd0-expr-binary-logor-first-error-support-lemma
 (implies
      (c::errorp (c::exec-expr-pure arg1 compst))
      (c::errorp (c::exec-expr-pure (c::expr-binary (c::binop-logor)
                                                    arg1 arg2)
                                    compst))))

Theorem: simpadd0-expr-binary-logor-second-error-support-lemma

(defthm simpadd0-expr-binary-logor-second-error-support-lemma
 (implies
  (and
   (not (c::errorp (c::exec-expr-pure arg1 compst)))
   (c::type-nonchar-integerp
       (c::type-of-value
            (c::expr-value->value (c::exec-expr-pure arg1 compst))))
   (not
       (c::test-value
            (c::expr-value->value (c::exec-expr-pure arg1 compst))))
   (c::errorp (c::exec-expr-pure arg2 compst)))
  (c::errorp (c::exec-expr-pure (c::expr-binary (c::binop-logor)
                                                arg1 arg2)
                                compst))))

Theorem: simpadd0-expr-binary-asg-support-lemma

(defthm simpadd0-expr-binary-asg-support-lemma
  (b* ((old (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            old-arg))
       (new (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            new-arg))
       (old-arg-result (c::exec-expr-pure old-arg compst))
       (new-arg-result (c::exec-expr-pure new-arg compst))
       (old-arg-value (c::expr-value->value old-arg-result))
       (new-arg-value (c::expr-value->value new-arg-result))
       (old-compst (c::exec-expr-asg old compst old-fenv limit))
       (new-compst (c::exec-expr-asg new compst new-fenv limit))
       (val (c::read-object (c::objdesign-of-var var compst)
                            compst))
       (type (c::type-of-value val)))
    (implies (and (not (equal (c::expr-kind old-arg) :call))
                  (not (equal (c::expr-kind new-arg) :call))
                  (not (c::errorp val))
                  (c::type-nonchar-integerp type)
                  (not (c::errorp old-compst))
                  (not (c::errorp new-arg-result))
                  (equal old-arg-value new-arg-value)
                  (equal (c::type-of-value old-arg-value)
                         type))
             (and (not (c::errorp new-compst))
                  (equal old-compst new-compst)))))

Theorem: simpadd0-expr-binary-asg-error-support-lemma

(defthm simpadd0-expr-binary-asg-error-support-lemma
 (implies
    (and (not (equal (c::expr-kind expr) :call))
         (or (c::errorp (c::exec-expr-pure (c::expr-ident var)
                                           compst))
             (c::errorp (c::exec-expr-pure expr compst))))
    (c::errorp (c::exec-expr-asg (c::expr-binary (c::binop-asg)
                                                 (c::expr-ident var)
                                                 expr)
                                 compst fenv limit))))