---

Step * of Lemma es-cut-at-property1

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀c:Cut(X;f). ∀i:Id.
    (no_repeats(E(X);c(i)) ∧ sorted-by(λx,y. x ≤loc y ;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))
⊢ no_repeats(E(X);c(i)) ∧ sorted-by(λx,y. x ≤loc y ;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.
        (no\_repeats(E(X);c(i))  \mwedge{}  sorted-by(\mlambda{}x,y.  x  \mleq{}loc  y  ;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