Nuprl - Pf append_segment 1 1 1 1 1 1 2 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. 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

((firstn(-1+x;nth_tl(i;as)) @ [nth_tl(i;as)[(-1+x)]]) @ firstn(k-(x+i);nth_tl(x+i;as))) = (firstn(x-1;nth_tl(i;as)) @ firstn(k-(x-1+i);nth_tl(x-1+i;as)))

By: ArithSimp 0 THEN RWH (LemmaC Thm* as,bs,cs:T*. ((as @ bs) @ cs) = (as @ (bs @ cs))) 0

Generated subgoal:

1 (firstn(-1+x;nth_tl(i;as)) @ [nth_tl(i;as)[(-1+x)]] @ firstn(-i+k+-x;nth_tl(i+x;as))) = (firstn(-1+x;nth_tl(i;as)) @ firstn(1+-i+k+-x;nth_tl(-1+i+x;as)))

About: