Commit 6d0a38cb authored by Ralf Jung's avatar Ralf Jung

note down equivalent def.n of frame_step by Jeehoon

parent 936db861
......@@ -30,6 +30,7 @@ Inductive step : relation (state sts * tokens sts) :=
tok s1 T1 tok s2 T2 step (s1,T1) (s2,T2).
Notation steps := (rtc step).
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
(* Probably equivalent definition: (\mathcal{L}(s') ⊥ T) ∧ s \rightarrow s' *)
| Frame_step T1 T2 :
T1 tok s1 T step (s1,T1) (s2,T2) frame_step T s1 s2.
Notation frame_steps T := (rtc (frame_step T)).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment