		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-no-prodecessors-round-1-p

Check if each certificate in round 1 of a DAG has no predecessors.

This is an invariant of the DAGs of validators, as proved elsewhere.

Definitions and Theorems

Theorem: dag-no-prodecessors-round-1-p-necc

(defthm dag-no-prodecessors-round-1-p-necc
  (implies (dag-no-prodecessors-round-1-p dag)
           (implies (and (in cert dag)
                         (equal (certificate->round cert) 1))
                    (emptyp (predecessors cert dag)))))

Theorem: booleanp-of-dag-no-prodecessors-round-1-p

(defthm booleanp-of-dag-no-prodecessors-round-1-p
  (b* ((yes/no (dag-no-prodecessors-round-1-p dag)))
    (booleanp yes/no))
  :rule-classes :rewrite)