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

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. T: Type
2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}

ki ((Case of nth_tl(i;as); nil nil ; a.as' nil) @ firstn(-i+k;nth_tl(i;as))) = firstn(-i+k;nth_tl(i;as))

By: Assert ((Case of nth_tl(i;as); nil nil ; a.as' nil) = nil)

Generated subgoals:

1 (Case of nth_tl(i;as); nil nil ; a.as' nil) = nil T*

2 6. (Case of nth_tl(i;as); nil nil ; a.as' nil) = nil T*
ki ((Case of nth_tl(i;as); nil nil ; a.as' nil) @ firstn(-i+k;nth_tl(i;as))) = firstn(-i+k;nth_tl(i;as))

About:

1	`(Case of nth_tl(i;as); nil nil ; a.as' nil) = nil T*`
2	6. `(Case of nth_tl(i;as); nil nil ; a.as' nil) = nil T*` `ki ((Case of nth_tl(i;as); nil nil ; a.as' nil) @ firstn(-i+k;nth_tl(i;as))) = firstn(-i+k;nth_tl(i;as))`