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

At: list-decomp-last 2 1 1 2 2
1. T: Type
2. s: T List
3. u: T
4. u1: T
5. v1: T List
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)]])
[[u; u1 / v1][(||v1||+1)]] ~ [[u1 / v1][(||[u1 / v1]||-1)]]
By: Subst ([u; u1 / v1][(||v1||+1)] ~ [u1 / v1][||v1||]) 0
Generated subgoals:

1 [u; u1 / v1][(||v1||+1)] ~ [u1 / v1][||v1||]1 step
 
2 [[u1 / v1][||v1||]] ~ [[u1 / v1][(||[u1 / v1]||-1)]]1 step

About:
listconsconsnilnatural_numberaddsubtractless_thanuniversesqequal

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