---

Step * 1 of Lemma list_ind_reverse_wf

.....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))
BY
{ ((D 0 THENA Auto) THEN NatInd (-1)) }

1
.....basecase..... 
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|| = 0 ∈ ℕ)
    ⇒ ((λ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
.....upcase..... 
1. A : Type
2. B : Type
3. L : A List
4. nilcase : B
5. F : B ⟶ (A List) ⟶ A ⟶ B
6. n : ℤ
7. 0 < n
8. ∀LL:A List
     ((||LL|| = (n - 1) ∈ ℕ)
     ⇒ ((λ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))
⊢ ∀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))

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  L  :  A  List
4.  nilcase  :  B
5.  F  :  B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B
\mvdash{}  \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

---

Latex:
((D  0  THENA  Auto)  THEN  NatInd  (-1))

---

Home Index