diff -r 6c5920fd02a7 -r b51d34113d47 Spiral.scala
--- a/Spiral.scala	Thu Apr 16 09:14:15 2020 +0100
+++ b/Spiral.scala	Thu May 07 11:36:15 2020 +0100
@@ -2,7 +2,6 @@
 import RexpRelated._
 import RexpRelated.Rexp._
 import Partial._
-import BRexp._
 import scala.collection.mutable.ListBuffer
 object Spiral{
 
@@ -27,7 +26,6 @@
     }
   }
   val alphabet = ("""abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789.:"=()\;-+*!<>\/%{} """+"\n\t").toSet//Set('a','b','c')
-  def bregx_tree(r: BRexp): Element = regx_tree(berase(r))
   def regx_tree(r: Rexp): Element = aregx_tree(internalise(r))
   def annotated_tree(r: ARexp): Element = {
     r match {
@@ -371,42 +369,7 @@
     }
   }
   val mkst = "abcdefghijklmnopqrstuvwxyz"
-  def weak_sub_check(r: Rexp, s: String, i: Int, f: (List[Rexp], Set[Rexp]) => Boolean){
-    //we first compute pders over the set of all strings on the alphabet
-    val pd = pderas(Set(r), i + 4)
-    //then "b-internalise" the regular expression into a brexp(this is essentially 
-    //attaching a bit Z to every alts to signify that they come from the original regular expression)
-    var old = brternalise(r)
-    //this is for comparison between normal simp and the weakened version of simp
-    //normal simp will be performed on syncold
-    //weakend simp will be performed on old
-    var syncold = internalise(r)
-    val all_chars = s.toList
-    for (i <- 0 to s.length - 1){
-      val syncder_res = bder(all_chars(i), syncold)
-      val syncsimp_res = super_bsimp(syncder_res)
-      //see brder for detailed explanation
-      //just changes bit Z to S when deriving an ALTS, 
-      //signifying that the structure has been "touched" and
-      //therefore able to be spilled in the bspill function
-      val der_res =  brder(all_chars(i), old)
-      val simp_res = br_simp(der_res)
-      val anatomy = bspill(simp_res)
-      //track if the number of regular expressions exceeds those in the PD set(remember PD means the pders over A*)
-      if(f(List(berase(simp_res)), pd)  == false ){
-        println(size(erase(syncsimp_res)))
-        println(size(berase(simp_res)))
-        println(bregx_tree(simp_res))
-        println(s)
-        println(i)
-        println(r)
-        println(anatomy.map(size).sum)
-        println(pd.map(size).sum)
-      }  
-      old = simp_res
-      syncold = syncsimp_res
-    }
-  }
+  
   def inclusion_truth(anatomy: List[Rexp], pd: Set[Rexp]): Boolean = {
     val aset = anatomy.toSet
     if(aset subsetOf pd){
@@ -427,11 +390,7 @@
   }
   val big_panda = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c')))))))
   val str_panda = "ccccb"
-  def check_all(){
 
-        weak_sub_check(big_panda, str_panda, 6, size_expansion_rate)
-
-  }
   def bstostick(bs: List[Bit]): Element = bs match {
     //case b::Nil => elem(b.toString)
     case b::bs1 => elem(b.toString) beside bstostick(bs1)