36   apply(simp)

    36   apply(simp)

    37   apply(auto)

    37   apply(auto)

    38   apply(rule_tac y="b" in list.exhaust)

    38   apply(rule_tac y="b" in list.exhaust)

    39   by(auto)

    39   by(auto)

    40 

    40 

    42   by (lexicographic_order)

    42   by (lexicographic_order)

    43 

    43 

    44 

    44 

    45 section {* The Synchronous Pi-Calculus *}

    45 section {* The Synchronous Pi-Calculus *}

    46 

    46 

   377   apply(simp add: eqvt_at_def)

   377   apply(simp add: eqvt_at_def)

   378   apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)

   378   apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)

   379   apply(simp)

   379   apply(simp)

   380   done

   380   done

   381 

   381 

   383   by (lexicographic_order)

   383   by (lexicographic_order)

   384 

   384 

   385 lemma forget_mix:

   385 lemma forget_mix:

   386   fixes g  :: guardedTerm_mix

   386   fixes g  :: guardedTerm_mix

   387   and   xg :: sumList_mix

   387   and   xg :: sumList_mix