		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-closedp

Check if a DAG is backward-closed.

That is, check if the previous certificates of each certificate in the DAG are all in the DAG.

Adding a certificate whose previous certificates are in the DAG preserves the closure of the DAG. It might be tempting to try and prove something like

(equal (dag-closedp (set::insert cert dag))
       (and (dag-closedp dag)
            (certificate-previous-in-dag-p cert dag)))

but that does not hold, because cert could be a predecessor certificate of some certificate in dag. So instead we prove the (right-to-left) implication.

Definitions and Theorems

Theorem: dag-closedp-necc

(defthm dag-closedp-necc
  (implies (dag-closedp dag)
           (implies (in cert dag)
                    (certificate-previous-in-dag-p cert dag))))

Theorem: booleanp-of-dag-closedp

(defthm booleanp-of-dag-closedp
  (b* ((yes/no (dag-closedp dag)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: dag-closedp-when-emptyp

(defthm dag-closedp-when-emptyp
  (implies (emptyp dag)
           (dag-closedp dag)))

Theorem: dag-closedp-of-insert

(defthm dag-closedp-of-insert
  (implies (and (certificatep cert)
                (certificate-setp dag)
                (dag-closedp dag)
                (certificate-previous-in-dag-p cert dag))
           (dag-closedp (insert cert dag))))