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

At: array-count-update 1
1. T: Type
2. P: T
3. a: array(T)
4. i: |a|
5. v: T
a[i:=v][i] ~ v
By:
RWO Thm* a:array(T), j,i:|a|, v:T. a[i:=v][j] ~ if j=i v else a[j] fi 0
THEN
SplitOnConclITE
Generated subgoals:

None

About:
boolifthenelsenatural_numberfunctionuniversesqequalall

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