		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-p

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

This is the predicate expressing the key property that we prove here, where cert is the certificate with f+1 or more successors. We universally quantify over a generic certificate cert1 whose round is greater than or equal to two plus the round of the given certificate cert. The existence of the path is expressed by saying that path-to-author+round applied to cert1 with the author and round of cert as targets yields exactly cert.

The certificate cert passed as input is the certificate A in the discussion in dag-omni-paths.

We prove that if the DAG has at least one certificate at least two rounds after the given one, then the given certificate must be in the DAG, because there is at least one path to it.

Definitions and Theorems

Theorem: dag-omni-paths-p-necc

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

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

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

Theorem: in-dag-when-dag-omni-paths-p

(defthm in-dag-when-dag-omni-paths-p
  (implies (and (certificate-setp dag)
                (dag-omni-paths-p cert dag)
                (in cert1 dag)
                (>= (certificate->round cert1)
                    (+ 2 (certificate->round cert)))
                cert)
           (in cert dag)))