PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
append
segment
1
1
1
1
1
1
1
1
1
1
1.
T:
Type
2.
as:
T*
3.
i:
{0...||as||}
4.
j:
{i...||as||}
5.
k:
{j...||as||}
(Case of nth_tl(i;as); nil
nil ; a.as'
nil) = nil
T*
By:
Let (w = nth_tl(i;as))
Generated subgoal:
1
6.
w:
T*
7.
w = nth_tl(i;as)
(Case of w; nil
nil ; a.as'
nil) = nil
T*
About:
(Case of w; nil 
nil ; a.as' nil) = nil 
T* (Case of nth_tl(i;as); nil nil ; a.as' nil) = nil T* (Case of w; nil nil ; a.as' nil) = nil T*
