Solution: Infer a term

1. \(\alpha (\lambda x. walks'x) john' \equiv_{\beta} slow'(walks'john')\)

\(\lambda p\lambda x.slow'(p\cnct{x})\)

1. \(\alpha (\lambda x. walks'x) john' \equiv_{\beta} slow'walks'john'\)

\(\lambda p\lambda x.slow'p\cnct{}x\)

Note that, first one obtains: \(slow'(\lambda x.walks'x)john'\)

then, after \(\eta-\)reduction, you get: \(slow'walks'john'\)

1. \(\alpha\cnct{mary'}john'(\lambda x.walks'x) \equiv_{\beta} walks'john' \land walks'mary'\)

\(\lambda x\lambda y\lambda p. p\cnct{y} \land p\cnct{x}\)

1. \(\alpha(\lambda x. talks'x)(\lambda x.smiles'x)john'\equiv_{\beta} smiles'john' \land talks'john'\)

\(\lambda p\lambda q\lambda x.q\cnct{x} \land p\cnct{x}\)

---