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 1 else 0 fi | i < |a|)
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] |
Try larger context:
Graphs