Logic Proof Problem.

[kartal]

I am trying to solve a natural deduction question. After I finished 4 of them the 5th one looks like a litle bit difficult.

This is my question

Symbol Meaning
R(x) ------>x is a river
L(x) ------>x is a lake
S(x) ------>x is a sea
F(x, y) --->x flows into y
UF(x, y)--> x ultimately flows into y

Using this symbols and meaning I need to prove a statement.

Vx(S(x) ---> ¬EzF(x, z)) premise
VxVy(F(x, y) ^ ¬EzF(y, z) ---> UF(x, y)) premise
--------------------------------------------------------------
VxVy(F(x, y) ^ S(y) ----> UF(x, y)) conclusion

I begin with V elemination

1.S(a) ---> ¬EzF(a, z)

2.F(a, b) ^ ¬EzF(b, z) ---> UF(a, b)

.
.
.
10.F(a, b) ^ S(b) ----> UF(a, b) after VxVy intro I can find the result But actually How I can derive This formula I couldnt find the starting point

Which one I need to take assumption and drive the next statement Or Do I need a second assumption

may be first I need to take S(a) as an assumtion after that If I can use if elimination for 1st premise then I can get ¬EzF(a, z) then I need to use if elemination for the second premise But for this I need to derive
F(a, b) ^ ¬EzF(b, z) How I can get this Again Do I need an assumption or It can be possible by only using the first premise


At this point I need some help

Or If you have any other suggestions for solution. No problem. The thinks which is writen above is my starting point. If It is wrong then please awaken me

Regards

[kartal]

I Found something for my solution but Again I need some help

1.Vx(S(x) ---> ¬EzF(x, z)) premise

2.VxVy(F(x, y) ^ ¬EzF(y, z) ---> UF(x, y)) premise

3.S(a) ---> ¬EzF(a, z) (1,V elim [x/b])

4.F(a, b) ^ ¬EzF(b, z) ---> UF(a, b) (2, V elim [x/a][y/b])

. 5. SUBDERIVATION

5.1 S(a) assumption
5.2 ¬EzF(a, z) (3, 5.1 --> elim)
.
.
.
.
10.F(a, b) ^ S(b) ----> UF(a, b)

Now I need to find F(a,b) then I can use ^ intro 5.2 and F(a,b)

So I can find F(a, b) ^ ¬EzF(b, z) and after that using --> elim I can achieve UF(a,b)


But my question is how I can carry F(a,b) can I assump it or is this a way to derive it from another way

[bettydlgc]

can you help me solve the following?

-(-P v -Q) therefore (P & Q)