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