--- a/Spiral.scala	Fri Apr 12 19:26:13 2019 +0100
+++ b/Spiral.scala	Sat Apr 13 16:18:23 2019 +0100
@@ -469,20 +469,45 @@
       println(cdbts)
       println("code v = retrieve internalise(r) v if |- v : r")
     }
+
+
+        val r_der_s = bders(st.toList, rg)
+    println(aregx_tree(r_der_s))
+    val bts = retrieve(r_der_s, unsimplified_vl)
+    val cdbts = code(unsimplified_vl)
+    val simprg = bsimp(r_der_s)
+    val frectv = decode(erase(simprg), cdbts)
+    val simpbts = retrieve(simprg, frectv)
+    if(bts == simpbts){
+      println("retrieve r v = retrieve (bsimp r) (decode bsimp(r) code(v))")
+      println("bits:")
+      //println(bts)
+      println(simpbts)
+      println("v = ")
+      println(unsimplified_vl)
+      println("frect v = ")
+      println(frectv)
+    }
     */
   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)
-    //println(vl)
-    val bts = retrieve(rg, vl)
-    val cdbts = code(vl)
-    val simprg = bsimp(rg)
-    val simpbts = retrieve(simprg, decode(erase(simprg), cdbts))
-    if(bts == simpbts){
-      println("retrieve r v = retrieve (bsimp r) (decode bsimp(r) code(v))")
-      println(bts)
-      println(simpbts)
+    val r_der_s = ders(st.toList, erase(rg))
+    val unsimplified_vl = mkeps(r_der_s)
+    val r_bder_s = bders( st.toList, rg)
+    val s_r_bder_s = bsimp(r_bder_s)
+    val bits1 = retrieve(r_bder_s, unsimplified_vl)
+    println(r_bder_s)
+    println(erase(r_bder_s))
+    println(s_r_bder_s)
+    println(erase(s_r_bder_s))
+    println(code(unsimplified_vl))
+    val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl)))
+    if(bits1 == bits2){
+      println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
+      println("Here v == mkeps r\\s and r == r\\s")
+      println(r_der_s, unsimplified_vl)
+      println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl))
     }
   }
   def radical_correctness(){