PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
nth
tl
lem0
2
1.
T:
Type
2.
y:
3.
0 < y
4.
as:T*. tl(nth_tl(y-1;as)) = nth_tl(y-1+1;as)
as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as)
By:
RecCaseSplit `nth_tl`
Generated subgoal:
1
5.
0 < y
6.
as:
T*
tl(nth_tl(y-1;tl(as))) = nth_tl(y+1;as)
About:
tl(nth_tl(y-1;tl(as))) = nth_tl(y+1;as)
as:T*. tl(nth_tl(y-1;as)) = nth_tl(y-1+1;as) as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) tl(nth_tl(y-1;tl(as))) = nth_tl(y+1;as)
