---

Step * of Lemma es-cut-at-property

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀c:Cut(X;f). ∀i:Id.
    ((∀e:E(X). ((e ∈ c(i)) ⇐⇒ (loc(e) = i ∈ Id) ∧ e ∈ c))
    ∧ (∀e,e':E(X).  (e before e' ∈ c(i) ⇐⇒ (e <loc e') ∧ (e' ∈ c(i)))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert c ∈ fset(E) BY
               (DVar `c' THEN Auto)⋅)
   THEN ((InstLemma `es-fset-at-property` [⌈es⌉;⌈i⌉;⌈c⌉]⋅ THENA Auto)
         THEN Fold `es-cut-at` (-1)
         THEN RepeatFor 2 (D -1))⋅) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. c : Cut(X;f)@i
6. i : Id@i
7. c ∈ fset(E)
8. ∀e:E. (e ∈ c ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ c(i)))
9. no_repeats(E;c(i))
10. sorted-by(λe,e'. e ≤loc e' ;c(i))
⊢ (∀e:E(X). ((e ∈ c(i)) ⇐⇒ (loc(e) = i ∈ Id) ∧ e ∈ c))
∧ (∀e,e':E(X).  (e before e' ∈ c(i) ⇐⇒ (e <loc e') ∧ (e' ∈ c(i))))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}c:Cut(X;f).  \mforall{}i:Id.
        ((\mforall{}e:E(X).  ((e  \mmember{}  c(i))  \mLeftarrow{}{}\mRightarrow{}  (loc(e)  =  i)  \mwedge{}  e  \mmember{}  c))
        \mwedge{}  (\mforall{}e,e':E(X).    (e  before  e'  \mmember{}  c(i)  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')  \mwedge{}  (e'  \mmember{}  c(i)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  c  \mmember{}  fset(E)  BY
                          (DVar  `c'  THEN  Auto)\mcdot{})
  THEN  ((InstLemma  `es-fset-at-property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  Fold  `es-cut-at`  (-1)
              THEN  RepeatFor  2  (D  -1))\mcdot{})

---

Home Index