---

Step * of Lemma global-eo_wf

∀[Info:Type]. ∀L:(Id × Info) List. (global-eo(L) ∈ EO+(Info))
BY
{ (Auto
   THEN Unfold `global-eo` 0
   THEN MemCD
   THEN Reduce 0
   THEN SplitAndConcl
   THEN Try (WithRuleCount 80000 ((Auto
                                   THEN Try ((RW assert_pushdownC (-1) THEN Auto))
                                   THEN All (RWO "not_squash")⋅
                                   THEN Auto'))⋅)
   THEN RenameVar `n' 3
   THEN (GenConclTerm ⌜fst(L[n])⌝⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜v⌝ 0⋅ THENA Auto)
   THEN (InstLemma `last_index_property` [⌜Id × Info⌝;⌜λ2p.fst(p) = v⌝;⌜firstn(n;L)⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜last_index(firstn(n;L);x.fst(x) = v)⌝⋅ THENA Auto)
   THEN RWO "length_firstn" (-2)
   THEN Auto
   THEN CallByValueReduce 0
   THEN Auto
   THEN AutoSplit) }

1
1. Info : Type
2. L : (Id × Info) List@i
3. n : ℕ||L||@i
4. v : Id@i
5. (fst(L[n])) = v ∈ Id@i
6. v1 : ℕn + 1@i
7. v1 ≠ 0
8. last_index(firstn(n;L);x.fst(x) = v) = v1 ∈ ℕ||firstn(n;L)|| + 1@i
9. (↑fst(firstn(n;L)[v1 - 1]) = v) ∧ (¬(∃x∈nth_tl(v1;firstn(n;L)). ↑fst(x) = v)) supposing 0 < v1@i
10. ¬(∃x∈firstn(n;L). ↑fst(x) = v) supposing v1 = 0 ∈ ℤ@i
⊢ (fst(L[v1 - 1])) = v ∈ Id

2
1. Info : Type
2. L : (Id × Info) List@i
3. n : ℕ||L||@i
4. x : ℕ||L||@i
5. x < n@i
6. (fst(L[x])) = (fst(L[n])) ∈ Id@i
7. v : Id@i
8. (fst(L[n])) = v ∈ Id@i
9. v1 : ℕn + 1@i
10. last_index(firstn(n;L);x.fst(x) = v) = v1 ∈ ℕ||firstn(n;L)|| + 1@i
11. (↑fst(firstn(n;L)[v1 - 1]) = v) ∧ (¬(∃x∈nth_tl(v1;firstn(n;L)). ↑fst(x) = v)) supposing 0 < v1@i
12. ¬(∃x∈firstn(n;L). ↑fst(x) = v) supposing v1 = 0 ∈ ℤ@i
13. v1 = 0 ∈ ℤ
⊢ ↓n < n

3
1. Info : Type
2. L : (Id × Info) List@i
3. n : ℕ||L||@i
4. x : ℕ||L||@i
5. x < n@i
6. (fst(L[x])) = (fst(L[n])) ∈ Id@i
7. eval i = fst(L[n]) in
   eval z = last_index(firstn(n;L);p.fst(p) = i) in
     if (z =z 0) then n else z - 1 fi  < n
8. v : Id@i
9. (fst(L[n])) = v ∈ Id@i
10. v1 : ℕn + 1@i
11. v1 ≠ 0
12. last_index(firstn(n;L);x.fst(x) = v) = v1 ∈ ℕ||firstn(n;L)|| + 1@i
13. (↑fst(firstn(n;L)[v1 - 1]) = v) ∧ (¬(∃x∈nth_tl(v1;firstn(n;L)). ↑fst(x) = v)) supposing 0 < v1@i
14. ¬(∃x∈firstn(n;L). ↑fst(x) = v) supposing v1 = 0 ∈ ℤ@i
⊢ ¬v1 - 1 < x

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}L:(Id  \mtimes{}  Info)  List.  (global-eo(L)  \mmember{}  EO+(Info))


By

---

Latex:
(Auto
  THEN  Unfold  `global-eo`  0
  THEN  MemCD
  THEN  Reduce  0
  THEN  SplitAndConcl
  THEN  Try  (WithRuleCount  80000  ((Auto
                                                                  THEN  Try  ((RW  assert\_pushdownC  (-1)  THEN  Auto))
                                                                  THEN  All  (RWO  "not\_squash")\mcdot{}
                                                                  THEN  Auto'))\mcdot{})
  THEN  RenameVar  `n'  3
  THEN  (GenConclTerm  \mkleeneopen{}fst(L[n])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `last\_index\_property`  [\mkleeneopen{}Id  \mtimes{}  Info\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.fst(p)  =  v\mkleeneclose{};\mkleeneopen{}firstn(n;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}last\_index(firstn(n;L);x.fst(x)  =  v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RWO  "length\_firstn"  (-2)
  THEN  Auto
  THEN  CallByValueReduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index