Step
*
of Lemma
lookup_before_start
∀a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|. ((↑before(k;map(λz.(fst(z));ps)))
⇒ ((ps[k]) = e ∈ |b|))
BY
{ ((RepeatMFor 4 (D 0)) THENA Auto) }
1
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. ps : |oal(a;b)|
⊢ (↑before(k;map(λz.(fst(z));ps)))
⇒ ((ps[k]) = e ∈ |b|)
Latex:
Latex:
\mforall{}a:LOSet. \mforall{}b:AbDMon. \mforall{}k:|a|. \mforall{}ps:|oal(a;b)|. ((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps))) {}\mRightarrow{} ((ps[k]) = e))
By
Latex:
((RepeatMFor 4 (D 0)) THENA Auto)
Home
Index