---

Step * 1 of Lemma select-append


1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[i:ℕ].  (v @ L2[i] ~ if i <z ||v|| then v[i] else L2[i - ||v||] fi )
4. L2 : Top List
5. i : ℕ
⊢ [u / (v @ L2)][i] ~ if i <z ||v|| + 1 then [u / v][i] else L2[i - ||v|| + 1] fi 
BY
{ (((RWO "select-cons select-nil" 0 THENM SplitOnConclITE) THENA Auto)
   THEN (RWW "3" 0⋅ THENA Auto)
   THEN Repeat (AutoSplit)
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[L2:Top  List].  \mforall{}[i:\mBbbN{}].    (v  @  L2[i]  \msim{}  if  i  <z  ||v||  then  v[i]  else  L2[i  -  ||v||]  fi  )
4.  L2  :  Top  List
5.  i  :  \mBbbN{}
\mvdash{}  [u  /  (v  @  L2)][i]  \msim{}  if  i  <z  ||v||  +  1  then  [u  /  v][i]  else  L2[i  -  ||v||  +  1]  fi 


By

---

Latex:
(((RWO  "select-cons  select-nil"  0  THENM  SplitOnConclITE)  THENA  Auto)
  THEN  (RWW  "3"  0\mcdot{}  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  Auto')\mcdot{}

---

Home Index