Step
*
2
1
1
of Lemma
first-eclass-val
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E. (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. ↑e ∈b first-eclass([u / v])
9. (↑e ∈b u) ∨ (∃X∈v. ↑e ∈b X)
10. ↑e ∈b u
11. ↑e ∈b u
⊢ first-eclass([u / v])(e) = u(e) ∈ A
BY
{ (MoveToConcl (-1)
THEN RepUR ``first-eclass in-eclass can-apply eclass-val do-apply`` 0
THEN All (Unfold `eclass`)
THEN All Thin
THEN ListInd (-3)
THEN Reduce 0) }
1
1. Info : Type
2. A : Type
3. u : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
4. es : EO+(Info)@i'
5. e : E@i
⊢ (↑(#(u es e) =z 1))
⇒ (only(u es e) = only(u es e) ∈ A)
2
1. Info : Type
2. A : Type
3. u : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. u1 : es:EO+(Info) ─→ e:E ─→ bag(A)
7. v : (es:EO+(Info) ─→ e:E ─→ bag(A)) List
8. (↑(#(u es e) =z 1))
⇒ (only(accumulate (with value b and list item X):
if (#(b) =z 1) then b else X es e fi
over list:
v
with starting value:
u es e))
= only(u es e)
∈ A)
⊢ (↑(#(u es e) =z 1))
⇒ (only(accumulate (with value b and list item X):
if (#(b) =z 1) then b else X es e fi
over list:
v
with starting value:
if (#(u es e) =z 1) then u es e else u1 es e fi ))
= only(u es e)
∈ A)
Latex:
Latex:
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. \mforall{}es:EO+(Info). \mforall{}e:E.
(\mexists{}X\mmember{}v. (\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (first-eclass(v)(e) = X(e))) supposing \muparrow{}e \mmember{}\msubb{} first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. \muparrow{}e \mmember{}\msubb{} first-eclass([u / v])
9. (\muparrow{}e \mmember{}\msubb{} u) \mvee{} (\mexists{}X\mmember{}v. \muparrow{}e \mmember{}\msubb{} X)
10. \muparrow{}e \mmember{}\msubb{} u
11. \muparrow{}e \mmember{}\msubb{} u
\mvdash{} first-eclass([u / v])(e) = u(e)
By
Latex:
(MoveToConcl (-1)
THEN RepUR ``first-eclass in-eclass can-apply eclass-val do-apply`` 0
THEN All (Unfold `eclass`)
THEN All Thin
THEN ListInd (-3)
THEN Reduce 0)
Home
Index