---

Step * 1 of Lemma sys-antecedent-closure

.....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))
BY
{ (BLemma `l_all_iff` THEN Auto) }

1
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')
8. f : sys-antecedent(es;X)@i
9. (f ∈ fs)@i
10. x@0 : E(X)@i
11. ¬((f x@0) = x@0 ∈ E(X))@i
⊢ rank (f x@0) < rank x@0

---

Latex:


.....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  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}e,e':E.    ((e  <  e')  {}\mRightarrow{}  rank  e  <  rank  e')
\mvdash{}  (\mforall{}f\mmember{}fs.\mforall{}x:E(X).  ((\mneg{}((f  x)  =  x))  {}\mRightarrow{}  rank  (f  x)  <  rank  x))


By

(BLemma  `l\_all\_iff`  THEN  Auto)

---

Home Index