source: src/ERTLptr/ERTLptrToLTLProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2949   8 years sacerdot Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
(edit) @2944   8 years sacerdot Some progress.
(edit) @2942   8 years sacerdot Many changes: 1. Coloured graphs are now specified in terms of …
(edit) @2940   8 years sacerdot 1. StatusSimulationHelper? changed to allow to use status_rel that …
(edit) @2938   8 years sacerdot 1. proof of "all eliminable are eliminable" completed 2. the notion of …
(edit) @2930   8 years sacerdot More progress. Some useless parameters have been removed from the …
(edit) @2922   8 years sacerdot Progress: proof of "eliminable statements can be eliminated" almost …
(edit) @2898   8 years piccolo 1) simplification of cond and seq case for StatusSimulationHelper? …
(edit) @2889   8 years sacerdot It works very nice!
(edit) @2883   8 years piccolo partial commit
(edit) @2863   8 years piccolo Added new invariant to good_if Generalized version of cond case for …
(edit) @2855   8 years piccolo little bug fixed in TranslateUtils?.
(edit) @2851   8 years piccolo partial commit
(edit) @2849   8 years piccolo partial commit
(edit) @2845   8 years piccolo ERTLptr to LTL correctness proof started
(add) @2796   8 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
Note: See TracRevisionLog for help on using the revision log.