---

Step * 1 2 1 of Lemma list_ind_reverse_wf


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))
9. LL : A List
10. ||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
{ (Reduce 0 THEN AutoSplit) }

1
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))
9. LL : A List
10. ||LL|| ≠ 0
11. ||LL|| = n ∈ ℕ
⊢ F 
  (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 )) 
   firstn(||LL|| - 1;LL)) 
  firstn(||LL|| - 1;LL) 
  last(LL) ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  L  :  A  List
4.  nilcase  :  B
5.  F  :  B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B
6.  n  :  \mBbbZ{}
7.  0  <  n
8.  \mforall{}LL:A  List
          ((||LL||  =  (n  -  1))
          {}\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))
9.  LL  :  A  List
10.  ||LL||  =  n
\mvdash{}  (\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:
(Reduce  0  THEN  AutoSplit)

---

Home Index