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

At: list-dec wf
L: List, i:||L||. 0 < L[i] L[i--] List
By:
Auto
THEN
Unfold `list-dec` 0
THEN
RepeatFor 2 (Analyze THEN (Try (Complete Auto)))
THEN
SplitOnConclITE
Generated subgoal:

11. L: List
2. i: ||L||
3. 0 < L[i]
4. j: ||L||
5. j = i
0L[j]-1		1 step

About:
listnatural_numbersubtractless_thanmemberimpliesall

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