Step * 2 2 of Lemma append-segment


1. Type
2. T
3. List
4. ∀i:{0...||v||}. ∀j:{i...||v||}. ∀k:{j...||v||}.
     ((firstn(j i;nth_tl(i;v)) firstn(k j;nth_tl(j;v))) firstn(k i;nth_tl(i;v)) ∈ (T List))
5. {0...||[u v]||}
6. ¬(i ≤ 0)
7. {i...||[u v]||}
8. {j...||[u v]||}
⊢ (firstn(j i;nth_tl(i 1;v)) firstn(k j;nth_tl(j 1;v))) firstn(k i;nth_tl(i 1;v)) ∈ (T List)
BY
((InstHyp [⌜1⌝;⌜1⌝;⌜1⌝4⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN RepeatFor ((EqCD THEN Try (Trivial)))
   THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}i:\{0...||v||\}.  \mforall{}j:\{i...||v||\}.  \mforall{}k:\{j...||v||\}.
          ((firstn(j  -  i;nth\_tl(i;v))  @  firstn(k  -  j;nth\_tl(j;v)))  =  firstn(k  -  i;nth\_tl(i;v)))
5.  i  :  \{0...||[u  /  v]||\}
6.  \mneg{}(i  \mleq{}  0)
7.  j  :  \{i...||[u  /  v]||\}
8.  k  :  \{j...||[u  /  v]||\}
\mvdash{}  (firstn(j  -  i;nth\_tl(i  -  1;v))  @  firstn(k  -  j;nth\_tl(j  -  1;v)))  =  firstn(k  -  i;nth\_tl(i  -  1;v))


By


Latex:
((InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{};\mkleeneopen{}j  -  1\mkleeneclose{};\mkleeneopen{}k  -  1\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  Auto)




Home Index