|
|
|
@943
|
9 years |
sacerdot |
…
|
|
|
|
@942
|
9 years |
sacerdot |
New invariant for the main theorem.
The new invariant is much more …
|
|
|
|
@941
|
9 years |
sacerdot |
Jmp case finished up to arithmetical properties.
|
|
|
|
@940
|
9 years |
mulligan |
more changes to inc case of main theorem
|
|
|
|
@939
|
9 years |
sacerdot |
Long Jmp case finished.
|
|
|
|
@938
|
9 years |
sacerdot |
…
|
|
|
|
@937
|
9 years |
mulligan |
resolved conflict in assembly_proof, more lemmas added
|
|
|
|
@936
|
9 years |
sacerdot |
Ticks are now handled correctly everywhere and the main proof takes …
|
|
|
|
@935
|
9 years |
mulligan |
changes to status and assembly proof
|
|
|
|
@934
|
9 years |
sacerdot |
…
|
|
|
|
@933
|
9 years |
sacerdot |
New proof strategy.
|
|
|
|
@932
|
9 years |
sacerdot |
…
|
|
|
|
@931
|
9 years |
sacerdot |
…
|
|
|
|
@930
|
9 years |
sacerdot |
Comment, Cost, ADD, ADC cases done.
|
|
|
|
@929
|
9 years |
mulligan |
added ticks_of function
|
|
|
|
@926
|
9 years |
sacerdot |
Main theorem false because of ticks :-(
|
|
|
|
@925
|
9 years |
sacerdot |
…
|
|
|
|
@924
|
9 years |
sacerdot |
…
|
|
|
|
@923
|
9 years |
sacerdot |
Main theorem made nice... but unprovable at the moment.
|
|
|
|
@921
|
9 years |
mulligan |
resolved conflict, fixed bugs
|
|
|
|
@919
|
9 years |
sacerdot |
Back to a readable statement.
|
|
|
|
@916
|
9 years |
sacerdot |
Fix for jump_expansion_policy.
|
|
|
|
@915
|
9 years |
mulligan |
finished changes to fetch_assembly_pseudo2
|
|
|
|
@912
|
9 years |
sacerdot |
Readable main theorem statement.
|
|
|
|
@911
|
9 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
|
@909
|
9 years |
sacerdot |
Back to the main theorem.
|
|
|
|
@908
|
9 years |
sacerdot |
Next big lemma proved!
|
|
|
|
@906
|
9 years |
sacerdot |
…
|
|
|
|
@905
|
9 years |
mulligan |
work from today
|
|
|
|
@904
|
9 years |
sacerdot |
Cleanup.
|
|
|
|
@903
|
9 years |
sacerdot |
Statement of new main lemma (as axiom).
|
|
|
|
@902
|
9 years |
sacerdot |
Cleanup.
|
|
|
|
@901
|
9 years |
sacerdot |
Second main lemma proved.
|
|
|
|
@897
|
9 years |
sacerdot |
Proof completed, fetch and assembly are mutual inverses.
|
|
|
|
@896
|
9 years |
sacerdot |
Proof finished (but ugly) :-)
|
|
|
|
@894
|
9 years |
sacerdot |
Bug more evident.
|
|
|
|
@893
|
9 years |
sacerdot |
Cleanup.
|
|
|
|
@892
|
9 years |
sacerdot |
First fundamental lemma almost finished.
|
|
|
|
@890
|
9 years |
sacerdot |
Better statement, begin of uniform proof.
|
|
|
|
@889
|
9 years |
sacerdot |
Minor changes because of the new, weaker (but much faster) delift.
|
|
|
|
@885
|
9 years |
sacerdot |
Proof almost finished, but rewritings are extremely slow.
|
|
|
|
@884
|
9 years |
sacerdot |
…
|
|
|
|
@883
|
9 years |
sacerdot |
Merged done well.
|
|
|
|
@877
|
9 years |
mulligan |
work from today
|
