Add and extend equivalences between closure operators:
↔
lemmas that relate rtc
, tc
, nsteps
, and bsteps
.→
lemmas rtc_nsteps
→ rtc_nsteps_1
,
nsteps_rtc
→ rtc_nsteps_2
, rtc_bsteps
→ rtc_bsteps_1
, and
bsteps_rtc
→ rtc_bsteps_2
.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
.