---

Step * of Lemma apply-updated-alist

∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
  (apply-alist(eq;update-alist(eq;L;x;z;v.f[v]);y)
  = case apply-alist(eq;L;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:InductionOnList }

1
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?))

2
1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. x : T
5. y : T
6. u : T × A@i
7. v : (T × A) List@i
8. ∀[z:A]. ∀[f:A ⟶ A].
     (apply-alist(eq;update-alist(eq;v;x;z;v.f[v]);y)
     = case apply-alist(eq;v;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?))
⊢ ∀[z:A]. ∀[f:A ⟶ A].
    (apply-alist(eq;update-alist(eq;[u / v];x;z;v.f[v]);y)
    = case apply-alist(eq;[u / v];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?))

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].  \mforall{}[L:(T  \mtimes{}  A)  List].  \mforall{}[z:A].  \mforall{}[f:A  {}\mrightarrow{}  A].
    (apply-alist(eq;update-alist(eq;L;x;z;v.f[v]);y)
    =  case  apply-alist(eq;L;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:InductionOnList

---

Home Index