|
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.
