Ignore:
Timestamp:
Feb 19, 2013, 7:24:20 PM (8 years ago)
Author:
campbell
Message:

Don't apply inv in after_n_steps to last state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Executions.ma

    r2487 r2682  
    6767  cases (step … s) [ #o #K * | 3: #m * ]
    6868  * #tr' #s'
    69   whd in ⊢ (% → ?); cases (inv s') [2: *]
     69  whd in ⊢ (% → ?);
    7070  #AW %{tr'} %{s'} %{AW}
    7171  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
Note: See TracChangeset for help on using the changeset viewer.