Changeset 1658 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Jan 25, 2012, 6:18:04 PM (8 years ago)
Author:
mulligan
Message:

asm costs changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1650 r1658  
    611611        generalize in match reachable_program_counter_witness;
    612612        generalize in match good_program_witness;
    613         <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?); (*
     613        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
    614614        -reachable_program_counter_witness #reachable_program_counter_witness
    615615        -good_program_witness #good_program_witness
    616         whd in ⊢ (??%?); @pair_elim *)
     616        whd in ⊢ (??%?); @pair_elim
    617617      ]
    618618    |2:
Note: See TracChangeset for help on using the changeset viewer.