Changeset 3488


Ignore:
Timestamp:
Sep 24, 2014, 3:56:55 PM (5 years ago)
Author:
sacerdot
Message:

One proof repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3486 r3488  
    376376                (λs.match s with [ FINAL ⇒ true | _ ⇒ false])
    377377                ???.
    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
    380383  [ #_ #EQ destruct] * normalize nodelta
    381384  [ #seq #lbl #_
     
    390393  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
    391394  * * #_ 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
    393399  [ #_ #EQ destruct] * normalize nodelta
    394400  [ #seq #lbl #_
     
    416422  ]
    417423  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
    419428  [ #_ #EQ destruct] * normalize nodelta
    420429  [ #seq #lbl #_
     
    429438  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
    430439  whd in ⊢ (??%% → ?); #EQ destruct % //
    431 qed.*)
     440qed.
    432441
    433442definition asm_concrete_trans_sys ≝
Note: See TracChangeset for help on using the changeset viewer.