PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
con
free
g
wf
1
1
1
1
1.
V:
Type
2.
T:
Type
3.
G:
Grammar(V;T)
4.
i:
||G.prod||
5.
a:
V
6.
||[inl(a)]|| = ||nil||+1
||nil||+1 > 0
By:
Assert (||nil|| = 0)
Generated subgoals:
1
||nil|| = 0
2
7.
||nil|| = 0
||nil||+1 > 0
About:
||nil|| = 0 ||nil||+1 > 0
||G.prod|| ||nil||+1 > 0 ||nil|| = 0 ||nil||+1 > 0
