		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-round-p

Check if all the certificates at a certain round that is at least two rounds after a given certificate have a path to that certificate.

This is a version of dag-omni-paths-p restricted to a given round, passed as input. The guard requires the given round to be at least two rounds after the certificate's round, which matches the antecedent in the universal quantification in the definition of dag-omni-paths-p.

The reason why we define this predicate is that below we prove dag-omni-paths-p by induction on rounds, starting from two rounds just after the certificate. With reference to the discussion in dag-omni-paths, cert is A, and the base case of the induction is for the generic certificate C two rounds after A, while the generic certificate D is at later rounds. So we prove below that this predicate holds for every round, in the induction proof.

Definitions and Theorems

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

(defthm dag-omni-paths-round-p-necc
 (implies
  (dag-omni-paths-round-p round cert dag)
  (implies
       (and (in cert1 dag)
            (equal (certificate->round cert1)
                   round))
       (equal (path-to-author+round cert1 (certificate->author cert)
                                    (certificate->round cert)
                                    dag)
              cert))))

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

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