Deduzione naturale

[slyb]

ciao
avrei bisogno di un piccolo aiuto o suggerimento per risolvere il seguente esercizio di DN

$forallx(notB(x) V C(x)), notexistsy(C(y) & A (y)) |- forallx(B(x) -> notA(x)) $

Ho iniziato a costruire le derivazioni ma non riesco ad andare avanti

$forallx(notB(x) V C(x))$
$notexistsy(C(y) & A (y))$
$-------------------$
$ B(a)$
$ --------------------$
$ notexistsy(C(y) & A (y))$
....
...
...
$ notA(a) $
$ B(a) -> notA(a) $
$-----------------$
$forallx(B(x) -> notA(x))$



Grazie in anticipo
B.

[Lord K]

Io procederei osservando che:

[tex]\displaystyle \forall x(\neg P(x) \wedge Q(x)) \vdash \forall x (P(x) \rightarrow Q(x))[/tex]

[tex]\displaystyle \forall x(P(x) \rightarrow Q(x)) \vdash \forall x (\neg P(x) \rightarrow \neg Q(x))[/tex]

[tex]\displaystyle \neg \exists xP(x) \vdash \forall x \neg P(x)[/tex]

da queste ottengo il risultato, prova