# HG changeset patch
# User Chengsong
# Date 1644085477 0
# Node ID 5c96fe5306a7bfd54829b93203ebdc8f2753cd8a
# Parent  1234e6bd4fd16a690b49765260d0db228d3a83db
exp

diff -r 1234e6bd4fd1 -r 5c96fe5306a7 thys2/blexer1.sc
--- a/thys2/blexer1.sc	Sat Feb 05 18:23:16 2022 +0000
+++ b/thys2/blexer1.sc	Sat Feb 05 18:24:37 2022 +0000
@@ -847,7 +847,7 @@
   println("the total number of terms is")
   //println(refSize)
   println(pderSTAR.size)
-  for(i <- List(1, 10, 100, 400, 800, 840, 900) ){
+  for(i <- List(1, 10, 100, 400, 800, 840, 841, 900) ){
     val prog0 = "a" * i
     //println(s"test: $prog0")
     println(s"testing with $i a's" )
@@ -860,12 +860,13 @@
     println("the number of distinct subterms for bsimp with strongDB and standardDB")
     println(subTerms.distinct.size)
     println(subTermsLarge.distinct.size)
+    println("which coincides with the number of PDER terms")
 
 
     // println(shortRexpOutput(erase(sbd)))
     // println(shortRexpOutput(erase(bd)))
     
-    println("pdersize, original, strongSimp")
+    println("pdersize, original, strongSimp, bsimp")
     println(refSize, size(STARREG),  asize(sbd), asize(bd))
 
     // val vres = strong_blexing_simp( STARREG, prog0)