|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
|
@994
|
10 years |
mulligan |
small changes
|
|
|
|
@993
|
10 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
|
@992
|
10 years |
mulligan |
a few more axioms closed
|
|
|
|
@991
|
10 years |
mulligan |
loads of axioms related to equality on instructions closed
|
|
|
|
@989
|
10 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
|
@988
|
10 years |
sacerdot |
Proof restored.
|
|
|
|
@987
|
10 years |
sacerdot |
Real parameterization over the policy.
|
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
|
@982
|
10 years |
boender |
- this should work (see previous commit)
|
|
|
|
@979
|
10 years |
sacerdot |
…
|
|
|
|
@977
|
10 years |
sacerdot |
#$%@#$@#$
|
|
|
|
@975
|
10 years |
sacerdot |
…
|
|
|
|
@972
|
10 years |
sacerdot |
…
|
|
|
|
@971
|
10 years |
sacerdot |
…
|
|
|
|
@959
|
10 years |
sacerdot |
…
|
|
|
|
@951
|
10 years |
sacerdot |
long call case completed
|
|
|
|
@950
|
10 years |
sacerdot |
Horrible sub-proof finished :-)
|
|
|
|
@949
|
10 years |
mulligan |
resolved conflict, work from today
|
|
|
|
@948
|
10 years |
sacerdot |
Some progress on the Call case.
|
|
|
|
@946
|
10 years |
sacerdot |
Jmp case repaired after addition of MAP hypothesis.
|
|
|
|
@945
|
10 years |
mulligan |
more small changes to proof of main thrm
|
|
|
|
@944
|
10 years |
mulligan |
split definition
|
|
|
|
@943
|
10 years |
sacerdot |
…
|
|
|
|
@942
|
10 years |
sacerdot |
New invariant for the main theorem.
The new invariant is much more …
|
|
|
|
@941
|
10 years |
sacerdot |
Jmp case finished up to arithmetical properties.
|
|
|
|
@940
|
10 years |
mulligan |
more changes to inc case of main theorem
|
|
|
|
@939
|
10 years |
sacerdot |
Long Jmp case finished.
|
|
|
|
@938
|
10 years |
sacerdot |
…
|
|
|
|
@937
|
10 years |
mulligan |
resolved conflict in assembly_proof, more lemmas added
|
|
|
|
@936
|
10 years |
sacerdot |
Ticks are now handled correctly everywhere and the main proof takes …
|
|
|
|
@935
|
10 years |
mulligan |
changes to status and assembly proof
|
|
|
|
@934
|
10 years |
sacerdot |
…
|
|
|
|
@933
|
10 years |
sacerdot |
New proof strategy.
|
|
|
|
@932
|
10 years |
sacerdot |
…
|
|
|
|
@931
|
10 years |
sacerdot |
…
|
|
|
|
@930
|
10 years |
sacerdot |
Comment, Cost, ADD, ADC cases done.
|
|
|
|
@929
|
10 years |
mulligan |
added ticks_of function
|
|
|
|
@926
|
10 years |
sacerdot |
Main theorem false because of ticks :-(
|
|
|
|
@925
|
10 years |
sacerdot |
…
|
|
|
|
@924
|
10 years |
sacerdot |
…
|
|
|
|
@923
|
10 years |
sacerdot |
Main theorem made nice... but unprovable at the moment.
|
|
|
|
@921
|
10 years |
mulligan |
resolved conflict, fixed bugs
|
|
|
|
@919
|
10 years |
sacerdot |
Back to a readable statement.
|
|
|
|
@916
|
10 years |
sacerdot |
Fix for jump_expansion_policy.
|
|
|
|
@915
|
10 years |
mulligan |
finished changes to fetch_assembly_pseudo2
|
|
|
|
@912
|
10 years |
sacerdot |
Readable main theorem statement.
|
|
|
|
@911
|
10 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
|
@909
|
10 years |
sacerdot |
Back to the main theorem.
|
|
|
|
@908
|
10 years |
sacerdot |
Next big lemma proved!
|
|
|
|
@906
|
10 years |
sacerdot |
…
|
|
|
|
@905
|
10 years |
mulligan |
work from today
|
|
|
|
@904
|
10 years |
sacerdot |
Cleanup.
|
|
|
|
@903
|
10 years |
sacerdot |
Statement of new main lemma (as axiom).
|
|
|
|
@902
|
10 years |
sacerdot |
Cleanup.
|
|
|
|
@901
|
10 years |
sacerdot |
Second main lemma proved.
|
|
|
|
@897
|
10 years |
sacerdot |
Proof completed, fetch and assembly are mutual inverses.
|
|
|
|
@896
|
10 years |
sacerdot |
Proof finished (but ugly) :-)
|
|
|
|
@894
|
10 years |
sacerdot |
Bug more evident.
|
|
|
|
@893
|
10 years |
sacerdot |
Cleanup.
|
|
|
|
@892
|
10 years |
sacerdot |
First fundamental lemma almost finished.
|
|
|
|
@890
|
10 years |
sacerdot |
Better statement, begin of uniform proof.
|
|
|
|
@889
|
10 years |
sacerdot |
Minor changes because of the new, weaker (but much faster) delift.
|
|
|
|
@885
|
10 years |
sacerdot |
Proof almost finished, but rewritings are extremely slow.
|
|
|
|
@884
|
10 years |
sacerdot |
…
|
|
|
|
@883
|
10 years |
sacerdot |
Merged done well.
|
|
|
|
@877
|
10 years |
mulligan |
work from today
|
