---

Step * of Lemma ranked-eo_wf

∀[Info:Type]. ∀[L:Id ─→ (Info List)]. ∀[rk:(i:Id × ℕ||L i||) ─→ ℕ].
  ranked-eo(L;rk) ∈ EO+(Info) supposing ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
BY
{ (Auto
   THEN Unfold `ranked-eo` 0
   THEN MemCD
   THEN Reduce 0
   THEN SplitAndConcl
   THEN Try (WithRuleCount 20000 ((Auto
                                   THEN Try ((RW assert_pushdownC (-1) THEN Auto))
                                   THEN All (RWO "not_squash")⋅
                                   THEN Auto'))⋅)
   THEN Try ((DProdsAndUnions THEN All Reduce))) }

1
1. Info : Type
2. L : Id ─→ (Info List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
5. i : Id@i
6. e1 : ℕ||L i||@i
⊢ ¬rk <i, e1> < rk if e1=0  then <i, e1>  else <i, e1 - 1>

2
1. Info : Type
2. L : Id ─→ (Info List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
⊢ ∀e,x:i:Id × ℕ||L i||.
    ((↓rk x < rk e)
    ⇒ ((fst(x)) = (fst(e)) ∈ Id)
    ⇒ ((↓rk if snd(e)=0  then e  else <fst(e), (snd(e)) - 1> < rk e)
       ∧ (¬↓rk if snd(e)=0  then e  else <fst(e), (snd(e)) - 1> < rk x)))

3
1. Info : Type
2. L : Id ─→ (Info List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
5. i1 : Id@i
6. e4 : ℕ||L i1||@i
7. i : Id@i
8. e3 : ℕ||L i||@i
9. i1 = i ∈ Id
10. rk <i1, e4> < rk <i, e3>@i
⊢ e4 < e3

4
1. Info : Type
2. L : Id ─→ (Info List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
5. i1 : Id@i
6. e4 : ℕ||L i1||@i
7. i : Id@i
8. e3 : ℕ||L i||@i
9. i1 = i ∈ Id
10. e4 < e3
⊢ ↓rk <i1, e4> < rk <i, e3>

5
1. Info : Type
2. L : Id ─→ (Info List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
5. i1 : Id@i
6. e4 : ℕ||L i1||@i
7. i : Id@i
8. e3 : ℕ||L i||@i
9. i1 = i ∈ Id
10. (↓rk <i1, e4> < rk <i, e3>) ⇒ (↑e4 <z e3)
11. (↓rk <i1, e4> < rk <i, e3>) ⇐ ↑e4 <z e3
12. ¬rk <i1, e4> < rk <i, e3>
13. ¬rk <i, e3> < rk <i1, e4>
⊢ <i1, e4> = <i, e3> ∈ (i:Id × ℕ||L i||)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[L:Id  {}\mrightarrow{}  (Info  List)].  \mforall{}[rk:(i:Id  \mtimes{}  \mBbbN{}||L  i||)  {}\mrightarrow{}  \mBbbN{}].
    ranked-eo(L;rk)  \mmember{}  EO+(Info)  supposing  \mforall{}i:Id.  \mforall{}j:\mBbbN{}||L  i||.  \mforall{}k:\mBbbN{}j.    rk  <i,  k>  <  rk  <i,  j>


By

---

Latex:
(Auto
  THEN  Unfold  `ranked-eo`  0
  THEN  MemCD
  THEN  Reduce  0
  THEN  SplitAndConcl
  THEN  Try  (WithRuleCount  20000  ((Auto
                                                                  THEN  Try  ((RW  assert\_pushdownC  (-1)  THEN  Auto))
                                                                  THEN  All  (RWO  "not\_squash")\mcdot{}
                                                                  THEN  Auto'))\mcdot{})
  THEN  Try  ((DProdsAndUnions  THEN  All  Reduce)))

---

Home Index