Nuprl - Proof: list-decomp-last 2

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

1. T: Type
2. s: T List
3. u: T
4. v: T List
5. 0 < ||v|| (v ~ (firstn(||v||-1;v) @ [v[(||v||-1)]]))
6. 0 < ||v||+1

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

By: Analyze -3 THEN Reduce 0 THEN RecUnfold `firstn` 0 THEN Reduce 0 THEN Try SplitOnConclITE THEN Reduce 0 THEN Analyze THEN Try Trivial THEN Try (Complete Auto)

Generated subgoal:

1 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)]]) 8 steps

About:

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