---

Step * of Lemma es-cut-at_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[c:Cut(X;f)]. ∀[i:Id].
  (c(i) ∈ {e:E(X)| loc(e) = i ∈ Id}  List)
BY
{ ((Auto THEN Unfold `es-cut-at` 0)
   THEN (InstLemma `es-fset-at_wf` [⌜es⌝;⌜i⌝;⌜c⌝]⋅ THENA (Auto THEN Try ((D (-2) THEN Auto))))
   THEN Assert ⌜c@i ∈ E(X) List⌝⋅) }

1
.....assertion..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. c : Cut(X;f)
6. i : Id
7. c@i ∈ E List
⊢ c@i ∈ E(X) List

2
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. c : Cut(X;f)
6. i : Id
7. c@i ∈ E List
8. c@i ∈ E(X) List
⊢ c@i ∈ {e:E(X)| loc(e) = i ∈ Id}  List

---

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].
    (c(i)  \mmember{}  \{e:E(X)|  loc(e)  =  i\}    List)


By

---

Latex:
((Auto  THEN  Unfold  `es-cut-at`  0)
  THEN  (InstLemma  `es-fset-at\_wf`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  Try  ((D  (-2)  THEN  Auto))))
  THEN  Assert  \mkleeneopen{}c@i  \mmember{}  E(X)  List\mkleeneclose{}\mcdot{})

---

Home Index