Solution (source code)

= Solution

With the convention that $p\leq q$ means that $p$ is stronger, a set $G\subseteq\mathbb P$ is a <generic filter> over $M$ when it is a filter and meets every <dense subset of a forcing order>[dense set] $D\subseteq\mathbb P$ with $D\in M$. Explicitly, $G$ is upward closed toward weaker conditions, every two members have a common stronger member in $G$, and $G\cap D\ne\varnothing$ for every such $D$.