Skip to content

Prove event_list_helper lemmas

Jaemin Choi requested to merge jaemin/event-list-helper-2 into graphs_multi

All lemmas in event_list_helper.v have been proven.

Several lemmas which had counterexamples or unnecessary conditions have been modified: event_list_insert_snoc, event_list_union_l, events_list_union_r, eids_complete_correct, linearization_snoc, and orders_consistent.

Merge request reports