Skip to content

GitLab

Merged
Created by Robbert Krebbers@robbertkrebbersMaintainer

Prove more equivalences for closure operators on relations.

Add and extend equivalences between closure operators:

  • Add ↔ lemmas that relate rtc, tc, nsteps, and bsteps.
  • Rename → lemmas rtc_nsteps → rtc_nsteps_1, nsteps_rtc → rtc_nsteps_2, rtc_bsteps → rtc_bsteps_1, and bsteps_rtc → rtc_bsteps_2.
  • Add lemmas that relate rtc, tc, nsteps, and bsteps to path representations as lists.

The _list lemmas were proposed by @jules and he provided an initial proof specific to rtc.

Edited by Robbert Krebbers