---

Step * of Lemma lookup_before_start_a

∀a:QOSet. ∀b:AbMon. ∀k:|a|. ∀ps:(|a| × |b|) List.
  ((↑(∀bk'(:|a|) ∈ map(λz.(fst(z));ps). (k' <b k))) ⇒ ((ps[k]) = e ∈ |b|))
BY
{ ((RepD THENM OnVar `ps' ListInd) THENA Auto) }

1
1. a : QOSet
2. b : AbMon
3. k : |a|
⊢ (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));[]). (k' <b k))) ⇒ (([][k]) = e ∈ |b|)

2
1. a : QOSet
2. b : AbMon
3. k : |a|
4. u : |a| × |b|
5. v : (|a| × |b|) List
6. (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k))) ⇒ ((v[k]) = e ∈ |b|)
⊢ (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));[u / v]). (k' <b k))) ⇒ (([u / v][k]) = e ∈ |b|)

---

Latex:

---

Latex:
\mforall{}a:QOSet.  \mforall{}b:AbMon.  \mforall{}k:|a|.  \mforall{}ps:(|a|  \mtimes{}  |b|)  List.
    ((\muparrow{}(\mforall{}\msubb{}k'(:|a|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (k'  <\msubb{}  k)))  {}\mRightarrow{}  ((ps[k])  =  e))


By

---

Latex:
((RepD  THENM  OnVar  `ps'  ListInd)  THENA  Auto)

---

Home Index