Solution
= Solution
A term is in <beta-normal form> when it contains no <beta-redex>, meaning no subterm of the form
$$
(\lambda x.M)N.
$$
Equivalently, no <beta reduction> can be performed anywhere in the term.
= Solution
A term is in <beta-normal form> when it contains no <beta-redex>, meaning no subterm of the form
$$
(\lambda x.M)N.
$$
Equivalently, no <beta reduction> can be performed anywhere in the term.