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:

11. 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:
alluniverselistunionimpliesexists
andequalnatural_numbersubtractadd