[STATEMENT]
lemma add_single_BK_to_left_tape:
  "\<lbrace>\<lambda>tap. tap = ([]  , <(m::nat, m)> ) \<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @Bk\<up>l )\<rbrace>
  \<Longrightarrow>
   \<lbrace>\<lambda>tap. tap = ([Bk], <(m     , m)> ) \<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @Bk\<up>l )\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
assume    "\<lbrace>\<lambda>tap. tap = ([], <(m::nat, m)> ) \<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have  "\<forall>z.\<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m::nat, m)> ) \<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
using Hoare_halt_add_Bks_left_tape_L1 Hoare_halt_add_Bks_left_tape
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
\<lbrace>\<lambda>tap. tap = ([], ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<forall>z. \<exists>stp k l. steps0 (1, Bk \<up> z, ?r) ?p stp = (0, Bk \<up> k, ?CR @ Bk \<up> l)
\<lbrace>\<lambda>tap. tap = ([], ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have  "\<lbrace>\<lambda>tap. tap = (Bk \<up> 1, <(m::nat, m)> ) \<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<forall>z. \<lbrace>\<lambda>tap. tap = (Bk \<up> z, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = (Bk \<up> 1, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = (Bk \<up> 1, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = (Bk \<up> 1, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = (Bk \<up> 1, <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (simp add: Hoare_haltE Hoare_haltI)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([Bk], <(m, m)>)\<rbrace> p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, r' @ Bk \<up> l)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma existence_of_decider_H2D0_for_H2_imp_False:
  assumes "\<exists>H2D0'. (\<forall>nl (tm::instr list).
          ((tm,nl) \<in> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk\<up>l)\<rbrace>)
       \<and>  ((tm,nl) \<notin> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>) )"
  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>H2D0'. \<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)
[PROOF STEP]
obtain H2D0' where
    w_H2D0': "(\<forall>nl (tm::instr list).
          ((tm,nl) \<in> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>)
       \<and>  ((tm,nl) \<notin> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>) )"
[PROOF STATE]
proof (prove)
using this:
\<exists>H2D0'. \<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)

goal (1 subgoal):
 1. (\<And>H2D0'. \<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)

goal (1 subgoal):
 1. False
[PROOF STEP]
(* first, create a composable version of the arbitrary and thus potentially non-composable machine H2D0' *)
[PROOF STATE]
proof (state)
this:
\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)
[PROOF STEP]
have "composable_tm0 (mk_composable0 H2D0') \<and> (\<forall>nl (tm::instr list).
          ((tm,nl) \<in> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>)
       \<and>  ((tm,nl) \<notin> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>) )"
[PROOF STATE]
proof (prove)
using this:
\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)

goal (1 subgoal):
 1. composable_tm0 (mk_composable0 H2D0') \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
by (auto simp add: Hoare_halt_tm_impl_Hoare_halt_mk_composable0_cell_list composable_tm0_mk_composable0 )
[PROOF STATE]
proof (state)
this:
composable_tm0 (mk_composable0 H2D0') \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
composable_tm0 (mk_composable0 H2D0') \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
have "\<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl (tm::instr list).
          ((tm,nl) \<in> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace>  H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>)
       \<and>  ((tm,nl) \<notin> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>) )"
[PROOF STATE]
proof (prove)
using this:
composable_tm0 (mk_composable0 H2D0') \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> mk_composable0 H2D0' \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. \<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. False
[PROOF STEP]
(* here we obtain the composable variant H2D0 of  H2D0' *)
[PROOF STATE]
proof (state)
this:
\<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
obtain H2D0 where w_H2D0: "composable_tm0 H2D0 \<and> (\<forall>nl (tm::instr list).
          ((tm,nl) \<in> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace>  H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>)
       \<and>  ((tm,nl) \<notin> H2 \<longrightarrow>\<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>) )"
[PROOF STATE]
proof (prove)
using this:
\<exists>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. (\<And>H2D0. composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. False
[PROOF STEP]
(* define the culprit tm_contra from the diagonal by using tm_copy and tm_dither *)
[PROOF STATE]
proof (state)
this:
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. False
[PROOF STEP]
define tm_contra where "tm_contra = (tm_copy |+| H2D0 |+| tm_dither)"
[PROOF STATE]
proof (state)
this:
tm_contra = tm_copy |+| H2D0 |+| tm_dither

goal (1 subgoal):
 1. False
[PROOF STEP]
from w_H2D0
[PROOF STATE]
proof (chain)
picking this:
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
have H_composable: "composable_tm0 (tm_copy |+| H2D0)"
[PROOF STATE]
proof (prove)
using this:
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. composable_tm0 (tm_copy |+| H2D0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
composable_tm0 (tm_copy |+| H2D0)

goal (1 subgoal):
 1. False
[PROOF STEP]
(* the stage is set: now, we derive the contradiction *)
[PROOF STATE]
proof (state)
this:
composable_tm0 (tm_copy |+| H2D0)

goal (1 subgoal):
 1. False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "(tm_contra, [code tm_contra]) \<in> H2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (tm_contra, [code tm_contra]) \<in> H2 \<Longrightarrow> False
 2. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(tm_contra, [code tm_contra]) \<in> H2

goal (2 subgoals):
 1. (tm_contra, [code tm_contra]) \<in> H2 \<Longrightarrow> False
 2. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<in> H2
[PROOF STEP]
have "(tm_contra, [code tm_contra]) \<in> H2"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<in> H2

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<in> H2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(tm_contra, [code tm_contra]) \<in> H2

goal (2 subgoals):
 1. (tm_contra, [code tm_contra]) \<in> H2 \<Longrightarrow> False
 2. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<in> H2
[PROOF STEP]
have inH2: "TMC_has_num_res tm_contra [code tm_contra]"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<in> H2

goal (1 subgoal):
 1. TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
by (auto simp add: H2_def)
[PROOF STATE]
proof (state)
this:
TMC_has_num_res tm_contra [code tm_contra]

goal (2 subgoals):
 1. (tm_contra, [code tm_contra]) \<in> H2 \<Longrightarrow> False
 2. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
(* (tm_contra, [code tm_contra]) \<in> H2  \<Longrightarrow> (tm_contra, [code tm_contra]) \<notin> H2 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
(* assertions *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
define P1 where "P1 \<equiv> \<lambda>tap. tap = ([]::cell list, <code tm_contra>)"
[PROOF STATE]
proof (state)
this:
P1 \<equiv> \<lambda>tap. tap = ([], <code tm_contra>)

goal (1 subgoal):
 1. False
[PROOF STEP]
define P2 where "P2 \<equiv> \<lambda>tap. tap = ([Bk]::cell list, <(code tm_contra, code tm_contra)>)"
[PROOF STATE]
proof (state)
this:
P2 \<equiv> \<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)

goal (1 subgoal):
 1. False
[PROOF STEP]
define Q3 where "Q3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)"
[PROOF STATE]
proof (state)
this:
Q3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. False
[PROOF STEP]
(* the play book for derivation of the contradiction,
   for the case: (tm_contra, [code tm_contra]) \<in> H2

         \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>  \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
         ---------------------------------
         first: \<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>Q3\<rbrace>    second: \<lbrace>Q3\<rbrace> tm_dither loops
         -------------------------------------------------------------------
                        \<lbrace>P1\<rbrace> tm_contra loops
*)

(* from \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>  \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>   show  first: \<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>Q3\<rbrace> *)
[PROOF STATE]
proof (state)
this:
Q3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. False
[PROOF STEP]
have first: "\<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>Q3\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>Q3\<rbrace>
[PROOF STEP]
proof (cases rule: Hoare_plus_halt)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
case A_halt
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
(* of tm_copy *)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
show "\<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>
[PROOF STEP]
unfolding P1_def P2_def tape_of_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> Suc (code tm_contra))\<rbrace> tm_copy \<lbrace>\<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)\<rbrace>
[PROOF STEP]
by (rule tm_copy_correct)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
case B_halt
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
(* of H2D0 *)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
from \<open>(tm_contra, [code tm_contra]) \<in> H2\<close> and w_H2D0
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<in> H2
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
have      "\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])> ) \<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<in> H2
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)  > ) \<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (simp add: Hoare_haltE Hoare_haltI tape_of_list_def tape_of_prod_def)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
show "\<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>
[PROOF STEP]
unfolding P2_def Q3_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
using add_single_BK_to_left_tape
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
\<lbrace>\<lambda>tap. tap = ([], <(?m, ?m)>)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?r' @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([Bk], <(?m, ?m)>)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?r' @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrace>P2\<rbrace> H2D0 \<lbrace>Q3\<rbrace>

goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
show "composable_tm0 tm_copy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
composable_tm0 tm_copy

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>Q3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* second: \<lbrace>P3\<rbrace> tm_dither loops *)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>Q3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
have second: "\<lbrace>Q3\<rbrace> tm_dither \<up>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q3\<rbrace> tm_dither \<up>
[PROOF STEP]
unfolding Q3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace> tm_dither \<up>
[PROOF STEP]
using tm_dither_loops''
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace> tm_dither \<up>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace> tm_dither \<up>
[PROOF STEP]
by (simp add: tape_of_nat_def )
[PROOF STATE]
proof (state)
this:
\<lbrace>Q3\<rbrace> tm_dither \<up>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* from first and second show  \<lbrace>P1\<rbrace> tm_contra loops *)
[PROOF STATE]
proof (state)
this:
\<lbrace>Q3\<rbrace> tm_dither \<up>

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<lbrace>P1\<rbrace> tm_contra \<up>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_contra \<up>
[PROOF STEP]
unfolding tm_contra_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy |+| H2D0 |+| tm_dither \<up>
[PROOF STEP]
by (rule Hoare_plus_unhalt[OF first second H_composable])
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_contra \<up>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* from \<lbrace>P1\<rbrace> tm_contra \<up>   show  \<not>TMC_has_num_res tm_contra [code tm_contra] *)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_contra \<up>

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>P1\<rbrace> tm_contra \<up>
[PROOF STEP]
have "\<not>TMC_has_num_res tm_contra [code tm_contra]"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>P1\<rbrace> tm_contra \<up>

goal (1 subgoal):
 1. \<not> TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
unfolding P1_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <code tm_contra>)\<rbrace> tm_contra \<up>

goal (1 subgoal):
 1. \<not> TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
by (metis (mono_tags) Hoare_halt_impl_not_Hoare_unhalt
                  TMC_has_num_res_def inH2 tape_of_list_def tape_of_nat_list.simps(2))
[PROOF STATE]
proof (state)
this:
\<not> TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
(* thus have contradiction *)
[PROOF STATE]
proof (state)
this:
\<not> TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
with inH2
[PROOF STATE]
proof (chain)
picking this:
TMC_has_num_res tm_contra [code tm_contra]
\<not> TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
TMC_has_num_res tm_contra [code tm_contra]
\<not> TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(tm_contra, [code tm_contra]) \<notin> H2

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<notin> H2
[PROOF STEP]
have "(tm_contra, [code tm_contra]) \<notin> H2"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<notin> H2

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(tm_contra, [code tm_contra]) \<notin> H2

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<notin> H2
[PROOF STEP]
have not_inH2: "\<not>TMC_has_num_res tm_contra [code tm_contra]"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<notin> H2

goal (1 subgoal):
 1. \<not> TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
by (auto simp add: H2_def)
[PROOF STATE]
proof (state)
this:
\<not> TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
(* (tm_contra, [code tm_contra]) \<notin> H2 \<Longrightarrow> (tm_contra, [code tm_contra]) \<in> H2 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
(* assertions *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
define P1 where "P1 \<equiv> \<lambda>tap. tap = ([]::cell list, <code tm_contra>)"
[PROOF STATE]
proof (state)
this:
P1 \<equiv> \<lambda>tap. tap = ([], <code tm_contra>)

goal (1 subgoal):
 1. False
[PROOF STEP]
define P2 where "P2 \<equiv> \<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)"
[PROOF STATE]
proof (state)
this:
P2 \<equiv> \<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)

goal (1 subgoal):
 1. False
[PROOF STEP]
define P3 where "P3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l )"
[PROOF STATE]
proof (state)
this:
P3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. False
[PROOF STEP]
(* the play book for derivation of the contradiction,
   for the case: (tm_contra, [code tm_contra]) \<notin> H2

         \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>  \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
         --------------------------------
         first: \<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>P3\<rbrace>   second: \<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>
         ----------------------------------------------------------------
                           \<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>
*)

(* from \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>  \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>     show    first: \<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>P3\<rbrace> *)
[PROOF STATE]
proof (state)
this:
P3 \<equiv> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. False
[PROOF STEP]
have first: "\<lbrace>P1\<rbrace> (tm_copy |+| H2D0) \<lbrace>P3\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>
[PROOF STEP]
proof (cases rule: Hoare_plus_halt)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
case A_halt
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
(* of tm_copy *)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>?Q\<rbrace>
 2. \<lbrace>?Q\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 3. composable_tm0 tm_copy
[PROOF STEP]
show "\<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>
[PROOF STEP]
unfolding P1_def P2_def tape_of_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> Suc (code tm_contra))\<rbrace> tm_copy \<lbrace>\<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)\<rbrace>
[PROOF STEP]
by (rule tm_copy_correct)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy \<lbrace>P2\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
case B_halt
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
(* of H2D0 *)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
from \<open>(tm_contra, [code tm_contra]) \<notin> H2\<close> and w_H2D0
[PROOF STATE]
proof (chain)
picking this:
(tm_contra, [code tm_contra]) \<notin> H2
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))
[PROOF STEP]
have      "\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])> ) \<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
(tm_contra, [code tm_contra]) \<notin> H2
composable_tm0 H2D0 \<and> (\<forall>nl tm. ((tm, nl) \<in> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>) \<and> ((tm, nl) \<notin> H2 \<longrightarrow> \<lbrace>\<lambda>tap. tap = ([], <(code tm, nl)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>))

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)  > ) \<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, [code tm_contra])>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (simp add: Hoare_haltE Hoare_haltI tape_of_list_def tape_of_prod_def)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (2 subgoals):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
 2. composable_tm0 tm_copy
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
show "\<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>
[PROOF STEP]
unfolding P2_def P3_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([Bk], <(code tm_contra, code tm_contra)>)\<rbrace> H2D0 \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (rule add_single_BK_to_left_tape)
[PROOF STATE]
proof (state)
this:
\<lbrace>P2\<rbrace> H2D0 \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
show "composable_tm0 tm_copy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composable_tm0 tm_copy
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
composable_tm0 tm_copy

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* second: \<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace> *)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
from tm_dither_halts
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @Bk\<up>l)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @Bk\<up>l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @ Bk \<up> l)
[PROOF STEP]
by (metis One_nat_def tm_dither_halts_aux Suc_1 append.right_neutral replicate.simps(1) )
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k. tap = (Bk \<up> k, <1>)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @ Bk \<up> l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @ Bk \<up> l)

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
using Hoare_halt_add_Bks_left_tape_L2 Hoare_halt_del_Bks_left_tape
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>l. steps0 (1, Bk \<up> n, [Oc, Oc]) tm_dither (Suc 1) = (0, Bk \<up> n, [Oc, Oc] @ Bk \<up> l)
\<forall>z. \<exists>stp k l. steps0 (1, Bk \<up> z, ?r) ?p stp = (0, Bk \<up> k, ?CR @ Bk \<up> l) \<Longrightarrow> \<lbrace>\<lambda>tap. \<exists>z. tap = (Bk \<up> z, ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace>
\<lbrace>\<lambda>tap. \<exists>z. tap = (Bk \<up> z, ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. tap = ([], ?r)\<rbrace> ?p \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, ?CR @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have second: "\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>
[PROOF STEP]
unfolding P3_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "Oc # [Oc] = [Oc, Oc]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Oc, Oc] = [Oc, Oc]
[PROOF STEP]
using One_nat_def replicate_Suc tape_of_nat_def
[PROOF STATE]
proof (prove)
using this:
1 = Suc 0
?x \<up> Suc ?n = ?x # ?x \<up> ?n
<?n> \<equiv> Oc \<up> Suc ?n

goal (1 subgoal):
 1. [Oc, Oc] = [Oc, Oc]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[Oc, Oc] = [Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], [Oc, Oc])\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Oc, Oc] = [Oc, Oc]
[PROOF STEP]
show "\<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace> tm_dither \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
[Oc, Oc] = [Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace> tm_dither \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace>
[PROOF STEP]
using tm_dither_halts''
[PROOF STATE]
proof (prove)
using this:
[Oc, Oc] = [Oc, Oc]
\<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace> tm_dither \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace> tm_dither \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace> tm_dither \<lbrace>\<lambda>p. \<exists>n na. p = (Bk \<up> n, [Oc, Oc] @ Bk \<up> na)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* from first and second show  \<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace> *)
[PROOF STATE]
proof (state)
this:
\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
with first
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>
\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>
[PROOF STEP]
have "\<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>
\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>
[PROOF STEP]
unfolding tm_contra_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>P1\<rbrace> tm_copy |+| H2D0 \<lbrace>P3\<rbrace>
\<lbrace>P3\<rbrace> tm_dither \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P1\<rbrace> tm_copy |+| H2D0 |+| tm_dither \<lbrace>P3\<rbrace>
[PROOF STEP]
proof (rule Hoare_plus_halt)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. composable_tm0 (tm_copy |+| H2D0)
[PROOF STEP]
from H_composable
[PROOF STATE]
proof (chain)
picking this:
composable_tm0 (tm_copy |+| H2D0)
[PROOF STEP]
show "composable_tm0 (tm_copy |+| H2D0)"
[PROOF STATE]
proof (prove)
using this:
composable_tm0 (tm_copy |+| H2D0)

goal (1 subgoal):
 1. composable_tm0 (tm_copy |+| H2D0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
composable_tm0 (tm_copy |+| H2D0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
(* from  \<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>    show    TMC_has_num_res tm_contra [code tm_contra] *)
[PROOF STATE]
proof (state)
this:
\<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>
[PROOF STEP]
have "TMC_has_num_res tm_contra [code tm_contra]"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>P1\<rbrace> tm_contra \<lbrace>P3\<rbrace>

goal (1 subgoal):
 1. TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
unfolding P1_def P3_def
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <code tm_contra>)\<rbrace> tm_contra \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc, Oc] @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
by (simp add: Hoare_haltE Hoare_haltI Hoare_halt_with_OcOc_imp_std_tap tape_of_list_def)
[PROOF STATE]
proof (state)
this:
TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
(* thus have contradiction *)
[PROOF STATE]
proof (state)
this:
TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
with not_inH2
[PROOF STATE]
proof (chain)
picking this:
\<not> TMC_has_num_res tm_contra [code tm_contra]
TMC_has_num_res tm_contra [code tm_contra]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> TMC_has_num_res tm_contra [code tm_contra]
TMC_has_num_res tm_contra [code tm_contra]

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma it_sum'_rule[sep_heap_rules]:
  "<is_it l p l' it>
    it_sum' it s
  <\<lambda>r. is_list l p * \<up>(r = s + sum_list l')>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t
[PROOF STEP]
proof (induct l' arbitrary: it s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>it s. <is_it l p [] it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list [])>\<^sub>t
 2. \<And>a l' it s. (\<And>it s. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <is_it l p (a # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>it s. <is_it l p [] it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list [])>\<^sub>t
 2. \<And>a l' it s. (\<And>it s. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <is_it l p (a # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it l p [] it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list [])>\<^sub>t
[PROOF STEP]
apply (subst it_sum'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it l p [] it> it_has_next it \<bind> (\<lambda>b. if b then it_next it \<bind> (\<lambda>(x, it'). it_sum' it' (s + x)) else return s) <\<lambda>r. is_list l p * \<up> (r = s + sum_list [])>\<^sub>t
[PROOF STEP]
apply (sep_auto intro: quit_iteration ent_true_drop(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<is_it l p [] it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list [])>\<^sub>t

goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <is_it l p (a # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <is_it l p (a # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
case (Cons x l')
[PROOF STATE]
proof (state)
this:
<is_it l p l' ?it> it_sum' ?it ?s <\<lambda>r. is_list l p * \<up> (r = ?s + sum_list l')>\<^sub>t

goal (1 subgoal):
 1. \<And>a l' it s. (\<And>it s. <is_it l p l' it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list l')>\<^sub>t) \<Longrightarrow> <is_it l p (a # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (a # l'))>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it l p (x # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t
[PROOF STEP]
apply (subst it_sum'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it l p (x # l') it> it_has_next it \<bind> (\<lambda>b. if b then it_next it \<bind> (\<lambda>(x, it'). it_sum' it' (s + x)) else return s) <\<lambda>r. is_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t
[PROOF STEP]
apply (sep_auto heap: Cons.hyps simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<is_it l p (x # l') it> it_sum' it s <\<lambda>r. is_list l p * \<up> (r = s + sum_list (x # l'))>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma it_sum_rule[sep_heap_rules]:
  "<is_list l p> it_sum p <\<lambda>r. is_list l p * \<up>(r=sum_list l)>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_list l p> it_sum p <\<lambda>r. is_list l p * \<up> (r = sum_list l)>\<^sub>t
[PROOF STEP]
unfolding it_sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_list l p> it_init p \<bind> (\<lambda>it. it_sum' it (0::'a)) <\<lambda>r. is_list l p * \<up> (r = sum_list l)>\<^sub>t
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma  nodes_connected_sym: "nodes_connected G a b = nodes_connected G b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected G a b = nodes_connected G b a
[PROOF STEP]
using is_path_undir_sym
[PROOF STATE]
proof (prove)
using this:
is_path_undir G ?v ?p ?v' \<Longrightarrow> is_path_undir G ?v' (rev (map (\<lambda>(u, w, u'). (u', w, u)) ?p)) ?v

goal (1 subgoal):
 1. nodes_connected G a b = nodes_connected G b a
[PROOF STEP]
by auto


[STATEMENT]
lemma  Domain_nodes_connected: "Domain {(x, y) |x y. nodes_connected G x y} = V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domain {(x, y) |x y. nodes_connected G x y} = V
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> V \<Longrightarrow> \<exists>y. nodes_connected G x y
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> \<exists>y. nodes_connected G x y
[PROOF STEP]
apply(rule exI[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> nodes_connected G x x
[PROOF STEP]
apply(rule exI[where x="[]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> is_path_undir G x [] x
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  Range_nodes_connected: "Range {(x, y) |x y. nodes_connected G x y} = V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range {(x, y) |x y. nodes_connected G x y} = V
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> V \<Longrightarrow> \<exists>xa. nodes_connected G xa x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> \<exists>xa. nodes_connected G xa x
[PROOF STEP]
apply(rule exI[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> nodes_connected G x x
[PROOF STEP]
apply(rule exI[where x="[]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> is_path_undir G x [] x
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done

\<comment> \<open>adaptation of a proof by Julian Biendarra\<close>


[STATEMENT]
lemma   nodes_connected_insert_per_union:
  "(nodes_connected (add_edge a w b H) x y) \<longleftrightarrow> (x,y) \<in> per_union {(x,y)| x y. nodes_connected H x y} a b"
  if  "subgraph H G" and PER: "part_equiv {(x,y)| x y. nodes_connected H x y}"
    and V: "a\<in>V" "b\<in>V" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
let ?uf = "{(x,y)| x y. nodes_connected H x y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
from valid_subgraph[OF \<open>subgraph H G\<close>]
[PROOF STATE]
proof (chain)
picking this:
valid_graph H
[PROOF STEP]
have valid_H: "valid_graph H"
[PROOF STATE]
proof (prove)
using this:
valid_graph H

goal (1 subgoal):
 1. valid_graph H
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
valid_graph H

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
from \<open>subgraph H G\<close>
[PROOF STATE]
proof (chain)
picking this:
subgraph H G
[PROOF STEP]
have nodes_H: "nodes H = V"
[PROOF STATE]
proof (prove)
using this:
subgraph H G

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
nodes H = V \<and> edges H \<subseteq> E

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nodes H = V

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
with \<open>a\<in>V\<close> \<open>b\<in>V\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
nodes H = V
[PROOF STEP]
have nodes_add_H: "nodes (add_edge a w b H) = nodes H"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
nodes H = V

goal (1 subgoal):
 1. nodes (add_edge a w b H) = nodes H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes (add_edge a w b H) = nodes H

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
have "Domain ?uf = nodes H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domain {(x, y) |x y. nodes_connected H x y} = nodes H
[PROOF STEP]
using valid_graph.Domain_nodes_connected[OF valid_H]
[PROOF STATE]
proof (prove)
using this:
Domain {(x, y) |x y. nodes_connected H x y} = nodes H

goal (1 subgoal):
 1. Domain {(x, y) |x y. nodes_connected H x y} = nodes H
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Domain {(x, y) |x y. nodes_connected H x y} = nodes H

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nodes_connected (add_edge a w b H) x y \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
assume "nodes_connected (add_edge a w b H) x y"
[PROOF STATE]
proof (state)
this:
nodes_connected (add_edge a w b H) x y

goal (2 subgoals):
 1. nodes_connected (add_edge a w b H) x y \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nodes_connected (add_edge a w b H) x y
[PROOF STEP]
obtain p where p: "is_path_undir (add_edge a w b H) x p y"
[PROOF STATE]
proof (prove)
using this:
nodes_connected (add_edge a w b H) x y

goal (1 subgoal):
 1. (\<And>p. is_path_undir (add_edge a w b H) x p y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path_undir (add_edge a w b H) x p y

goal (2 subgoals):
 1. nodes_connected (add_edge a w b H) x y \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
from \<open>a\<in>V\<close> \<open>b\<in>V\<close> \<open>Domain {(x,y)| x y. nodes_connected H x y} = nodes H\<close> nodes_H
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
nodes H = V
[PROOF STEP]
have [simp]: "a\<in>Domain (per_union ?uf a b)" "b\<in>Domain (per_union ?uf a b)"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
nodes H = V

goal (1 subgoal):
 1. a \<in> Domain (per_union {(x, y) |x y. nodes_connected H x y} a b) &&& b \<in> Domain (per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> Domain (per_union {(x, y) |x y. nodes_connected H x y} a b)
b \<in> Domain (per_union {(x, y) |x y. nodes_connected H x y} a b)

goal (2 subgoals):
 1. nodes_connected (add_edge a w b H) x y \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
from PER
[PROOF STATE]
proof (chain)
picking this:
part_equiv {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have PER': "part_equiv (per_union ?uf a b)"
[PROOF STATE]
proof (prove)
using this:
part_equiv {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. part_equiv (per_union {(x, y) |x y. nodes_connected H x y} a b)
[PROOF STEP]
by (auto simp: union_part_equivp)
[PROOF STATE]
proof (state)
this:
part_equiv (per_union {(x, y) |x y. nodes_connected H x y} a b)

goal (2 subgoals):
 1. nodes_connected (add_edge a w b H) x y \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
show "(x,y) \<in> per_union ?uf a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
proof (cases "(a, w, b) \<in> set p \<or> (b, w, a) \<in> set p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(a, w, b) \<in> set p \<or> (b, w, a) \<in> set p

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
from valid_graph.is_path_undir_split_distinct[OF add_edge_valid[OF valid_H] p True]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p' p'' u u'. is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y \<and> length p' < length p \<and> length p'' < length p \<and> (u \<in> {a, b} \<and> u' \<in> {a, b}) \<and> (a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''
[PROOF STEP]
obtain p' p'' u u' where
        "is_path_undir (add_edge a w b H) x p' u \<and>
        is_path_undir (add_edge a w b H) u' p'' y" and
        u: "u\<in>{a,b} \<and> u'\<in>{a,b}" and
        "(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and>
        (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''"
[PROOF STATE]
proof (prove)
using this:
\<exists>p' p'' u u'. is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y \<and> length p' < length p \<and> length p'' < length p \<and> (u \<in> {a, b} \<and> u' \<in> {a, b}) \<and> (a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''

goal (1 subgoal):
 1. (\<And>p' u u' p''. \<lbrakk>is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y; u \<in> {a, b} \<and> u' \<in> {a, b}; (a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y
u \<in> {a, b} \<and> u' \<in> {a, b}
(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
with \<open>a\<in>V\<close> \<open>b\<in>V\<close> \<open>Domain ?uf = nodes H\<close> \<open>subgraph H G\<close>
        valid_graph.add_edge_was_path[OF valid_H]
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
subgraph H G
\<lbrakk>is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y; (?a, ?b, ?c) \<notin> set ?p; (?c, ?b, ?a) \<notin> set ?p; ?a \<in> nodes H; ?c \<in> nodes H\<rbrakk> \<Longrightarrow> is_path_undir H ?x ?p ?y
is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y
u \<in> {a, b} \<and> u' \<in> {a, b}
(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''
[PROOF STEP]
have "is_path_undir H x p' u \<and> is_path_undir H u' p'' y"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
subgraph H G
\<lbrakk>is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y; (?a, ?b, ?c) \<notin> set ?p; (?c, ?b, ?a) \<notin> set ?p; ?a \<in> nodes H; ?c \<in> nodes H\<rbrakk> \<Longrightarrow> is_path_undir H ?x ?p ?y
is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y
u \<in> {a, b} \<and> u' \<in> {a, b}
(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''

goal (1 subgoal):
 1. is_path_undir H x p' u \<and> is_path_undir H u' p'' y
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
nodes H = V \<and> edges H \<subseteq> E
\<lbrakk>is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y; (?a, ?b, ?c) \<notin> set ?p; (?c, ?b, ?a) \<notin> set ?p; ?a \<in> nodes H; ?c \<in> nodes H\<rbrakk> \<Longrightarrow> is_path_undir H ?x ?p ?y
is_path_undir (add_edge a w b H) x p' u \<and> is_path_undir (add_edge a w b H) u' p'' y
u \<in> {a, b} \<and> u' \<in> {a, b}
(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''

goal (1 subgoal):
 1. is_path_undir H x p' u \<and> is_path_undir H u' p'' y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir H x p' u \<and> is_path_undir H u' p'' y

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
with V  u nodes_H
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
u \<in> {a, b} \<and> u' \<in> {a, b}
nodes H = V
is_path_undir H x p' u \<and> is_path_undir H u' p'' y
[PROOF STEP]
have comps: "(x,u) \<in> ?uf \<and> (u', y) \<in> ?uf"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
u \<in> {a, b} \<and> u' \<in> {a, b}
nodes H = V
is_path_undir H x p' u \<and> is_path_undir H u' p'' y

goal (1 subgoal):
 1. (x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
from comps
[PROOF STATE]
proof (chain)
picking this:
(x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have "(x,u) \<in> per_union ?uf a b"
[PROOF STATE]
proof (prove)
using this:
(x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (x, u) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
apply(intro per_union_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> (x, u) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, u) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x, u) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
from u \<open>a\<in>V\<close> \<open>b\<in>V\<close> \<open>Domain ?uf = nodes H\<close> nodes_H
        part_equiv_refl'[OF PER' \<open>a\<in>Domain (per_union ?uf a b)\<close>]
        part_equiv_refl'[OF PER' \<open>b\<in>Domain (per_union ?uf a b)\<close>] part_equiv_sym[OF PER']
        per_union_related[OF PER]
[PROOF STATE]
proof (chain)
picking this:
u \<in> {a, b} \<and> u' \<in> {a, b}
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
nodes H = V
(a, a) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(b, b) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(?x, ?y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> (?y, ?x) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
\<lbrakk>?a \<in> Domain {(x, y) |x y. nodes_connected H x y}; ?b \<in> Domain {(x, y) |x y. nodes_connected H x y}\<rbrakk> \<Longrightarrow> (?a, ?b) \<in> per_union {(x, y) |x y. nodes_connected H x y} ?a ?b
[PROOF STEP]
have "(u,u') \<in> per_union ?uf a b"
[PROOF STATE]
proof (prove)
using this:
u \<in> {a, b} \<and> u' \<in> {a, b}
a \<in> V
b \<in> V
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
nodes H = V
(a, a) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(b, b) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(?x, ?y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> (?y, ?x) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
\<lbrakk>?a \<in> Domain {(x, y) |x y. nodes_connected H x y}; ?b \<in> Domain {(x, y) |x y. nodes_connected H x y}\<rbrakk> \<Longrightarrow> (?a, ?b) \<in> per_union {(x, y) |x y. nodes_connected H x y} ?a ?b

goal (1 subgoal):
 1. (u, u') \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, u') \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
also (part_equiv_trans[OF PER'])
[PROOF STATE]
proof (state)
this:
(u, u') \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
from comps
[PROOF STATE]
proof (chain)
picking this:
(x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have "(u',y) \<in> per_union ?uf a b"
[PROOF STATE]
proof (prove)
using this:
(x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (u', y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
apply(intro per_union_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, u) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (u', y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> (u', y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u', y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (2 subgoals):
 1. (a, w, b) \<in> set p \<or> (b, w, a) \<in> set p \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
 2. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
finally (part_equiv_trans[OF PER'])
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (1 subgoal):
 1. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p)

goal (1 subgoal):
 1. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
with \<open>a\<in>V\<close> \<open>b\<in>V\<close> nodes_H valid_graph.add_edge_was_path[OF valid_H p(1)]
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
nodes H = V
\<lbrakk>(a, w, b) \<notin> set p; (b, w, a) \<notin> set p; a \<in> nodes H; b \<in> nodes H\<rbrakk> \<Longrightarrow> is_path_undir H x p y
\<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p)
[PROOF STEP]
have "is_path_undir H x p y"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
nodes H = V
\<lbrakk>(a, w, b) \<notin> set p; (b, w, a) \<notin> set p; a \<in> nodes H; b \<in> nodes H\<rbrakk> \<Longrightarrow> is_path_undir H x p y
\<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p)

goal (1 subgoal):
 1. is_path_undir H x p y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir H x p y

goal (1 subgoal):
 1. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
with     nodes_add_H
[PROOF STATE]
proof (chain)
picking this:
nodes (add_edge a w b H) = nodes H
is_path_undir H x p y
[PROOF STEP]
have "(x,y)\<in>?uf"
[PROOF STATE]
proof (prove)
using this:
nodes (add_edge a w b H) = nodes H
is_path_undir H x p y

goal (1 subgoal):
 1. (x, y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. \<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p) \<Longrightarrow> (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
from per_union_impl[OF this]
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} ?a ?b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} ?a ?b

goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
assume asm: "(x, y) \<in> per_union ?uf a b"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b

goal (1 subgoal):
 1. (x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
show "nodes_connected (add_edge a w b H) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y
[PROOF STEP]
proof (cases "(x, y) \<in> ?uf")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
 2. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (2 subgoals):
 1. (x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
 2. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with nodes_add_H
[PROOF STATE]
proof (chain)
picking this:
nodes (add_edge a w b H) = nodes H
(x, y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have "nodes_connected H x y"
[PROOF STATE]
proof (prove)
using this:
nodes (add_edge a w b H) = nodes H
(x, y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. nodes_connected H x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes_connected H x y

goal (2 subgoals):
 1. (x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
 2. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with valid_graph.add_edge_is_path[OF valid_H]
[PROOF STATE]
proof (chain)
picking this:
is_path_undir H ?x ?p ?y \<Longrightarrow> is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y
nodes_connected H x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_path_undir H ?x ?p ?y \<Longrightarrow> is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y
nodes_connected H x y

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nodes_connected (add_edge a w b H) x y

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(x, y) \<notin> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with asm part_equiv_sym[OF PER]
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(?x, ?y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> (?y, ?x) \<in> {(x, y) |x y. nodes_connected H x y}
(x, y) \<notin> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have "(x,a) \<in> ?uf \<and> (b,y) \<in> ?uf \<or>
              (x,b) \<in> ?uf \<and> (a,y) \<in> ?uf"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b
(?x, ?y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> (?y, ?x) \<in> {(x, y) |x y. nodes_connected H x y}
(x, y) \<notin> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (b, y) \<in> {(x, y) |x y. nodes_connected H x y} \<or> (x, b) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (a, y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
unfolding per_union_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<union> {(x, y). (x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (y, b) \<in> {(x, y) |x y. nodes_connected H x y}} \<union> {(y, x). (x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (y, b) \<in> {(x, y) |x y. nodes_connected H x y}}
(?x, ?y) \<in> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> (?y, ?x) \<in> {(x, y) |x y. nodes_connected H x y}
(x, y) \<notin> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (b, y) \<in> {(x, y) |x y. nodes_connected H x y} \<or> (x, b) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (a, y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (b, y) \<in> {(x, y) |x y. nodes_connected H x y} \<or> (x, b) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (a, y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with  \<open>a\<in>V\<close> \<open>b\<in>V\<close> nodes_H nodes_add_H
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
b \<in> V
nodes H = V
nodes (add_edge a w b H) = nodes H
(x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (b, y) \<in> {(x, y) |x y. nodes_connected H x y} \<or> (x, b) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (a, y) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
obtain p q p' q'
          where "is_path_undir H x p a \<and> is_path_undir H b q y \<or>
                 is_path_undir H x p' b \<and> is_path_undir H a q' y"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
b \<in> V
nodes H = V
nodes (add_edge a w b H) = nodes H
(x, a) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (b, y) \<in> {(x, y) |x y. nodes_connected H x y} \<or> (x, b) \<in> {(x, y) |x y. nodes_connected H x y} \<and> (a, y) \<in> {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. (\<And>p q p' q'. is_path_undir H x p a \<and> is_path_undir H b q y \<or> is_path_undir H x p' b \<and> is_path_undir H a q' y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_path_undir H x p a \<and> is_path_undir H b q y \<or> is_path_undir H x p' b \<and> is_path_undir H a q' y

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with valid_graph.add_edge_is_path[OF valid_H]
[PROOF STATE]
proof (chain)
picking this:
is_path_undir H ?x ?p ?y \<Longrightarrow> is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y
is_path_undir H x p a \<and> is_path_undir H b q y \<or> is_path_undir H x p' b \<and> is_path_undir H a q' y
[PROOF STEP]
have "is_path_undir (add_edge a w b H) x p a \<and>
              is_path_undir (add_edge a w b H) b q y \<or>
              is_path_undir (add_edge a w b H) x p' b \<and>
              is_path_undir (add_edge a w b H) a q' y"
[PROOF STATE]
proof (prove)
using this:
is_path_undir H ?x ?p ?y \<Longrightarrow> is_path_undir (add_edge ?a ?b ?c H) ?x ?p ?y
is_path_undir H x p a \<and> is_path_undir H b q y \<or> is_path_undir H x p' b \<and> is_path_undir H a q' y

goal (1 subgoal):
 1. is_path_undir (add_edge a w b H) x p a \<and> is_path_undir (add_edge a w b H) b q y \<or> is_path_undir (add_edge a w b H) x p' b \<and> is_path_undir (add_edge a w b H) a q' y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path_undir (add_edge a w b H) x p a \<and> is_path_undir (add_edge a w b H) b q y \<or> is_path_undir (add_edge a w b H) x p' b \<and> is_path_undir (add_edge a w b H) a q' y

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with valid_graph.is_path_undir_split'[OF add_edge_valid[OF valid_H]]
[PROOF STATE]
proof (chain)
picking this:
is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v (?p1.0 @ (?u, ?w, ?u') # ?p2.0) ?v' = (is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v ?p1.0 ?u \<and> ((?u, ?w, ?u') \<in> edges (add_edge ?v1 ?e1 ?v'1 H) \<or> (?u', ?w, ?u) \<in> edges (add_edge ?v1 ?e1 ?v'1 H)) \<and> is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?u' ?p2.0 ?v')
is_path_undir (add_edge a w b H) x p a \<and> is_path_undir (add_edge a w b H) b q y \<or> is_path_undir (add_edge a w b H) x p' b \<and> is_path_undir (add_edge a w b H) a q' y
[PROOF STEP]
have "is_path_undir (add_edge a w b H) x (p @ (a, w, b) # q) y \<or>
              is_path_undir (add_edge a w b H) x (p' @ (b, w, a) # q') y"
[PROOF STATE]
proof (prove)
using this:
is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v (?p1.0 @ (?u, ?w, ?u') # ?p2.0) ?v' = (is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v ?p1.0 ?u \<and> ((?u, ?w, ?u') \<in> edges (add_edge ?v1 ?e1 ?v'1 H) \<or> (?u', ?w, ?u) \<in> edges (add_edge ?v1 ?e1 ?v'1 H)) \<and> is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?u' ?p2.0 ?v')
is_path_undir (add_edge a w b H) x p a \<and> is_path_undir (add_edge a w b H) b q y \<or> is_path_undir (add_edge a w b H) x p' b \<and> is_path_undir (add_edge a w b H) a q' y

goal (1 subgoal):
 1. is_path_undir (add_edge a w b H) x (p @ (a, w, b) # q) y \<or> is_path_undir (add_edge a w b H) x (p' @ (b, w, a) # q') y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir (add_edge a w b H) x (p @ (a, w, b) # q) y \<or> is_path_undir (add_edge a w b H) x (p' @ (b, w, a) # q') y

goal (1 subgoal):
 1. (x, y) \<notin> {(x, y) |x y. nodes_connected H x y} \<Longrightarrow> nodes_connected (add_edge a w b H) x y
[PROOF STEP]
with valid_graph.is_path_undir_sym[OF add_edge_valid[OF valid_H]]
[PROOF STATE]
proof (chain)
picking this:
is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v ?p ?v' \<Longrightarrow> is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v' (rev (map (\<lambda>(u, w, u'). (u', w, u)) ?p)) ?v
is_path_undir (add_edge a w b H) x (p @ (a, w, b) # q) y \<or> is_path_undir (add_edge a w b H) x (p' @ (b, w, a) # q') y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v ?p ?v' \<Longrightarrow> is_path_undir (add_edge ?v1 ?e1 ?v'1 H) ?v' (rev (map (\<lambda>(u, w, u'). (u', w, u)) ?p)) ?v
is_path_undir (add_edge a w b H) x (p @ (a, w, b) # q) y \<or> is_path_undir (add_edge a w b H) x (p' @ (b, w, a) # q') y

goal (1 subgoal):
 1. nodes_connected (add_edge a w b H) x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nodes_connected (add_edge a w b H) x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nodes_connected (add_edge a w b H) x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nodes_connected (add_edge a w b H) x y = ((x, y) \<in> per_union {(x, y) |x y. nodes_connected H x y} a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  is_path_undir_append: "is_path_undir G v p1 u \<Longrightarrow> is_path_undir G u p2 w
      \<Longrightarrow> is_path_undir G v (p1@p2) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path_undir G v p1 u; is_path_undir G u p2 w\<rbrakk> \<Longrightarrow> is_path_undir G v (p1 @ p2) w
[PROOF STEP]
using is_path_undir_split
[PROOF STATE]
proof (prove)
using this:
is_path_undir G ?v (?p1.0 @ ?p2.0) ?v' = (\<exists>u. is_path_undir G ?v ?p1.0 u \<and> is_path_undir G u ?p2.0 ?v')

goal (1 subgoal):
 1. \<lbrakk>is_path_undir G v p1 u; is_path_undir G u p2 w\<rbrakk> \<Longrightarrow> is_path_undir G v (p1 @ p2) w
[PROOF STEP]
by auto