---

Step * of Lemma list_ind_reverse_unfold

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

1
1. A : Type
2. B : Type
3. nilcase : B
4. F : B ⟶ (A List) ⟶ A ⟶ B
5. L : A List
6. ||L|| > 0
⊢ if (||L|| =z 0) then nilcase else F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L) fi  
~ F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}nilcase:B.  \mforall{}F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B.  \mforall{}L:A  List.
        ((||L||  >  0)
        {}\mRightarrow{}  (list\_ind\_reverse(L;nilcase;F)  \msim{}  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F) 
                                                                                firstn(||L||  -  1;L) 
                                                                                last(L)))


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)

---

Home Index