---

Step * of Lemma at_cWObar

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀n:ℕ. ∀s:cWO-rel(R)-consistent-seq(n).  ((cWObar() n s) ⇒ (¬{a:T| cWO-rel(R) n s (inl a)} ))
BY
{ (InstLemma `cWObar_wf` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN RepUR ``cWObar`` -3
   THEN RepUR ``cWO-rel`` -1
   THEN (D -1 THENA Auto)
   THEN (Assert (↑isr(s (n - 1))) ∧ (↑isl(s (n - 1))) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜s (n - 1)⌝⋅ THENA Auto)
   THEN D (-2)⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}n:\mBbbN{}.  \mforall{}s:cWO-rel(R)-consistent-seq(n).    ((cWObar()  n  s)  {}\mRightarrow{}  (\mneg{}\{a:T|  cWO-rel(R)  n  s  (inl  a)\}  ))


By

---

Latex:
(InstLemma  `cWObar\_wf`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``cWObar``  -3
  THEN  RepUR  ``cWO-rel``  -1
  THEN  (D  -1  THENA  Auto)
  THEN  (Assert  (\muparrow{}isr(s  (n  -  1)))  \mwedge{}  (\muparrow{}isl(s  (n  -  1)))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}s  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-2)\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index