---

Step * of Lemma member-update-alist1

∀[A,T:Type].
  ∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List. ∀z:A. ∀f:A ⟶ A. ∀y:T.
    ((y ∈ map(λp.(fst(p));update-alist(eq;L;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));L)) ∨ (y = x ∈ T))
BY
{ (InductionOnList
   THEN (Unfold `update-alist` 0 THEN Reduce 0 THEN Try (Fold `update-alist` 0))
   THEN RepUR ``eqof`` 0
   THEN Try (((DVar `u' THEN Reduce 0)
              THEN (SplitOnConclITE THENA Auto)
              THEN Reduce 0
              THEN Auto
              THEN (All (RWO "cons_member") THENA Auto)
              THEN Try ((RWO "8" (-1) THENA Auto))
              THEN Try ((RWO "8" 0 THENA Auto))
              THEN Try ((ProveProp THEN Auto))))) }

1
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
⊢ ∀z:A. ∀f:A ⟶ A. ∀y:T.  ((y ∈ [x]) ⇐⇒ (y ∈ []) ∨ (y = x ∈ T))

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 = u1 ∈ T) ∨ (y ∈ map(λp.(fst(p));v))) ∨ (y = x ∈ T)
⊢ (y = x ∈ T) ∨ (y ∈ map(λp.(fst(p));v))

---

Latex:

---

Latex:
\mforall{}[A,T:Type].
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:(T  \mtimes{}  A)  List.  \mforall{}z:A.  \mforall{}f:A  {}\mrightarrow{}  A.  \mforall{}y:T.
        ((y  \mmember{}  map(\mlambda{}p.(fst(p));update-alist(eq;L;x;z;v.f[v])))  \mLeftarrow{}{}\mRightarrow{}  (y  \mmember{}  map(\mlambda{}p.(fst(p));L))  \mvee{}  (y  =  x))


By

---

Latex:
(InductionOnList
  THEN  (Unfold  `update-alist`  0  THEN  Reduce  0  THEN  Try  (Fold  `update-alist`  0))
  THEN  RepUR  ``eqof``  0
  THEN  Try  (((DVar  `u'  THEN  Reduce  0)
                        THEN  (SplitOnConclITE  THENA  Auto)
                        THEN  Reduce  0
                        THEN  Auto
                        THEN  (All  (RWO  "cons\_member")  THENA  Auto)
                        THEN  Try  ((RWO  "8"  (-1)  THENA  Auto))
                        THEN  Try  ((RWO  "8"  0  THENA  Auto))
                        THEN  Try  ((ProveProp  THEN  Auto)))))

---

Home Index