---

Step * of Lemma list_ind_reverse_wf

∀[A,B:Type]. ∀[L:A List]. ∀[nilcase:B]. ∀[F:B ⟶ (A List) ⟶ A ⟶ B].  (list_ind_reverse(L;nilcase;F) ∈ B)
BY
{ (ProveWfLemma
   THEN RW (AddrC [2] UnrollRecursionC) 0
   THEN (Assert ∀n:ℕ. ∀LL:A List.
                  ((||LL|| = n ∈ ℕ)
                  ⇒ ((λF@0,l. if (||l|| =z 0)
                              then nilcase
                              else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l)
                              fi ) 
                      fix((λF@0,l. if (||l|| =z 0)
                                  then nilcase
                                  else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l)
                                  fi )) 
                      LL ∈ B)) BY
               skip{Auto})
   THEN skip{Auto}) }

1
.....assertion..... 
1. A : Type
2. B : Type
3. L : A List
4. nilcase : B
5. F : B ⟶ (A List) ⟶ A ⟶ B
⊢ ∀n:ℕ. ∀LL:A List.
    ((||LL|| = n ∈ ℕ)
    ⇒ ((λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi ) 
        fix((λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi )) 
        LL ∈ B))

2
1. A : Type
2. B : Type
3. L : A List
4. nilcase : B
5. F : B ⟶ (A List) ⟶ A ⟶ B
6. ∀n:ℕ. ∀LL:A List.
     ((||LL|| = n ∈ ℕ)
     ⇒ ((λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi ) 
         fix((λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi )) 
         LL ∈ B))
⊢ (λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi ) 
  fix((λF@0,l. if (||l|| =z 0) then nilcase else F (F@0 firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi )) 
  L ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[nilcase:B].  \mforall{}[F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (list\_ind\_reverse(L;nilcase;F)  \mmember{}  B)


By

---

Latex:
(ProveWfLemma
  THEN  RW  (AddrC  [2]  UnrollRecursionC)  0
  THEN  (Assert  \mforall{}n:\mBbbN{}.  \mforall{}LL:A  List.
                                ((||LL||  =  n)
                                {}\mRightarrow{}  ((\mlambda{}F@0,l.  if  (||l||  =\msubz{}  0)
                                                        then  nilcase
                                                        else  F  (F@0  firstn(||l||  -  1;l))  firstn(||l||  -  1;l)  last(l)
                                                        fi  ) 
                                        fix((\mlambda{}F@0,l.  if  (||l||  =\msubz{}  0)
                                                                then  nilcase
                                                                else  F  (F@0  firstn(||l||  -  1;l))  firstn(||l||  -  1;l)  last(l)
                                                                fi  )) 
                                        LL  \mmember{}  B))  BY
                          skip\{Auto\})
  THEN  skip\{Auto\})

---

Home Index