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


**Hypothesis.** In [interaction calculus](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.3594) $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ x\_1 = x\_1, \dots, x\_n = x\_n \rangle$, where the $\Gamma$ mapping is defined in [a compact encoding](http://arxiv.org/abs/1304.2290) for $\lambda$-terms, $M, N \in \Lambda\_0$ are combinators, and $n \geq 1$, *if and only if* $\lambda K\beta\eta \vdash M = N$.


In the case if the hypothesis holds true, we have an effective model for the $\lambda K\beta\eta$ equational theory.



Hypothesis: interaction-based model for λKβη
One counterexample for the forward implication ($\not\Rightarrow$) is $M \equiv \lambda x.x\ I\ I$ and $M \equiv \lambda x.x\ I\ F$. Indeed,


$$
\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \rightarrow^\* \langle \varnothing\ |\ x = x\rangle,
$$


but $M$ and $N$ are different $\beta\eta$-normal forms.


Another counterexample ($\not\Leftarrow$) is an equation $M \equiv I = K\ I\ \Omega \equiv N$ which is valid in $\lambda K\beta\eta$. Indeed,
$$
\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \rightarrow^\* \langle \varnothing\ |\ x = x, \Gamma(\Omega, \epsilon) \rangle,
$$
while the subnet $\langle \varnothing\ |\ \Gamma(\Omega, \epsilon)\rangle$ does not have a normal form.


On the other hand, the hypothesis might still be provable for $\lambda I\beta\eta$-calculus.


