|
|
@2109
|
9 years |
mulligan |
Finished porting the large, main lemma to the new notion of jump …
|
|
|
@2108
|
9 years |
mulligan |
Various axioms closed and others moved around. Uncommented main lemma …
|
|
|
@2047
|
9 years |
mulligan |
Big bugs in policy calculations found. Waiting for Jaap's commit.
|
|
|
@2039
|
9 years |
sacerdot |
New, better interface for subaddressing_mode_elim
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2026
|
9 years |
mulligan |
Added a new file to house the main theorem as the type checking time …
|
|
|
@2024
|
9 years |
mulligan |
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
|
|
|
@2023
|
9 years |
mulligan |
Closed main lemma modulo closing trivial subgoals about commutations …
|
|
|
@2020
|
9 years |
mulligan |
CJNE case complete, DJNZ case almost complete
|
|
|
@2018
|
9 years |
mulligan |
CJNE case a complete mess.
|
|
|
@2017
|
9 years |
mulligan |
Large swathes of proof of main lemma added.
|
|
|
@1985
|
9 years |
mulligan |
A single `false' case for unconditional jumps completed.
|
|
|
@1984
|
9 years |
mulligan |
Most proof obligations closed in main_lemma apart from those of the …
|
|
|
@1983
|
9 years |
mulligan |
Changes to simplify the simpler cases of the main_lemma.
|
|
|
@1979
|
9 years |
sacerdot |
Very very very tricky lemma closed. A dreadful mix of JM equality …
|
|
|
@1978
|
9 years |
sacerdot |
Two more cases completed.
|
|
|
@1977
|
9 years |
sacerdot |
Unblocked: let ... as hides two different terms, one that uses Leibniz …
|
|
|
@1975
|
9 years |
mulligan |
Work from today on closing main_thm.
|
|
|
@1971
|
9 years |
sacerdot |
1. Interpret.ma:
we need to prove
\sigma (execute_preinstruction …
|
|
|
@1969
|
9 years |
sacerdot |
Some more progress, but now we must prove something on a Russell …
|
|
|
@1967
|
9 years |
sacerdot |
Mov case completed.
|
|
|
@1966
|
9 years |
mulligan |
Progress made on main_thm proof: trying to find a pattern to use …
|
|
|
@1963
|
9 years |
sacerdot |
More progress in restoring the original proof.
|
|
|
@1958
|
9 years |
mulligan |
Marked divergence in StatusProofs?.ma
|
|
|
@1952
|
9 years |
sacerdot |
AssemblyProof? splitted.
|