Skip to content

Introduce bi_nsteps and add timeless results for bi closures

Simcha van Collem requested to merge svancollem/iris:bi-closure-timeless into master

This MR adds lemmas to show that bi_tc R and bi_rtc R are Timeless whenever R itself is Timeless. It does so by introducing bi_nsteps, which are n-step R reductions, and using its equivalences with bi_tc and bi_rtc.

Merge request reports