Last change
on this file since 1499 was
1499,
checked in by mulligan, 9 years ago
|
part way through main statement transcription
|
File size:
403 bytes
|
Line | |
---|
1 | include "ASM/ASMCosts.ma". |
---|
2 | include "ASM/WellLabeled.ma". |
---|
3 | include "ASM/Status.ma". |
---|
4 | |
---|
5 | axiom 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.