Check if statements, blocks, and related entities.
Function:
(defun stmt-unambp (stmt) (declare (xargs :guard (stmtp stmt))) (let ((__function__ 'stmt-unambp)) (declare (ignorable __function__)) (stmt-case stmt :labeled (and (label-unambp stmt.label) (stmt-unambp stmt.stmt)) :compound (block-item-list-unambp stmt.items) :expr (expr-option-unambp stmt.expr?) :if (and (expr-unambp stmt.test) (stmt-unambp stmt.then)) :ifelse (and (expr-unambp stmt.test) (stmt-unambp stmt.then) (stmt-unambp stmt.else)) :switch (and (expr-unambp stmt.target) (stmt-unambp stmt.body)) :while (and (expr-unambp stmt.test) (stmt-unambp stmt.body)) :dowhile (and (stmt-unambp stmt.body) (expr-unambp stmt.test)) :for-expr (and (expr-option-unambp stmt.init) (expr-option-unambp stmt.test) (expr-option-unambp stmt.next) (stmt-unambp stmt.body)) :for-decl (and (decl-unambp stmt.init) (expr-option-unambp stmt.test) (expr-option-unambp stmt.next) (stmt-unambp stmt.body)) :for-ambig nil :goto t :continue t :break t :return (expr-option-unambp stmt.expr?))))
Function:
(defun block-item-unambp (item) (declare (xargs :guard (block-itemp item))) (let ((__function__ 'block-item-unambp)) (declare (ignorable __function__)) (block-item-case item :decl (decl-unambp item.unwrap) :stmt (stmt-unambp item.unwrap) :ambig nil)))
Function:
(defun block-item-list-unambp (items) (declare (xargs :guard (block-item-listp items))) (let ((__function__ 'block-item-list-unambp)) (declare (ignorable __function__)) (or (endp items) (and (block-item-unambp (car items)) (block-item-list-unambp (cdr items))))))
Theorem:
(defthm return-type-of-stmt-unambp.yes/no (b* ((?yes/no (stmt-unambp stmt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-item-unambp.yes/no (b* ((?yes/no (block-item-unambp item))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-item-list-unambp.yes/no (b* ((?yes/no (block-item-list-unambp items))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm stmt-unambp-of-stmt-fix-stmt (equal (stmt-unambp (stmt-fix stmt)) (stmt-unambp stmt)))
Theorem:
(defthm block-item-unambp-of-block-item-fix-item (equal (block-item-unambp (block-item-fix item)) (block-item-unambp item)))
Theorem:
(defthm block-item-list-unambp-of-block-item-list-fix-items (equal (block-item-list-unambp (block-item-list-fix items)) (block-item-list-unambp items)))
Theorem:
(defthm stmt-unambp-stmt-equiv-congruence-on-stmt (implies (stmt-equiv stmt stmt-equiv) (equal (stmt-unambp stmt) (stmt-unambp stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-item-unambp-block-item-equiv-congruence-on-item (implies (block-item-equiv item item-equiv) (equal (block-item-unambp item) (block-item-unambp item-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-item-list-unambp-block-item-list-equiv-congruence-on-items (implies (block-item-list-equiv items items-equiv) (equal (block-item-list-unambp items) (block-item-list-unambp items-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-item-list-unambp-of-cons (equal (block-item-list-unambp (cons acl2::a acl2::x)) (and (block-item-unambp acl2::a) (block-item-list-unambp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-cdr-when-block-item-list-unambp (implies (block-item-list-unambp (double-rewrite acl2::x)) (block-item-list-unambp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-when-not-consp (implies (not (consp acl2::x)) (block-item-list-unambp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-unambp-of-car-when-block-item-list-unambp (implies (block-item-list-unambp acl2::x) (iff (block-item-unambp (car acl2::x)) (or (consp acl2::x) (block-item-unambp nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-append (equal (block-item-list-unambp (append acl2::a acl2::b)) (and (block-item-list-unambp acl2::a) (block-item-list-unambp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-list-fix (equal (block-item-list-unambp (list-fix acl2::x)) (block-item-list-unambp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-sfix (iff (block-item-list-unambp (sfix acl2::x)) (or (block-item-list-unambp acl2::x) (not (setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-insert (iff (block-item-list-unambp (insert acl2::a acl2::x)) (and (block-item-list-unambp (sfix acl2::x)) (block-item-unambp acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-delete (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-mergesort (iff (block-item-list-unambp (mergesort acl2::x)) (block-item-list-unambp (list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-union (iff (block-item-list-unambp (union acl2::x acl2::y)) (and (block-item-list-unambp (sfix acl2::x)) (block-item-list-unambp (sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-intersect-1 (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-intersect-2 (implies (block-item-list-unambp acl2::y) (block-item-list-unambp (intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-difference (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-duplicated-members (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-rev (equal (block-item-list-unambp (rev acl2::x)) (block-item-list-unambp (list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-rcons (iff (block-item-list-unambp (rcons acl2::a acl2::x)) (and (block-item-unambp acl2::a) (block-item-list-unambp (list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-unambp-when-member-equal-of-block-item-list-unambp (and (implies (and (member-equal acl2::a acl2::x) (block-item-list-unambp acl2::x)) (block-item-unambp acl2::a)) (implies (and (block-item-list-unambp acl2::x) (member-equal acl2::a acl2::x)) (block-item-unambp acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (block-item-list-unambp acl2::y)) (block-item-list-unambp acl2::x)) (implies (and (block-item-list-unambp acl2::y) (subsetp-equal acl2::x acl2::y)) (block-item-list-unambp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-set-equiv-congruence (implies (set-equiv acl2::x acl2::y) (equal (block-item-list-unambp acl2::x) (block-item-list-unambp acl2::y))) :rule-classes :congruence)
Theorem:
(defthm block-item-list-unambp-of-set-difference-equal (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-intersection-equal-1 (implies (block-item-list-unambp (double-rewrite acl2::x)) (block-item-list-unambp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-intersection-equal-2 (implies (block-item-list-unambp (double-rewrite acl2::y)) (block-item-list-unambp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-union-equal (equal (block-item-list-unambp (union-equal acl2::x acl2::y)) (and (block-item-list-unambp (list-fix acl2::x)) (block-item-list-unambp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-take (implies (block-item-list-unambp (double-rewrite acl2::x)) (iff (block-item-list-unambp (take acl2::n acl2::x)) (or (block-item-unambp nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-repeat (iff (block-item-list-unambp (repeat acl2::n acl2::x)) (or (block-item-unambp acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-unambp-of-nth-when-block-item-list-unambp (implies (and (block-item-list-unambp acl2::x) (< (nfix acl2::n) (len acl2::x))) (block-item-unambp (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-update-nth (implies (block-item-list-unambp (double-rewrite acl2::x)) (iff (block-item-list-unambp (update-nth acl2::n acl2::y acl2::x)) (and (block-item-unambp acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (block-item-unambp nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-butlast (implies (block-item-list-unambp (double-rewrite acl2::x)) (block-item-list-unambp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-nthcdr (implies (block-item-list-unambp (double-rewrite acl2::x)) (block-item-list-unambp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-last (implies (block-item-list-unambp (double-rewrite acl2::x)) (block-item-list-unambp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-remove (implies (block-item-list-unambp acl2::x) (block-item-list-unambp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm block-item-list-unambp-of-revappend (equal (block-item-list-unambp (revappend acl2::x acl2::y)) (and (block-item-list-unambp (list-fix acl2::x)) (block-item-list-unambp acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm stmt-unambp-of-stmt-labeled (equal (stmt-unambp (stmt-labeled label stmt)) (and (label-unambp label) (stmt-unambp stmt))))
Theorem:
(defthm stmt-unambp-of-stmt-compound (equal (stmt-unambp (stmt-compound items)) (block-item-list-unambp items)))
Theorem:
(defthm stmt-unambp-of-stmt-expr (equal (stmt-unambp (stmt-expr expr?)) (expr-option-unambp expr?)))
Theorem:
(defthm stmt-unambp-of-stmt-if (equal (stmt-unambp (stmt-if test then)) (and (expr-unambp test) (stmt-unambp then))))
Theorem:
(defthm stmt-unambp-of-stmt-ifelse (equal (stmt-unambp (stmt-ifelse test then else)) (and (expr-unambp test) (stmt-unambp then) (stmt-unambp else))))
Theorem:
(defthm stmt-unambp-of-stmt-switch (equal (stmt-unambp (stmt-switch target body)) (and (expr-unambp target) (stmt-unambp body))))
Theorem:
(defthm stmt-unambp-of-stmt-while (equal (stmt-unambp (stmt-while test body)) (and (expr-unambp test) (stmt-unambp body))))
Theorem:
(defthm stmt-unambp-of-stmt-dowhile (equal (stmt-unambp (stmt-dowhile body test)) (and (stmt-unambp body) (expr-unambp test))))
Theorem:
(defthm stmt-unambp-of-stmt-for-expr (equal (stmt-unambp (stmt-for-expr init test next body)) (and (expr-option-unambp init) (expr-option-unambp test) (expr-option-unambp next) (stmt-unambp body))))
Theorem:
(defthm stmt-unambp-of-stmt-for-decl (equal (stmt-unambp (stmt-for-decl init test next body)) (and (decl-unambp init) (expr-option-unambp test) (expr-option-unambp next) (stmt-unambp body))))
Theorem:
(defthm stmt-unambp-when-goto (implies (stmt-case stmt :goto) (stmt-unambp stmt)))
Theorem:
(defthm stmt-unambp-of-stmt-continue (stmt-unambp (stmt-continue)))
Theorem:
(defthm stmt-unambp-of-stmt-break (stmt-unambp (stmt-break)))
Theorem:
(defthm stmt-unambp-of-stmt-return (equal (stmt-unambp (stmt-return expr?)) (expr-option-unambp expr?)))
Theorem:
(defthm block-item-unambp-of-block-item-decl (equal (block-item-unambp (block-item-decl decl)) (decl-unambp decl)))
Theorem:
(defthm block-item-unambp-of-block-item-stmt (equal (block-item-unambp (block-item-stmt stmt)) (stmt-unambp stmt)))
Theorem:
(defthm label-unamb-of-stmt-labeled->label (implies (and (stmt-unambp stmt) (stmt-case stmt :labeled)) (label-unambp (stmt-labeled->label stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-labeled->stmt (implies (and (stmt-unambp stmt) (stmt-case stmt :labeled)) (stmt-unambp (stmt-labeled->stmt stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-compound->items (implies (and (stmt-unambp stmt) (stmt-case stmt :compound)) (block-item-list-unambp (stmt-compound->items stmt))))
Theorem:
(defthm expr-optionp-unamb-of-stmt-expr->expr? (implies (and (stmt-unambp stmt) (stmt-case stmt :expr)) (expr-option-unambp (stmt-expr->expr? stmt))))
Theorem:
(defthm expr-unamb-of-stmt-if->test (implies (and (stmt-unambp stmt) (stmt-case stmt :if)) (expr-unambp (stmt-if->test stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-if->then (implies (and (stmt-unambp stmt) (stmt-case stmt :if)) (stmt-unambp (stmt-if->then stmt))))
Theorem:
(defthm expr-unamb-of-stmt-ifelse->test (implies (and (stmt-unambp stmt) (stmt-case stmt :ifelse)) (expr-unambp (stmt-ifelse->test stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-ifelse->then (implies (and (stmt-unambp stmt) (stmt-case stmt :ifelse)) (stmt-unambp (stmt-ifelse->then stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-ifelse->else (implies (and (stmt-unambp stmt) (stmt-case stmt :ifelse)) (stmt-unambp (stmt-ifelse->else stmt))))
Theorem:
(defthm expr-unamb-of-stmt-switch->target (implies (and (stmt-unambp stmt) (stmt-case stmt :switch)) (expr-unambp (stmt-switch->target stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-switch->body (implies (and (stmt-unambp stmt) (stmt-case stmt :switch)) (stmt-unambp (stmt-switch->body stmt))))
Theorem:
(defthm expr-unamb-of-stmt-while->test (implies (and (stmt-unambp stmt) (stmt-case stmt :while)) (expr-unambp (stmt-while->test stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-while->body (implies (and (stmt-unambp stmt) (stmt-case stmt :while)) (stmt-unambp (stmt-while->body stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-dowhile->body (implies (and (stmt-unambp stmt) (stmt-case stmt :dowhile)) (stmt-unambp (stmt-dowhile->body stmt))))
Theorem:
(defthm expr-unamb-of-stmt-dowhile->test (implies (and (stmt-unambp stmt) (stmt-case stmt :dowhile)) (expr-unambp (stmt-dowhile->test stmt))))
Theorem:
(defthm expr-option-unambp-of-stmt-for-expr->init (implies (and (stmt-unambp stmt) (stmt-case stmt :for-expr)) (expr-option-unambp (stmt-for-expr->init stmt))))
Theorem:
(defthm expr-option-unambp-of-stmt-for-expr->test (implies (and (stmt-unambp stmt) (stmt-case stmt :for-expr)) (expr-option-unambp (stmt-for-expr->test stmt))))
Theorem:
(defthm expr-option-unambp-of-stmt-for-expr->next (implies (and (stmt-unambp stmt) (stmt-case stmt :for-expr)) (expr-option-unambp (stmt-for-expr->next stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-for-expr->body (implies (and (stmt-unambp stmt) (stmt-case stmt :for-expr)) (stmt-unambp (stmt-for-expr->body stmt))))
Theorem:
(defthm decl-unambp-of-stmt-for-decl->init (implies (and (stmt-unambp stmt) (stmt-case stmt :for-decl)) (decl-unambp (stmt-for-decl->init stmt))))
Theorem:
(defthm expr-option-unambp-of-stmt-for-decl->test (implies (and (stmt-unambp stmt) (stmt-case stmt :for-decl)) (expr-option-unambp (stmt-for-decl->test stmt))))
Theorem:
(defthm expr-option-unambp-of-stmt-for-decl->next (implies (and (stmt-unambp stmt) (stmt-case stmt :for-decl)) (expr-option-unambp (stmt-for-decl->next stmt))))
Theorem:
(defthm stmt-unamb-of-stmt-for-decl->body (implies (and (stmt-unambp stmt) (stmt-case stmt :for-decl)) (stmt-unambp (stmt-for-decl->body stmt))))
Theorem:
(defthm expr-optionp-unamb-of-stmt-return->expr? (implies (and (stmt-unambp stmt) (stmt-case stmt :return)) (expr-option-unambp (stmt-return->expr? stmt))))
Theorem:
(defthm not-for-ambig-when-stmt-unambp (implies (stmt-unambp stmt) (not (equal (stmt-kind stmt) :for-ambig))) :rule-classes :forward-chaining)
Theorem:
(defthm decl-unamb-of-block-item-decl->unwrap (implies (and (block-item-unambp item) (block-item-case item :decl)) (decl-unambp (block-item-decl->unwrap item))))
Theorem:
(defthm stmt-unamb-of-block-item-stmt->unwrap (implies (and (block-item-unambp item) (block-item-case item :stmt)) (stmt-unambp (block-item-stmt->unwrap item))))
Theorem:
(defthm not-ambig-when-block-item-unambp (implies (block-item-unambp item) (not (equal (block-item-kind item) :ambig))) :rule-classes :forward-chaining)