Step * 2 of Lemma nth_tl_decomp


1. Type
2. : ℤ
3. 0 < m
4. ∀[L:T List]. nth_tl(m 1;L) [L[m 1] nth_tl(1 (m 1);L)] supposing 1 < ||L||
⊢ ∀[L:T List]
    if m ≤then else nth_tl(m 1;tl(L)) fi  [L[m] if m ≤then else nth_tl((1 m) 1;tl(L)) fi 
    supposing m < ||L||
BY
(RepeatFor ((D THENA Auto))
   THEN ((InstHyp [⌜tl(L)⌝(-3) ⋅ THENM HypSubst' -1 0) THENA (RWW "length_tl" THEN Auto))
   THEN AutoSplit
   THEN EqCD
   THEN Try (Complete (Auto))) }

1
1. Type
2. : ℤ
3. ¬(m ≤ 0)
4. 0 < m
5. ∀[L:T List]. nth_tl(m 1;L) [L[m 1] nth_tl(1 (m 1);L)] supposing 1 < ||L||
6. List
7. m < ||L||
8. nth_tl(m 1;tl(L)) [tl(L)[m 1] nth_tl(1 (m 1);tl(L))]
⊢ tl(L)[m 1] L[m]


Latex:


Latex:

1.  T  :  Type
2.  m  :  \mBbbZ{}
3.  0  <  m
4.  \mforall{}[L:T  List].  nth\_tl(m  -  1;L)  \msim{}  [L[m  -  1]  /  nth\_tl(1  +  (m  -  1);L)]  supposing  m  -  1  <  ||L||
\mvdash{}  \mforall{}[L:T  List]
        if  m  \mleq{}z  0  then  L  else  nth\_tl(m  -  1;tl(L))  fi    \msim{}  [L[m]  / 
                                                                                                          if  1  +  m  \mleq{}z  0
                                                                                                          then  L
                                                                                                          else  nth\_tl((1  +  m)  -  1;tl(L))
                                                                                                          fi  ] 
        supposing  m  <  ||L||


By


Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((InstHyp  [\mkleeneopen{}tl(L)\mkleeneclose{}]  (-3)  \mcdot{}  THENM  HypSubst'  -1  0)  THENA  (RWW  "length\_tl"  0  THEN  Auto))
  THEN  AutoSplit
  THEN  EqCD
  THEN  Try  (Complete  (Auto)))




Home Index