PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
g
eq
wf
1
1.
V1:
Type
2.
V2:
Type
3.
T:
Type
4.
G1:
Grammar(V1;T)
5.
G2:
Grammar(V2;T)
(
l:(Void+T)*. (
l.[S]
l)(l)
(
l.[S]
l)(l))
Prop
By:
Analyze
Generated subgoals:
1
(Void+T)*
Type
2
6.
l:
(Void+T)*
((
l.[S]
l)(l)
(
l.[S]
l)(l))
Prop
About:
(Void+T)* 
Type ((
l.[S] 
l)(l) 
(l.[S] l)(l)) Prop (
l:(Void+T)*. (l.[S] l)(l) (l.[S] l)(l)) Prop (Void+T)* Type ((l.[S] l)(l) (l.[S] l)(l)) Prop
