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

Two combinators $M$ and $N$ are solvable and equivalent in HP-complete $\lambda$-theory if and only if 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.

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.