---

Step * 1 1 1 1 2 of Lemma sys-antecedent-closure


1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. u : sys-antecedent(es;X)
5. v : sys-antecedent(es;X) List
6. ∀f:sys-antecedent(es;X). ((f ∈ v) ⇒ (f ∈ sys-antecedent(es;X)))
⊢ ∀f:sys-antecedent(es;X). ((f ∈ [u / v]) ⇒ (f ∈ sys-antecedent(es;X)))
BY
{ Auto }

---

Latex:



1.  Info  :  Type@i'
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  u  :  sys-antecedent(es;X)
5.  v  :  sys-antecedent(es;X)  List
6.  \mforall{}f:sys-antecedent(es;X).  ((f  \mmember{}  v)  {}\mRightarrow{}  (f  \mmember{}  sys-antecedent(es;X)))
\mvdash{}  \mforall{}f:sys-antecedent(es;X).  ((f  \mmember{}  [u  /  v])  {}\mRightarrow{}  (f  \mmember{}  sys-antecedent(es;X)))


By

Auto

---

Home Index