diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 5c37021d..c83867f1 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1174,6 +1174,8 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +Axiom semantics_determinate: forall p, determinate (semantics p). + (** Determinacy of the [Asm] semantics. *) (* TODO. |