--- a/progs/Matcher2.thy	Tue Oct 18 19:14:33 2016 +0100
+++ b/progs/Matcher2.thy	Tue Oct 18 20:39:54 2016 +0100
@@ -359,9 +359,8 @@
 done
 
 lemma L_der_NTIMES:
-  shows "L(der c (NTIMES r n)) = (if n = 0 then {} else if nullable r then 
-       L(SEQ (der c r) (UPNTIMES r (n - 1)))
-       else L(SEQ (der c r) (NTIMES r (n - 1))))"
+  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
+         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
 apply(induct n)
 apply(simp)
 apply(simp)
@@ -376,6 +375,9 @@
 apply(simp)
 by (metis Suc_pred atMost_iff le_Suc_eq)
 
+lemma "L(der c (UPNTIMES r 0)) = {}"
+by simp
+
 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 using assms
 proof(induct n)