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