Step * 3 2 of Lemma split_tail_lemma


1. Type
2. A ⟶ 𝔹
3. A
4. ¬↑f[u]
5. List
6. p1 List
7. p2 List
⊢ ((¬↑null(p1))  (¬↑f[last(p1)]))
 (¬↑null(fst(case p1 of [] => <[u], p2> x::y => <[u p1], p2> esac)))
 (¬↑f[last(fst(case p1 of [] => <[u], p2> x::y => <[u p1], p2> esac))])
BY
(ListInd (-2) THEN Reduce THEN Auto)⋅ }


Latex:


Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  \mneg{}\muparrow{}f[u]
5.  v  :  A  List
6.  p1  :  A  List
7.  p2  :  A  List
\mvdash{}  ((\mneg{}\muparrow{}null(p1))  {}\mRightarrow{}  (\mneg{}\muparrow{}f[last(p1)]))
{}\mRightarrow{}  (\mneg{}\muparrow{}null(fst(case  p1  of  []  =>  <[u],  p2>  |  x::y  =>  <[u  /  p1],  p2>  esac)))
{}\mRightarrow{}  (\mneg{}\muparrow{}f[last(fst(case  p1  of  []  =>  <[u],  p2>  |  x::y  =>  <[u  /  p1],  p2>  esac))])


By


Latex:
(ListInd  (-2)  THEN  Reduce  0  THEN  Auto)\mcdot{}




Home Index