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 -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. EClass(Top)@i'
4. fs sys-antecedent(es;X) List@i
5. 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