equal
deleted
inserted
replaced
15 S &\to& \epsilon \mid b A \mid a B \nonumber\\ |
15 S &\to& \epsilon \mid b A \mid a B \nonumber\\ |
16 A &\to& a S \mid b A A \nonumber\\ |
16 A &\to& a S \mid b A A \nonumber\\ |
17 B &\to& b S \mid a B B \nonumber |
17 B &\to& b S \mid a B B \nonumber |
18 \end{eqnarray} |
18 \end{eqnarray} |
19 At the end we say a few words about the relationship between |
19 At the end we say a few words about the relationship between |
20 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. |
20 the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version. |
21 |
21 |
22 We start by fixing the alphabet, which consists only of @{term a}'s |
22 We start by fixing the alphabet, which consists only of @{term a}'s |
23 and~@{term b}'s: |
23 and~@{term b}'s: |
24 *} |
24 *} |
25 |
25 |
281 by(force simp add: min_less_iff_disj split add: nat_diff_split) |
281 by(force simp add: min_less_iff_disj split add: nat_diff_split) |
282 |
282 |
283 text{* |
283 text{* |
284 We conclude this section with a comparison of our proof with |
284 We conclude this section with a comparison of our proof with |
285 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
285 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
286 \cite[p.\ts81]{HopcroftUllman}. |
286 @{cite \<open>p.\ts81\<close> HopcroftUllman}. |
287 For a start, the textbook |
287 For a start, the textbook |
288 grammar, for no good reason, excludes the empty word, thus complicating |
288 grammar, for no good reason, excludes the empty word, thus complicating |
289 matters just a little bit: they have 8 instead of our 7 productions. |
289 matters just a little bit: they have 8 instead of our 7 productions. |
290 |
290 |
291 More importantly, the proof itself is different: rather than |
291 More importantly, the proof itself is different: rather than |