source: src/ERTLptr/ERTLptrToLTLProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3254   7 years sacerdot Code I always forgot to commit. To be ported to ERTLtoLTLProof.ma.
(edit) @2949   7 years sacerdot Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
(edit) @2944   7 years sacerdot Some progress.
(edit) @2942   7 years sacerdot Many changes: 1. Coloured graphs are now specified in terms of …
(edit) @2940   7 years sacerdot 1. StatusSimulationHelper? changed to allow to use status_rel that …
(edit) @2938   7 years sacerdot 1. proof of "all eliminable are eliminable" completed 2. the notion of …
(edit) @2930   7 years sacerdot More progress. Some useless parameters have been removed from the …
(edit) @2922   7 years sacerdot Progress: proof of "eliminable statements can be eliminated" almost …
(edit) @2898   7 years piccolo 1) simplification of cond and seq case for StatusSimulationHelper?
(edit) @2889   7 years sacerdot It works very nice!
(edit) @2883   7 years piccolo partial commit
(edit) @2863   7 years piccolo Added new invariant to good_if Generalized version of cond case for …
(edit) @2855   7 years piccolo little bug fixed in TranslateUtils?.
(edit) @2851   7 years piccolo partial commit
(edit) @2849   7 years piccolo partial commit
(edit) @2845   7 years piccolo ERTLptr to LTL correctness proof started
(add) @2796   7 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.