Nuprl - Pf append_segment 1 1 1 1 1 1 2 1 1 1 1 1 1 1

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: append segment 1 1 1 1 1 1 2 1 1 1 1 1 1 1

1. T: Type
2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}
6. x:
7. 0 < x
8. kx+i

hd(nth_tl(-1+x;nth_tl(i;as))).firstn(-i+k+-x;nth_tl(i+x;as)) = firstn(1+-i+k+-x;nth_tl(-1+i+x;as))

By: Inst Thm* x,y:, as:T*. nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as) [T;-1+x;i;as]

Generated subgoal:

1 9. nth_tl(-1+x;nth_tl(i;as)) = nth_tl(-1+x+i;as)
hd(nth_tl(-1+x;nth_tl(i;as))).firstn(-i+k+-x;nth_tl(i+x;as)) = firstn(1+-i+k+-x;nth_tl(-1+i+x;as))

About: