diff -r 0573615e41a3 -r 83b021fc7d29 Spiral.scala
--- a/Spiral.scala	Mon Jul 08 21:21:54 2019 +0100
+++ b/Spiral.scala	Wed Jul 10 23:16:14 2019 +0100
@@ -559,6 +559,15 @@
     println(s"bs1=${bs1}, bs3=${bs3}")
     //println(decode(erase(a_v._1), bs3))
   }
+  def christian_def2(){
+    val a = AALTS(List(Z), List(AZERO, ASEQ(List(), AALTS(List(),List(AONE(List()), ACHAR(Nil, 'b'))), ACHAR(Nil, 'b'))  )   )
+    val unsimp = bsimp(bder('b',a))
+    val simped = bsimp(bder('b', bsimp(a)))
+    println(bsimp(a))
+    if(unsimp == simped){
+      println(s"bsimp(bder c r) = ${unsimp}, whereas bsimp(bder c bsimp r) = ${simped}")
+    }
+  }
   def essence_posix(){
     //val s = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
     val s0 = "a"
@@ -577,7 +586,8 @@
     //correctness_proof_convenient_path()
     //retrieve_experience()
     //neat_retrieve()
-    test_bsimp2()
+    //test_bsimp2()
+    christian_def2()
     //christian_def()
     //essence_posix()
   }