619 text {*

   619 text {*

   620   The following lemma tries to derive the Hoare logic rule for sequentially combined TMs.

   620   The following lemma tries to derive the Hoare logic rule for sequentially combined TMs.

   621   It deals with the situtation when both @{text "A"} and @{text "B"} are terminated.

   621   It deals with the situtation when both @{text "A"} and @{text "B"} are terminated.

   622 *}

   622 *}

   623 

   623 

   624 lemma t_merge_halt: 

   626 lemma t_merge_halt: 

   625   assumes aimpb: "Q1 \<turnstile>-> P2"

   627   assumes aimpb: "Q1 \<turnstile>-> P2"

   626   shows "P1 \<turnstile>->  \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (A |+| B)  stp = (0, tp') \<and> Q2 tp')"

   628   shows "P1 \<turnstile>->  \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (A |+| B)  stp = (0, tp') \<and> Q2 tp')"

   627 proof(simp add: t_imply_def, auto)

   629 proof(simp add: t_imply_def, auto)

   628   fix a b

   630   fix a b