--- a/thys2/PDerivs.thy	Wed Jan 12 14:14:51 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Jan 12 15:24:10 2022 +0000
@@ -615,6 +615,10 @@
 " concatLen (ALT v1 v2) =  max (concatLen v1) (concatLen v2)" |
 " concatLen (STAR v) = Suc (concatLen v)" 
 
+text\<open>Antimirov's Theorem 3.8:\<close>
+lemma Maxsubterms38:
+  shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)"
+
 
 
 export_code height pders subs pderso in Scala module_name Pders