(3steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
count
pairs
wf
T
:Type,
L
:
T
List,
P
:(
T
T
). count(
x
<
y
in
L
|
P
(
x
,
y
))
By:
Unfold `count_pairs` 0 THEN Try (Complete Auto)
Generated subgoal:
1
1.
T
: Type
2.
L
:
T
List
3.
P
:
T
T
0
sum(if (
i
<
j
)
P
(
L
[
i
],
L
[
j
])
1 else 0 fi |
i
< ||
L
||;
j
< ||
L
||)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
T:Type, L:T List, P:(T
T
). count(x < y in L | P(x,y)) 
T:Type, L:T List, P:(TT). count(x < y in L | P(x,y)) T
0
sum(if (i<
j)
P(L[i],L[j])
1 else 0 fi | i < ||L||; j < ||L||)
