---

Step * 1 2 of Lemma list-eo-pred


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
BY
{ (BoolCase ⌈n - 1 <z ||L||⌉⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  n  :  \mBbbN{}||L||@i
4.  n  \mneq{}  0
5.  0  <  n@i
\mvdash{}  if  n  -  1  <z  ||L||  then  n  -  1
if  i  =  i  \mwedge{}\msubb{}  (\mneg{}\msubb{}n  -  1  <z  n)  \mwedge{}\msubb{}  (\mneg{}\msubb{}n  <z  n  -  1)  then  n
else  pred(n  -  1)
fi    \msim{}  n  -  1


By

---

Latex:
(BoolCase  \mkleeneopen{}n  -  1  <z  ||L||\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index