Step * 2 1 1 1 1 of Lemma no-repeats-iff-count


1. Type
2. eq EqDecider(T)
3. List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| 1 ∈ ℤ)
5. : ℕ
6. : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i j ∈ ℕ)
10. L[i] L[j] ∈ T
11. i < j
⊢ [L[i]; L[j]] ⊆ L
BY
(BLemma `sublist_pair` THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;L)||;||filter(eq  x;L)||  =  1)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||L||
8.  j  <  ||L||
9.  \mneg{}(i  =  j)
10.  L[i]  =  L[j]
11.  i  <  j
\mvdash{}  [L[i];  L[j]]  \msubseteq{}  L


By


Latex:
(BLemma  `sublist\_pair`  THEN  Auto)




Home Index