		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-round-p-step-case

Step case of our proof by induction.

This is a simple consequence of dag-omni-paths-round-p-of-next-round, but it is formulated in a way usable in the proof by induction. Instead of rounds r' and r'+1, this theorem is formulated in terms of rounds a + 2 + d and a + 2 + d + 1, where a is the round of A and d is a generic ``delta'' from a+2. Note that this has the same weaker hypothesis on A, namely that is not nil, as opposed to being in the DAG.

Definitions and Theorems

Theorem: dag-omni-paths-round-p-step-case

(defthm dag-omni-paths-round-p-step-case
 (implies
    (and (certificate-setp dag)
         (certificate-set-unequivocalp dag)
         (dag-closedp dag)
         (dag-predecessor-quorum-p dag blockchain)
         cert (natp round-delta)
         (dag-omni-paths-round-p (+ round-delta
                                    (+ 2 (certificate->round cert)))
                                 cert dag))
    (dag-omni-paths-round-p (+ (1+ round-delta)
                               (+ 2 (certificate->round cert)))
                            cert dag)))