Changeset 1880 for src/RTLabs/semantics.ma

Timestamp:

Apr 6, 2012, 4:57:22 PM (9 years ago)

Author:

campbell

Message:

Show that RTLabs flat traces are determined by their starting state, and
that structured traces can be flattened, so must describe the same
execution as a flat trace from the same starting point.

File:

• src/RTLabs/semantics.ma (modified) (1 diff)

src/RTLabs/semantics.ma

@@ -326 +326 @@
 ] qed.
 
+
+lemma initial_state_is_not_final : ∀p,s.
+  make_initial_state p = OK ? s →
+  RTLabs_is_final s = None ?.
+#p #s whd in ⊢ (??%? → ?);
+@bind_ok #m #Em
+@bind_ok #b #Eb
+@bind_ok #f #Ef
+#E destruct
+@refl
+qed.