---

Step * 3 of Lemma sys-antecedent-filter-image

.....wf..... 
1. Info : Type
2. A : Type
3. B : Type
4. g : A ─→ bag(B)
5. es : EO+(Info)
6. X : EClass(A)
7. f : E(X) ─→ E(X)
8. ∀x:E(X). f x c≤ x
9. ∀a:E(X). ((¬((f a) = a ∈ E(X))) ⇒ (#(g X(a)) = 1 ∈ ℤ) ⇒ (#(g X(f a)) = 1 ∈ ℤ))
10. f1 : E(g[X]) ─→ E(g[X])
⊢ ∀x:E(g[X]). f1 x c≤ x ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  g  :  A  {}\mrightarrow{}  bag(B)
5.  es  :  EO+(Info)
6.  X  :  EClass(A)
7.  f  :  E(X)  {}\mrightarrow{}  E(X)
8.  \mforall{}x:E(X).  f  x  c\mleq{}  x
9.  \mforall{}a:E(X).  ((\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\#(g  X(a))  =  1)  {}\mRightarrow{}  (\#(g  X(f  a))  =  1))
10.  f1  :  E(g[X])  {}\mrightarrow{}  E(g[X])
\mvdash{}  \mforall{}x:E(g[X]).  f1  x  c\mleq{}  x  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index