PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
derive
refl
1
3
1.
V:
Type
2.
T:
Type
3.
G:
Grammar(V;T)
4.
l:
(V+T)*
5.
a:
(V+T)* List
(l = a[0] & (
i:
(||a||-1). a[i]
a[(i+1)]) & a[(||a||-1)] = l)
Prop
By:
Analyze 5
Generated subgoals:
None
About:
(l = a[0] & (
i:
(||a||-1). a[i] 
a[(i+1)]) & a[(||a||-1)] = l) 
Prop
