Nuprl - Proof: list-decomp-last 2 1 1

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

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)]])

[u1 / v1] ~ (firstn(||v1||+1+1-1-1;[u1 / v1]) @ [[u; u1 / v1][(||v1||+1+1-1)]])

By: NthHypSq -1 THEN Analyze THEN Analyze

Generated subgoals:

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

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

About:

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

1	`firstn(\|\|v1\|\|+1+1-1-1;[u1 / v1]) ~ firstn(\|\|[u1 / v1]\|\|-1;[u1 / v1])`	1 step

2	`[[u; u1 / v1][(\|\|v1\|\|+1+1-1)]] ~ [[u1 / v1][(\|\|[u1 / v1]\|\|-1)]]`	5 steps