1447 lemma neg:

  1448   shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and>  (r2 \<leadsto>* bsimp r1) )"

  1449   apply(rule notI)

  1450   apply(erule exE)

  1451   apply(erule conjE)

  1452   oops

  1453 

  1454 

  1455 

  1456 

  1457 lemma reduction_always_in_bsimp:

  1458   shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False"

  1459   apply(erule rrewrite.cases)

  1460          apply simp

  1461         apply auto

  1462 

  1463   oops

  1464 

  1465 (*

  1466 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] 

  1467 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto>

  1468 fuse [] (AALTs bs1, [a, b])

  1469 rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ]

  1470 

  1471 *)

  1472 

  1473 lemma normal_bsimp: 

  1474   shows "\<nexists>r'. bsimp r \<leadsto> r'"

  1475   oops

  1476 

  1477   (*r' size bsimp r > size r' 

  1478     r' \<leadsto>* bsimp bsimp r

  1479 size bsimp r > size r' \<ge> size bsimp bsimp r*)

  1480