# Stuck on formal proofs. Not sure how to continue

I'm stuck on what how to continue. I know I'm missing a few steps but this is what I have so far. Thank you in advance!

1. ¬Cube(b) → Small(b)
2. Small(c) → (Small(d) ∨ Small(e))
3. Small(d) → ¬Small(c)
4. Cube(b) → ¬Small(e)

1. Small(c)

1. ¬Small(b)
1. ¬Cube(b)
2. Small(b) (→ Elim 1,7)
3. ⊥ (⊥intro 6, 8)

10.Cube(b) (¬Intro 7-9)

1. ¬Small(e) (→ Elim 4,10)

Goal: Small(c) → Small(b)

1. $\qquad \qquad Small(d) \vee Small(e)$ ($\rightarrow$ Elim 2,5)

2. $\qquad \qquad \qquad Small(d)$

3. $\qquad \qquad \qquad Small(e)$

4. $\qquad \qquad \qquad \bot$ ($\bot$ Intro 11,14)

5. $\qquad \qquad\qquad Small(d)$ ($\bot$ Elim 15)

6. $\qquad \qquad Small(d)$ ($\vee$ Elim 12, 13-13, 14-16)

7. $\qquad \qquad \neg Small(c)$ ($\rightarrow$ Elim 17, 3)

8. $\qquad \qquad \bot$ ($\bot$ Intro 5,18)

9. $\qquad \neg \neg Small(b)$ ($\neg$ Intro 6-19)

10. $\qquad Small(b)$ ($\neg$ Elim 20)

11. $Small(b) \rightarrow Small(c)$ ($\rightarrow$ Intro 5-21)

• I'm not sure what you did with step #17 because it didn't check out. Can you elaborate? – ashley Dec 4 '16 at 4:17
• In step 13 I started a subproof, but the assumption was at the same time the last lone of that subproof (yes, you can do that!). On line 14 I started a subproof as well, endig with line 16. So on line 17 I point to the disjunction on line 12, as well as to those two subproofs, and do $\vee$ Elim. – Bram28 Dec 4 '16 at 13:44
• Yes that's exactly what I did but it didn't check out. imgur.com/a/6hcLT Here is the screenshot what I have. – ashley Dec 4 '16 at 17:03
• @ashley you need to close the subproof you just opened on line 13. So get rid of that subproof that you now have on 14-16, go to line 13, and do CTRL-E for end subproof, and then redo the suproof for Small(d). So now the two subproofs are at the same level, and right after each other, rather than that the second subproof is within the first subproof. – Bram28 Dec 4 '16 at 19:11
• Oh I see! Thank you so much for your help! – ashley Dec 4 '16 at 20:23