Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

Question

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't work), and because I couldn't find a relevant lemma in the papers themselves.

I'm referring in particular to the definition by Czajka [1] of the relation $\rightarrow^\infty_{\beta\bot}$, called infinitary Böhm-reduction. I've looked at [2], which however does not include Böhm-reduction (such that the defined relation isn't confluent IIUC, which is a problem for me).

Rationale: Defining reduction for infinitary $\lambda$-calculus is tricky. In particular, you cannot create an "infinite transitive closure" which allows an infinite number of transitivity steps, but you need to be more careful. In particular, if you define multi-step reduction coinductively, you cannot include a transitive rule, lest your relation becomes total and thus degenerate. So one ends up doing transitivity elimination, which is not always trivial; and given how unintuitive coinduction is, I'm afraid I'd fool myself when attempting a proof.

[1] Łukasz Czajka, 2014. A Coinductive Confluence Proof for Infinitary Lambda-Calculus. Proc. of Rewriting and Typed Lambda Calculi, Springer. http://www.mimuw.edu.pl/~lukaszcz/coind.pdf

[2] Jorg Endrullis and Andrew Polonsky, 2011. Infinitary Rewriting Coinductively. In Proc. of TYPES, volume 19 of LIPIcs, pages 16–27. Schloss Dagstuhl. http://drops.dagstuhl.de/opus/volltexte/2013/3897/

[3] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries, 1997. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93–125. http://www.sciencedirect.com/science/article/pii/S0304397596001715

Answer 1

I think you'll find that the exact same proof of Lemma 3 in [1] (the proof itself appears in [2]) concerning $\rightarrow^\infty_\beta$ also holds for $\rightarrow^\infty_{\beta\bot}$: indeed, they are defined in the same way from $\rightarrow^*_\beta$ and $\rightarrow^*_{\beta\bot}$ respectively, which are transitive by definition!

The lemma holds for an arbitrary reflexive-transitive congruence relation in place of $\rightarrow^*_{\beta\bot}$, as you can verify in [2] without needing to go into the detail of the coinductive proofs. In particular, the proofs of lemmas 4.1-5 in [2] are unchanged (with extra induction cases in 4.4).