[STATEMENT]
lemma (in wf_digraph) awalk_del_vert:
  "\<lbrakk> awalk u p v; x \<notin> set (awalk_verts u p) \<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v
[PROOF STEP]
proof(induction p arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
awalk u [] v
x \<notin> set (awalk_verts u [])

goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk u [] v
x \<notin> set (awalk_verts u [])
[PROOF STEP]
have "set (awalk_verts u []) = {u}"
[PROOF STATE]
proof (prove)
using this:
awalk u [] v
x \<notin> set (awalk_verts u [])

goal (1 subgoal):
 1. set (awalk_verts u []) = {u}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (awalk_verts u []) = {u}

goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
with Nil
[PROOF STATE]
proof (chain)
picking this:
awalk u [] v
x \<notin> set (awalk_verts u [])
set (awalk_verts u []) = {u}
[PROOF STEP]
have "x \<noteq> u"
[PROOF STATE]
proof (prove)
using this:
awalk u [] v
x \<notin> set (awalk_verts u [])
set (awalk_verts u []) = {u}

goal (1 subgoal):
 1. x \<noteq> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<noteq> u

goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> u

goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
from Nil
[PROOF STATE]
proof (chain)
picking this:
awalk u [] v
x \<notin> set (awalk_verts u [])
[PROOF STEP]
have "u = v"
[PROOF STATE]
proof (prove)
using this:
awalk u [] v
x \<notin> set (awalk_verts u [])

goal (1 subgoal):
 1. u = v
[PROOF STEP]
unfolding awalk_def
[PROOF STATE]
proof (prove)
using this:
u \<in> verts G \<and> set [] \<subseteq> arcs G \<and> cas u [] v
x \<notin> set (awalk_verts u [])

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

goal (2 subgoals):
 1. \<And>u. \<lbrakk>awalk u [] v; x \<notin> set (awalk_verts u [])\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u [] v
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> u
u = v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
u = v

goal (1 subgoal):
 1. pre_digraph.awalk (del_vert x) u [] v
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
u = v
awalk u [] v
x \<notin> set (awalk_verts u [])

goal (1 subgoal):
 1. pre_digraph.awalk (del_vert x) u [] v
[PROOF STEP]
by (simp add: awalk_hd_in_verts pre_digraph.verts_del_vert
        wf_digraph.awalk_Nil_iff wf_digraph_del_vert)
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk (del_vert x) u [] v

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>awalk ?u2 p v; x \<notin> set (awalk_verts ?u2 p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) ?u2 p v
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>awalk ?u2 p v; x \<notin> set (awalk_verts ?u2 p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) ?u2 p v
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
obtain u' where u': "pre_digraph.awalk (del_vert x) u' p v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>awalk ?u2 p v; x \<notin> set (awalk_verts ?u2 p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) ?u2 p v
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))

goal (1 subgoal):
 1. (\<And>u'. pre_digraph.awalk (del_vert x) u' p v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using awalk_Cons_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>awalk ?u2 p v; x \<notin> set (awalk_verts ?u2 p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) ?u2 p v
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))
awalk ?u (?e # ?es) ?w = (?e \<in> arcs G \<and> ?u = tail G ?e \<and> awalk (head G ?e) ?es ?w)

goal (1 subgoal):
 1. (\<And>u'. pre_digraph.awalk (del_vert x) u' p v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk (del_vert x) u' p v

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk (del_vert x) u' p v

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
have "head G a \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))

goal (1 subgoal):
 1. head G a \<noteq> x
[PROOF STEP]
using hd_in_awalk_verts(1) awalk_Cons_iff
[PROOF STATE]
proof (prove)
using this:
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))
awalk ?u ?p ?v \<Longrightarrow> ?u \<in> set (awalk_verts ?u ?p)
awalk ?u (?e # ?es) ?w = (?e \<in> arcs G \<and> ?u = tail G ?e \<and> awalk (head G ?e) ?es ?w)

goal (1 subgoal):
 1. head G a \<noteq> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
head G a \<noteq> x

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>awalk u p v; x \<notin> set (awalk_verts u p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u p v; awalk u (a # p) v; x \<notin> set (awalk_verts u (a # p))\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.awalk (del_vert x) u' p v
head G a \<noteq> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk (del_vert x) u' p v
head G a \<noteq> x

goal (1 subgoal):
 1. pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk (del_vert x) u' p v
head G a \<noteq> x
\<lbrakk>awalk ?u2 p v; x \<notin> set (awalk_verts ?u2 p)\<rbrakk> \<Longrightarrow> pre_digraph.awalk (del_vert x) ?u2 p v
awalk u (a # p) v
x \<notin> set (awalk_verts u (a # p))

goal (1 subgoal):
 1. pre_digraph.awalk (del_vert x) u (a # p) v
[PROOF STEP]
by (auto simp: awalk_Cons_iff head_del_vert pre_digraph.del_vert_simps(2)
        tail_del_vert wf_digraph.awalk_Cons_iff wf_digraph_del_vert)
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk (del_vert x) u (a # p) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pre_digraph) arcs_del_vert2:
  "arcs (del_vert v) = arcs G - in_arcs G v - out_arcs G v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcs (del_vert v) = arcs G - in_arcs G v - out_arcs G v
[PROOF STEP]
using arcs_del_vert
[PROOF STATE]
proof (prove)
using this:
arcs (del_vert ?u) = {a \<in> arcs G. tail G a \<noteq> ?u \<and> head G a \<noteq> ?u}

goal (1 subgoal):
 1. arcs (del_vert v) = arcs G - in_arcs G v - out_arcs G v
[PROOF STEP]
by force


[STATEMENT]
lemma (in wf_digraph) strongly_con_imp_reachable_eq_verts:
  "\<lbrakk> r \<in> verts G; strongly_connected G \<rbrakk> \<Longrightarrow> {x. r \<rightarrow>\<^sup>* x} = verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; strongly_connected G\<rbrakk> \<Longrightarrow> {x. r \<rightarrow>\<^sup>* x} = verts G
[PROOF STEP]
unfolding strongly_connected_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; verts G \<noteq> {} \<and> (\<forall>u\<in>verts G. \<forall>v\<in>verts G. u \<rightarrow>\<^sup>* v)\<rbrakk> \<Longrightarrow> {x. r \<rightarrow>\<^sup>* x} = verts G
[PROOF STEP]
using reachable_in_verts(2)
[PROOF STATE]
proof (prove)
using this:
?u \<rightarrow>\<^sup>* ?v \<Longrightarrow> ?v \<in> verts G

goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; verts G \<noteq> {} \<and> (\<forall>u\<in>verts G. \<forall>v\<in>verts G. u \<rightarrow>\<^sup>* v)\<rbrakk> \<Longrightarrow> {x. r \<rightarrow>\<^sup>* x} = verts G
[PROOF STEP]
by blast


[STATEMENT]
lemma (in wf_digraph) strongly_con_imp_sp_finite:
  "\<lbrakk> u \<in> verts G; v \<in> verts G; strongly_connected G \<rbrakk> \<Longrightarrow> \<mu> w u v < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> verts G; v \<in> verts G; strongly_connected G\<rbrakk> \<Longrightarrow> \<mu> w u v < \<infinity>
[PROOF STEP]
unfolding strongly_connected_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> verts G; v \<in> verts G; verts G \<noteq> {} \<and> (\<forall>u\<in>verts G. \<forall>v\<in>verts G. u \<rightarrow>\<^sup>* v)\<rbrakk> \<Longrightarrow> \<mu> w u v < \<infinity>
[PROOF STEP]
using \<mu>_reach_conv
[PROOF STATE]
proof (prove)
using this:
(\<mu> ?f ?u ?v < \<infinity>) = (?u \<rightarrow>\<^sup>* ?v)

goal (1 subgoal):
 1. \<lbrakk>u \<in> verts G; v \<in> verts G; verts G \<noteq> {} \<and> (\<forall>u\<in>verts G. \<forall>v\<in>verts G. u \<rightarrow>\<^sup>* v)\<rbrakk> \<Longrightarrow> \<mu> w u v < \<infinity>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in fin_digraph) min_cost_awalk2:
  assumes "\<mu> w a b \<noteq> \<infinity>" "\<mu> w a b \<noteq> -\<infinity>"
  shows "\<exists>p. apath a p b \<and> \<mu> w a b = awalk_cost w p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>
[PROOF STEP]
have "a \<rightarrow>\<^sup>* b"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* b
[PROOF STEP]
using \<mu>_reach_conv
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>
(\<mu> ?f ?u ?v < \<infinity>) = (?u \<rightarrow>\<^sup>* ?v)

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<rightarrow>\<^sup>* b

goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<rightarrow>\<^sup>* b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b

goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
using no_neg_cyc_reach_imp_path
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b
\<lbrakk>?u \<rightarrow>\<^sup>* ?v; \<And>p. awalk ?u p ?v \<Longrightarrow> \<nexists>w c. awalk w c w \<and> w \<in> set (awalk_verts ?u p) \<and> awalk_cost ?f c < 0\<rbrakk> \<Longrightarrow> \<exists>p. apath ?u p ?v \<and> \<mu> ?f ?u ?v = ereal (awalk_cost ?f p)

goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
using assms(2) neg_cycle_imp_inf_\<mu>
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b
\<lbrakk>?u \<rightarrow>\<^sup>* ?v; \<And>p. awalk ?u p ?v \<Longrightarrow> \<nexists>w c. awalk w c w \<and> w \<in> set (awalk_verts ?u p) \<and> awalk_cost ?f c < 0\<rbrakk> \<Longrightarrow> \<exists>p. apath ?u p ?v \<and> \<mu> ?f ?u ?v = ereal (awalk_cost ?f p)
\<mu> w a b \<noteq> - \<infinity>
\<lbrakk>awalk ?u ?p ?v; awalk ?w ?c ?w; ?w \<in> set (awalk_verts ?u ?p); awalk_cost ?f ?c < 0\<rbrakk> \<Longrightarrow> \<mu> ?f ?u ?v = - \<infinity>

goal (1 subgoal):
 1. \<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. apath a p b \<and> \<mu> w a b = ereal (awalk_cost w p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in fin_digraph) sp_triangle:
  assumes "a \<in> verts G" "b \<in> verts G" "c \<in> verts G"
      and w_non_neg: "\<forall>e \<in> arcs G. w e \<ge> 0"
    shows "\<mu> w a c \<le> \<mu> w a b + \<mu> w b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> w a c \<le> \<mu> w a b + \<mu> w b c
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c \<Longrightarrow> False
[PROOF STEP]
assume "\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c"
[PROOF STATE]
proof (state)
this:
\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c

goal (1 subgoal):
 1. \<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c
[PROOF STEP]
have *: "\<mu> w a c > \<mu> w a b + \<mu> w b c"
[PROOF STATE]
proof (prove)
using this:
\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c

goal (1 subgoal):
 1. \<mu> w a b + \<mu> w b c < \<mu> w a c
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<mu> w a b + \<mu> w b c < \<mu> w a c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> w a b + \<mu> w b c < \<mu> w a c

goal (1 subgoal):
 1. \<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c \<Longrightarrow> False
[PROOF STEP]
consider (minf) "\<mu> w a c = -\<infinity>" | (pinf) "\<mu> w a c = \<infinity>"
    | (fin) "\<mu> w a c \<noteq> -\<infinity> \<and> \<mu> w a c \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<mu> w a c = - \<infinity> \<Longrightarrow> thesis; \<mu> w a c = \<infinity> \<Longrightarrow> thesis; \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<mu> w a c = - \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c = \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (1 subgoal):
 1. \<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<mu> w a c = - \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c = \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<mu> w a c = - \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c = \<infinity> \<Longrightarrow> ?thesis2; \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<mu> w a c = - \<infinity> \<Longrightarrow> False
 2. \<mu> w a c = \<infinity> \<Longrightarrow> False
 3. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
case minf
[PROOF STATE]
proof (state)
this:
\<mu> w a c = - \<infinity>

goal (3 subgoals):
 1. \<mu> w a c = - \<infinity> \<Longrightarrow> False
 2. \<mu> w a c = \<infinity> \<Longrightarrow> False
 3. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c = - \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c = - \<infinity>

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

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
case pinf
[PROOF STATE]
proof (state)
this:
\<mu> w a c = \<infinity>

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c = \<infinity>
[PROOF STEP]
have "\<mu> w a b < \<infinity>" "\<mu> w b c < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c = \<infinity>

goal (1 subgoal):
 1. \<mu> w a b < \<infinity> &&& \<mu> w b c < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w a b < \<infinity>
\<mu> w b c < \<infinity>

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b < \<infinity>
\<mu> w b c < \<infinity>
[PROOF STEP]
have "a \<rightarrow>\<^sup>* b" "b \<rightarrow>\<^sup>* c"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b < \<infinity>
\<mu> w b c < \<infinity>

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* b &&& b \<rightarrow>\<^sup>* c
[PROOF STEP]
using \<mu>_reach_conv
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b < \<infinity>
\<mu> w b c < \<infinity>
(\<mu> ?f ?u ?v < \<infinity>) = (?u \<rightarrow>\<^sup>* ?v)

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* b &&& b \<rightarrow>\<^sup>* c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<rightarrow>\<^sup>* b
b \<rightarrow>\<^sup>* c

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<rightarrow>\<^sup>* b
b \<rightarrow>\<^sup>* c
[PROOF STEP]
have "a \<rightarrow>\<^sup>* c"
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b
b \<rightarrow>\<^sup>* c

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* c
[PROOF STEP]
using reachable_trans
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b
b \<rightarrow>\<^sup>* c
\<lbrakk>?u \<rightarrow>\<^sup>* ?v; ?v \<rightarrow>\<^sup>* ?w\<rbrakk> \<Longrightarrow> ?u \<rightarrow>\<^sup>* ?w

goal (1 subgoal):
 1. a \<rightarrow>\<^sup>* c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<rightarrow>\<^sup>* c

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<rightarrow>\<^sup>* c
[PROOF STEP]
have "\<mu> w a c \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* c

goal (1 subgoal):
 1. \<mu> w a c \<noteq> \<infinity>
[PROOF STEP]
using \<mu>_reach_conv
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* c
(\<mu> ?f ?u ?v < \<infinity>) = (?u \<rightarrow>\<^sup>* ?v)

goal (1 subgoal):
 1. \<mu> w a c \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w a c \<noteq> \<infinity>

goal (2 subgoals):
 1. \<mu> w a c = \<infinity> \<Longrightarrow> False
 2. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
with pinf
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a c = \<infinity>
\<mu> w a c \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> w a c = \<infinity>
\<mu> w a c \<noteq> \<infinity>

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

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
case fin
[PROOF STATE]
proof (state)
this:
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>
[PROOF STEP]
have "\<mu> w a b \<noteq> \<infinity>" "\<mu> w b c \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>

goal (1 subgoal):
 1. \<mu> w a b \<noteq> \<infinity> &&& \<mu> w b c \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w b c \<noteq> \<infinity>

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w b c \<noteq> \<infinity>

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
from fin *
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>
\<mu> w a b + \<mu> w b c < \<mu> w a c
[PROOF STEP]
have "\<mu> w a b \<noteq> -\<infinity>" "\<mu> w b c \<noteq> -\<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>
\<mu> w a b + \<mu> w b c < \<mu> w a c

goal (1 subgoal):
 1. \<mu> w a b \<noteq> - \<infinity> &&& \<mu> w b c \<noteq> - \<infinity>
[PROOF STEP]
using w_non_neg sp_non_neg_if_w_non_neg
[PROOF STATE]
proof (prove)
using this:
\<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity>
\<mu> w a b + \<mu> w b c < \<mu> w a c
\<forall>e\<in>arcs G. 0 \<le> w e
\<forall>e\<in>arcs G. 0 \<le> ?w e \<Longrightarrow> 0 \<le> \<mu> ?w ?u ?v

goal (1 subgoal):
 1. \<mu> w a b \<noteq> - \<infinity> &&& \<mu> w b c \<noteq> - \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w a b \<noteq> - \<infinity>
\<mu> w b c \<noteq> - \<infinity>

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w b c \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>
\<mu> w b c \<noteq> - \<infinity>
[PROOF STEP]
have
      "\<exists>p. awalk a p b \<and> awalk_cost w p = \<mu> w a b"
      "\<exists>p. awalk b p c \<and> awalk_cost w p = \<mu> w b c"
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w b c \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>
\<mu> w b c \<noteq> - \<infinity>

goal (1 subgoal):
 1. \<exists>p. awalk a p b \<and> ereal (awalk_cost w p) = \<mu> w a b &&& \<exists>p. awalk b p c \<and> ereal (awalk_cost w p) = \<mu> w b c
[PROOF STEP]
using min_cost_awalk2
[PROOF STATE]
proof (prove)
using this:
\<mu> w a b \<noteq> \<infinity>
\<mu> w b c \<noteq> \<infinity>
\<mu> w a b \<noteq> - \<infinity>
\<mu> w b c \<noteq> - \<infinity>
\<lbrakk>\<mu> ?w ?a ?b \<noteq> \<infinity>; \<mu> ?w ?a ?b \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> \<exists>p. apath ?a p ?b \<and> \<mu> ?w ?a ?b = ereal (awalk_cost ?w p)

goal (1 subgoal):
 1. \<exists>p. awalk a p b \<and> ereal (awalk_cost w p) = \<mu> w a b &&& \<exists>p. awalk b p c \<and> ereal (awalk_cost w p) = \<mu> w b c
[PROOF STEP]
by (fastforce intro: awalkI_apath)+
[PROOF STATE]
proof (state)
this:
\<exists>p. awalk a p b \<and> ereal (awalk_cost w p) = \<mu> w a b
\<exists>p. awalk b p c \<and> ereal (awalk_cost w p) = \<mu> w b c

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. awalk a p b \<and> ereal (awalk_cost w p) = \<mu> w a b
\<exists>p. awalk b p c \<and> ereal (awalk_cost w p) = \<mu> w b c
[PROOF STEP]
obtain p1 p2 where
        "awalk a p1 b" "awalk_cost w p1 = \<mu> w a b" and
        "awalk b p2 c" "awalk_cost w p2 = \<mu> w b c"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. awalk a p b \<and> ereal (awalk_cost w p) = \<mu> w a b
\<exists>p. awalk b p c \<and> ereal (awalk_cost w p) = \<mu> w b c

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>awalk a p1 b; ereal (awalk_cost w p1) = \<mu> w a b; awalk b p2 c; ereal (awalk_cost w p2) = \<mu> w b c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
awalk a p1 b
ereal (awalk_cost w p1) = \<mu> w a b
awalk b p2 c
ereal (awalk_cost w p2) = \<mu> w b c

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk a p1 b
ereal (awalk_cost w p1) = \<mu> w a b
awalk b p2 c
ereal (awalk_cost w p2) = \<mu> w b c
[PROOF STEP]
have "awalk a (p1@p2) c \<and> awalk_cost w (p1@p2) = \<mu> w a b + \<mu> w b c"
[PROOF STATE]
proof (prove)
using this:
awalk a p1 b
ereal (awalk_cost w p1) = \<mu> w a b
awalk b p2 c
ereal (awalk_cost w p2) = \<mu> w b c

goal (1 subgoal):
 1. awalk a (p1 @ p2) c \<and> ereal (awalk_cost w (p1 @ p2)) = \<mu> w a b + \<mu> w b c
[PROOF STEP]
by (auto intro: awalk_appendI) (metis plus_ereal.simps(1))
[PROOF STATE]
proof (state)
this:
awalk a (p1 @ p2) c \<and> ereal (awalk_cost w (p1 @ p2)) = \<mu> w a b + \<mu> w b c

goal (1 subgoal):
 1. \<mu> w a c \<noteq> - \<infinity> \<and> \<mu> w a c \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk a (p1 @ p2) c \<and> ereal (awalk_cost w (p1 @ p2)) = \<mu> w a b + \<mu> w b c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
awalk a (p1 @ p2) c \<and> ereal (awalk_cost w (p1 @ p2)) = \<mu> w a b + \<mu> w b c

goal (1 subgoal):
 1. False
[PROOF STEP]
using min_cost_le_walk_cost
[PROOF STATE]
proof (prove)
using this:
awalk a (p1 @ p2) c \<and> ereal (awalk_cost w (p1 @ p2)) = \<mu> w a b + \<mu> w b c
awalk ?u ?p ?v \<Longrightarrow> \<mu> ?c ?u ?v \<le> ereal (awalk_cost ?c ?p)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>\<not> \<mu> w a c \<le> \<mu> w a b + \<mu> w b c\<close>)
[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 domain_make_vert:"domain_block (make_vert_block n) = int n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (make_vert_block n) = int n
[PROOF STEP]
by (induction n) (auto)


[STATEMENT]
lemma codomain_make_vert:"codomain_block (make_vert_block n) = int n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block n) = int n
[PROOF STEP]
by (induction n) (auto)


[STATEMENT]
lemma Nil_right_tensor:"(basic ([])) \<otimes> xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basic [] \<otimes> xs = xs
[PROOF STEP]
by (cases xs) (auto)


[STATEMENT]
lemma "tensor (basic [vert]) (basic ([vert])) = (basic (([vert]) \<otimes> ([vert])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basic [vert] \<otimes> basic [vert] = basic ([vert] \<otimes> [vert])
[PROOF STEP]
by simp


[STATEMENT]
lemma tensor_domain_wall_additivity:
 "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. xs = basic x1 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. xs = basic x1 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume A:"xs = basic x"
[PROOF STATE]
proof (state)
this:
xs = basic x

goal (2 subgoals):
 1. \<And>x1. xs = basic x1 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = basic x
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
using this:
xs = basic x

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
proof(cases ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = basic x; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = basic x; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume B:"ys = basic y"
[PROOF STATE]
proof (state)
this:
ys = basic y

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = basic x; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (x \<otimes> y) = domain_block x + domain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (x \<otimes> y) = domain_block x + domain_block y
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (x \<otimes> y) = domain_block x + domain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (x \<otimes> y) = domain_block x + domain_block y

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = basic x; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_block (x \<otimes> y) = domain_block x + domain_block y
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
using this:
domain_block (x \<otimes> y) = domain_block x + domain_block y

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
using tensor.simps(1) A B
[PROOF STATE]
proof (prove)
using this:
domain_block (x \<otimes> y) = domain_block x + domain_block y
basic ?x \<otimes> basic ?y = basic (?x \<otimes> ?y)
xs = basic x
ys = basic y

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = basic x; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume C:"ys = (z*zs)"
[PROOF STATE]
proof (state)
this:
ys = z * zs

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
proof(cases "(codomain_block x) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume "codomain_block x = 0"
[PROOF STATE]
proof (state)
this:
codomain_block x = 0

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_block x = 0
[PROOF STEP]
have "(xs \<otimes> ys) = (x \<otimes> z)*zs"
[PROOF STATE]
proof (prove)
using this:
codomain_block x = 0

goal (1 subgoal):
 1. xs \<otimes> ys = (x \<otimes> z) * zs
[PROOF STEP]
using A C tensor.simps(4)
[PROOF STATE]
proof (prove)
using this:
codomain_block x = 0
xs = basic x
ys = z * zs
?x * ?xs \<otimes> ?y * ?ys = (?x \<otimes> ?y) * (?xs \<otimes> ?ys)

goal (1 subgoal):
 1. xs \<otimes> ys = (x \<otimes> z) * zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<otimes> ys = (x \<otimes> z) * zs

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<otimes> ys = (x \<otimes> z) * zs
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)"
[PROOF STATE]
proof (prove)
using this:
xs \<otimes> ys = (x \<otimes> z) * zs

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall ys = domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall ys = domain_block z
[PROOF STEP]
unfolding domain_wall_def C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (z * zs) = domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block z

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block z

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall xs = domain_block x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall xs = domain_block x
[PROOF STEP]
unfolding domain_wall_def A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (basic x) = domain_block x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block x

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block x

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (x \<otimes> z) = domain_block x + domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (x \<otimes> z) = domain_block x + domain_block z

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
domain_wall ys = domain_block z
domain_wall xs = domain_block x
domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
domain_wall ys = domain_block z
domain_wall xs = domain_block x
domain_block (x \<otimes> z) = domain_block x + domain_block z

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume "codomain_block x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
codomain_block x \<noteq> 0

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "(xs \<otimes> ys)
                 = (x \<otimes> z)
                    *((basic (make_vert_block (nat (codomain_block x))))\<otimes> zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> ys = (x \<otimes> z) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> zs)
[PROOF STEP]
using tensor.simps(3) A C \<open>codomain_block x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
basic ?x \<otimes> ?y * ?ys = (if codomain_block ?x = 0 then (?x \<otimes> ?y) * ?ys else (?x \<otimes> ?y) * (basic (make_vert_block (nat (codomain_block ?x))) \<otimes> ?ys))
xs = basic x
ys = z * zs
codomain_block x \<noteq> 0

goal (1 subgoal):
 1. xs \<otimes> ys = (x \<otimes> z) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> zs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<otimes> ys = (x \<otimes> z) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> zs)

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<otimes> ys = (x \<otimes> z) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> zs)
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)"
[PROOF STATE]
proof (prove)
using this:
xs \<otimes> ys = (x \<otimes> z) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> zs)

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall ys = domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall ys = domain_block z
[PROOF STEP]
unfolding domain_wall_def C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (z * zs) = domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block z

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block z

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall xs = domain_block x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall xs = domain_block x
[PROOF STEP]
unfolding domain_wall_def A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (basic x) = domain_block x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block x

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block x

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (x \<otimes> z) = domain_block x + domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (x \<otimes> z) = domain_block x + domain_block z

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
domain_wall ys = domain_block z
domain_wall xs = domain_block x
domain_block (x \<otimes> z) = domain_block x + domain_block z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_block (x \<otimes> z)
domain_wall ys = domain_block z
domain_wall xs = domain_block x
domain_block (x \<otimes> z) = domain_block x + domain_block z

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = basic x; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (2 subgoals):
 1. \<And>x1. xs = basic x1 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix z zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume D:"xs = z * zs"
[PROOF STATE]
proof (state)
this:
xs = z * zs

goal (1 subgoal):
 1. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = z * zs
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
using this:
xs = z * zs

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
proof(cases ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = z * zs; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = z * zs; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume E:"ys = basic y"
[PROOF STATE]
proof (state)
this:
ys = basic y

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = z * zs; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = basic y
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys"
[PROOF STATE]
proof (prove)
using this:
ys = basic y

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
proof(cases "codomain_block y = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume "codomain_block y = 0"
[PROOF STATE]
proof (state)
this:
codomain_block y = 0

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "(xs \<otimes> ys) = (z \<otimes> y)*zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> y) * zs
[PROOF STEP]
using tensor.simps(2)  D E \<open>codomain_block y = 0\<close>
[PROOF STATE]
proof (prove)
using this:
?x * ?xs \<otimes> basic ?y = (if codomain_block ?y = 0 then (?x \<otimes> ?y) * ?xs else (?x \<otimes> ?y) * (?xs \<otimes> basic (make_vert_block (nat (codomain_block ?y)))))
xs = z * zs
ys = basic y
codomain_block y = 0

goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> y) * zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<otimes> ys = (z \<otimes> y) * zs

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<otimes> ys = (z \<otimes> y) * zs
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)"
[PROOF STATE]
proof (prove)
using this:
xs \<otimes> ys = (z \<otimes> y) * zs

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall xs = domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall xs = domain_block z
[PROOF STEP]
unfolding domain_wall_def D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (z * zs) = domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall ys = domain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall ys = domain_block y
[PROOF STEP]
unfolding domain_wall_def E
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (basic y) = domain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block y

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block y

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (z \<otimes> y) = domain_block z + domain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (z \<otimes> y) = domain_block z + domain_block y

goal (2 subgoals):
 1. \<lbrakk>ys = basic y; codomain_block y = 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
domain_wall xs = domain_block z
domain_wall ys = domain_block y
domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
domain_wall xs = domain_block z
domain_wall ys = domain_block y
domain_block (z \<otimes> y) = domain_block z + domain_block y

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume "codomain_block y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
codomain_block y \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "(xs \<otimes> ys)
               =
                (z \<otimes> y)
                  *(zs\<otimes>(basic (make_vert_block (nat (codomain_block y)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> y) * (zs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
using tensor.simps(3) D E \<open>codomain_block y \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
basic ?x \<otimes> ?y * ?ys = (if codomain_block ?x = 0 then (?x \<otimes> ?y) * ?ys else (?x \<otimes> ?y) * (basic (make_vert_block (nat (codomain_block ?x))) \<otimes> ?ys))
xs = z * zs
ys = basic y
codomain_block y \<noteq> 0

goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> y) * (zs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<otimes> ys = (z \<otimes> y) * (zs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<otimes> ys = (z \<otimes> y) * (zs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)"
[PROOF STATE]
proof (prove)
using this:
xs \<otimes> ys = (z \<otimes> y) * (zs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall ys = domain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall ys = domain_block y
[PROOF STEP]
unfolding domain_wall_def E
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (basic y) = domain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block y

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block y

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall xs = domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall xs = domain_block z
[PROOF STEP]
unfolding domain_wall_def D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (z * zs) = domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (z \<otimes> y) = domain_block z + domain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (z \<otimes> y) = domain_block z + domain_block y

goal (1 subgoal):
 1. \<lbrakk>ys = basic y; codomain_block y \<noteq> 0\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
domain_wall ys = domain_block y
domain_wall xs = domain_block z
domain_block (z \<otimes> y) = domain_block z + domain_block y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> y)
domain_wall ys = domain_block y
domain_wall xs = domain_block z
domain_block (z \<otimes> y) = domain_block z + domain_block y

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>xs = z * zs; ys = basic x1\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
 2. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
fix w ws
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
assume F:"ys = w*ws"
[PROOF STATE]
proof (state)
this:
ys = w * ws

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "(xs \<otimes> ys) = (z \<otimes> w) * (zs \<otimes> ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> w) * (zs \<otimes> ws)
[PROOF STEP]
using D F
[PROOF STATE]
proof (prove)
using this:
xs = z * zs
ys = w * ws

goal (1 subgoal):
 1. xs \<otimes> ys = (z \<otimes> w) * (zs \<otimes> ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<otimes> ys = (z \<otimes> w) * (zs \<otimes> ws)

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<otimes> ys = (z \<otimes> w) * (zs \<otimes> ws)
[PROOF STEP]
have "domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)"
[PROOF STATE]
proof (prove)
using this:
xs \<otimes> ys = (z \<otimes> w) * (zs \<otimes> ws)

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall ys = domain_block w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall ys = domain_block w
[PROOF STEP]
unfolding domain_wall_def F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (w * ws) = domain_block w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block w

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall ys = domain_block w

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_wall xs = domain_block z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall xs = domain_block z
[PROOF STEP]
unfolding domain_wall_def D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_wall domain_block (\<lambda>x ys ysa. domain_block x) (z * zs) = domain_block z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall xs = domain_block z

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
have "domain_block (z \<otimes> w) = domain_block z + domain_block w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_block (z \<otimes> w) = domain_block z + domain_block w
[PROOF STEP]
using domain_additive
[PROOF STATE]
proof (prove)
using this:
domain_block (?x \<otimes> ?y) = domain_block ?x + domain_block ?y

goal (1 subgoal):
 1. domain_block (z \<otimes> w) = domain_block z + domain_block w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_block (z \<otimes> w) = domain_block z + domain_block w

goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>xs = z * zs; ys = x21 * x22\<rbrakk> \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)
domain_wall ys = domain_block w
domain_wall xs = domain_block z
domain_block (z \<otimes> w) = domain_block z + domain_block w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_block (z \<otimes> w)
domain_wall ys = domain_block w
domain_wall xs = domain_block z
domain_block (z \<otimes> w) = domain_block z + domain_block w

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. \<And>x21 x22. xs = x21 * x22 \<Longrightarrow> domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal (1 subgoal):
 1. domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> ys) = domain_wall xs + domain_wall ys

goal:
No subgoals!
[PROOF STEP]
qed