---

Step * of Lemma not_over_implies

P,Q:.  (SqStable(P)  (R:. (R  (R)))  ((P  Q)  {P  (Q)}))
BY
{ ((Unfold `guard` 0 THEN Auto) THEN InstHyp [P] (-2)  THEN Auto THEN D (-1) THEN Unhide THEN D (-1) THEN Auto) }

1
1. P : @i'
2. Q : @i'
3. SqStable(P)@i
4. R:. (R  (R))@i'
5. (P  Q)@i
6. P
 P


\mforall{}P,Q:\mBbbP{}.    (SqStable(P)  {}\mRightarrow{}  (\mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R)))  {}\mRightarrow{}  (\mneg{}(P  {}\mRightarrow{}  Q)  \mLeftarrow{}{}\mRightarrow{}  \{P  \mwedge{}  (\mneg{}Q)\}))


By

((Unfold  `guard`  0  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}P\mkleeneclose{}]  (-2)  \mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Unhide
  THEN  D  (-1)
  THEN  Auto)



Home Index