diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 Spiral.scala
--- a/Spiral.scala	Sat Mar 23 11:53:09 2019 +0000
+++ b/Spiral.scala	Wed Apr 10 16:34:34 2019 +0100
@@ -434,14 +434,15 @@
   }
   //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set)
   def pushbits(r: ARexp): ARexp = r match {
-    case AALTS(bs, rs) => AALTS(Nil, rs.map(fuse(bs, _)))
+    case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
     case r => r
   }
   def correctness_proof_convenient_path(){
-    for(i <- 1 to 1)
+    for(i <- 1 to 10000)
     {
-        val s = "baa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
-        val r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),'c'), ACHAR(List(S),'b'))),ASEQ(List(),ASTAR(List(),ACHAR(List(),'a')),AALTS(List(),List(ACHAR(List(Z),'a'), ACHAR(List(S),'a'))))))//internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
+        val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+        val r = internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
         for(j <- 0 to s.length - 1){
           val ss = s.slice(0, j+ 1)
           val nangao = ders_simp(r, ss.toList)
@@ -463,6 +464,18 @@
         }
     }
   }
+  def retrieve_experience(){
+    val rg = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) 
+    val st = "abaab"
+    val vl = blexing_simp(erase(rg), st)
+    val bts = retrieve(rg, vl)
+    val cdbts = code(vl)
+    if(bts != cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
+      println(bts)
+      println(cdbts)
+      println("NOoooooo.....!")
+    }
+  }
   def radical_correctness(){
     enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
     random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
@@ -470,7 +483,8 @@
   def main(args: Array[String]) {
     //check_all()   
     //radical_correctness()
-    correctness_proof_convenient_path()
+    //correctness_proof_convenient_path()
+    retrieve_experience()
   } 
 }