---

Step * 1 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 0 <z ||L|| then 0
   if i = i ∧b (¬b0 <z a) ∧b (¬ba <z 0) then a
   else pred(0)
   fi  <z a)
∧b (¬ba <z if 0 <z ||L|| then 0
   if i = i ∧b (¬b0 <z a) ∧b (¬ba <z 0) then a
   else pred(0)
   fi ))
∨b(¬bif 0 <z ||L|| then 0
  if i = i ∧b (¬b0 <z a) ∧b (¬ba <z 0) then a
  else pred(0)
  fi  <z ||L||) ~ tt
BY
{ ((HypSubst' (-1) 0 THEN Reduce 0) THEN Subst' i = i ~ tt 0 THEN Reduce 0 THEN Try (AutoSplit) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((HypSubst'  (-1)  0  THEN  Reduce  0)
  THEN  Subst'  i  =  i  \msim{}  tt  0
  THEN  Reduce  0
  THEN  Try  (AutoSplit)
  THEN  Auto)

---

Home Index