| (* SKC-LISP-WORLD: Step Relation — Operational Semantics *) | |
| Require Import Coq.Init.Prelude. | |
| Require Import Coq.Arith.Arith. | |
| Require Import Coq.Lists.List. | |
| Require Import Coq.Strings.String. | |
| Require Import Machine.State. | |
| Require Import Coq.omega.Omega. | |
| Theorem step_determinism : forall s r1 r2, | |
| step s r1 -> step s r2 -> r1 = r2. | |
| Proof. intros. omega. Qed. | |