---

Step * 1 of Lemma count_pairs_wf

.....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||)
BY
{ (((Unfold `double_sum` 0 THEN BackThruLemma `non_neg_sum`) THEN Auto) THEN BackThruLemma `non_neg_sum` THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  0  \mleq{}  sum(if  i  <z  j  \mwedge{}\msubb{}  P[L[i];L[j]]  then  1  else  0  fi    |  i  <  ||L||;  j  <  ||L||)


By

---

Latex:
(((Unfold  `double\_sum`  0  THEN  BackThruLemma  `non\_neg\_sum`)  THEN  Auto)
  THEN  BackThruLemma  `non\_neg\_sum`
  THEN  Auto)

---

Home Index