--- a/.hgignore	Wed Jan 12 14:14:51 2022 +0000
+++ b/.hgignore	Wed Jan 12 15:24:10 2022 +0000
@@ -1,4 +1,5 @@
 syntax: glob
+thys2/session_graph.pdf
 Fahad\Eclipse\.metadata\.lock
 Fahad\Eclipse\.metadata\.plugins\org.eclipse.core.resources\.history\11\e096942ef16100141bd68cdd3ac1b72d
 Fahad\Eclipse\.metadata\.plugins\org.eclipse.core.resources\.history\14\2059415eea6100141bd68cdd3ac1b72d
@@ -254,4 +255,4 @@
 Fahad\Eclipse\ScalaProjects\.worksheet\src\CodeSamples.Test.scala
 Fahad\Eclipse\ScalaProjects\.worksheet\src\Handouts.Handout2.scala
 Fahad\Eclipse\ScalaProjects\.worksheet\src\Handouts.RegularExpression1.scala
-progs\scala\target\.history
\ No newline at end of file
+progs\scala\target\.history

--- 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