is mentioned by

Thm* P:(T), a:array(T), i:|a|, v:T. array-count(v.P(v);a[i:=v]) = array-count(v.P(v);a)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi	[array-count-update]
Thm* a:array(T), j,i:|a|, v:T. a[i:=v][j] ~ if j=i v else a[j] fi	[array-update-select]
Thm* L: List, i,j:||L||. 0 < L[i] L[i--][j] = if j=i L[j]-1 else L[j] fi	[list-dec-select]
Def array-count(v.P(v);a) == sum(if P(a[i]) 1 else 0 fi | i < |a|)	[array-count]
Def a[i:=v] == < |a|,j.if j=i v else a[j] fi >	[array-update]
Def L[i--] == mklist(||L||;j.if j=i L[j]-1 else L[j] fi)	[list-dec]

In prior sections: bool 1 mb nat mb list 2 graph 1 1 int 2 num thy 1 list 1 prog 1 mb list 1

Try larger context: Graphs