source: src/ASM/CostsProof.ma @ 1499

Last change on this file since 1499 was 1499, checked in by mulligan, 8 years ago

part way through main statement transcription

File size: 403 bytes
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4
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 TracBrowser for help on using the repository browser.