---

Step * 2 of Lemma member-update-alist1


1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. u1 : T
6. u2 : A
7. v : (T × A) List
8. ∀z:A. ∀f:A ⟶ A. ∀y:T.
     ((y ∈ map(λp.(fst(p));update-alist(eq;v;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));v)) ∨ (y = x ∈ T))
9. u1 = x ∈ T
10. z : A
11. f : A ⟶ A
12. y : T
13. ((y = u1 ∈ T) ∨ (y ∈ map(λp.(fst(p));v))) ∨ (y = x ∈ T)
⊢ (y = x ∈ T) ∨ (y ∈ map(λp.(fst(p));v))
BY
{ SplitOrHyps }

1
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. u1 : T
6. u2 : A
7. v : (T × A) List
8. ∀z:A. ∀f:A ⟶ A. ∀y:T.
     ((y ∈ map(λp.(fst(p));update-alist(eq;v;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));v)) ∨ (y = x ∈ T))
9. u1 = x ∈ T
10. z : A
11. f : A ⟶ A
12. y : T
13. y = u1 ∈ T
⊢ (y = x ∈ T) ∨ (y ∈ map(λp.(fst(p));v))

2
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. u1 : T
6. u2 : A
7. v : (T × A) List
8. ∀z:A. ∀f:A ⟶ A. ∀y:T.
     ((y ∈ map(λp.(fst(p));update-alist(eq;v;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));v)) ∨ (y = x ∈ T))
9. u1 = x ∈ T
10. z : A
11. f : A ⟶ A
12. y : T
13. (y ∈ map(λp.(fst(p));v))
⊢ (y = x ∈ T) ∨ (y ∈ map(λp.(fst(p));v))

3
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. u1 : T
6. u2 : A
7. v : (T × A) List
8. ∀z:A. ∀f:A ⟶ A. ∀y:T.
     ((y ∈ map(λp.(fst(p));update-alist(eq;v;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));v)) ∨ (y = x ∈ T))
9. u1 = x ∈ T
10. z : A
11. f : A ⟶ A
12. y : T
13. y = x ∈ T
⊢ (y = x ∈ T) ∨ (y ∈ map(λp.(fst(p));v))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [T]  :  Type
3.  eq  :  EqDecider(T)
4.  x  :  T
5.  u1  :  T
6.  u2  :  A
7.  v  :  (T  \mtimes{}  A)  List
8.  \mforall{}z:A.  \mforall{}f:A  {}\mrightarrow{}  A.  \mforall{}y:T.
          ((y  \mmember{}  map(\mlambda{}p.(fst(p));update-alist(eq;v;x;z;v.f[v])))  \mLeftarrow{}{}\mRightarrow{}  (y  \mmember{}  map(\mlambda{}p.(fst(p));v))  \mvee{}  (y  =  x))
9.  u1  =  x
10.  z  :  A
11.  f  :  A  {}\mrightarrow{}  A
12.  y  :  T
13.  ((y  =  u1)  \mvee{}  (y  \mmember{}  map(\mlambda{}p.(fst(p));v)))  \mvee{}  (y  =  x)
\mvdash{}  (y  =  x)  \mvee{}  (y  \mmember{}  map(\mlambda{}p.(fst(p));v))


By

---

Latex:
SplitOrHyps

---

Home Index