• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
          • Correctness
          • Definition
            • Initialization
            • Transitions
            • States
            • Events
            • Reachability
              • System-state-reachable-from-p
                • System-state-reachablep
            • Library-extensions
          • Aleovm
          • Leo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Reachability

    System-state-reachable-from-p

    Check if a system state is reachable from another one.

    This is the case when there is a list of zero or more events that are possible in the starting state (one after the other), and that lead to the state of interest (one after the other).

    Definitions and Theorems

    Theorem: system-state-reachable-from-p-suff

    (defthm system-state-reachable-from-p-suff
      (implies (and (event-listp events)
                    (events-possiblep events from)
                    (equal (system-state-fix systate)
                           (events-next events from)))
               (system-state-reachable-from-p systate from)))

    Theorem: booleanp-of-system-state-reachable-from-p

    (defthm booleanp-of-system-state-reachable-from-p
      (b* ((yes/no (system-state-reachable-from-p systate from)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: system-state-reachable-from-p-of-system-state-fix-systate

    (defthm system-state-reachable-from-p-of-system-state-fix-systate
      (equal (system-state-reachable-from-p (system-state-fix systate)
                                            from)
             (system-state-reachable-from-p systate from)))

    Theorem: system-state-reachable-from-p-system-state-equiv-congruence-on-systate

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

    Theorem: system-state-reachable-from-p-of-system-state-fix-from

    (defthm system-state-reachable-from-p-of-system-state-fix-from
     (equal
         (system-state-reachable-from-p systate (system-state-fix from))
         (system-state-reachable-from-p systate from)))

    Theorem: system-state-reachable-from-p-system-state-equiv-congruence-on-from

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