		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-rounds-p

Check if dag-omni-paths-rounds-p holds for all rounds that are at least two rounds after the given certificate.

This provides an alternative definition of dag-omni-paths-p as a quantification over the rounds of dag-omni-paths-round-p, which is convenient for our proof by induction, as mentioned above. We prove that it is indeed equivalent to dag-omni-paths-p, which is conceptually easy but takes a few steps to deal with the quantifiers.

Definitions and Theorems

Theorem: dag-omni-paths-rounds-p-necc

(defthm dag-omni-paths-rounds-p-necc
  (implies (dag-omni-paths-rounds-p cert dag)
           (implies (and (posp round)
                         (>= round (+ 2 (certificate->round cert))))
                    (dag-omni-paths-round-p round cert dag))))

Theorem: booleanp-of-dag-omni-paths-rounds-p

(defthm booleanp-of-dag-omni-paths-rounds-p
  (b* ((yes/no (dag-omni-paths-rounds-p cert dag)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: dag-omni-paths-p-alt-def

(defthm dag-omni-paths-p-alt-def
  (equal (dag-omni-paths-p cert dag)
         (dag-omni-paths-rounds-p cert dag)))