Interaction-based approximation for HP-complete λ-theory?

Question

We are looking for a proof or counter-examples for the following hypothesis.

Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either $$ \exists n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n\rangle, $$ or $$ \forall n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n, \Delta\rangle, $$ where $\Gamma(M, x)$ and $\Gamma^*(N, x)$ are defined in a compact encoding for $\lambda$-terms in interaction calculus.

Any help would be appreciated.

Answer 1

One counterexample for the forward implication ($\not\Rightarrow$) is solvable $M \equiv N \equiv \lambda x.x\ \Omega$. Indeed, $$ \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \not\rightarrow^* \langle\varnothing\ |\ x_1 = x_1, x_2 = x_2, \Delta\rangle. $$

Another counterexample ($\not\Leftarrow$) is based on $I = J$ demonstrated in arXiv:1304.2290. Specifically, if $M \equiv \lambda x.x\ I\ I$ and $N \equiv \lambda x.x\ J\ \Omega$, then $$ \forall n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n, \Delta\rangle. $$ However, $M\ F = I$ is solvable while $N\ F = \Omega$ is not, which contradicts sensibility.