PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: append segment 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. x = j-i
8. j = x+i
9. kx+i

(firstn(x;nth_tl(i;as)) @ firstn(k-(x+i);nth_tl(x+i;as))) = firstn(k-i;nth_tl(i;as))
By:
Thin 8
THEN
Thin 7
THEN
NatInd 6
Generated subgoals:

1 k0+i (firstn(0;nth_tl(i;as)) @ firstn(k-(0+i);nth_tl(0+i;as))) = firstn(k-i;nth_tl(i;as))
26. x:
7. 0 < x
8. kx-1+i (firstn(x-1;nth_tl(i;as)) @ firstn(k-(x-1+i);nth_tl(x-1+i;as))) = firstn(k-i;nth_tl(i;as))
kx+i (firstn(x;nth_tl(i;as)) @ firstn(k-(x+i);nth_tl(x+i;as))) = firstn(k-i;nth_tl(i;as))

About:
equallistsubtractadduniversenatural_numberimplies