		Search-engine friendly clone of the ACL2 documentation.

Nonforking-anchors-def-and-init-and-next

Nonforking-anchors-p

Definition of the invariant: given two correct validators in the system, their sequences of committed anchor do not fork.

Definitions and Theorems

Theorem: nonforking-anchors-p-necc

(defthm nonforking-anchors-p-necc
 (implies
  (nonforking-anchors-p systate)
  (implies
     (and (in val1 (correct-addresses systate))
          (in val2 (correct-addresses systate)))
     (lists-noforkp
          (committed-anchors (get-validator-state val1 systate))
          (committed-anchors (get-validator-state val2 systate))))))

Theorem: booleanp-of-nonforking-anchors-p

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

Theorem: nonforking-anchors-p-of-system-state-fix-systate

(defthm nonforking-anchors-p-of-system-state-fix-systate
  (equal (nonforking-anchors-p (system-state-fix systate))
         (nonforking-anchors-p systate)))

Theorem: nonforking-anchors-p-system-state-equiv-congruence-on-systate

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