Changeset 1923 for src/ASM/CostsProof.ma
- Timestamp:
- May 8, 2012, 3:43:37 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1921 r1923 675 675 |8: 676 676 #end_flag #start_status #end_status #trace_any_label #costed_assm 677 #unrepeating_witness 677 #unrepeating_witness' 678 678 whd in ⊢ (??%?); whd in ⊢ (??(?%?)?); 679 679 >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) … … 687 687 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 688 688 normalize in match (nth_safe ? ? ? ?); 689 whd in costed_assm; lapply costed_assm -costed_assm689 whd in costed_assm; lapply costed_assm 690 690 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 691 691 [1: … … 698 698 #cost -block_cost_assm #block_cost_assm 699 699 cases (block_cost_assm ??? trace_any_label ???) 700 try @refl 701 [1: 702 assumption 703 |2: 704 (* XXX: !!! *) 705 cases daemon 706 ] 700 try @refl assumption 707 701 ] 708 702 ]
Note: See TracChangeset
for help on using the changeset viewer.