---

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


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 ∈ ℤ))
⊢ f ∈ E(g[X]) ─→ E(g[X])
BY
{ (ExtWith [`a'] [⌈E(X) ─→ E(X)⌉]⋅ THEN Auto)⋅ }

1
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. a : E(g[X])
⊢ f a ∈ E(g[X])

---

Latex:

---

Latex:

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))
\mvdash{}  f  \mmember{}  E(g[X])  {}\mrightarrow{}  E(g[X])


By

---

Latex:
(ExtWith  [`a']  [\mkleeneopen{}E(X)  {}\mrightarrow{}  E(X)\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index