Using natural deduction to show $(\neg s \to t) \land \neg (s \land t) , k \to \neg f, t \to k \vdash f\to s$

Question

Could someone please tell me if i have proved this sequence correct or not? Is it ok to state e.g. ¬f in row 7, but then assume f in row 13?

(¬s → t) ∧ ¬(s ∧ t) , k → ¬f, t → k ⊢ f→ s

1   (¬s → t) ∧ ¬(s ∧ t)     premis
2   k → ¬f                  premis
3   t → k                   premis
4   ¬s → t                  ∧e1, 1
------------------------------ 1 proof-box
    5   t         assumption
    6   k         →e 3,5
    7   ¬f        →e 2,6
------------------------------ 1 end of proof-box
8   t → ¬f    →i 5-7
------------------------------ 2 proof-box
    9   ¬s        assumption
    10  t         →e 4,9
    11  ¬f        →e 10,8
------------------------------ 2 end of proof-box
12  ¬s → ¬f   →i 9-11
------------------------------ 3 proof-box
    13  f       assumption
------------------------------ 4 proof-box
        14  ¬s      assumption
        15  ¬f      →e 12,14
        16  ⊥       →e 13,15
------------------------------ 4 end of proof-box
    17  ¬¬s     →i 14-16
    18  s       ¬¬e 17
------------------------------ 3 end of proof-box
19  f → s   →i 13-18

Answer 1

Your proof is valid. It is a little inelegant, but every inference is good.

It is essentially a proof by reductio ad absurdum (inside a conditional proof).

Assume f, assume not s, then derive a contradiction (¬f contradicts f). Therefore proving f → s.

So, you proof can be pruned a bit, by merging all those conditional proofs into one.

 1 (¬s → t) ∧ ¬(s ∧ t)   premis 
 2 k → ¬f                          premis 
 3 t → k                            premis
 4 ¬s → t                          ∧e1, 1
       5 f                              assumption 
            6 ¬s                      assumption
            7 t                         → e 6, 4
            8 k                        → e 7, 3
            9 ¬f                      → e 8,  2
           10 ⊥                     ¬e 5, 8
      11 ¬¬s                        ¬i 6-10
      12 s                            ¬¬e 11
 13 f → s                          →i 5-12