242    apply(erule exE)+

   242    apply(erule exE)+

   243    apply simp

   243    apply simp

   244   apply simp

   244   apply simp

   245   by(meson neq_Nil_conv)

   245   by(meson neq_Nil_conv)

   246   

   246   

   247 

   250 

   248 

   251 

   249 

   252 

   250 

   253 

   251 lemma rSEQ_mono:

   254 lemma rSEQ_mono:

  1136 

  1139 

  1137 lemma head_one_more_simp:

  1140 lemma head_one_more_simp:

  1138   shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"

  1141   shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"

  1139   by (simp add: rsimp_idem)

  1142   by (simp add: rsimp_idem)

  1140 

  1143 

  1142   shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"

  1145   shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"

  1143   using head_one_more_simp rders_simp_append rders_simp_one_char by presburger

  1146   using head_one_more_simp rders_simp_append rders_simp_one_char by presburger

  1144 

  1147 

  1145 

  1148 

  1146 

  1149