source: src/ASM/AssemblyProofSplitSplit.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2273   8 years sacerdot 1. lemmas moved from all files to Test.ma 2. most of the lemmas in …
(edit) @2269   8 years sacerdot Proof completely repaired up to …
(edit) @2267   8 years sacerdot Call is now proved using the new strategy.
(edit) @2266   8 years sacerdot All daemons closed in Jmp case.
(edit) @2264   8 years sacerdot 1) Major change: we now always use the efficient way of resolving …
(edit) @2140   8 years mulligan Done the hardest cases in the main theorem. Just got a few daemons to …
(edit) @2139   8 years mulligan Changes to get the main lemma compiling again. Changes pushed into …
(edit) @2131   8 years sacerdot No more need for functional extensionality.
(edit) @2129   8 years mulligan Large changes from today trying to complete the main theorem. Again :(
(edit) @2127   8 years sacerdot Last daemon closed
(edit) @2123   8 years boender - moved is_well_labeled_p to Status and instruction_is_label to ASM …
(edit) @2122   8 years sacerdot More stuff moved around in proper places
(edit) @2110   8 years sacerdot …
(edit) @2062   8 years sacerdot Everything repaired (broken because of new proof obligation for fetch).
(edit) @2051   8 years mulligan Finished the Jmp case in the main theorem.
(edit) @2047   8 years mulligan Big bugs in policy calculations found. Waiting for Jaap's commit.
(edit) @2027   8 years mulligan Got the main lemma to apply in the proof of main theorem again and …
(add) @2026   8 years mulligan Added a new file to house the main theorem as the type checking time …
Note: See TracRevisionLog for help on using the revision log.