		Search-engine friendly clone of the ACL2 documentation.

Execution-limit-monotonicity

Exec-monotone

Monotonicity of the execution functions with respect to limits.

See execution-limit-monotonicity for motivation.

we also disable the theorems in exec-2limits-to-exec, now that they have served their purpose in the proof here.

Definitions and Theorems

Theorem: exec-fun-limit-monotone

(defthm exec-fun-limit-monotone
  (b* (((mv val? &)
        (exec-fun fun args compst fenv limit)))
    (implies (and (not (errorp val?))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-fun fun args compst fenv limit1)
                    (exec-fun fun args compst fenv limit)))))

Theorem: exec-expr-limit-monotone

(defthm exec-expr-limit-monotone
  (b* (((mv eval? &)
        (exec-expr e compst fenv limit)))
    (implies (and (not (errorp eval?))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-expr e compst fenv limit1)
                    (exec-expr e compst fenv limit)))))

Theorem: exec-expr-list-limit-monotone

(defthm exec-expr-list-limit-monotone
  (b* (((mv eval? &)
        (exec-expr-list es compst fenv limit)))
    (implies (and (not (errorp eval?))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-expr-list es compst fenv limit1)
                    (exec-expr-list es compst fenv limit)))))

Theorem: exec-stmt-limit-monotone

(defthm exec-stmt-limit-monotone
  (b* (((mv sval &)
        (exec-stmt s compst fenv limit)))
    (implies (and (not (errorp sval))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-stmt s compst fenv limit1)
                    (exec-stmt s compst fenv limit)))))

Theorem: exec-stmt-while-limit-monotone

(defthm exec-stmt-while-limit-monotone
 (b* (((mv sval &)
       (exec-stmt-while test body compst fenv limit)))
   (implies (and (not (errorp sval))
                 (>= (nfix limit1) (nfix limit)))
            (equal (exec-stmt-while test body compst fenv limit1)
                   (exec-stmt-while test body compst fenv limit)))))

Theorem: exec-stmt-dowhile-limit-monotone

(defthm exec-stmt-dowhile-limit-monotone
  (b* (((mv sval &)
        (exec-stmt-dowhile body test compst fenv limit)))
    (implies
         (and (not (errorp sval))
              (>= (nfix limit1) (nfix limit)))
         (equal (exec-stmt-dowhile body test compst fenv limit1)
                (exec-stmt-dowhile body test compst fenv limit)))))

Theorem: exec-initer-limit-monotone

(defthm exec-initer-limit-monotone
  (b* (((mv ival &)
        (exec-initer initer compst fenv limit)))
    (implies (and (not (errorp ival))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-initer initer compst fenv limit1)
                    (exec-initer initer compst fenv limit)))))

Theorem: exec-obj-declon-limit-monotone

(defthm exec-obj-declon-limit-monotone
  (b* ((compst1 (exec-obj-declon declon compst fenv limit)))
    (implies (and (not (errorp compst1))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-obj-declon declon compst fenv limit1)
                    (exec-obj-declon declon compst fenv limit)))))

Theorem: exec-block-item-limit-monotone

(defthm exec-block-item-limit-monotone
  (b* (((mv sval &)
        (exec-block-item item compst fenv limit)))
    (implies (and (not (errorp sval))
                  (>= (nfix limit1) (nfix limit)))
             (equal (exec-block-item item compst fenv limit1)
                    (exec-block-item item compst fenv limit)))))

Theorem: exec-block-item-list-limit-monotone

(defthm exec-block-item-list-limit-monotone
 (b* (((mv sval &)
       (exec-block-item-list items compst fenv limit)))
  (implies (and (not (errorp sval))
                (>= (nfix limit1) (nfix limit)))
           (equal (exec-block-item-list items compst fenv limit1)
                  (exec-block-item-list items compst fenv limit)))))