Changeset 2296 for src/RTLabs/semantics.ma
 Timestamp:
 Aug 13, 2012, 2:18:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/semantics.ma
r2295 r2296 352 352 ] qed. 353 353 354 lemma final_cannot_move : ∀ge,s. 355 RTLabs_is_final s ≠ None ? → 356 ∃err. eval_statement ge s = Wrong ??? err. 357 #ge * 358 [ #f #fs #m * #F cases (F ?) @refl 359  #a #b #c #d #e * #F cases (F ?) @refl 360  #a #b #c #d * #F cases (F ?) @refl 361  #r #F % [2: @refl  skip ] 362 ] qed. 363 364 lemma step_not_final : ∀ge,s,tr,s'. 365 eval_statement ge s = Value … 〈tr,s'〉 → 366 RTLabs_is_final s = None ?. 367 #ge #s #tr #s' #EX 368 lapply (final_cannot_move ge s) 369 cases (RTLabs_is_final s) 370 [ //  #r #F cases (F ?) [ #m #E >E in EX; #EX destruct  % #E destruct ] 371 qed. 354 372 355 373 lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset
for help on using the changeset viewer.