---

Step * of Lemma count_index_pairs_wf

∀[T:Type]. ∀[P:L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℕ||L|| ⟶ 𝔹]. ∀[L:T List].  (count(i<j<||L|| : P L i j) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN Assert count(i<j<||L|| : P L i j) ∈ ℤ) }

1
.....assertion..... 
1. T : Type
2. P : L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℕ||L|| ⟶ 𝔹
3. L : T List
⊢ count(i<j<||L|| : P L i j) ∈ ℤ

2
1. T : Type
2. P : L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℕ||L|| ⟶ 𝔹
3. L : T List
4. count(i<j<||L|| : P L i j) ∈ ℤ
⊢ count(i<j<||L|| : P L i j) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:L:(T  List)  {}\mrightarrow{}  \mBbbN{}||L||  -  1  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (count(i<j<||L||  :  P  L  i  j)  \mmember{}  \mBbbN{})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  count(i<j<||L||  :  P  L  i  j)  \mmember{}  \mBbbZ{})

---

Home Index