---

Step * 2 of Lemma last-insert


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[x:T]. (last(insert(x;v)) = if null(v) then x else last(v) fi  ∈ T)
⊢ ∀[x:T]. (last(insert(x;[u / v])) = last([u / v]) ∈ T)
BY
{ (Unfold `insert` 0 THEN (RWO "eval_list_sq" 0 THENA Auto) THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[x:T]. (last(insert(x;v)) = if null(v) then x else last(v) fi  ∈ T)
6. x : T
⊢ last(if x ∈b <u, v> then <u, v> else [x / <u, v>] fi ) = last([u / v]) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[x:T].  (last(insert(x;v))  =  if  null(v)  then  x  else  last(v)  fi  )
\mvdash{}  \mforall{}[x:T].  (last(insert(x;[u  /  v]))  =  last([u  /  v]))


By

---

Latex:
(Unfold  `insert`  0  THEN  (RWO  "eval\_list\_sq"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index