[STATEMENT]
lemma simp1: "(codomain_block y) \<noteq> 0 \<Longrightarrow>
       is_tangle_diagram (xs)
\<and> is_tangle_diagram ((basic (make_vert_block (nat (codomain_block y))))) \<longrightarrow>
               is_tangle_diagram (xs \<otimes>  ((basic (make_vert_block (nat (codomain_block y)))))) \<Longrightarrow>
(is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y))
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
assume A: "(codomain_block y) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
codomain_block y \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
assume B:
     " is_tangle_diagram (xs)
     \<and> is_tangle_diagram ((basic (make_vert_block (nat (codomain_block y)))))
      \<longrightarrow>
       is_tangle_diagram (xs \<otimes>  ((basic (make_vert_block (nat (codomain_block y))))))"
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have " is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs
[PROOF STEP]
by (metis is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have "(is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
using is_tangle_diagram.simps(1)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic ?x) = True

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs
is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
have
   " ((is_tangle_diagram xs)
   \<and>(is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))))
    \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))
      \<Longrightarrow>
       is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow>
       is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram xs
is_tangle_diagram (basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have 1:"codomain_block y = domain_wall (basic (make_vert_block (nat (codomain_block y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block y = domain_wall (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
using codomain_block_nonnegative domain_make_vert domain_wall.simps(1) int_nat_eq
[PROOF STATE]
proof (prove)
using this:
0 \<le> codomain_block ?x
domain_block (make_vert_block ?n) = int ?n
domain_wall (basic ?x) = domain_block ?x
int (nat ?z) = (if 0 \<le> ?z then ?z else 0)

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

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block y = domain_wall (basic (make_vert_block (nat (codomain_block y))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have 2:"is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow>
                 codomain_block x = domain_wall xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> 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) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> codomain_block x = domain_wall xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> codomain_block x = domain_wall xs

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> codomain_block x = domain_wall xs

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have "codomain_block (x \<otimes> y) = codomain_block x +codomain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (x \<otimes> y) = codomain_block x + codomain_block y
[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> y) = codomain_block x + codomain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> y) = codomain_block x + codomain_block y

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

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
have "domain_wall (xs \<otimes> (basic (make_vert_block (nat (codomain_block y)))))
                 = domain_wall xs + domain_wall (basic (make_vert_block (nat (codomain_block y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = domain_wall xs + domain_wall (basic (make_vert_block (nat (codomain_block y))))
[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 (nat (codomain_block y)))) = domain_wall xs + domain_wall (basic (make_vert_block (nat (codomain_block y))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = domain_wall xs + domain_wall (basic (make_vert_block (nat (codomain_block y))))

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

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

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

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

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))
codomain_block y = domain_wall (basic (make_vert_block (nat (codomain_block y))))
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> codomain_block x = domain_wall xs
codomain_block (x \<otimes> y) = codomain_block x + codomain_block y
domain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = domain_wall xs + domain_wall (basic (make_vert_block (nat (codomain_block y))))
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> domain_wall (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) = codomain_block (x \<otimes> y)
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 xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (xs \<otimes> basic (make_vert_block (nat (codomain_block y)))))

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

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
by (metis "Tangle_Algebra.2" \<open>
        codomain_block y \<noteq> 0\<close> is_tangle_make_vert_right)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)

goal (1 subgoal):
 1. \<lbrakk>codomain_block y \<noteq> 0; is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simp2:
 "(codomain_block x) \<noteq> 0
 \<Longrightarrow>
   is_tangle_diagram  (basic (make_vert_block (nat (codomain_block x))))
 \<and> is_tangle_diagram (ys)
    \<longrightarrow>
      is_tangle_diagram ((basic (make_vert_block (nat (codomain_block x)))) \<otimes> ys)
     \<Longrightarrow>
    (is_tangle_diagram (basic x)
   \<and> is_tangle_diagram (y*ys)
         \<longrightarrow> is_tangle_diagram ((basic x) \<otimes> (y*ys)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
assume A: "(codomain_block x) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
codomain_block x \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
assume B: "is_tangle_diagram  (basic (make_vert_block (nat (codomain_block x))))
            \<and> is_tangle_diagram (ys) \<longrightarrow>
              is_tangle_diagram
                            ((basic (make_vert_block (nat (codomain_block x)))) \<otimes> ys)"
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have " is_tangle_diagram (basic x) \<and> is_tangle_diagram (y*ys)
                                               \<longrightarrow> is_tangle_diagram ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ys
[PROOF STEP]
by (metis is_tangle_diagram.simps(2))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ys

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ys

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have "(is_tangle_diagram
                          (basic (make_vert_block (nat (codomain_block x))))) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))))
[PROOF STEP]
using is_tangle_diagram.simps(1)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic ?x) = True

goal (1 subgoal):
 1. is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ys
is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))))
[PROOF STEP]
have
      " ((is_tangle_diagram ys)
               \<and>(is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))))
    \<longrightarrow> is_tangle_diagram ((basic (make_vert_block (nat (codomain_block x)))) \<otimes> ys))
    \<Longrightarrow>
     is_tangle_diagram (basic x) \<and> is_tangle_diagram (y*ys) \<longrightarrow>
                is_tangle_diagram
                        (( basic (make_vert_block (nat (codomain_block x)))) \<otimes> ys)"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ys
is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))))

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

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram ys \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have 1:"codomain_block x
                         = domain_wall (basic (make_vert_block (nat (codomain_block x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block x = domain_wall (basic (make_vert_block (nat (codomain_block x))))
[PROOF STEP]
using codomain_block_nonnegative domain_make_vert domain_wall.simps(1)
              int_nat_eq
[PROOF STATE]
proof (prove)
using this:
0 \<le> codomain_block ?x
domain_block (make_vert_block ?n) = int ?n
domain_wall (basic ?x) = domain_block ?x
int (nat ?z) = (if 0 \<le> ?z then ?z else 0)

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

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block x = domain_wall (basic (make_vert_block (nat (codomain_block x))))

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have 2:"is_tangle_diagram (basic x) \<and> is_tangle_diagram (y*ys) \<longrightarrow>
                 codomain_block y = domain_wall ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
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 (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have "codomain_block (x \<otimes> y) = codomain_block x +codomain_block y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomain_block (x \<otimes> y) = codomain_block x + codomain_block y
[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> y) = codomain_block x + codomain_block y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> y) = codomain_block x + codomain_block y

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
codomain_block (x \<otimes> y) = codomain_block x + codomain_block y

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
have "domain_wall ((basic (make_vert_block (nat (codomain_block x)))) \<otimes> ys)
                 = domain_wall (basic (make_vert_block (nat (codomain_block x))))
                   + domain_wall ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = domain_wall (basic (make_vert_block (nat (codomain_block x)))) + domain_wall ys
[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 (nat (codomain_block x))) \<otimes> ys) = domain_wall (basic (make_vert_block (nat (codomain_block x)))) + domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = domain_wall (basic (make_vert_block (nat (codomain_block x)))) + domain_wall ys

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = domain_wall (basic (make_vert_block (nat (codomain_block x)))) + domain_wall ys

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

goal (1 subgoal):
 1. is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block (x \<otimes> y)
[PROOF STEP]
by (metis "1" "2" calculation(4))
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block (x \<otimes> y)

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

goal (1 subgoal):
 1. is_tangle_diagram ys \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys))
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram ys \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)
codomain_block x = domain_wall (basic (make_vert_block (nat (codomain_block x))))
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
codomain_block (x \<otimes> y) = codomain_block x + codomain_block y
domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = domain_wall (basic (make_vert_block (nat (codomain_block x)))) + domain_wall ys
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> domain_wall (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) = codomain_block (x \<otimes> y)
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 ys \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram ys \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram ((x \<otimes> y) * (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys))

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

goal (1 subgoal):
 1. is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
by (metis "Tangle_Algebra.3" A B)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)

goal (1 subgoal):
 1. \<lbrakk>codomain_block x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simp3:
 "is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
 \<Longrightarrow>
     is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys)
     \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
assume A: "is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)"
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
have "is_tangle_diagram (x*xs) \<longrightarrow> (codomain_block x = domain_wall xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<longrightarrow> 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) = (if is_tangle_diagram ?xs then codomain_block ?x = domain_wall ?xs else False)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
have "is_tangle_diagram (y*ys) \<longrightarrow> (codomain_block y = domain_wall ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
[PROOF STEP]
using is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
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 (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs
is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
[PROOF STEP]
have "is_tangle_diagram (x*xs)\<and> is_tangle_diagram (y*ys)
              \<longrightarrow> codomain_block (x \<otimes> y) = domain_wall (xs \<otimes> ys)"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs
is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block (x \<otimes> y) = domain_wall (xs \<otimes> ys)
[PROOF STEP]
using codomain_additive tensor_domain_wall_additivity
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<longrightarrow> codomain_block x = domain_wall xs
is_tangle_diagram (y * ys) \<longrightarrow> codomain_block y = domain_wall ys
codomain_block (?x \<otimes> ?y) = codomain_block ?x + codomain_block ?y
domain_wall (?xs \<otimes> ?ys) = domain_wall ?xs + domain_wall ?ys

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

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block (x \<otimes> y) = domain_wall (xs \<otimes> ys)

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
have "is_tangle_diagram (x*xs)\<and> is_tangle_diagram (y*ys)
              \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
[PROOF STEP]
using A is_tangle_diagram.simps(2)
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
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 * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> 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 tensor.simps(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. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block (x \<otimes> y) = domain_wall (xs \<otimes> ys)
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
x * xs \<otimes> y * ys = (x \<otimes> y) * (xs \<otimes> ys)
[PROOF STEP]
have "is_tangle_diagram (x*xs)\<and> is_tangle_diagram (y*ys)
              \<longrightarrow> is_tangle_diagram ((x*xs) \<otimes> (y*ys))"
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> codomain_block (x \<otimes> y) = domain_wall (xs \<otimes> ys)
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)
x * xs \<otimes> y * ys = (x \<otimes> y) * (xs \<otimes> ys)

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

goal (1 subgoal):
 1. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem is_tangle_diagramness:
 shows"(is_tangle_diagram x)\<and>(is_tangle_diagram y) \<longrightarrow>is_tangle_diagram (tensor x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram x \<and> is_tangle_diagram y \<longrightarrow> is_tangle_diagram (x \<otimes> y)
[PROOF STEP]
proof(induction x y  rule:tensor.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. is_tangle_diagram (basic x) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (basic x \<otimes> basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 4. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
fix z w
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. is_tangle_diagram (basic x) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (basic x \<otimes> basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 4. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
let ?case = "(is_tangle_diagram (basic z))\<and>(is_tangle_diagram (basic w))
                  \<longrightarrow>is_tangle_diagram ((basic z) \<otimes> (basic w))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. is_tangle_diagram (basic x) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (basic x \<otimes> basic y)
 2. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 3. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 4. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (basic z) \<and> is_tangle_diagram (basic w) \<longrightarrow> is_tangle_diagram (basic z \<otimes> basic w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic z) \<and> is_tangle_diagram (basic w) \<longrightarrow> is_tangle_diagram (basic z \<otimes> basic w)

goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 3. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 3. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> 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> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 3. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
let ?case = "(is_tangle_diagram (x*xs))\<and>(is_tangle_diagram (basic y))
                  \<longrightarrow>is_tangle_diagram ((x*xs) \<otimes> (basic y))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y. (codomain_block y \<noteq> 0 \<Longrightarrow> is_tangle_diagram xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block y)))) \<longrightarrow> is_tangle_diagram (xs \<otimes> basic (make_vert_block (nat (codomain_block y))))) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
 2. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 3. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
from simp1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>codomain_block ?y \<noteq> 0; is_tangle_diagram ?xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?y)))) \<longrightarrow> is_tangle_diagram (?xs \<otimes> basic (make_vert_block (nat (codomain_block ?y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (?x * ?xs) \<and> is_tangle_diagram (basic ?y) \<longrightarrow> is_tangle_diagram (?x * ?xs \<otimes> basic ?y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>codomain_block ?y \<noteq> 0; is_tangle_diagram ?xs \<and> is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?y)))) \<longrightarrow> is_tangle_diagram (?xs \<otimes> basic (make_vert_block (nat (codomain_block ?y))))\<rbrakk> \<Longrightarrow> is_tangle_diagram (?x * ?xs) \<and> is_tangle_diagram (basic ?y) \<longrightarrow> is_tangle_diagram (?x * ?xs \<otimes> basic ?y)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)
[PROOF STEP]
by (metis "Tangle_Algebra.2" add.commute codomain_additive comm_monoid_add_class.add_0
                is_tangle_diagram.simps(2) is_tangle_make_vert_right)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (x * xs) \<and> is_tangle_diagram (basic y) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> basic y)

goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 2. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 2. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> 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> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 2. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
let ?case = "(is_tangle_diagram (basic x))\<and>(is_tangle_diagram (y*ys))
                  \<longrightarrow>is_tangle_diagram ((basic x) \<otimes> (y*ys))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y ys. (codomain_block x \<noteq> 0 \<Longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x)))) \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block x))) \<otimes> ys)) \<Longrightarrow> is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
 2. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
from simp2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>codomain_block ?x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?x)))) \<and> is_tangle_diagram ?ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?x))) \<otimes> ?ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic ?x) \<and> is_tangle_diagram (?y * ?ys) \<longrightarrow> is_tangle_diagram (basic ?x \<otimes> ?y * ?ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>codomain_block ?x \<noteq> 0; is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?x)))) \<and> is_tangle_diagram ?ys \<longrightarrow> is_tangle_diagram (basic (make_vert_block (nat (codomain_block ?x))) \<otimes> ?ys)\<rbrakk> \<Longrightarrow> is_tangle_diagram (basic ?x) \<and> is_tangle_diagram (?y * ?ys) \<longrightarrow> is_tangle_diagram (basic ?x \<otimes> ?y * ?ys)

goal (1 subgoal):
 1. is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)
[PROOF STEP]
by (metis "Tangle_Algebra.3" codomain_additive comm_monoid_add_class.add_0
                   is_tangle_diagram.simps(2) is_tangle_make_vert_left)
[PROOF STATE]
proof (state)
this:
is_tangle_diagram (basic x) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (basic x \<otimes> y * ys)

goal (1 subgoal):
 1. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
fix x y xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
assume A:"  is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)"
[PROOF STATE]
proof (state)
this:
is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)

goal (1 subgoal):
 1. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
let ?case =
    "is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys) \<Longrightarrow> is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
from simp3
[PROOF STATE]
proof (chain)
picking this:
is_tangle_diagram ?xs \<and> is_tangle_diagram ?ys \<longrightarrow> is_tangle_diagram (?xs \<otimes> ?ys) \<Longrightarrow> is_tangle_diagram (?x * ?xs) \<and> is_tangle_diagram (?y * ?ys) \<longrightarrow> is_tangle_diagram (?x * ?xs \<otimes> ?y * ?ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram ?xs \<and> is_tangle_diagram ?ys \<longrightarrow> is_tangle_diagram (?xs \<otimes> ?ys) \<Longrightarrow> is_tangle_diagram (?x * ?xs) \<and> is_tangle_diagram (?y * ?ys) \<longrightarrow> is_tangle_diagram (?x * ?xs \<otimes> ?y * ?ys)

goal (1 subgoal):
 1. is_tangle_diagram (x * xs) \<and> is_tangle_diagram (y * ys) \<longrightarrow> is_tangle_diagram (x * xs \<otimes> y * ys)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram ?xs \<and> is_tangle_diagram ?ys \<longrightarrow> is_tangle_diagram (?xs \<otimes> ?ys) \<Longrightarrow> is_tangle_diagram (?x * ?xs) \<and> is_tangle_diagram (?y * ?ys) \<longrightarrow> is_tangle_diagram (?x * ?xs \<otimes> ?y * ?ys)
is_tangle_diagram xs \<and> is_tangle_diagram ys \<longrightarrow> is_tangle_diagram (xs \<otimes> ys)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem tensor_preserves_is_tangle:
 assumes "is_tangle_diagram x"
     and "is_tangle_diagram y"
 shows "is_tangle_diagram (x \<otimes> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_tangle_diagram (x \<otimes> y)
[PROOF STEP]
using assms  is_tangle_diagramness
[PROOF STATE]
proof (prove)
using this:
is_tangle_diagram x
is_tangle_diagram y
is_tangle_diagram ?x \<and> is_tangle_diagram ?y \<longrightarrow> is_tangle_diagram (?x \<otimes> ?y)

goal (1 subgoal):
 1. is_tangle_diagram (x \<otimes> y)
[PROOF STEP]
by auto


[STATEMENT]
theorem well_defined_compose:
 assumes "is_tangle_diagram x"
     and "is_tangle_diagram y"
 shows "(Abs_Tangle_Diagram x) \<otimes> (Abs_Tangle_Diagram y) = (Abs_Tangle_Diagram (x \<otimes> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_Tangle_Diagram x \<otimes> Abs_Tangle_Diagram y = Abs_Tangle_Diagram (x \<otimes> y)
[PROOF STEP]
using  Abs_Tangle_Diagram_inverse assms(1) assms(2)
      mem_Collect_eq tensor_preserves_is_tangle
     tensor_Tangle_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> {x. is_tangle_diagram x} \<Longrightarrow> Rep_Tangle_Diagram (Abs_Tangle_Diagram ?y) = ?y
is_tangle_diagram x
is_tangle_diagram y
(?a \<in> Collect ?P) = ?P ?a
\<lbrakk>is_tangle_diagram ?x; is_tangle_diagram ?y\<rbrakk> \<Longrightarrow> is_tangle_diagram (?x \<otimes> ?y)
?x \<otimes> ?y = Abs_Tangle_Diagram (Rep_Tangle_Diagram ?x \<otimes> Rep_Tangle_Diagram ?y)

goal (1 subgoal):
 1. Abs_Tangle_Diagram x \<otimes> Abs_Tangle_Diagram y = Abs_Tangle_Diagram (x \<otimes> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma intD[dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> A \<Longrightarrow> A w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> A \<Longrightarrow> A w
[PROOF STEP]
assume a:"\<turnstile> A"
[PROOF STATE]
proof (state)
this:
\<turnstile> A

goal (1 subgoal):
 1. \<turnstile> A \<Longrightarrow> A w
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> A
[PROOF STEP]
have "\<forall>w. w \<Turnstile> A"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> A

goal (1 subgoal):
 1. \<forall>w. A w
[PROOF STEP]
by (auto simp add: Valid_def)
[PROOF STATE]
proof (state)
this:
\<forall>w. A w

goal (1 subgoal):
 1. \<turnstile> A \<Longrightarrow> A w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w. A w

goal (1 subgoal):
 1. A w
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intI [intro!]: assumes P1:"(\<And> w. w \<Turnstile> A)" shows "\<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A ?w

goal (1 subgoal):
 1. \<turnstile> A
[PROOF STEP]
by (auto simp: Valid_def)


[STATEMENT]
lemma inteq_reflection: assumes P1: "\<turnstile> x=y" shows  "(x \<equiv> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<equiv> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<equiv> y
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> x = y
[PROOF STEP]
have P2: "\<forall>w. x w = y w"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> x = y

goal (1 subgoal):
 1. \<forall>w. x w = y w
[PROOF STEP]
by (unfold Valid_def unl_lift2)
[PROOF STATE]
proof (state)
this:
\<forall>w. x w = y w

goal (1 subgoal):
 1. x \<equiv> y
[PROOF STEP]
hence P3:"x=y"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. x w = y w

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x \<equiv> y
[PROOF STEP]
thus "x \<equiv> y"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x \<equiv> y
[PROOF STEP]
by (rule "eq_reflection")
[PROOF STATE]
proof (state)
this:
x \<equiv> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma int_simps:
  "\<turnstile> (x=x) = #True"
  "\<turnstile> (\<not> #True) = #False"
  "\<turnstile> (\<not> #False) = #True"
  "\<turnstile> (\<not>\<not> P) = P"
  "\<turnstile> ((\<not> P) = P) = #False"
  "\<turnstile> (P = (\<not>P)) = #False"
  "\<turnstile> (P \<noteq> Q) = (P = (\<not> Q))"
  "\<turnstile> (#True=P) = P"
  "\<turnstile> (P=#True) = P"
  "\<turnstile> (#True \<longrightarrow> P) = P"
  "\<turnstile> (#False \<longrightarrow> P) = #True"
  "\<turnstile> (P \<longrightarrow> #True) = #True"
  "\<turnstile> (P \<longrightarrow> P) = #True"
  "\<turnstile> (P \<longrightarrow> #False) = (\<not>P)"
  "\<turnstile> (P \<longrightarrow> ~P) = (\<not>P)"
  "\<turnstile> (P \<and> #True) = P"
  "\<turnstile> (#True \<and> P) = P"
  "\<turnstile> (P \<and> #False) = #False"
  "\<turnstile> (#False \<and> P) = #False"
  "\<turnstile> (P \<and> P) = P"
  "\<turnstile> (P \<and> ~P) = #False"
  "\<turnstile> (\<not>P \<and> P) = #False"
  "\<turnstile> (P \<or> #True) = #True"
  "\<turnstile> (#True \<or> P) = #True"
  "\<turnstile> (P \<or> #False) = P"
  "\<turnstile> (#False \<or> P) = P"
  "\<turnstile> (P \<or> P) = P"
  "\<turnstile> (P \<or> \<not>P) = #True"
  "\<turnstile> (\<not>P \<or> P) = #True"
  "\<turnstile> (\<forall> x. P) = P"
  "\<turnstile> (\<exists> x. P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<turnstile> x = x = #True &&& \<turnstile> \<not> #True = #False &&& \<turnstile> \<not> #False = #True) &&& (\<turnstile> \<not> \<not> P = P &&& \<turnstile> \<not> P = P = #False) &&& \<turnstile> P = \<not> P = #False &&& \<turnstile> P \<noteq> Q = (P = \<not> Q)) &&& ((\<turnstile> #True = P = P &&& \<turnstile> P = #True = P) &&& \<turnstile> (#True \<longrightarrow> P) = P &&& \<turnstile> (#False \<longrightarrow> P) = #True) &&& (\<turnstile> (P \<longrightarrow> #True) = #True &&& \<turnstile> (P \<longrightarrow> P) = #True) &&& \<turnstile> (P \<longrightarrow> #False) = \<not> P &&& \<turnstile> (P \<longrightarrow> \<not> P) = \<not> P) &&& (((\<turnstile> (P \<and> #True) = P &&& \<turnstile> (#True \<and> P) = P) &&& \<turnstile> (P \<and> #False) = #False &&& \<turnstile> (#False \<and> P) = #False) &&& (\<turnstile> (P \<and> P) = P &&& \<turnstile> (P \<and> \<not> P) = #False) &&& \<turnstile> (\<not> P \<and> P) = #False &&& \<turnstile> (P \<or> #True) = #True) &&& ((\<turnstile> (#True \<or> P) = #True &&& \<turnstile> (P \<or> #False) = P) &&& \<turnstile> (#False \<or> P) = P &&& \<turnstile> (P \<or> P) = P) &&& (\<turnstile> (P \<or> \<not> P) = #True &&& \<turnstile> (\<not> P \<or> P) = #True) &&& \<turnstile> (\<forall>x. P) = P &&& \<turnstile> (\<exists>x. P) = P
[PROOF STEP]
by auto


[STATEMENT]
lemma Not_Rall: "\<turnstile> (\<not>(\<forall> x. F x)) = (\<exists> x. \<not>F x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<not> (\<forall>x. F x) = (\<exists>x. \<not> F x)
[PROOF STEP]
by auto


[STATEMENT]
lemma Not_Rex: "\<turnstile> (\<not>(\<exists> x. F x)) = (\<forall> x. \<not>F x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<not> (\<exists>x. F x) = (\<forall>x. \<not> F x)
[PROOF STEP]
by auto


[STATEMENT]
lemma TrueW [simp]: "\<turnstile> #True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> #True
[PROOF STEP]
by auto


[STATEMENT]
lemma int_eq: "\<turnstile> X = Y \<Longrightarrow> X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> X = Y \<Longrightarrow> X = Y
[PROOF STEP]
by (auto simp: inteq_reflection)


[STATEMENT]
lemma int_iffI:
  assumes "\<turnstile> F \<longrightarrow> G" and "\<turnstile> G \<longrightarrow> F"
  shows "\<turnstile> F = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> F = G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile> F \<longrightarrow> G
\<turnstile> G \<longrightarrow> F

goal (1 subgoal):
 1. \<turnstile> F = G
[PROOF STEP]
by force


[STATEMENT]
lemma int_iffD1: assumes h: "\<turnstile> F = G" shows "\<turnstile> F \<longrightarrow> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> F \<longrightarrow> G
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
\<turnstile> F = G

goal (1 subgoal):
 1. \<turnstile> F \<longrightarrow> G
[PROOF STEP]
by auto


[STATEMENT]
lemma int_iffD2: assumes h: "\<turnstile> F = G" shows "\<turnstile> G \<longrightarrow> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> G \<longrightarrow> F
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
\<turnstile> F = G

goal (1 subgoal):
 1. \<turnstile> G \<longrightarrow> F
[PROOF STEP]
by auto


[STATEMENT]
lemma lift_imp_trans:
  assumes "\<turnstile> A \<longrightarrow> B" and "\<turnstile> B \<longrightarrow> C"
  shows "\<turnstile> A \<longrightarrow> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> A \<longrightarrow> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile> A \<longrightarrow> B
\<turnstile> B \<longrightarrow> C

goal (1 subgoal):
 1. \<turnstile> A \<longrightarrow> C
[PROOF STEP]
by force


[STATEMENT]
lemma lift_imp_neg: assumes "\<turnstile> A \<longrightarrow> B" shows "\<turnstile> \<not>B \<longrightarrow> \<not>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<not> B \<longrightarrow> \<not> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile> A \<longrightarrow> B

goal (1 subgoal):
 1. \<turnstile> \<not> B \<longrightarrow> \<not> A
[PROOF STEP]
by auto


[STATEMENT]
lemma lift_and_com:  "\<turnstile> (A \<and> B) = (B \<and> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> (A \<and> B) = (B \<and> A)
[PROOF STEP]
by auto


[STATEMENT]
lemma gen_dfs_outer_initial:
  assumes "finite (E\<^sup>*``V0)"
  shows "gen_dfs_outer E (E\<^sup>*``V0) V0 V0 {} brk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_outer E (E\<^sup>* `` V0) V0 V0 {} brk
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (E\<^sup>* `` V0)

goal (1 subgoal):
 1. gen_dfs_outer E (E\<^sup>* `` V0) V0 V0 {} brk
[PROOF STEP]
unfolding gen_dfs_outer_def
[PROOF STATE]
proof (prove)
using this:
finite (E\<^sup>* `` V0)

goal (1 subgoal):
 1. V0 \<subseteq> E\<^sup>* `` V0 \<and> E `` E\<^sup>* `` V0 \<subseteq> E\<^sup>* `` V0 \<and> finite (E\<^sup>* `` V0) \<and> {} \<subseteq> E\<^sup>* `` V0 \<and> (\<not> brk \<longrightarrow> E `` {} \<subseteq> {}) \<and> V0 - V0 \<subseteq> {}
[PROOF STEP]
by (auto intro: rev_ImageI)


[STATEMENT]
lemma gen_dfs_pre_initial:
  assumes "gen_dfs_outer E U V0 it V False"
  assumes "v0\<in>U - V"
  shows "gen_dfs_pre E U {} V v0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_pre E U {} V v0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_outer E U V0 it V False
v0 \<in> U - V

goal (1 subgoal):
 1. gen_dfs_pre E U {} V v0
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_outer_def
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` V \<subseteq> V) \<and> V0 - it \<subseteq> V
v0 \<in> U - V

goal (1 subgoal):
 1. E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> v0 \<in> U \<and> E `` (V - {}) \<subseteq> V \<and> v0 \<notin> V \<and> {} \<subseteq> V \<and> (\<forall>v\<in>{}. (v, v0) \<in> (E \<inter> {} \<times> UNIV)\<^sup>*)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fin_U_imp_wf:
  assumes "finite U"
  shows "wf (gen_dfs_var U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (gen_dfs_var U)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite U

goal (1 subgoal):
 1. wf (gen_dfs_var U)
[PROOF STEP]
unfolding gen_dfs_var_def
[PROOF STATE]
proof (prove)
using this:
finite U

goal (1 subgoal):
 1. wf (finite_psupset U)
[PROOF STEP]
by auto


[STATEMENT]
lemma gen_dfs_pre_imp_wf:
  assumes "gen_dfs_pre E U S V u0"
  shows "wf (gen_dfs_var U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (gen_dfs_var U)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0

goal (1 subgoal):
 1. wf (gen_dfs_var U)
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_var_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)

goal (1 subgoal):
 1. wf (finite_psupset U)
[PROOF STEP]
by auto


[STATEMENT]
lemma gen_dfs_pre_imp_fin:
  assumes "gen_dfs_pre E U S V u0"
  shows "finite (E `` {u0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (E `` {u0})
[PROOF STEP]
apply (rule finite_subset[where B="U"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. E `` {u0} \<subseteq> U
 2. finite U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0

goal (2 subgoals):
 1. E `` {u0} \<subseteq> U
 2. finite U
[PROOF STEP]
unfolding gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)

goal (2 subgoals):
 1. E `` {u0} \<subseteq> U
 2. finite U
[PROOF STEP]
by auto


[STATEMENT]
lemma gen_dfs_pre_imp_fe:
  assumes "gen_dfs_pre E U S V u0"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0
    (E``{u0}) (insert u0 V) False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (E `` {u0}) (insert u0 V) False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0

goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (E `` {u0}) (insert u0 V) False
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_fe_inv_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)

goal (1 subgoal):
 1. (\<not> False \<longrightarrow> E `` (insert u0 V - insert u0 S) \<subseteq> insert u0 V) \<and> E `` {u0} - E `` {u0} \<subseteq> insert u0 V \<and> insert u0 V \<subseteq> insert u0 V \<and> insert u0 V \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - E `` {u0} - insert u0 S)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_fe_inv_pres_visited:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "t\<in>it" "it\<subseteq>E``{u0}" "t\<in>V'"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V' False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it - {t}) V' False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False
t \<in> it
it \<subseteq> E `` {u0}
t \<in> V'

goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it - {t}) V' False
[PROOF STEP]
unfolding gen_dfs_fe_inv_def
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
(\<not> False \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - it \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)
t \<in> it
it \<subseteq> E `` {u0}
t \<in> V'

goal (1 subgoal):
 1. (\<not> False \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - (it - {t}) \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_upper_aux:
  assumes "(x,y)\<in>E'\<^sup>*"
  assumes "(u0,x)\<in>E"
  assumes "u0\<in>U"
  assumes "E'\<subseteq>E"
  assumes "E``U \<subseteq> U"
  shows "y\<in>U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> E'\<^sup>*
(u0, x) \<in> E
u0 \<in> U
E' \<subseteq> E
E `` U \<subseteq> U

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
by induct auto


[STATEMENT]
lemma gen_dfs_fe_inv_imp_var:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "t\<in>it" "it\<subseteq>E``{u0}" "t\<notin>V'"
  shows "(V',V) \<in> gen_dfs_var U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V', V) \<in> gen_dfs_var U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'

goal (1 subgoal):
 1. (V', V) \<in> gen_dfs_var U
[PROOF STEP]
unfolding gen_dfs_fe_inv_def gen_dfs_pre_def gen_dfs_var_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> False \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - it \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'

goal (1 subgoal):
 1. (V', V) \<in> finite_psupset U
[PROOF STEP]
apply (clarsimp simp add: finite_psupset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subset> V' \<and> V' \<subseteq> U
[PROOF STEP]
apply (blast dest: gen_dfs_upper_aux)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done