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:
\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
((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