---

Step * of Lemma fseg_select

No Annotations
∀[T:Type]
  ∀l1,l2:T List.
    (fseg(T;l1;l2) ⇐⇒ (||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[(||l2|| - ||l1||) + i] ∈ T supposing i < ||l1||))
BY
{ (Auto' THEN Try ((BLemma `fseg_length` THEN Auto))) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. fseg(T;l1;l2)
5. i : ℕ
6. i < ||l1||
⊢ l1[i] = l2[(||l2|| - ||l1||) + i] ∈ T

2
1. [T] : Type
2. l1 : T List
3. l2 : T List
4. (||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[(||l2|| - ||l1||) + i] ∈ T supposing i < ||l1||)
⊢ fseg(T;l1;l2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}l1,l2:T  List.
        (fseg(T;l1;l2)
        \mLeftarrow{}{}\mRightarrow{}  (||l1||  \mleq{}  ||l2||)  c\mwedge{}  (\mforall{}i:\mBbbN{}.  l1[i]  =  l2[(||l2||  -  ||l1||)  +  i]  supposing  i  <  ||l1||))


By

---

Latex:
(Auto'  THEN  Try  ((BLemma  `fseg\_length`  THEN  Auto)))

---

Home Index