Step
*
of Lemma
es-cut-exists
∀[Info:Type]
∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀s:fset(E(X)).
∃c:Cut(X;f). (s ⊆ c ∧ (∀[c':Cut(X;f)]. c ⊆ c' supposing s ⊆ c'))
BY
{ (Auto
THEN InstLemma `sys-antecedent-closure` [Info; ⌈es⌉;⌈X⌉;⌈[f; X-pred]⌉;⌈s⌉]⋅
THEN Auto
THEN ParallelLast
THEN Auto) }
1
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. s : fset(E(X))@i
6. c : fset(E(X))
7. (c = [f; X-pred] closure of s)
8. s ⊆ c
9. c' : Cut(X;f)
10. s ⊆ c'
⊢ c ⊆ c'
Latex:
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:sys-antecedent(es;X). \mforall{}s:fset(E(X)).
\mexists{}c:Cut(X;f). (s \msubseteq{} c \mwedge{} (\mforall{}[c':Cut(X;f)]. c \msubseteq{} c' supposing s \msubseteq{} c'))
By
Latex:
(Auto
THEN InstLemma `sys-antecedent-closure` [Info; \mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}[f; X-pred]\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
THEN Auto
THEN ParallelLast
THEN Auto)
Home
Index