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

.....assertion..... 
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')
8. sys-antecedent(es;X)@i
9. (f ∈ fs)@i
10. E(X)@i
11. ¬((f x) x ∈ E(X))@i
⊢ f ∈ sys-antecedent(es;X)
BY
(Lemmaize[-3] THEN InductionOnList) }

1
1. Info Type@i'
2. es EO+(Info)@i'
3. EClass(Top)@i'
⊢ ∀f:sys-antecedent(es;X). ((f ∈ [])  (f ∈ sys-antecedent(es;X)))

2
1. Info Type@i'
2. es EO+(Info)@i'
3. EClass(Top)@i'
4. sys-antecedent(es;X)
5. 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)))


Latex:


.....assertion..... 
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  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}e,e':E.    ((e  <  e')  {}\mRightarrow{}  rank  e  <  rank  e')
8.  f  :  sys-antecedent(es;X)@i
9.  (f  \mmember{}  fs)@i
10.  x  :  E(X)@i
11.  \mneg{}((f  x)  =  x)@i
\mvdash{}  f  \mmember{}  sys-antecedent(es;X)


By

(Lemmaize[-3]  THEN  InductionOnList)




Home Index