Nuprl - Proof: array-count-update

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

T:Type, 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

By: Auto THEN Unfold `array-count` 0 THEN Reduce 0 THEN Inst Thm* n:, f:(n), m:n. sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n) [|a|;x.if P(a[i:=v][x]) 1 else 0 fi;i] THEN All ReduceSOAps THEN HypSubst -1 0 THEN Thin -1 THEN Inst Thm* n:, f:(n), m:n. sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n) [|a|;x.if P(a[x]) 1 else 0 fi;i] THEN All ReduceSOAps THEN HypSubst -1 0 THEN Thin -1 THEN Subst (a[i:=v][i] ~ v) 0

Generated subgoals:

1 1. T: Type
2. P: T
3. a: array(T)
4. i: |a|
5. v: T
a[i:=v][i] ~ v 1 step

2 1. T: Type
2. P: T
3. a: array(T)
4. i: |a|
5. v: T
if P(v) 1 else 0 fi+sum(if x=i0 ;P(a[i:=v][x])1 else 0 fi | x < |a|) = if P(a[i]) 1 else 0 fi+sum(if x=i0 ;P(a[x])1 else 0 fi | x < |a|)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi 1 step

About:

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1	1. `T:` `Type` 2. `P:` `T` 3. `a:` `array(T)` 4. `i:` `\|a\|` 5. `v:` `T` `a[i:=v][i] ~ v`	1 step

2	1. `T:` `Type` 2. `P:` `T` 3. `a:` `array(T)` 4. `i:` `\|a\|` 5. `v:` `T` `if P(v) 1 else 0 fi+sum(if x=i0 ;P(a[i:=v][x])1 else 0 fi \| x < \|a\|) = if P(a[i]) 1 else 0 fi+sum(if x=i0 ;P(a[x])1 else 0 fi \| x < \|a\|)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi`	1 step