Step * of Lemma select-append

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

1
1. Top
2. Top List
3. ∀[L2:Top List]. ∀[i:ℕ].  (v L2[i] if i <||v|| then v[i] else L2[i ||v||] fi )
4. L2 Top List
5. : ℕ
⊢ [u (v L2)][i] if i <||v|| 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