---

Step * of Lemma i-closed-closed

∀I:Interval. (i-closed(I) ⇒ closed-rset(λx.(x ∈ I)))
BY
{ (Auto
   THEN RepUR ``closed-rset`` 0
   THEN Auto
   THEN RepeatFor 2 (D -1)
   THEN Reduce (-1)
   THEN (RepeatFor 2 (D 1) THEN D 2)
   THEN (Try (DVar `x1') THEN Try (DVar `x2'))
   THEN All (RepUR ``i-member i-closed``)
   THEN Auto
   THEN Try (RenameVar `a' 1)
   THEN Try (RenameVar `b' 2)
   THEN ((InstLemma `rleq-limit` [⌜x⌝;⌜λ2n.b⌝;⌜y⌝;⌜b⌝]⋅ THEN Complete (Auto))
   ORELSE (InstLemma `rleq-limit` [⌜λ2n.a⌝;⌜x⌝;⌜a⌝;⌜y⌝]⋅ THEN Complete (Auto))
   )) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  (i-closed(I)  {}\mRightarrow{}  closed-rset(\mlambda{}x.(x  \mmember{}  I)))


By

---

Latex:
(Auto
  THEN  RepUR  ``closed-rset``  0
  THEN  Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  (-1)
  THEN  (RepeatFor  2  (D  1)  THEN  D  2)
  THEN  (Try  (DVar  `x1')  THEN  Try  (DVar  `x2'))
  THEN  All  (RepUR  ``i-member  i-closed``)
  THEN  Auto
  THEN  Try  (RenameVar  `a'  1)
  THEN  Try  (RenameVar  `b'  2)
  THEN  ((InstLemma  `rleq-limit`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))
  ORELSE  (InstLemma  `rleq-limit`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))
  ))

---

Home Index