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](http://mathgate.info/cebrown/notes/barendregt.php#4) 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](http://arxiv.org/abs/1304.2290).


Any help would be appreciated.



Interaction-based approximation for HP-complete λ-theory?
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.


