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

At: list-dec-length 1
1. L: List
2. i: ||L||
3. 0 < L[i]
(j.if j=i L[j]-1 else L[j] fi) ||L||
By:
Analyze
THEN
Try (Complete Auto)
THEN
SplitOnConclITE
Generated subgoal:

14. j: ||L||
5. j = i
0L[j]-1		1 step

About:
listifthenelsenatural_numbersubtractless_thanlambdafunctionmember

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