Changeset 3488
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3486 r3488 376 376 (λs.match s with [ FINAL ⇒ true  _ ⇒ false]) 377 377 ???. 378 @hide_prf cases daemon qed. (* 379 [ #s1 #s2 #l inversion(fetch ???) normalize nodelta 378 @hide_prf 379 [ #s1 #s2 #l 380 cases s1 normalize nodelta [1,2: #abs destruct] s1 #s1 381 cases s2 normalize nodelta [1: #_ * 2: #_ * #_ #EQ >EQ normalize /2/ ] #s2 382 inversion(fetch ???) normalize nodelta 380 383 [ #_ #EQ destruct] * normalize nodelta 381 384 [ #seq #lbl #_ … … 390 393 normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) H 391 394 * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // 392  #s1 #s2 #l inversion(fetch ???) normalize nodelta 395  #s1 #s2 #l 396 cases s1 normalize nodelta [2: #_ * 3: #s1 ] 397 cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ] 398 inversion(fetch ???) normalize nodelta 393 399 [ #_ #EQ destruct] * normalize nodelta 394 400 [ #seq #lbl #_ … … 416 422 ] 417 423 whd in ⊢ (??%% → ?); #EQ destruct destruct % // 418  #s1 #s2 #l inversion(fetch ???) normalize nodelta 424  #s1 #s2 #l 425 cases s1 normalize nodelta [1,2: #abs destruct ] #s1 426 cases s2 normalize nodelta [ #_ *  #_ * /2/ ] #s2 427 inversion(fetch ???) normalize nodelta 419 428 [ #_ #EQ destruct] * normalize nodelta 420 429 [ #seq #lbl #_ … … 429 438 normalize nodelta #H cases(bind_inversion ????? H) H #x * #_ 430 439 whd in ⊢ (??%% → ?); #EQ destruct % // 431 qed. *)440 qed. 432 441 433 442 definition asm_concrete_trans_sys ≝
Note: See TracChangeset
for help on using the changeset viewer.