---

Step * 2 of Lemma list-eo-first


1. L : Top List@i
2. i : Id@i
3. a : ℕ||L||@i
4. a ≠ 0
⊢ (i = i
∧b (¬bif a - 1 <z ||L|| then a - 1
   if i = i ∧b (¬ba - 1 <z a) ∧b (¬ba <z a - 1) then a
   else pred(a - 1)
   fi  <z a)
∧b (¬ba <z if a - 1 <z ||L|| then a - 1
   if i = i ∧b (¬ba - 1 <z a) ∧b (¬ba <z a - 1) then a
   else pred(a - 1)
   fi ))
∨b(¬bif a - 1 <z ||L|| then a - 1
  if i = i ∧b (¬ba - 1 <z a) ∧b (¬ba <z a - 1) then a
  else pred(a - 1)
  fi  <z ||L||) ~ ff
BY
{ ((BoolCase ⌈a - 1 <z ||L||⌉⋅ THENA Auto) THEN Auto') }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index