1. ~S ∧ ~R Premise
2. ~S 1, Simplification (SIMP)
3. ~R 1, SIMP
4. ~R ∧ ~S 3,2 Conjunction Introduction (CI)
// Note, we could have just done Commutation of 1 to arrive at (~R ∧ ~S) in one step
5.:: S v R Conditional Proof (CP) assumption #1
// Either S or R is true, let's assume S is true first...
6.:: S CP assumption #2
7.:: ~(~R ∧ ~S) Clearly (~R ∧ ~S) can not be true, because S is true. The rule name here escapes me.
// Now assume R is true
8.:: R CP assumption #3
9.:: ~(~R ∧ ~S) Clearly (~R ∧ ~S) can not be true, because R is true. Same rule as line 7.
10.:: (S v R) --> ~(~R ∧ ~S) 5-9, CP
11.:: (~R ∧ ~S) --> ~(S v R) 10, Transposition (if A --> B then ~B --> ~A)
12. (~R ∧ ~S) --> ~(S v R) 5-11, CP
*DONE*
