---

Step * 1 1 1 1 1 1 1 of Lemma global-eo-first


1. L : (Id × Top) List
2. e : ℕ||L||
3. e ∈ E
4. pred(e) ∈ E
⊢ (pred(e) =z e) ∨bff = (∀x∈upto(e).¬bfst(L[x]) = fst(L[e]))_b
BY
{ (Unfold `es-pred` 0
   THEN Fold `es-eq-E` 0
   THEN (RWO "global-eo-dom" 0 THENA Auto)
   THEN Reduce 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN RepUR ``let es-base-pred global-eo mk-extended-eo mk-eo mk-eo-record`` 0
   THEN (GenConclTerm ⌜fst(L[e])⌝⋅ THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (InstLemma `last_index_property` [⌜Id × Top⌝;⌜λ2p.fst(p) = v⌝;⌜firstn(e;L)⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜last_index(firstn(e;L);x.fst(x) = v)⌝⋅ THENA Auto)
   THEN RWO "length_firstn" (-2)
   THEN Auto) }

1
1. L : (Id × Top) List
2. e : ℕ||L||
3. e ∈ E
4. pred(e) ∈ E
5. v : Id@i
6. (fst(L[e])) = v ∈ Id@i
7. v1 : ℕe + 1@i
8. last_index(firstn(e;L);x.fst(x) = v) = v1 ∈ ℕ||firstn(e;L)|| + 1@i
9. (↑fst(firstn(e;L)[v1 - 1]) = v) ∧ (¬(∃x∈nth_tl(v1;firstn(e;L)). ↑fst(x) = v)) supposing 0 < v1@i
10. ¬(∃x∈firstn(e;L). ↑fst(x) = v) supposing v1 = 0 ∈ ℤ@i
⊢ (if (v1 =z 0) then e else v1 - 1 fi  =z e) ∨bff = (∀x∈upto(e).¬bfst(L[x]) = v)_b

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  e  :  \mBbbN{}||L||
3.  e  \mmember{}  E
4.  pred(e)  \mmember{}  E
\mvdash{}  (pred(e)  =\msubz{}  e)  \mvee{}\msubb{}ff  =  (\mforall{}x\mmember{}upto(e).\mneg{}\msubb{}fst(L[x])  =  fst(L[e]))\_b


By

---

Latex:
(Unfold  `es-pred`  0
  THEN  Fold  `es-eq-E`  0
  THEN  (RWO  "global-eo-dom"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  RepUR  ``let  es-base-pred  global-eo  mk-extended-eo  mk-eo  mk-eo-record``  0
  THEN  (GenConclTerm  \mkleeneopen{}fst(L[e])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (InstLemma  `last\_index\_property`  [\mkleeneopen{}Id  \mtimes{}  Top\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.fst(p)  =  v\mkleeneclose{};\mkleeneopen{}firstn(e;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}last\_index(firstn(e;L);x.fst(x)  =  v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RWO  "length\_firstn"  (-2)
  THEN  Auto)

---

Home Index