Changeset 1499


Ignore:
Timestamp:
Nov 7, 2011, 5:06:05 PM (8 years ago)
Author:
mulligan
Message:

part way through main statement transcription

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1498 r1499  
     1include "ASM/ASMCosts.ma".
     2include "ASM/WellLabeled.ma".
     3include "ASM/Status.ma".
    14
    2 
     5axiom main_statement:
     6  ∀s: Status.
     7  ∀cost_labels: BitVectorTrie Byte 16.
     8    let program_counter ≝ program_counter … s in
     9      ∀cost_label: Byte.
     10      ∀s': Status.
     11      ∀n: nat.
     12        (lookup_opt … program_counter cost_labels) = (Some … cost_label) ∧
     13        s' = (execute n s) → ?.
     14       
Note: See TracChangeset for help on using the changeset viewer.