PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: append segment 1 1 1 1 1 1 2 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(x;nth_tl(i;as)) @ 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: Inst Thm* x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]]) [T;x-1;nth_tl(i;as)]
Generated subgoal:

19. firstn(x-1+1;nth_tl(i;as)) = (firstn(x-1;nth_tl(i;as)) @ [nth_tl(i;as)[(x-1)]])
(firstn(x;nth_tl(i;as)) @ 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)))

About:
equallistsubtractaddnatural_numberuniverseintless_than