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

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 1 1 1 1 1 2

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
9. tl(nth_tl(-1+i+x;as)) = nth_tl(i+x;as)
10. aas: T*
11. aas = nth_tl(-1+i+x;as)
12. aas = nil

hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)

By: Thin -2 THEN ListInd 10

Generated subgoals:

1 nil = nil T* hd(nil).firstn(-i+k+-x;tl(nil)) = firstn(1+-i+k+-x;nil) T*

2 11. u: T
12. v: T*
13. v = nil hd(v).firstn(-i+k+-x;tl(v)) = firstn(1+-i+k+-x;v)
u.v = nil hd((u.v)).firstn(-i+k+-x;tl((u.v))) = firstn(1+-i+k+-x;u.v)

About:

1	`nil = nil T* hd(nil).firstn(-i+k+-x;tl(nil)) = firstn(1+-i+k+-x;nil) T*`
2	11. `u:` `T` 12. `v:` `T*` 13. `v = nil hd(v).firstn(-i+k+-x;tl(v)) = firstn(1+-i+k+-x;v)` `u.v = nil hd((u.v)).firstn(-i+k+-x;tl((u.v))) = firstn(1+-i+k+-x;u.v)`