Ignore:
Timestamp:
Apr 6, 2012, 4:57:22 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1878 r1880  
    326326] qed.
    327327
     328
     329lemma initial_state_is_not_final : ∀p,s.
     330  make_initial_state p = OK ? s →
     331  RTLabs_is_final s = None ?.
     332#p #s whd in ⊢ (??%? → ?);
     333@bind_ok #m #Em
     334@bind_ok #b #Eb
     335@bind_ok #f #Ef
     336#E destruct
     337@refl
     338qed.
Note: See TracChangeset for help on using the changeset viewer.