---

Step * of Lemma sys-antecedent-closure

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀fs:sys-antecedent(es;X) List. ∀s:fset(E(X)).  ∃c:fset(E(X)). (c = fs closure of s)
BY
{ ((Auto THEN ((InstLemma `es-causl-swellfnd` [⌜es⌝]⋅ THENM D -1 THENM RenameVar `rank' (-2)) THENA Auto))
   THEN InstLemma `fset-closure-exists` [⌜E(X)⌝;⌜es-eq(es)⌝;⌜rank⌝;⌜fs⌝;⌜s⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. fs : sys-antecedent(es;X) List@i
5. s : fset(E(X))@i
6. rank : E ⟶ ℕ
7. ∀e,e':E.  ((e < e') ⇒ rank e < rank e')
⊢ (∀f∈fs.∀x:E(X). ((¬((f x) = x ∈ E(X))) ⇒ rank (f x) < rank x))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}fs:sys-antecedent(es;X)  List.  \mforall{}s:fset(E(X)).
        \mexists{}c:fset(E(X)).  (c  =  fs  closure  of  s)


By

---

Latex:
((Auto
    THEN  ((InstLemma  `es-causl-swellfnd`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENM  D  -1  THENM  RenameVar  `rank'  (-2))  THENA  Auto)
    )
  THEN  InstLemma  `fset-closure-exists`  [\mkleeneopen{}E(X)\mkleeneclose{};\mkleeneopen{}es-eq(es)\mkleeneclose{};\mkleeneopen{}rank\mkleeneclose{};\mkleeneopen{}fs\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index