Solution (source code)

= Solution

Repeated use of $U\to V\equiv\neg U\lor V$ yields
$$
\varphi_n\equiv\neg A_n\lor\neg A_{n-1}\lor\cdots\lor\neg A_2\lor A_1.
$$
This <logical disjunction> is false exactly when $A_2,\ldots,A_n$ are all true and $A_1$ is false. There is precisely one such <Boolean valuation> out of the $2^n$ assignments to the $n$ independent propositional variables. Thus \b[the number of <satisfying assignments> is $2^n-1$]. This is the <satisfying-assignment count for nested implications>; the implication brackets associate to the right here.