Changeset 1910 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Apr 27, 2012, 5:48:20 PM (8 years ago)
Author:
mulligan
Message:

Finished proof modulo termination argument

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1900 r1910  
    677677        cases (block_cost ? ? ? ? ? ?)
    678678        #cost -block_cost_assm #block_cost_assm
    679         cases (block_cost_assm ? ? ? trace_any_label (refl …))
    680         #_ #assm >assm %
     679        cases (block_cost_assm ? ? ? trace_any_label (refl …)) %
    681680      ]
    682681    ]
Note: See TracChangeset for help on using the changeset viewer.