		Search-engine friendly clone of the ACL2 documentation.

Committees

Update-committee-with-transaction-list

Update a committee with a list of transactions.

Signature
(update-committee-with-transaction-list transs commtt) → new-commtt
Arguments: transs — Guard (transaction-listp transs).; commtt — Guard (committeep commtt).
Returns: new-commtt — Type (committeep new-commtt).

We update the committee with each transaction in the list, from left to right.

Definitions and Theorems

Function: update-committee-with-transaction-list

(defun update-committee-with-transaction-list (transs commtt)
  (declare (xargs :guard (and (transaction-listp transs)
                              (committeep commtt))))
  (let ((__function__ 'update-committee-with-transaction-list))
    (declare (ignorable __function__))
    (b* (((when (endp transs))
          (committee-fix commtt))
         (commtt (update-committee-with-transaction (car transs)
                                                    commtt)))
      (update-committee-with-transaction-list (cdr transs)
                                              commtt))))

Theorem: committeep-of-update-committee-with-transaction-list

(defthm committeep-of-update-committee-with-transaction-list
  (b* ((new-commtt
            (update-committee-with-transaction-list transs commtt)))
    (committeep new-commtt))
  :rule-classes :rewrite)

Theorem: update-committee-with-transaction-list-of-transaction-list-fix-transs

(defthm
 update-committee-with-transaction-list-of-transaction-list-fix-transs
 (equal (update-committee-with-transaction-list
             (transaction-list-fix transs)
             commtt)
        (update-committee-with-transaction-list transs commtt)))

Theorem: update-committee-with-transaction-list-transaction-list-equiv-congruence-on-transs

(defthm
 update-committee-with-transaction-list-transaction-list-equiv-congruence-on-transs
 (implies
  (transaction-list-equiv transs transs-equiv)
  (equal
      (update-committee-with-transaction-list transs commtt)
      (update-committee-with-transaction-list transs-equiv commtt)))
 :rule-classes :congruence)

Theorem: update-committee-with-transaction-list-of-committee-fix-commtt

(defthm
     update-committee-with-transaction-list-of-committee-fix-commtt
  (equal (update-committee-with-transaction-list
              transs (committee-fix commtt))
         (update-committee-with-transaction-list transs commtt)))

Theorem: update-committee-with-transaction-list-committee-equiv-congruence-on-commtt

(defthm
 update-committee-with-transaction-list-committee-equiv-congruence-on-commtt
 (implies
  (committee-equiv commtt commtt-equiv)
  (equal
      (update-committee-with-transaction-list transs commtt)
      (update-committee-with-transaction-list transs commtt-equiv)))
 :rule-classes :congruence)