diff -r 0efa7ffd96ff -r b257b9ba8a25 thys2/PDerivs.thy
--- a/thys2/PDerivs.thy	Tue Jan 11 23:58:39 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Jan 12 14:14:51 2022 +0000
@@ -333,15 +333,15 @@
 qed 
 
 text\<open>Antimirov's Corollary 3.5:\<close>
-
+(*W stands for word set*)
 corollary card_pders_set_le_awidth: 
-  shows "card (pders_Set A r) \<le> awidth r + 1"
+  shows "card (pders_Set W r) \<le> awidth r + 1"
 proof -
-  have "card (pders_Set A r) \<le> card (pders_Set UNIV r)"
+  have "card (pders_Set W r) \<le> card (pders_Set UNIV r)"
     by (simp add: card_mono finite_pders_set pders_Set_subset)
   also have "... \<le> awidth r + 1"
     by (rule card_pders_set_UNIV_le_awidth)
-  finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
+  finally show "card (pders_Set W r) \<le> awidth r + 1" by simp
 qed
 
 (* other result by antimirov *)
@@ -602,6 +602,20 @@
   sledgehammer
   oops
 
+lemma pdero_result: 
+  shows "pdero  c (STAR (ALT (CH c) (SEQ (CH c) (CH c)))) =  {SEQ (CH c)(STAR (ALT (CH c) (SEQ (CH c) (CH c)))),(STAR (ALT (CH c) (SEQ (CH c) (CH c))))}"
+  apply(simp)
+  by auto
+
+fun concatLen :: "rexp \<Rightarrow> nat" where
+"concatLen ZERO = 0" |
+"concatLen ONE = 0" |
+"concatLen (CH c) = 0" |
+"concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" |
+" concatLen (ALT v1 v2) =  max (concatLen v1) (concatLen v2)" |
+" concatLen (STAR v) = Suc (concatLen v)" 
+
+
 
 export_code height pders subs pderso in Scala module_name Pders 
 export_code pdero pderso in Scala module_name Pderso