---

Step * of Lemma list_ind_reverse_unfold1

∀[A,B:Type].
  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.
    (list_ind_reverse(L;nilcase;F) ~ if (||L|| =z 0)
    then nilcase
    else F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)
    fi )
BY
{ (Auto
   THEN Unfold `list_ind_reverse` 0
   THEN RW(AddrC[1;1] UnrollRecursionC) 0
   THEN Reduce 0
   THEN Fold `list_ind_reverse` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}nilcase:B.  \mforall{}F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B.  \mforall{}L:A  List.
        (list\_ind\_reverse(L;nilcase;F)  \msim{}  if  (||L||  =\msubz{}  0)
        then  nilcase
        else  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F)  firstn(||L||  -  1;L)  last(L)
        fi  )


By

---

Latex:
(Auto
  THEN  Unfold  `list\_ind\_reverse`  0
  THEN  RW(AddrC[1;1]  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Fold  `list\_ind\_reverse`  0
  THEN  Auto)

---

Home Index