1452 lemma neg:

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

  1454   apply(rule notI)

  1455   apply(erule exE)

  1456   apply(erule conjE)

  1457   oops

  1458 

  1459 

  1460 

  1461 

  1462 lemma reduction_always_in_bsimp:

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

  1464   apply(erule rrewrite.cases)

  1465          apply simp

  1466         apply auto

  1467 

  1468   oops

  1469 

  1470 (*

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

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

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

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

  1475 

  1476 *)

  1477 

  1478 lemma normal_bsimp: 

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

  1480   oops

  1481 

  1482   (*r' size bsimp r > size r' 

  1483     r' \<leadsto>* bsimp bsimp r

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

  1485