---

Step * of Lemma until-class-simple-comb

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(Top)].
  ((X until Y) = λxs,ys.if bag-null(ys) then xs else {} fi |X;Prior(Y)| ∈ EClass(A))
BY
{ WithCumulativity ((Unfold `eclass` 0 THEN Auto)
                    THEN RepUR ``until-class simple-comb2 simple-comb`` 0
                    THEN RepeatFor 2 ((Ext
                                       THEN Reduce 0
                                       THEN Auto
                                       THEN Try (RepeatFor 2 ((All (Fold `eclass`) THEN Auto)))))
                    THEN RenameVar `es' (-2)
                    THEN RenameVar `e' (-1)
                    THEN (InstLemma `class-pred-cases` [⌜Info⌝;⌜Top⌝;⌜Y⌝;⌜es⌝;⌜e⌝]⋅ THENA Auto)
                    THEN Repeat ((D -1 THEN ExRepD))
                    THEN HypSubst' (-1) 0
                    THEN Reduce 0
                    THEN Auto
                    THEN Try (Complete ((All (Fold `eclass`) THEN Auto)⋅))
                    THEN OldAutoSplit
                    THEN SqExRepD
                    THEN (RWO "no-classrel-iff-empty<" (-1)
                          THEN Auto
                          THEN Try (((InstHyp [⌜v⌝] (-1)⋅ THENM D -1) THENA Auto)))⋅)⋅ }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. e' : E
8. (e' <loc e)
9. v : Top
10. v ∈ Y(e')
11. ∀e''<e.(↓∃v:Top. v ∈ Y(e'')) ⇒ e'' ≤loc e' 
12. class-pred(Y;es;e) = (inl e') ∈ (E + Top)
13. ∀v:Top. (¬v ∈ Prior(Y)(e))
⊢ v ∈ Prior(Y)(e)

2
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. ∀e'<e.∀v:Top. (¬v ∈ Y(e'))
8. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
9. ¬(∀v:Top. (¬v ∈ Prior(Y)(e)))
⊢ (X es e) = {} ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(Top)].
    ((X  until  Y)  =  \mlambda{}xs,ys.if  bag-null(ys)  then  xs  else  \{\}  fi  |X;Prior(Y)|)


By

---

Latex:
WithCumulativity  ((Unfold  `eclass`  0  THEN  Auto)
                                    THEN  RepUR  ``until-class  simple-comb2  simple-comb``  0
                                    THEN  RepeatFor  2  ((Ext
                                                                          THEN  Reduce  0
                                                                          THEN  Auto
                                                                          THEN  Try  (RepeatFor  2  ((All  (Fold  `eclass`)  THEN  Auto)))))
                                    THEN  RenameVar  `es'  (-2)
                                    THEN  RenameVar  `e'  (-1)
                                    THEN  (InstLemma  `class-pred-cases`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}Top\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                    THEN  Repeat  ((D  -1  THEN  ExRepD))
                                    THEN  HypSubst'  (-1)  0
                                    THEN  Reduce  0
                                    THEN  Auto
                                    THEN  Try  (Complete  ((All  (Fold  `eclass`)  THEN  Auto)\mcdot{}))
                                    THEN  OldAutoSplit
                                    THEN  SqExRepD
                                    THEN  (RWO  "no-classrel-iff-empty<"  (-1)
                                                THEN  Auto
                                                THEN  Try  (((InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-1)\mcdot{}  THENM  D  -1)  THENA  Auto)))\mcdot{})\mcdot{}

---

Home Index