---

Step * 1 1 of Lemma lookup_before_start

.....assertion..... 
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. ps : |oal(a;b)|
⊢ ∀d:ℕ. ∀ps:|oal(a;b)|.  ((||ps|| ≤ d) ⇒ (↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = e ∈ |b|))
BY
{ (Thin (-1)
   THEN (CompleteInductionOnNat THEN Auto)
   THEN (Assert ∀p1:|oal(a;b)|. (||p1|| < ||ps|| ⇒ (↑before(k;map(λz.(fst(z));p1))) ⇒ ((p1[k]) = e ∈ |b|)) BY
               (Auto THEN InstHyp [⌜||p1||⌝;⌜p1⌝] 5⋅ THEN Auto THEN Auto'))
   THEN Thin 5
   THEN ThinVar `d'
   THEN MoveToConcl (-2)) }

1
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. ps : |oal(a;b)|
5. ∀p1:|oal(a;b)|. (||p1|| < ||ps|| ⇒ (↑before(k;map(λz.(fst(z));p1))) ⇒ ((p1[k]) = e ∈ |b|))
⊢ (↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = e ∈ |b|)

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  LOSet
2.  b  :  AbDMon
3.  k  :  |a|
4.  ps  :  |oal(a;b)|
\mvdash{}  \mforall{}d:\mBbbN{}.  \mforall{}ps:|oal(a;b)|.    ((||ps||  \mleq{}  d)  {}\mRightarrow{}  (\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  ((ps[k])  =  e))


By

---

Latex:
(Thin  (-1)
  THEN  (CompleteInductionOnNat  THEN  Auto)
  THEN  (Assert  \mforall{}p1:|oal(a;b)|
                                (||p1||  <  ||ps||  {}\mRightarrow{}  (\muparrow{}before(k;map(\mlambda{}z.(fst(z));p1)))  {}\mRightarrow{}  ((p1[k])  =  e))  BY
                          (Auto  THEN  InstHyp  [\mkleeneopen{}||p1||\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{}]  5\mcdot{}  THEN  Auto  THEN  Auto'))
  THEN  Thin  5
  THEN  ThinVar  `d'
  THEN  MoveToConcl  (-2))

---

Home Index