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.
Theorem:
(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:
(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:
(defthm dag-omni-paths-p-alt-def (equal (dag-omni-paths-p cert dag) (dag-omni-paths-rounds-p cert dag)))