600   /*

   601   lemma retrieve_encode_STARS:

   602   assumes "∀v∈set vs. ⊨ v : r ∧ code v = retrieve (intern r) v"

   603   shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"

   604   */

   605   def retrieve_encode_STARS(){

   606     val r =  ALT(CHAR('a'), SEQ(CHAR('a'),CHAR('b')) ) 

   607     //val v =  Stars(List(Sequ(Chr('a'), Chr('b')),  Chr('a')) )

   608     val v1 = Right(Sequ(Chr('a'), Chr('b')))

   609     val v2 = Left(Chr('a'))

   610     val compressed1 = code(v1)

   611     val compressed2 = code(v2)

   612     val xompressed1 = retrieve(internalise(r), v1)

   613     val xompressed2 = retrieve(internalise(r), v2)

   614     println(compressed1, compressed2, xompressed1, xompressed2)

   615     val v = Stars(List(v1, v2))

   616     val compressed = code(v)

   617     val a = ASTAR(List(), internalise(r))

   618     val xompressed = retrieve(a, v)

   619     println(compressed, xompressed)

   620   }

   621   //what does contains7 do?

   622   //it causes exception

   623   //relation between retreive, bder and injection

   624   // a match error occurs when doing the injection

   625   def contains7(){

   626     val r = STAR( SEQ(CHAR('a'),CHAR('b')) )

   627     val v = Sequ(Chr('b'), Stars(List(Sequ(Chr('a'), Chr('b')))))

   628     val a = internalise(r)

   629     val c = 'a'

   630     val v_aug = inj(r, c, v)

   631     println("bder c r:")

   632     println(bder(c, a))

   633     println("r:")

   634     println(a)

   635     println("bits they can both produce:")

   636     println(retrieve(a, v_aug))

   637   }

   638   def der_seq(r:ARexp, s: List[Char],acc: List[ARexp]) : List[ARexp] = s match{

   639     case Nil => acc ::: List(r)

   640     case c::cs => der_seq(bder(c, r), cs, acc ::: List(r))

   641   }

   642   def der_seq_rev(r:ARexp, s: List[Char], acc: List[ARexp]): List[ARexp] = s match{

   643     case Nil => r::acc

   644     case c::cs =>der_seq_rev(r, cs, bders(s, r) :: acc  )

   645   }

   646   def re_close(l1: List[ARexp], l2: List[ARexp], re_init: ARexp): ARexp = l1 match {

   647     case Nil => re_init

   648     case c::cs => if(bnullable(c)) re_close(cs, l2.tail, AALTS(List(), List(re_init, fuse(mkepsBC(c), l2.head)) ) ) 

   649     else re_close(cs, l2.tail, re_init)

   650   }

   651   def closed_string_der(r1: ARexp, r2: ARexp, s: String): ARexp = {

   652     val l1 = der_seq(r1, s.toList, Nil)

   653     val l2 = der_seq_rev(r2, s.toList, Nil)

   654     val Re = re_close(l1.reverse, l2, ASEQ(List(), l1.last, l2.head))

   655     print(Re)

   656     val Comp = bders( s.toList, ASEQ(List(), r1, r2))

   657     print(Comp  )

   658     if(Re != Comp){

   659       println("boooooooooooooooo!joihniuguyfuyftyftyufuyids gheioueghrigdhxilj")

   660     }

   661     Re

   662   }

   663   def newxp1(){

   664     val r1 = internalise("ab"|"")

   665     val r2 = internalise(("b")%)

   666     val s = "abbbbb"

   667     val s2= "bbbbb"

   668     val s3 = "aaaaaa"

   669     //closed_string_der(r1, r2, s)

   670     //closed_string_der(r1, r2, s2)

   671     closed_string_der(r1, r2, s3)

   672   }

   674     newxp1()

   675   //contains7()

   676   //retrieve_encode_STARS()