---

Step * 1 of Lemma firstn-append


∀[L2:Top List]. ∀[n:ℕ].
  (case L2 of [] => [] | a::as' => if 0 <z n then [a / firstn(n - 1;as')] else [] fi  esac ~ if n ≤z 0
  then []
  else case L2 of [] => [] | a::as' => if 0 <z n - 0 then [a / firstn(n - 0 - 1;as')] else [] fi  esac
  fi )
BY
{ (Auto THEN (D (-2)) THEN Reduce 0 THEN Try (Trivial) THEN RepeatFor 3 ((SplitOnConclITE THEN Auto'))) }

---

Latex:

---

Latex:

\mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}].
    (case  L2  of  []  =>  []  |  a::as'  =>  if  0  <z  n  then  [a  /  firstn(n  -  1;as')]  else  []  fi    esac 
    \msim{}  if  n  \mleq{}z  0
    then  []
    else  case  L2  of 
                  []  =>  [] 
                  a::as'  =>
                    if  0  <z  n  -  0  then  [a  /  firstn(n  -  0  -  1;as')]  else  []  fi   
              esac
    fi  )


By

---

Latex:
(Auto
  THEN  (D  (-2))
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RepeatFor  3  ((SplitOnConclITE  THEN  Auto')))

---

Home Index