		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-round-p-of-round-delta

Induction proof.

We prove by induction that dag-omni-paths-round-p holds for every round of the form a + 2 + d, where a is the round of A, and d is a generic ``delta'' from a + 2. We use the previously proved base and step cases; it should be clear why the step case was formulated in terms of a + 2 + d and a + 2 + d + 1.

Definitions and Theorems

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

(defthm dag-omni-paths-round-p-of-round-delta
 (implies
  (and
   (certificate-setp dag1)
   (certificate-setp dag2)
   (certificate-set-unequivocalp dag1)
   (certificate-set-unequivocalp dag2)
   (certificate-sets-unequivocalp dag1 dag2)
   (dag-closedp dag1)
   (dag-closedp dag2)
   (dag-has-committees-p dag1 blockchain1)
   (dag-has-committees-p dag2 blockchain2)
   (dag-in-committees-p dag1 blockchain1)
   (dag-in-committees-p dag2 blockchain2)
   (same-active-committees-p blockchain1 blockchain2)
   (dag-predecessor-quorum-p dag2 blockchain2)
   (in cert dag1)
   (> (committee-members-stake
           (cert-set->author-set (successors cert dag1))
           (active-committee-at-round (1+ (certificate->round cert))
                                      blockchain1))
      (committee-max-faulty-stake
           (active-committee-at-round (1+ (certificate->round cert))
                                      blockchain1)))
   (natp round-delta))
  (dag-omni-paths-round-p (+ round-delta
                             (+ 2 (certificate->round cert)))
                          cert dag2)))