PrintForm
Definitions
graph
1
2
Sections
Graphs
Doc
At:
array-update-select
T:Type, a:array(T), j,i:
|a|, v:T. a[i:=v][j] ~ if j=
i
v else a[j] fi
By:
UnivCD
THEN
Repeat ((Unfolds [`array-select`;`array-update`] 0) THEN (Reduce 0))
THEN
SplitOnConclITE
Generated subgoals:
None
About:
PrintForm
Definitions
graph
1
2
Sections
Graphs
Doc
T:Type, a:array(T), j,i:
|a|, v:T. a[i:=v][j] ~ if j=
i
v else a[j] fi