(Context: this is a problem from the middle of my dissertation work, abstracted into a more general problem. It's related to showing that some liveness properties hold, so perhaps work from something like CTL could apply.)
Say you have some tree of possibly infinite depth with root node $n_0$. (EDIT: the number of children per node is bounded, in case that helps.) There exists a special set $G$ of "good" nodes in the tree such that for every path from $n_0$ through the tree, that path contains a node in $G$ (although that node can be at any arbitrary depth).
Now, say there is some property $P$ on nodes of the tree such that $P(n)$ holds if and only if:
- $n \in G$, or
- for every child node $n'$ of $n$, $P(n')$ holds.
To prove: $P(n_0)$ holds
$P$ is practically another way of saying "every path has a node in $G$", so this seems almost trivial. However, I can't seem to formally prove it. An inductive proof seems like the way to go ("I expect my children to all be in P if I'm not in $G$ myself, so $P$ should hold for me"), but what to induct on? Something like "distance until the farthest "good" node" seems natural, but I'm not sure such a bound exists.
I'm reasonably sure this statement can be proved, so how to prove it? Is there indeed a bound on the farthest "good node", and if so, what is the argument that such a bound exists?