---

Step * 2 of Lemma apply-updated-alist


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?))
BY
{ (RepeatFor 2 (ParallelLast)
   THEN DVar `u'
   THEN (Unfold `update-alist` 0 THEN Reduce 0 THEN Fold `update-alist` 0)
   THEN Unfold `eqof` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN (Unfold `apply-alist` 0 THEN Reduce 0 THEN Fold `apply-alist` 0)
   THEN RepeatFor 2 ((SplitOnConclITE THEN Auto))
   THEN Reduce 0
   THEN Auto
   THEN Try (OnMaybeHyp 15 (\h. (D h THEN Complete (Auto))))
   THEN (SplitOnHypITE -4  THEN Auto)⋅
   THEN (GenConclAtAddr [2] THEN D -2 THEN Reduce 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  eq  :  EqDecider(T)
4.  x  :  T
5.  y  :  T
6.  u  :  T  \mtimes{}  A@i
7.  v  :  (T  \mtimes{}  A)  List@i
8.  \mforall{}[z:A].  \mforall{}[f:A  {}\mrightarrow{}  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  \mcdot{}    fi  )
\mvdash{}  \mforall{}[z:A].  \mforall{}[f:A  {}\mrightarrow{}  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  \mcdot{}    fi  )


By

---

Latex:
(RepeatFor  2  (ParallelLast)
  THEN  DVar  `u'
  THEN  (Unfold  `update-alist`  0  THEN  Reduce  0  THEN  Fold  `update-alist`  0)
  THEN  Unfold  `eqof`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  (Unfold  `apply-alist`  0  THEN  Reduce  0  THEN  Fold  `apply-alist`  0)
  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto))
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (OnMaybeHyp  15  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))
  THEN  (SplitOnHypITE  -4    THEN  Auto)\mcdot{}
  THEN  (GenConclAtAddr  [2]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index