Transform statements, blocks, and related entities.
Function:
(defun simpadd0-stmt (stmt) (declare (xargs :guard (stmtp stmt))) (let ((__function__ 'simpadd0-stmt)) (declare (ignorable __function__)) (stmt-case stmt :labeled (make-stmt-labeled :label (simpadd0-label stmt.label) :stmt (simpadd0-stmt stmt.stmt)) :compound (stmt-compound (simpadd0-block-item-list stmt.items)) :expr (stmt-expr (simpadd0-expr-option stmt.expr?)) :if (make-stmt-if :test (simpadd0-expr stmt.test) :then (simpadd0-stmt stmt.then)) :ifelse (make-stmt-ifelse :test (simpadd0-expr stmt.test) :then (simpadd0-stmt stmt.then) :else (simpadd0-stmt stmt.else)) :switch (make-stmt-switch :target (simpadd0-expr stmt.target) :body (simpadd0-stmt stmt.body)) :while (make-stmt-while :test (simpadd0-expr stmt.test) :body (simpadd0-stmt stmt.body)) :dowhile (make-stmt-dowhile :body (simpadd0-stmt stmt.body) :test (simpadd0-expr stmt.test)) :for-expr (make-stmt-for-expr :init (simpadd0-expr-option stmt.init) :test (simpadd0-expr-option stmt.test) :next (simpadd0-expr-option stmt.next) :body (simpadd0-stmt stmt.body)) :for-decl (make-stmt-for-decl :init (simpadd0-decl stmt.init) :test (simpadd0-expr-option stmt.test) :next (simpadd0-expr-option stmt.next) :body (simpadd0-stmt stmt.body)) :for-ambig (prog2$ (raise "Misusage error: ~x0." (stmt-fix stmt)) (stmt-fix stmt)) :goto (stmt-fix stmt) :continue (stmt-fix stmt) :break (stmt-fix stmt) :return (stmt-return (simpadd0-expr-option stmt.expr?)))))
Function:
(defun simpadd0-block-item (item) (declare (xargs :guard (block-itemp item))) (let ((__function__ 'simpadd0-block-item)) (declare (ignorable __function__)) (block-item-case item :decl (block-item-decl (simpadd0-decl item.unwrap)) :stmt (block-item-stmt (simpadd0-stmt item.unwrap)) :ambig (prog2$ (raise "Misusage error: ~x0." (block-item-fix item)) (block-item-fix item)))))
Function:
(defun simpadd0-block-item-list (items) (declare (xargs :guard (block-item-listp items))) (let ((__function__ 'simpadd0-block-item-list)) (declare (ignorable __function__)) (cond ((endp items) nil) (t (cons (simpadd0-block-item (car items)) (simpadd0-block-item-list (cdr items)))))))
Theorem:
(defthm return-type-of-simpadd0-stmt.new-stmt (b* ((?new-stmt (simpadd0-stmt stmt))) (stmtp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-block-item.new-item (b* ((?new-item (simpadd0-block-item item))) (block-itemp new-item)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-block-item-list.new-items (b* ((?new-items (simpadd0-block-item-list items))) (block-item-listp new-items)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-stmt-of-stmt-fix-stmt (equal (simpadd0-stmt (stmt-fix stmt)) (simpadd0-stmt stmt)))
Theorem:
(defthm simpadd0-block-item-of-block-item-fix-item (equal (simpadd0-block-item (block-item-fix item)) (simpadd0-block-item item)))
Theorem:
(defthm simpadd0-block-item-list-of-block-item-list-fix-items (equal (simpadd0-block-item-list (block-item-list-fix items)) (simpadd0-block-item-list items)))
Theorem:
(defthm simpadd0-stmt-stmt-equiv-congruence-on-stmt (implies (c$::stmt-equiv stmt stmt-equiv) (equal (simpadd0-stmt stmt) (simpadd0-stmt stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-block-item-block-item-equiv-congruence-on-item (implies (c$::block-item-equiv item item-equiv) (equal (simpadd0-block-item item) (simpadd0-block-item item-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-block-item-list-block-item-list-equiv-congruence-on-items (implies (c$::block-item-list-equiv items items-equiv) (equal (simpadd0-block-item-list items) (simpadd0-block-item-list items-equiv))) :rule-classes :congruence)