source: src/ASM/CostsProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1511   8 years mulligan proofs, added, changes to execute_1_0 function therefore required to …
(edit) @1509   8 years mulligan i hate subtraction over the nats
(edit) @1506   8 years mulligan changes to costs proof over weekend
(edit) @1503   8 years mulligan inductive type complete
(edit) @1502   8 years mulligan changes to inductive defn
(edit) @1501   8 years sacerdot We must take in account the labelled_p predicate.
(edit) @1500   8 years sacerdot Proof sketch for one of the two main proofs.
(edit) @1499   8 years mulligan part way through main statement transcription
(add) @1498   8 years mulligan added new file for proof that costs are preserved at asm level
Note: See TracRevisionLog for help on using the revision log.