---

Step * 1 of Lemma firstn_firstn


1. u : Top
2. v : Top List
3. ∀[n:ℤ]. ∀[m:ℕn + 1].  (firstn(m;firstn(n;v)) ~ firstn(m;v))
4. n : ℤ
5. m : ℕn + 1
⊢ case if 0 <z n then [u / firstn(n - 1;v)] else [] fi  of 
    [] => [] 
    a::as' =>
     if 0 <z m then [a / firstn(m - 1;as')] else [] fi  
esac ~ if 0 <z m then [u / firstn(m - 1;v)] else [] fi 
BY
{ ((((SplitOnConclITE THENA (Auto THEN Auto')) THEN Reduce 0 THEN SplitOnConclITE) THENA (Auto THEN Auto'))
   THEN Try (Complete (Auto'))
   ) }

1
.....truecase..... 
1. u : Top
2. v : Top List
3. ∀[n:ℤ]. ∀[m:ℕn + 1].  (firstn(m;firstn(n;v)) ~ firstn(m;v))
4. n : ℤ
5. m : ℕn + 1
6. 0 < n
7. 0 < m
⊢ [u / firstn(m - 1;firstn(n - 1;v))] ~ [u / firstn(m - 1;v)]

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbZ{}].  \mforall{}[m:\mBbbN{}n  +  1].    (firstn(m;firstn(n;v))  \msim{}  firstn(m;v))
4.  n  :  \mBbbZ{}
5.  m  :  \mBbbN{}n  +  1
\mvdash{}  case  if  0  <z  n  then  [u  /  firstn(n  -  1;v)]  else  []  fi    of 
        []  =>  [] 
        a::as'  =>
          if  0  <z  m  then  [a  /  firstn(m  -  1;as')]  else  []  fi   
esac  \msim{}  if  0  <z  m  then  [u  /  firstn(m  -  1;v)]  else  []  fi 


By

---

Latex:
((((SplitOnConclITE  THENA  (Auto  THEN  Auto'))  THEN  Reduce  0  THEN  SplitOnConclITE)
    THENA  (Auto  THEN  Auto')
    )
  THEN  Try  (Complete  (Auto'))
  )

---

Home Index