---

Step * 1 of Lemma list-eo-pred


1. L : Top List@i
2. i : Id@i
3. n : ℕ||L||@i
4. 0 < n@i
⊢ let p = pred1(n) in
      if es-dom(list-eo(L;i)) p then p
      if es-eq(list-eo(L;i)) p n then n
      else pred(p)
      fi  ~ n - 1
BY
{ (RepUR ``es-base-pred list-eo mk-extended-eo mk-eo mk-eo-record`` 0
   THEN RepUR ``es-dom es-eq es-locless es-loc`` 0
   THEN (BoolCase ⌈(n =z 0)⌉⋅ THENA Auto)
   THEN RepUR ``let`` 0) }

1
1. L : Top List@i
2. i : Id@i
3. n : ℕ||L||@i
4. 0 < n@i
5. n = 0 ∈ ℤ
⊢ if 0 <z ||L|| then 0
if i = i ∧b (¬b0 <z n) ∧b (¬bn <z 0) then n
else pred(0)
fi  ~ n - 1

2
1. L : Top List@i
2. i : Id@i
3. n : ℕ||L||@i
4. n ≠ 0
5. 0 < n@i
⊢ if n - 1 <z ||L|| then n - 1
if i = i ∧b (¬bn - 1 <z n) ∧b (¬bn <z n - 1) then n
else pred(n - 1)
fi  ~ n - 1

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  n  :  \mBbbN{}||L||@i
4.  0  <  n@i
\mvdash{}  let  p  =  pred1(n)  in
            if  es-dom(list-eo(L;i))  p  then  p
            if  es-eq(list-eo(L;i))  p  n  then  n
            else  pred(p)
            fi    \msim{}  n  -  1


By

---

Latex:
(RepUR  ``es-base-pred  list-eo  mk-extended-eo  mk-eo  mk-eo-record``  0
  THEN  RepUR  ``es-dom  es-eq  es-locless  es-loc``  0
  THEN  (BoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``let``  0)

---

Home Index