---

Step * 1 of Lemma apply-updated-alist


1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. x : T
5. y : T
⊢ ∀[z:A]. ∀[f:A ⟶ A].
    (apply-alist(eq;update-alist(eq;[];x;z;v.f[v]);y)
    = case apply-alist(eq;[];y)
       of inl(v) =>
       inl if eq x y then f[v] else v fi 
       | inr(any) =>
       if eq x y then inl z else inr ⋅  fi 
    ∈ (A?))
BY
{ TACTIC:(Auto THEN RepUR ``update-alist apply-alist eqof`` 0 THEN (SplitOnConclITE THEN Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  eq  :  EqDecider(T)
4.  x  :  T
5.  y  :  T
\mvdash{}  \mforall{}[z:A].  \mforall{}[f:A  {}\mrightarrow{}  A].
        (apply-alist(eq;update-alist(eq;[];x;z;v.f[v]);y)
        =  case  apply-alist(eq;[];y)
              of  inl(v)  =>
              inl  if  eq  x  y  then  f[v]  else  v  fi 
              |  inr(any)  =>
              if  eq  x  y  then  inl  z  else  inr  \mcdot{}    fi  )


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``update-alist  apply-alist  eqof``  0
                THEN  (SplitOnConclITE  THEN  Auto)
                THEN  Auto)

---

Home Index