I don't have numbers for the lines yet, but here's the bones of my current strategy.
Exists-x (~P(x) || Q(x)) ......... premise. (I'm pretty sure that's right.
)
Open up an "Arb-Box"... x
0 ~P(x
0) || Q(x
0)
.... deal with the cases here? Or take it to the next level?
Open up a box in which to get a contradiction of P(x
0) && Q(x
0)
...
...
It ends in "bottom".
So after that inner box we have ~ P(x
0) && Q(x
0) ....... ~i (the previous box)
....
This is a "Chi" to end the exists-+-"arb-that-exists" box, so we're allowed to take it out? ... This is NOT such a "Chi", is it? A little bell rings saying you can't use the arbitrary x in your Chi....
OK. Enough doubt! Carry on.
The idea Was, come out of the box with ~ P(x) && Q(x), which I'm almost certain is wrong.
Obviously were it not wrong, one would easily move from there to "Exists" to reach the conclusion sought.
There you go. I won't edit this. Mistakes are often far more interesting than correct answers.