[STATEMENT]
lemma tensor_codomain_wall_additivity:
 "codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys
[PROOF STEP]
proof(induction xs ys  rule:tensor.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. codomain_wall (basic x \<otimes> basic y) = codomain_wall (basic x) + codomain_wall (basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 4. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. codomain_wall (basic x \<otimes> basic y) = codomain_wall (basic x) + codomain_wall (basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 4. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
let ?case = "(codomain_wall ((basic xs) \<otimes> (basic ys))
                       = (codomain_wall (basic (xs)))
                              + (codomain_wall (basic ys)))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. codomain_wall (basic x \<otimes> basic y) = codomain_wall (basic x) + codomain_wall (basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 4. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (basic xs \<otimes> basic ys) = codomain_wall (basic xs) + codomain_wall (basic ys)
[PROOF STEP]
using codomain_wall.simps codomain_block.simps tensor.simps
[PROOF STATE]
proof (prove)
using this:
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys
codomain_block [] = 0
codomain_block (?x # ?y) = codomain ?x + codomain_block ?y
basic ?x \<otimes> basic ?y = basic (?x \<otimes> ?y)
?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)))))
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))
?x * ?xs \<otimes> ?y * ?ys = (?x \<otimes> ?y) * (?xs \<otimes> ?ys)

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

goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 3. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 3. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
fix x xs y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 3. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
assume case_2:
         "codomain_block y \<noteq> 0
           \<Longrightarrow> codomain_wall
                (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
                  = codomain_wall xs
                     + codomain_wall
                          (basic (make_vert_block (nat (codomain_block y))))"
[PROOF STATE]
proof (state)
this:
codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))

goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 3. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
let ?case = "codomain_wall ((x*xs)\<otimes> (basic y))
                  = (codomain_wall (x*xs)) + (codomain_wall (basic y))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 3. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
proof(cases "(codomain_block y = 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. codomain_block y = 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
codomain_block y = 0

goal (2 subgoals):
 1. codomain_block y = 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
have "((x*xs)\<otimes> (basic y)) =  (x \<otimes> y)*xs "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * xs \<otimes> basic y = (x \<otimes> y) * xs
[PROOF STEP]
using "Tangle_Algebra.2" True
[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)))))
codomain_block y = 0

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

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

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

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

goal (1 subgoal):
 1. codomain_wall ((x \<otimes> y) * xs) = codomain_wall xs
[PROOF STEP]
using codomain_wall.simps
[PROOF STATE]
proof (prove)
using this:
codomain_wall (x * xs \<otimes> basic y) = codomain_wall ((x \<otimes> y) * xs)
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys

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

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

goal (1 subgoal):
 1. codomain_wall xs = codomain_wall xs + codomain_wall (basic y)
[PROOF STEP]
using True codomain_wall.simps(1)
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * xs) = codomain_wall xs
codomain_block y = 0
codomain_wall (basic ?x) = codomain_block ?x

goal (1 subgoal):
 1. codomain_wall xs = codomain_wall xs + codomain_wall (basic y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_wall xs = codomain_wall xs + codomain_wall (basic y)

goal (2 subgoals):
 1. codomain_block y = 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
 2. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_wall xs = codomain_wall xs + codomain_wall (basic y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
codomain_wall xs = codomain_wall xs + codomain_wall (basic y)

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

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
codomain_block y \<noteq> 0

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
have "(x*xs) \<otimes> (basic y)
                 = (x \<otimes> y)
                     *(xs\<otimes>(basic (make_vert_block (nat (codomain_block y)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
codomain_block y \<noteq> 0

goal (1 subgoal):
 1. x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
by (metis "Tangle_Algebra.2")
[PROOF STATE]
proof (state)
this:
x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

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

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

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_wall (x * xs \<otimes> basic y) = codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))

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

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

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) = codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
have "...
                  = codomain_wall xs
                     + codomain_wall
                          (basic (make_vert_block (nat (codomain_block y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
using case_2 False
[PROOF STATE]
proof (prove)
using this:
codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))
codomain_block y \<noteq> 0

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

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
have "... = codomain_wall (x*xs)
                       + codomain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y
[PROOF STEP]
using codomain_wall.simps
[PROOF STATE]
proof (prove)
using this:
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys

goal (1 subgoal):
 1. codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y
[PROOF STEP]
by (metis codomain_block_nonnegative   codomain_make_vert int_nat_eq)
[PROOF STATE]
proof (state)
this:
codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
have "... = codomain_wall (x*xs) + codomain_wall (basic y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (x * xs) + codomain_block y = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
using codomain_wall.simps(1)
[PROOF STATE]
proof (prove)
using this:
codomain_wall (basic ?x) = codomain_block ?x

goal (1 subgoal):
 1. codomain_wall (x * xs) + codomain_block y = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_wall (x * xs) + codomain_block y = codomain_wall (x * xs) + codomain_wall (basic y)

goal (1 subgoal):
 1. codomain_block y \<noteq> 0 \<Longrightarrow> codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
codomain_wall (x * xs \<otimes> basic y) = codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))
codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) = codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))
codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y
codomain_wall (x * xs) + codomain_block y = codomain_wall (x * xs) + codomain_wall (basic y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * xs \<otimes> basic y = (x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
codomain_wall (x * xs \<otimes> basic y) = codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))
codomain_wall ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) = codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
codomain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y))))
codomain_wall xs + codomain_wall (basic (make_vert_block (nat (codomain_block y)))) = codomain_wall (x * xs) + codomain_block y
codomain_wall (x * xs) + codomain_block y = codomain_wall (x * xs) + codomain_wall (basic y)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
codomain_wall (x * xs \<otimes> basic y) = codomain_wall (x * xs) + codomain_wall (basic y)

goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
fix x y ys
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
assume case_3:"(codomain_block x \<noteq> 0 \<Longrightarrow>
        codomain_wall
             (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)
            = codomain_wall
               (basic (make_vert_block (nat (codomain_block x))))
                  + codomain_wall ys)"
[PROOF STATE]
proof (state)
this:
codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys

goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
let ?case = "codomain_wall ((basic x) \<otimes> (y*ys))
                  = codomain_wall (basic x) + codomain_wall (y*ys)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys) \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
proof(cases "codomain_block x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
codomain_block x = 0

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
have "(basic x)\<otimes>(y*ys) = (x \<otimes> y)*ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basic x \<otimes> y * ys = (x \<otimes> y) * ys
[PROOF STEP]
using True 3
[PROOF STATE]
proof (prove)
using this:
codomain_block x = 0
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))

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

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

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

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

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

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

goal (1 subgoal):
 1. codomain_wall ys = codomain_wall ys + codomain_wall (basic x)
[PROOF STEP]
using codomain_wall.simps(1) True
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * ys) = codomain_wall ys
codomain_wall (basic ?x) = codomain_block ?x
codomain_block x = 0

goal (1 subgoal):
 1. codomain_wall ys = codomain_wall ys + codomain_wall (basic x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_wall ys = codomain_wall ys + codomain_wall (basic x)

goal (2 subgoals):
 1. codomain_block x = 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
 2. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_wall ys = codomain_wall ys + codomain_wall (basic x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
codomain_wall ys = codomain_wall ys + codomain_wall (basic x)

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

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
codomain_block x \<noteq> 0

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
have "(basic x) \<otimes> (y*ys)
                 = (x \<otimes> y)
                    *((basic (make_vert_block (nat (codomain_block x))))\<otimes> ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basic x \<otimes> y * ys = (x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)
[PROOF STEP]
using False 3
[PROOF STATE]
proof (prove)
using this:
codomain_block x \<noteq> 0
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))

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

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

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

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

goal (1 subgoal):
 1. codomain_wall ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) = codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)
[PROOF STEP]
using codomain_wall.simps(2)
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) = codomain_wall ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys))
codomain_wall (?x * ?ys) = codomain_wall ?ys

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

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

goal (1 subgoal):
 1. codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block x + codomain_wall ys
[PROOF STEP]
using codomain_wall.simps case_3 False
                      codomain_block_nonnegative codomain_make_vert int_nat_eq
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) = codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys
codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_wall (basic (make_vert_block (nat (codomain_block x)))) + codomain_wall ys
codomain_block x \<noteq> 0
0 \<le> codomain_block ?x
codomain_block (make_vert_block ?n) = int ?n
int (nat ?z) = (if 0 \<le> ?z then ?z else 0)

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

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

goal (1 subgoal):
 1. codomain_block x + codomain_wall ys = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
using codomain_wall.simps
[PROOF STATE]
proof (prove)
using this:
codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block x + codomain_wall ys
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys

goal (1 subgoal):
 1. codomain_block x + codomain_wall ys = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block x + codomain_wall ys = codomain_wall (basic x) + codomain_wall (y * ys)

goal (1 subgoal):
 1. codomain_block x \<noteq> 0 \<Longrightarrow> codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_block x + codomain_wall ys = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
codomain_block x + codomain_wall ys = codomain_wall (basic x) + codomain_wall (y * ys)

goal (1 subgoal):
 1. codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)
[PROOF STEP]
by (metis \<open>basic x \<otimes> y * ys = (x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<close> \<open>codomain_wall ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) = codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<close> \<open>codomain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block x + codomain_wall ys\<close>)
[PROOF STATE]
proof (state)
this:
codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
codomain_wall (basic x \<otimes> y * ys) = codomain_wall (basic x) + codomain_wall (y * ys)

goal (1 subgoal):
 1. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
fix x xs y ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
assume case_4:"codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys "
[PROOF STATE]
proof (state)
this:
codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys

goal (1 subgoal):
 1. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
let ?case = "codomain_wall ((x*xs) \<otimes> (y*ys))
                      = codomain_wall (x*xs) + codomain_wall (y*ys)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys \<Longrightarrow> codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
have " ((x*xs) \<otimes> (y*ys)) = (x \<otimes> y)*(xs \<otimes> ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * xs \<otimes> y * ys = (x \<otimes> y) * (xs \<otimes> ys)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
?x * ?xs \<otimes> ?y * ?ys = (?x \<otimes> ?y) * (?xs \<otimes> ?ys)

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

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

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

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

goal (1 subgoal):
 1. codomain_wall ((x \<otimes> y) * (xs \<otimes> ys)) = codomain_wall (xs \<otimes> ys)
[PROOF STEP]
using codomain_wall.simps(2)
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * (xs \<otimes> ys)) = codomain_wall ((x \<otimes> y) * (xs \<otimes> ys))
codomain_wall (?x * ?ys) = codomain_wall ?ys

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

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

goal (1 subgoal):
 1. codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys
[PROOF STEP]
using case_4
[PROOF STATE]
proof (prove)
using this:
codomain_wall ((x \<otimes> y) * (xs \<otimes> ys)) = codomain_wall (xs \<otimes> ys)
codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys

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

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

goal (1 subgoal):
 1. codomain_wall xs + codomain_wall ys = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
using codomain_wall.simps(2)
[PROOF STATE]
proof (prove)
using this:
codomain_wall (xs \<otimes> ys) = codomain_wall xs + codomain_wall ys
codomain_wall (?x * ?ys) = codomain_wall ?ys

goal (1 subgoal):
 1. codomain_wall xs + codomain_wall ys = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_wall xs + codomain_wall ys = codomain_wall (x * xs) + codomain_wall (y * ys)

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

goal (1 subgoal):
 1. codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)
[PROOF STEP]
by (metis \<open>codomain_wall ((x \<otimes> y) * (xs \<otimes> ys)) = codomain_wall (xs \<otimes> ys)\<close> \<open>x * xs \<otimes> y * ys = (x \<otimes> y) * (xs \<otimes> ys)\<close> case_4)
[PROOF STATE]
proof (state)
this:
codomain_wall (x * xs \<otimes> y * ys) = codomain_wall (x * xs) + codomain_wall (y * ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem is_tangle_make_vert_right:
 "(is_tangle_diagram xs)
          \<Longrightarrow> is_tangle_diagram (xs \<otimes> (basic (make_vert_block n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. is_tangle_diagram (basic x) \<Longrightarrow> is_tangle_diagram (basic x \<otimes> basic (make_vert_block n))
 2. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
case (basic xs)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic xs)

goal (2 subgoals):
 1. \<And>x. is_tangle_diagram (basic x) \<Longrightarrow> is_tangle_diagram (basic x \<otimes> basic (make_vert_block n))
 2. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic xs \<otimes> basic (make_vert_block n))

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
case (prod x xs)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n))
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have
        "codomain_block (x \<otimes> (make_vert_block 0))
               = (codomain_block x) + codomain_block(make_vert_block 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (x \<otimes> make_vert_block 0) = codomain_block x + codomain_block (make_vert_block 0)
[PROOF STEP]
using  codomain_additive
[PROOF STATE]
proof (prove)
using this:
codomain_block (?x \<otimes> ?y) = codomain_block ?x + codomain_block ?y

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> make_vert_block 0) = codomain_block x + codomain_block (make_vert_block 0)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "codomain_block (make_vert_block 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block 0) = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
codomain_block (x \<otimes> make_vert_block 0) = codomain_block x + codomain_block (make_vert_block 0)
codomain_block (make_vert_block 0) = 0
[PROOF STEP]
have "codomain_block (x \<otimes> (make_vert_block 0)) = codomain_block (x)"
[PROOF STATE]
proof (prove)
using this:
codomain_block (x \<otimes> make_vert_block 0) = codomain_block x + codomain_block (make_vert_block 0)
codomain_block (make_vert_block 0) = 0

goal (1 subgoal):
 1. codomain_block (x \<otimes> make_vert_block 0) = codomain_block x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> make_vert_block 0) = codomain_block x

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> make_vert_block 0) = codomain_block x

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "is_tangle_diagram xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram xs
[PROOF STEP]
using prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram xs
[PROOF STEP]
by (metis is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram xs
[PROOF STEP]
have "is_tangle_diagram ((x \<otimes> (make_vert_block 0))*xs)"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs

goal (1 subgoal):
 1. is_tangle_diagram ((x \<otimes> make_vert_block 0) * xs)
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs
is_tangle_diagram (?x * ?xs) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. is_tangle_diagram ((x \<otimes> make_vert_block 0) * xs)
[PROOF STEP]
by (metis calculation prod.prems)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram ((x \<otimes> make_vert_block 0) * xs)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram ((x \<otimes> make_vert_block 0) * xs)
[PROOF STEP]
have "is_tangle_diagram ((x*xs) \<otimes> (basic (make_vert_block 0)))"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram ((x \<otimes> make_vert_block 0) * xs)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block 0))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block 0))

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
using  "0"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block 0))
n = 0

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
n = Suc k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "codomain_block (make_vert_block (k+1)) = int (k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
using codomain_make_vert
[PROOF STATE]
proof (prove)
using this:
codomain_block (make_vert_block ?n) = int ?n

goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
have "(nat (codomain_block (make_vert_block (k+1)))) = k+1"
[PROOF STATE]
proof (prove)
using this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)

goal (1 subgoal):
 1. nat (codomain_block (make_vert_block (k + 1))) = k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1
[PROOF STEP]
have "make_vert_block (nat (codomain_block (make_vert_block (k+1))))
                             = make_vert_block (k+1)"
[PROOF STATE]
proof (prove)
using this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1

goal (1 subgoal):
 1. make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "codomain_wall (basic (make_vert_block (k+1)))>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
using make_vert_block.simps codomain_wall.simps  Suc_eq_plus1
       codomain_make_vert of_nat_0_less_iff zero_less_Suc
[PROOF STATE]
proof (prove)
using this:
make_vert_block 0 = []
make_vert_block (Suc ?n) = vert # make_vert_block ?n
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys
Suc ?n = ?n + 1
codomain_block (make_vert_block ?n) = int ?n
((0::?'a) < of_nat ?n) = (0 < ?n)
0 < Suc ?n

goal (1 subgoal):
 1. 0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < codomain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
have 1: "(x*xs) \<otimes> (basic (make_vert_block (k+1)))
             =  (x\<otimes>(make_vert_block (k+1)))*(xs\<otimes>(basic (make_vert_block (k+1))))"
[PROOF STATE]
proof (prove)
using this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. x * xs \<otimes> basic (make_vert_block (k + 1)) = (x \<otimes> make_vert_block (k + 1)) * (xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
using tensor.simps(2)
[PROOF STATE]
proof (prove)
using this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))
?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)))))

goal (1 subgoal):
 1. x * xs \<otimes> basic (make_vert_block (k + 1)) = (x \<otimes> make_vert_block (k + 1)) * (xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * xs \<otimes> basic (make_vert_block (k + 1)) = (x \<otimes> make_vert_block (k + 1)) * (xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "domain_wall (xs\<otimes>(basic (make_vert_block (k+1))))
                 = domain_wall xs + domain_wall (basic (make_vert_block (k+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
using tensor_domain_wall_additivity
[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> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
have 2:
          "domain_wall (xs\<otimes>(basic (make_vert_block (k+1))))
                  = (domain_wall xs) + int (k+1)"
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
[PROOF STEP]
using domain_make_vert domain_wall.simps(1)
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
domain_block (make_vert_block ?n) = int ?n
domain_wall (basic ?x) = domain_block ?x

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have 3: "codomain_block (x \<otimes> (make_vert_block (k+1)))
                 = codomain_block x + int (k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (x \<otimes> make_vert_block (k + 1)) = codomain_block x + int (k + 1)
[PROOF STEP]
using  codomain_additive codomain_make_vert
[PROOF STATE]
proof (prove)
using this:
codomain_block (?x \<otimes> ?y) = codomain_block ?x + codomain_block ?y
codomain_block (make_vert_block ?n) = int ?n

goal (1 subgoal):
 1. codomain_block (x \<otimes> make_vert_block (k + 1)) = codomain_block x + int (k + 1)
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> make_vert_block (k + 1)) = codomain_block x + int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "is_tangle_diagram (x*xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs)
[PROOF STEP]
using prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs)
[PROOF STEP]
have 4:"codomain_block x = domain_wall xs"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. codomain_block x = domain_wall xs
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)
is_tangle_diagram (?x * ?xs) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. codomain_block x = domain_wall xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
codomain_block x = domain_wall xs

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
from 2 3 4
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
codomain_block (x \<otimes> make_vert_block (k + 1)) = codomain_block x + int (k + 1)
codomain_block x = domain_wall xs
[PROOF STEP]
have
       "domain_wall (xs\<otimes>(basic (make_vert_block (k+1))))
               = codomain_block (x \<otimes> (make_vert_block (k+1))) "
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
codomain_block (x \<otimes> make_vert_block (k + 1)) = codomain_block x + int (k + 1)
codomain_block x = domain_wall xs

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = codomain_block (x \<otimes> make_vert_block (k + 1))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
have "is_tangle_diagram (xs\<otimes>(basic (make_vert_block (k+1))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
using prod.hyps prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n))
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
by (metis Suc Suc_eq_plus1 is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = codomain_block (x \<otimes> make_vert_block (k + 1))
is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
have "is_tangle_diagram ((x*xs) \<otimes> (basic (make_vert_block (k+1))))"
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = codomain_block (x \<otimes> make_vert_block (k + 1))
is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = domain_wall xs + int (k + 1)
domain_wall (xs \<otimes> basic (make_vert_block (k + 1))) = codomain_block (x \<otimes> make_vert_block (k + 1))
is_tangle_diagram (xs \<otimes> basic (make_vert_block (k + 1)))
x * xs \<otimes> basic (make_vert_block (k + 1)) = (x \<otimes> make_vert_block (k + 1)) * (xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
using  Suc Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block (k + 1)))
n = Suc k
Suc ?n = ?n + 1

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block n)); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (x1a * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))

goal (1 subgoal):
 1. is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs \<otimes> basic (make_vert_block n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem is_tangle_make_vert_left:
 "(is_tangle_diagram xs) \<Longrightarrow> is_tangle_diagram ((basic (make_vert_block n)) \<otimes> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs)
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. is_tangle_diagram (basic x) \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> basic x)
 2. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
case (basic xs)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic xs)

goal (2 subgoals):
 1. \<And>x. is_tangle_diagram (basic x) \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> basic x)
 2. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> basic xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> basic xs)

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
case (prod x xs)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs)
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have
        "codomain_block ( (make_vert_block 0) \<otimes> x)
               = (codomain_block x) + codomain_block(make_vert_block 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x + codomain_block (make_vert_block 0)
[PROOF STEP]
using  codomain_additive
[PROOF STATE]
proof (prove)
using this:
codomain_block (?x \<otimes> ?y) = codomain_block ?x + codomain_block ?y

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x + codomain_block (make_vert_block 0)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "codomain_block (make_vert_block 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block 0) = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x + codomain_block (make_vert_block 0)
codomain_block (make_vert_block 0) = 0
[PROOF STEP]
have "codomain_block ( (make_vert_block 0) \<otimes> x) = codomain_block (x)"
[PROOF STATE]
proof (prove)
using this:
codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x + codomain_block (make_vert_block 0)
codomain_block (make_vert_block 0) = 0

goal (1 subgoal):
 1. codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block 0 \<otimes> x) = codomain_block x

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "is_tangle_diagram xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram xs
[PROOF STEP]
using prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram xs
[PROOF STEP]
by (metis is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram xs
[PROOF STEP]
have "is_tangle_diagram (( (make_vert_block 0) \<otimes> x)*xs)"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs

goal (1 subgoal):
 1. is_tangle_diagram ((make_vert_block 0 \<otimes> x) * xs)
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs
is_tangle_diagram (?x * ?xs) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. is_tangle_diagram ((make_vert_block 0 \<otimes> x) * xs)
[PROOF STEP]
by (metis calculation prod.prems)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram ((make_vert_block 0 \<otimes> x) * xs)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram ((make_vert_block 0 \<otimes> x) * xs)
[PROOF STEP]
have "is_tangle_diagram ((basic (make_vert_block 0)) \<otimes> (x*xs) )"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram ((make_vert_block 0 \<otimes> x) * xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block 0) \<otimes> x * xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block 0) \<otimes> x * xs)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
 2. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (basic (make_vert_block 0) \<otimes> x * xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic (make_vert_block 0) \<otimes> x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
using  "0"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic (make_vert_block 0) \<otimes> x * xs)
n = 0

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
n = Suc k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "codomain_block (make_vert_block (k+1)) = int (k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
using codomain_make_vert
[PROOF STATE]
proof (prove)
using this:
codomain_block (make_vert_block ?n) = int ?n

goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)
[PROOF STEP]
have "(nat (codomain_block (make_vert_block (k+1)))) = k+1"
[PROOF STATE]
proof (prove)
using this:
codomain_block (make_vert_block (k + 1)) = int (k + 1)

goal (1 subgoal):
 1. nat (codomain_block (make_vert_block (k + 1))) = k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1
[PROOF STEP]
have "make_vert_block (nat (codomain_block (make_vert_block (k+1))))
                             = make_vert_block (k+1)"
[PROOF STATE]
proof (prove)
using this:
nat (codomain_block (make_vert_block (k + 1))) = k + 1

goal (1 subgoal):
 1. make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "codomain_wall (basic (make_vert_block (k+1)))>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
using make_vert_block.simps codomain_wall.simps  Suc_eq_plus1
              codomain_make_vert of_nat_0_less_iff zero_less_Suc
[PROOF STATE]
proof (prove)
using this:
make_vert_block 0 = []
make_vert_block (Suc ?n) = vert # make_vert_block ?n
codomain_wall (basic ?x) = codomain_block ?x
codomain_wall (?x * ?ys) = codomain_wall ?ys
Suc ?n = ?n + 1
codomain_block (make_vert_block ?n) = int ?n
((0::?'a) < of_nat ?n) = (0 < ?n)
0 < Suc ?n

goal (1 subgoal):
 1. 0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < codomain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
have 1: "  (basic (make_vert_block (k+1))) \<otimes> (x*xs)
             =  ((make_vert_block (k+1)) \<otimes> x)*((basic (make_vert_block (k+1))) \<otimes> xs)"
[PROOF STATE]
proof (prove)
using this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. basic (make_vert_block (k + 1)) \<otimes> x * xs = (make_vert_block (k + 1) \<otimes> x) * (basic (make_vert_block (k + 1)) \<otimes> xs)
[PROOF STEP]
using tensor.simps(3)
[PROOF STATE]
proof (prove)
using this:
make_vert_block (nat (codomain_block (make_vert_block (k + 1)))) = make_vert_block (k + 1)
0 < codomain_wall (basic (make_vert_block (k + 1)))
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))

goal (1 subgoal):
 1. basic (make_vert_block (k + 1)) \<otimes> x * xs = (make_vert_block (k + 1) \<otimes> x) * (basic (make_vert_block (k + 1)) \<otimes> xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
basic (make_vert_block (k + 1)) \<otimes> x * xs = (make_vert_block (k + 1) \<otimes> x) * (basic (make_vert_block (k + 1)) \<otimes> xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "domain_wall ((basic (make_vert_block (k+1))) \<otimes> xs)
                 = domain_wall xs + domain_wall (basic (make_vert_block (k+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
using tensor_domain_wall_additivity
[PROOF STATE]
proof (prove)
using this:
domain_wall (?xs \<otimes> ?ys) = domain_wall ?xs + domain_wall ?ys

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
[PROOF STEP]
have 2:
          "domain_wall ((basic (make_vert_block (k+1))) \<otimes> xs)
                  = (domain_wall xs) + int (k+1)"
[PROOF STATE]
proof (prove)
using this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))

goal (1 subgoal):
 1. domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
[PROOF STEP]
using domain_make_vert domain_wall.simps(1)
[PROOF STATE]
proof (prove)
using this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + domain_wall (basic (make_vert_block (k + 1)))
domain_block (make_vert_block ?n) = int ?n
domain_wall (basic ?x) = domain_block ?x

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have 3: "codomain_block ( (make_vert_block (k+1)) \<otimes> x)
                 = codomain_block x + int (k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1) \<otimes> x) = codomain_block x + int (k + 1)
[PROOF STEP]
using  codomain_additive codomain_make_vert
[PROOF STATE]
proof (prove)
using this:
codomain_block (?x \<otimes> ?y) = codomain_block ?x + codomain_block ?y
codomain_block (make_vert_block ?n) = int ?n

goal (1 subgoal):
 1. codomain_block (make_vert_block (k + 1) \<otimes> x) = codomain_block x + int (k + 1)
[PROOF STEP]
by (simp add: codomain_additive)
[PROOF STATE]
proof (state)
this:
codomain_block (make_vert_block (k + 1) \<otimes> x) = codomain_block x + int (k + 1)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "is_tangle_diagram (x*xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs)
[PROOF STEP]
using prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs)
[PROOF STEP]
have 4:"codomain_block x = domain_wall xs"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. codomain_block x = domain_wall xs
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs)
is_tangle_diagram (?x * ?xs) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. codomain_block x = domain_wall xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
codomain_block x = domain_wall xs

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
from 2 3 4
[PROOF STATE]
proof (chain)
picking this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
codomain_block (make_vert_block (k + 1) \<otimes> x) = codomain_block x + int (k + 1)
codomain_block x = domain_wall xs
[PROOF STEP]
have
       "domain_wall ((basic (make_vert_block (k+1))) \<otimes> xs)
               = codomain_block ((make_vert_block (k+1)) \<otimes> x)"
[PROOF STATE]
proof (prove)
using this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
codomain_block (make_vert_block (k + 1) \<otimes> x) = codomain_block x + int (k + 1)
codomain_block x = domain_wall xs

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = codomain_block (make_vert_block (k + 1) \<otimes> x)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
have "is_tangle_diagram ((basic (make_vert_block (k+1))) \<otimes> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)
[PROOF STEP]
using prod.hyps prod.prems
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs)
is_tangle_diagram (x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)
[PROOF STEP]
by (metis Suc Suc_eq_plus1 is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = codomain_block (make_vert_block (k + 1) \<otimes> x)
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)
[PROOF STEP]
have "is_tangle_diagram ((basic (make_vert_block (k+1))) \<otimes> (x*xs))"
[PROOF STATE]
proof (prove)
using this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = codomain_block (make_vert_block (k + 1) \<otimes> x)
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = domain_wall xs + int (k + 1)
domain_wall (basic (make_vert_block (k + 1)) \<otimes> xs) = codomain_block (make_vert_block (k + 1) \<otimes> x)
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> xs)
basic (make_vert_block (k + 1)) \<otimes> x * xs = (make_vert_block (k + 1) \<otimes> x) * (basic (make_vert_block (k + 1)) \<otimes> xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
using  Suc Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic (make_vert_block (k + 1)) \<otimes> x * xs)
n = Suc k
Suc ?n = ?n + 1

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)

goal (1 subgoal):
 1. \<And>x1a xs. \<lbrakk>is_tangle_diagram xs \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> xs); is_tangle_diagram (x1a * xs)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic (make_vert_block n) \<otimes> x1a * xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block n) \<otimes> x * xs)

goal:
No subgoals!
[PROOF STEP]
qed