		Search-engine friendly clone of the ACL2 documentation.

Tree-list-tuple10

Tree-list-tuple10-fix

Fixing function for tree-list-tuple10 structures.

Signature
(tree-list-tuple10-fix x) → new-x
Arguments: x — Guard (tree-list-tuple10p x).
Returns: new-x — Type (tree-list-tuple10p new-x).

Definitions and Theorems

Function: tree-list-tuple10-fix$inline

(defun tree-list-tuple10-fix$inline (x)
  (declare (xargs :guard (tree-list-tuple10p x)))
  (let ((__function__ 'tree-list-tuple10-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((1st (tree-list-fix (cdr (std::da-nth 0 x))))
              (2nd (tree-list-fix (cdr (std::da-nth 1 x))))
              (3rd (tree-list-fix (cdr (std::da-nth 2 x))))
              (4th (tree-list-fix (cdr (std::da-nth 3 x))))
              (5th (tree-list-fix (cdr (std::da-nth 4 x))))
              (6th (tree-list-fix (cdr (std::da-nth 5 x))))
              (7th (tree-list-fix (cdr (std::da-nth 6 x))))
              (8th (tree-list-fix (cdr (std::da-nth 7 x))))
              (9th (tree-list-fix (cdr (std::da-nth 8 x))))
              (10th (tree-list-fix (cdr (std::da-nth 9 x)))))
           (list (cons '1st 1st)
                 (cons '2nd 2nd)
                 (cons '3rd 3rd)
                 (cons '4th 4th)
                 (cons '5th 5th)
                 (cons '6th 6th)
                 (cons '7th 7th)
                 (cons '8th 8th)
                 (cons '9th 9th)
                 (cons '10th 10th)))
         :exec x)))

Theorem: tree-list-tuple10p-of-tree-list-tuple10-fix

(defthm tree-list-tuple10p-of-tree-list-tuple10-fix
  (b* ((new-x (tree-list-tuple10-fix$inline x)))
    (tree-list-tuple10p new-x))
  :rule-classes :rewrite)

Theorem: tree-list-tuple10-fix-when-tree-list-tuple10p

(defthm tree-list-tuple10-fix-when-tree-list-tuple10p
  (implies (tree-list-tuple10p x)
           (equal (tree-list-tuple10-fix x) x)))

Function: tree-list-tuple10-equiv$inline

(defun tree-list-tuple10-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (tree-list-tuple10p acl2::x)
                              (tree-list-tuple10p acl2::y))))
  (equal (tree-list-tuple10-fix acl2::x)
         (tree-list-tuple10-fix acl2::y)))

Theorem: tree-list-tuple10-equiv-is-an-equivalence

(defthm tree-list-tuple10-equiv-is-an-equivalence
  (and (booleanp (tree-list-tuple10-equiv x y))
       (tree-list-tuple10-equiv x x)
       (implies (tree-list-tuple10-equiv x y)
                (tree-list-tuple10-equiv y x))
       (implies (and (tree-list-tuple10-equiv x y)
                     (tree-list-tuple10-equiv y z))
                (tree-list-tuple10-equiv x z)))
  :rule-classes (:equivalence))

Theorem: tree-list-tuple10-equiv-implies-equal-tree-list-tuple10-fix-1

(defthm
      tree-list-tuple10-equiv-implies-equal-tree-list-tuple10-fix-1
  (implies (tree-list-tuple10-equiv acl2::x x-equiv)
           (equal (tree-list-tuple10-fix acl2::x)
                  (tree-list-tuple10-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: tree-list-tuple10-fix-under-tree-list-tuple10-equiv

(defthm tree-list-tuple10-fix-under-tree-list-tuple10-equiv
  (tree-list-tuple10-equiv (tree-list-tuple10-fix acl2::x)
                           acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-tree-list-tuple10-fix-1-forward-to-tree-list-tuple10-equiv

(defthm
 equal-of-tree-list-tuple10-fix-1-forward-to-tree-list-tuple10-equiv
 (implies (equal (tree-list-tuple10-fix acl2::x)
                 acl2::y)
          (tree-list-tuple10-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-tree-list-tuple10-fix-2-forward-to-tree-list-tuple10-equiv

(defthm
 equal-of-tree-list-tuple10-fix-2-forward-to-tree-list-tuple10-equiv
 (implies (equal acl2::x (tree-list-tuple10-fix acl2::y))
          (tree-list-tuple10-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: tree-list-tuple10-equiv-of-tree-list-tuple10-fix-1-forward

(defthm tree-list-tuple10-equiv-of-tree-list-tuple10-fix-1-forward
  (implies (tree-list-tuple10-equiv (tree-list-tuple10-fix acl2::x)
                                    acl2::y)
           (tree-list-tuple10-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: tree-list-tuple10-equiv-of-tree-list-tuple10-fix-2-forward

(defthm tree-list-tuple10-equiv-of-tree-list-tuple10-fix-2-forward
 (implies
   (tree-list-tuple10-equiv acl2::x (tree-list-tuple10-fix acl2::y))
   (tree-list-tuple10-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)