PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
list-dec-select
L:
List, i,j:
||L||. 0 < L[i]
L[i--][j] = if j=
i
L[j]-1 else L[j] fi
By:
Auto
THEN
Unfold `list-dec` 0
THEN
RWO
Thm*
n:
, f:(
n
T), i:
n. mklist(n;f)[i] = f(i) 0
THEN
Try (Complete Auto)
THEN
Reduce 0
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
L:
List, i,j:||L||. 0 < L[i] 
L[i--][j] = if j=
i
L[j]-1 else L[j] fi
n:, f:(n
T), i:n. mklist(n;f)[i] = f(i)
0
