---

Step * of Lemma select-append

∀[L1,L2:Top List]. ∀[i:ℕ].  (L1 @ L2[i] ~ if i <z ||L1|| then L1[i] else L2[i - ||L1||] fi )
BY
{ (InductionOnList THEN Reduce 0 THEN (UnivCD THENA Auto) THEN Try ((SplitOnConclITE THEN Complete (Auto)))) }

1
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 

---

Latex:

---

Latex:
\mforall{}[L1,L2:Top  List].  \mforall{}[i:\mBbbN{}].    (L1  @  L2[i]  \msim{}  if  i  <z  ||L1||  then  L1[i]  else  L2[i  -  ||L1||]  fi  )


By

---

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

---

Home Index