---

Step * of Lemma list-eo-first

∀L:Top List. ∀i:Id. ∀a:ℕ||L||.  (first(a) ~ (a =z 0))
BY
{ (Intros⋅
   THEN RepUR ``es-first es-dom`` 0
   THEN RecUnfold `es-pred` 0
   THEN RepUR ``let list-eo mk-extended-eo mk-eo mk-eo-record es-dom`` 0
   THEN RepUR ``es-base-pred es-eq es-locless es-loc es-eq-E`` 0
   THEN (BoolCase ⌜(a =z 0)⌝⋅ THENA Auto)) }

1
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

2
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

---

Latex:

---

Latex:
\mforall{}L:Top  List.  \mforall{}i:Id.  \mforall{}a:\mBbbN{}||L||.    (first(a)  \msim{}  (a  =\msubz{}  0))


By

---

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

---

Home Index