Ignore:
Timestamp:
Jul 18, 2012, 2:56:12 PM (8 years ago)
Author:
mulligan
Message:

Closed major daemons in the supporting lemmas of the main lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2197 r2209  
    473473         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    474474    | INDIRECT i ⇒
    475        let d ≝ get_register … s [[false;false;i]] in
    476        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
     475        let d ≝ get_register … s [[false;false;i]] in
     476        let address ≝ bit_address_of_register … s [[false;false;i]] in
     477          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
     478            ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    477479    | EXT_INDIRECT _ ⇒ true
    478480    | REGISTER r ⇒
Note: See TracChangeset for help on using the changeset viewer.