PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
derive
trans
V,T:Type, G:Grammar(V;T), l,m,n:(V+T)*. (l
m)
(m
n)
(l
n)
By:
Unfold `derive` 0
THEN
Reduce 0
THEN
Try (Analyze 8)
THEN
Try (Analyze 7)
Generated subgoal:
1
1.
V:
Type
2.
T:
Type
3.
G:
Grammar(V;T)
4.
l:
(V+T)*
5.
m:
(V+T)*
6.
n:
(V+T)*
7.
a1:
(V+T)* List
8.
l = a1[0]
9.
i:
(||a1||-1). a1[i]
a1[(i+1)]
10.
a1[(||a1||-1)] = m
11.
a:
(V+T)* List
12.
m = a[0]
13.
i:
(||a||-1). a[i]
a[(i+1)]
14.
a[(||a||-1)] = n
a:((V+T)* List
). l = a[0] & (
i:
(||a||-1). a[i]
a[(i+1)]) & a[(||a||-1)] = n
About: