

@2143

8 years 
mulligan 
Changes to the subaddressing mode elim functions moved into their …



@2140

8 years 
mulligan 
Done the hardest cases in the main theorem. Just got a few daemons to …



@2139

8 years 
mulligan 
Changes to get the main lemma compiling again. Changes pushed into …



@2131

8 years 
sacerdot 
No more need for functional extensionality.



@2129

8 years 
mulligan 
Large changes from today trying to complete the main theorem. Again :(



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2122

8 years 
sacerdot 
More stuff moved around in proper places



@2121

8 years 
sacerdot 
More functions moved to the places they belong to



@2114

8 years 
sacerdot 
Proof repaired



@2109

8 years 
mulligan 
Finished porting the large, main lemma to the new notion of jump …



@2108

8 years 
mulligan 
Various axioms closed and others moved around. Uncommented main lemma …



@2047

8 years 
mulligan 
Big bugs in policy calculations found. Waiting for Jaap's commit.



@2039

8 years 
sacerdot 
New, better interface for subaddressing_mode_elim



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2026

8 years 
mulligan 
Added a new file to house the main theorem as the type checking time …



@2024

8 years 
mulligan 
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …



@2023

8 years 
mulligan 
Closed main lemma modulo closing trivial subgoals about commutations …



@2020

8 years 
mulligan 
CJNE case complete, DJNZ case almost complete



@2018

8 years 
mulligan 
CJNE case a complete mess.



@2017

8 years 
mulligan 
Large swathes of proof of main lemma added.



@1985

8 years 
mulligan 
A single `false' case for unconditional jumps completed.



@1984

8 years 
mulligan 
Most proof obligations closed in main_lemma apart from those of the …



@1983

8 years 
mulligan 
Changes to simplify the simpler cases of the main_lemma.



@1979

8 years 
sacerdot 
Very very very tricky lemma closed. A dreadful mix of JM equality …



@1978

8 years 
sacerdot 
Two more cases completed.



@1977

8 years 
sacerdot 
Unblocked: let ... as hides two different terms, one that uses Leibniz …



@1975

8 years 
mulligan 
Work from today on closing main_thm.



@1971

8 years 
sacerdot 
1. Interpret.ma:
we need to prove
\sigma (execute_preinstruction …



@1969

8 years 
sacerdot 
Some more progress, but now we must prove something on a Russell …



@1967

8 years 
sacerdot 
Mov case completed.



@1966

8 years 
mulligan 
Progress made on main_thm proof: trying to find a pattern to use …



@1963

8 years 
sacerdot 
More progress in restoring the original proof.



@1958

8 years 
mulligan 
Marked divergence in StatusProofs?.ma



@1952

8 years 
sacerdot 
AssemblyProof? splitted.
