---

Step * of Lemma regext-Regularset

∀a:Set{i:l}. Regular(regext(a))
BY
{ (InstLemma `regext-Regularcoset` []
   THEN ParallelLast
   THEN Unfold `Regularcoset` -1
   THEN D -1
   THEN D 0
   THEN Try (Trivial)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN (D -4 With ⌜λx,y. ((x ∈ B) ∧ (y ∈ regext(a)) ∧ (R x y))⌝  THENA Auto)
   THEN (D -1 THENA (D 0 THEN Reduce 0 THEN Auto THEN RWO "-5<" 0 THEN Auto))
   THEN (D -1 THENA (ParallelLast THEN Reduce 0 THEN RepeatFor 3 (ParallelLast) THEN Auto))
   THEN ExRepD
   THEN D 0 With ⌜b⌝ 
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -3)
   THEN RepeatFor 2 (ParallelLast)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:Set\{i:l\}.  Regular(regext(a))


By

---

Latex:
(InstLemma  `regext-Regularcoset`  []
  THEN  ParallelLast
  THEN  Unfold  `Regularcoset`  -1
  THEN  D  -1
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  (D  -4  With  \mkleeneopen{}\mlambda{}x,y.  ((x  \mmember{}  B)  \mwedge{}  (y  \mmember{}  regext(a))  \mwedge{}  (R  x  y))\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENA  (D  0  THEN  Reduce  0  THEN  Auto  THEN  RWO  "-5<"  0  THEN  Auto))
  THEN  (D  -1  THENA  (ParallelLast  THEN  Reduce  0  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto))
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}b\mkleeneclose{} 
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -3)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index