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