(11steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
list-decomp-last
2
1
1.
T:
Type
2.
s:
T List
3.
u:
T
4.
u1:
T
5.
v1:
T List
6.
0 < ||[u1 / v1]||
([u1 / v1] ~ (firstn(||[u1 / v1]||-1;[u1 / v1]) @ [[u1 / v1][(||[u1 / v1]||-1)]]))
7.
0 < ||[u1 / v1]||+1
8.
0 < ||v1||+1+1-1
[u1 / v1] ~ (firstn(||v1||+1+1-1-1;[u1 / v1]) @ [[u; u1 / v1][(||v1||+1+1-1)]])
By:
Analyze -3
Generated subgoal:
1
6.
0 < ||[u1 / v1]||+1
7.
0 < ||v1||+1+1-1
8.
[u1 / v1] ~ (firstn(||[u1 / v1]||-1;[u1 / v1]) @ [[u1 / v1][(||[u1 / v1]||-1)]])
[u1 / v1] ~ (firstn(||v1||+1+1-1-1;[u1 / v1]) @ [[u; u1 / v1][(||v1||+1+1-1)]])
7
steps
About:
(11steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc