---

Step * of Lemma contrapos_elim2

P,Q:.  ((R:. (R  (R)))  ((Q)  (P))  {(P)  (Q)})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN InstHyp [Q] 3
   THEN Auto
   THEN D (-1)
   THEN skip{D 0}
   THEN Auto
   THEN (D (-3) THEN Auto)
   THEN Try (Complete ((D 0 THEN Auto)))
   THEN (Assert P BY
               Auto)
   THEN Auto) }


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


By

(Unfold  `guard`  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}Q\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  skip\{D  0\}
  THEN  Auto
  THEN  (D  (-3)  THEN  Auto)
  THEN  Try  (Complete  ((D  0  THEN  Auto)))
  THEN  (Assert  \mdownarrow{}P  BY
                          Auto)
  THEN  Auto)



Home Index