---

Step * of Lemma count_pairs_wf

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ T ⟶ 𝔹].  (count(x < y in L | P[x;y]) ∈ ℕ)
BY
{ ((Unfold `count_pairs` 0 THEN Auto) THEN MemTypeCD THEN Try (Complete (Auto))) }

1
.....set predicate..... 
1. T : Type
2. L : T List
3. P : T ⟶ T ⟶ 𝔹
⊢ 0 ≤ sum(if i <z j ∧b P[L[i];L[j]] then 1 else 0 fi  | i < ||L||; j < ||L||)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].    (count(x  <  y  in  L  |  P[x;y])  \mmember{}  \mBbbN{})


By

---

Latex:
((Unfold  `count\_pairs`  0  THEN  Auto)  THEN  MemTypeCD  THEN  Try  (Complete  (Auto)))

---

Home Index