PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
derive
refl
1
1
1
1.
V:
Type
2.
T:
Type
3.
G:
Grammar(V;T)
4.
l:
(V+T)*
||[l]|| > 0
By:
RWH (LemmaC
Thm*
a:A, as:A*. ||a.as|| = ||as||+1) 0
Generated subgoal:
1
||nil||+1 > 0
About:
||[l]|| > 0
a:A, as:A*. ||a.as|| = ||as||+1)
0 ||nil||+1 > 0
