---

Step * 1 of Lemma not_over_implies


1. P : @i'
2. Q : @i'
3. SqStable(P)@i
4. R:. (R  (R))@i'
5. (P  Q)@i
6. P
 P
BY
{ (D (-2) THEN Auto) }



1.  P  :  \mBbbP{}@i'
2.  Q  :  \mBbbP{}@i'
3.  SqStable(P)@i
4.  \mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R))@i'
5.  \mneg{}(P  {}\mRightarrow{}  Q)@i
6.  \mneg{}P
\mvdash{}  P


By

(D  (-2)  THEN  Auto)



Home Index