---

Step * 1 1 of Lemma list-eo-pred


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
BY
{ Auto' }

---

Latex:

---

Latex:

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


By

---

Latex:
Auto'

---

Home Index