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

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.

-
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.