		Search-engine friendly clone of the ACL2 documentation.

Omni-paths-def-and-implied

Omni-paths-p

Definition of the invariant: given two (equal or different) correct validators, if at least one anchor is committed in one, the other has a path to the same anchor from every certificate at least two rounds after the anchor.

Definitions and Theorems

Theorem: omni-paths-p-necc

(defthm omni-paths-p-necc
 (implies
  (omni-paths-p systate)
  (implies
   (and (in val1 (correct-addresses systate))
        (in val2 (correct-addresses systate)))
   (b* ((vstate1 (get-validator-state val1 systate))
        (vstate2 (get-validator-state val2 systate))
        (anchor (last-anchor vstate1)))
     (implies anchor
              (dag-omni-paths-p anchor
                                (validator-state->dag vstate2)))))))

Theorem: booleanp-of-omni-paths-p

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

Theorem: omni-paths-p-of-system-state-fix-systate

(defthm omni-paths-p-of-system-state-fix-systate
  (equal (omni-paths-p (system-state-fix systate))
         (omni-paths-p systate)))

Theorem: omni-paths-p-system-state-equiv-congruence-on-systate

(defthm omni-paths-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (omni-paths-p systate)
                  (omni-paths-p systate-equiv)))
  :rule-classes :congruence)