[STATEMENT]
lemma ptensor_mat_assoc:
  assumes "vars1 \<inter> vars2 = {}"
    and "(vars1 \<union> vars2) \<inter> vars3 = {}"
    and "vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..< length dims}"
  shows "ptensor_mat dims (vars1 \<union> vars2) vars3 (ptensor_mat dims vars1 vars2 m1 m2) m3 =
         ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (ptensor_mat dims vars2 vars3 m2 m3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2.ptensor_mat dims (vars1 \<union> vars2) vars3 (partial_state2.ptensor_mat dims vars1 vars2 m1 m2) m3 = partial_state2.ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (partial_state2.ptensor_mat dims vars2 vars3 m2 m3)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.ptensor_mat dims (vars1 \<union> vars2) vars3 (partial_state2.ptensor_mat dims vars1 vars2 m1 m2) m3 = partial_state2.ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (partial_state2.ptensor_mat dims vars2 vars3 m2 m3)
[PROOF STEP]
interpret a: partial_state2 dims vars1 vars2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars1 vars2
[PROOF STEP]
by (unfold_locales, rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.ptensor_mat dims (vars1 \<union> vars2) vars3 (a.ptensor_mat m1 m2) m3 = partial_state2.ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (partial_state2.ptensor_mat dims vars2 vars3 m2 m3)
[PROOF STEP]
interpret b: partial_state2 dims "vars1 \<union> vars2" vars3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 (vars1 \<union> vars2) vars3
[PROOF STEP]
by (unfold_locales, rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = partial_state2.ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (partial_state2.ptensor_mat dims vars2 vars3 m2 m3)
[PROOF STEP]
interpret c: partial_state2 dims vars2 vars3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars2 vars3
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(vars1 \<union> vars2) \<inter> vars3 = {}

goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = partial_state2.ptensor_mat dims vars1 (vars2 \<union> vars3) m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
interpret d: partial_state2 dims vars1 "vars2 \<union> vars3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars1 (vars2 \<union> vars3)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have uassoc: "vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have **: "{i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)} = vars1 \<union> vars2 \<union> vars3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)} = vars1 \<union> vars2 \<union> vars3
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)} = vars1 \<union> vars2 \<union> vars3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)} = vars1 \<union> vars2 \<union> vars3

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have finite_union: "finite (vars1 \<union> vars2 \<union> vars3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars1 \<union> vars2 \<union> vars3)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. finite (vars1 \<union> vars2 \<union> vars3)
[PROOF STEP]
using subset_eq_atLeast0_lessThan_finite
[PROOF STATE]
proof (prove)
using this:
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}
?N \<subseteq> {0..<?n} \<Longrightarrow> finite ?N

goal (1 subgoal):
 1. finite (vars1 \<union> vars2 \<union> vars3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (vars1 \<union> vars2 \<union> vars3)

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m1eq: "digit_encode a.dims0 (digit_decode b.dims1 (nths (digit_encode b.dims0 i) b.vars1'))
    = nths (digit_encode b.dims0 i) b.vars1'" if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode a.dims0 (digit_decode b.dims1 (nths (digit_encode b.dims0 i) b.vars1')) = nths (digit_encode b.dims0 i) b.vars1'
[PROOF STEP]
unfolding a.dims0_def a.vars0_def b.dims1_def b.dims0_def b.vars0_def b.vars1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode (nths dims (vars1 \<union> vars2)) (digit_decode (nths dims (vars1 \<union> vars2)) (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)))) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (subst digit_encode_decode)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) \<lhd> nths dims (vars1 \<union> vars2)
 2. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (rule valid_index_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i \<lhd> nths dims (vars1 \<union> vars2 \<union> vars3)
 2. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
 3. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (rule digit_encode_valid_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
 2. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
 3. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < state_sig.d b.dims0

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
 2. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
 3. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
unfolding state_sig.d_def b.dims0_def b.vars0_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
 2. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
 3. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> digit_encode a.dims0 (digit_decode b.dims1 (nths (digit_encode b.dims0 ?i1) b.vars1')) = nths (digit_encode b.dims0 ?i1) b.vars1'

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m1index: "partial_state.encode1 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i)
    = partial_state.encode1 d.dims0 d.vars1' i" if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i) = partial_state.encode1 d.dims0 d.vars1' i
[PROOF STEP]
unfolding partial_state.encode1_def partial_state.dims1_def a.nths_vars1' d.nths_vars1' b.nths_vars1'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode d.dims1 (nths (digit_encode a.dims0 (digit_decode b.dims1 (nths (digit_encode b.dims0 i) b.vars1'))) a.vars1') = digit_decode d.dims1 (nths (digit_encode d.dims0 i) d.vars1')
[PROOF STEP]
apply (rule arg_cong[where f="digit_decode d.dims1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (digit_encode a.dims0 (digit_decode b.dims1 (nths (digit_encode b.dims0 i) b.vars1'))) a.vars1' = nths (digit_encode d.dims0 i) d.vars1'
[PROOF STEP]
apply (subst m1eq[OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode b.dims0 i) b.vars1') a.vars1' = nths (digit_encode d.dims0 i) d.vars1'
[PROOF STEP]
unfolding a.vars0_def a.vars1'_def b.dims0_def b.vars0_def b.vars1'_def d.dims0_def d.vars0_def d.vars1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using nths_assoc_three_A[OF assms(1-2)]
[PROOF STATE]
proof (prove)
using this:
nths (nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars1) = nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars1)

goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using uassoc
[PROOF STATE]
proof (prove)
using this:
nths (nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars1) = nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars1)
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> partial_state.encode1 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' ?i1) = partial_state.encode1 d.dims0 d.vars1' ?i1

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m2eq1: "digit_encode a.dims0 (digit_decode (nths b.dims0 b.vars1') (nths (digit_encode b.dims0 i) b.vars1'))
    = nths (digit_encode b.dims0 i) b.vars1'"
    if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode a.dims0 (digit_decode (nths b.dims0 b.vars1') (nths (digit_encode b.dims0 i) b.vars1')) = nths (digit_encode b.dims0 i) b.vars1'
[PROOF STEP]
unfolding a.dims0_def a.vars0_def b.nths_vars1' b.dims1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode (nths dims (vars1 \<union> vars2)) (digit_decode (nths dims (vars1 \<union> vars2)) (nths (digit_encode b.dims0 i) b.vars1')) = nths (digit_encode b.dims0 i) b.vars1'
[PROOF STEP]
apply (subst digit_encode_decode)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode b.dims0 i) b.vars1' \<lhd> nths dims (vars1 \<union> vars2)
 2. nths (digit_encode b.dims0 i) b.vars1' = nths (digit_encode b.dims0 i) b.vars1'
[PROOF STEP]
unfolding b.vars1'_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode b.dims0 i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) \<lhd> nths dims (vars1 \<union> vars2)
 2. nths (digit_encode b.dims0 i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) = nths (digit_encode b.dims0 i) (ind_in_set b.vars0 ` (vars1 \<union> vars2))
[PROOF STEP]
apply (rule valid_index_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode b.dims0 i \<lhd> nths dims b.vars0
 2. vars1 \<union> vars2 \<subseteq> b.vars0
 3. nths (digit_encode b.dims0 i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) = nths (digit_encode b.dims0 i) (ind_in_set b.vars0 ` (vars1 \<union> vars2))
[PROOF STEP]
unfolding b.dims0_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode (nths dims b.vars0) i \<lhd> nths dims b.vars0
 2. vars1 \<union> vars2 \<subseteq> b.vars0
 3. nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2))
[PROOF STEP]
apply (rule digit_encode_valid_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < prod_list (nths dims b.vars0)
 2. vars1 \<union> vars2 \<subseteq> b.vars0
 3. nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < state_sig.d b.dims0

goal (3 subgoals):
 1. i < prod_list (nths dims b.vars0)
 2. vars1 \<union> vars2 \<subseteq> b.vars0
 3. nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims b.vars0) i) (ind_in_set b.vars0 ` (vars1 \<union> vars2))
[PROOF STEP]
unfolding state_sig.d_def b.dims0_def b.vars0_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
 2. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
 3. nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> digit_encode a.dims0 (digit_decode (nths b.dims0 b.vars1') (nths (digit_encode b.dims0 ?i1) b.vars1')) = nths (digit_encode b.dims0 ?i1) b.vars1'

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m2eq2: "digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 i) (- d.vars1')))
    = nths (digit_encode d.dims0 i) (- d.vars1')"
    if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 i) (- d.vars1'))) = nths (digit_encode d.dims0 i) (- d.vars1')
[PROOF STEP]
unfolding c.dims0_def c.vars0_def d.nths_vars2' d.dims2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode (nths dims (vars2 \<union> vars3)) (digit_decode (nths dims (vars2 \<union> vars3)) (nths (digit_encode d.dims0 i) (- d.vars1'))) = nths (digit_encode d.dims0 i) (- d.vars1')
[PROOF STEP]
apply (subst digit_encode_decode)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode d.dims0 i) (- d.vars1') \<lhd> nths dims (vars2 \<union> vars3)
 2. nths (digit_encode d.dims0 i) (- d.vars1') = nths (digit_encode d.dims0 i) (- d.vars1')
[PROOF STEP]
unfolding d.vars1'_def d.vars0_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) \<lhd> nths dims (vars2 \<union> vars3)
 2. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
 2. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode d.dims0 i)
 3. nths (digit_encode d.dims0 i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 4. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode d.dims0 i)
 2. nths (digit_encode d.dims0 i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 3. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode d.dims0 i)
[PROOF STEP]
apply (auto simp only: length_digit_encode d.dims0_def d.vars0_def length_nths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)}
[PROOF STEP]
by (auto simp add: ** uassoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode d.dims0 i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 2. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (rule valid_index_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode d.dims0 i \<lhd> nths dims (vars1 \<union> (vars2 \<union> vars3))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode d.dims0 i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
unfolding d.dims0_def d.vars0_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i \<lhd> nths dims (vars1 \<union> (vars2 \<union> vars3))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (rule digit_encode_valid_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < state_sig.d b.dims0

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
unfolding state_sig.d_def b.dims0_def b.vars0_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using uassoc
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 ?i1) (- d.vars1'))) = nths (digit_encode d.dims0 ?i1) (- d.vars1')

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m2index: "partial_state.encode2 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i) =
    partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i)"
    if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i) = partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i)
[PROOF STEP]
unfolding partial_state.encode2_def partial_state.encode1_def
      partial_state.dims2_def a.nths_vars2' partial_state.dims1_def c.nths_vars1'
      a.dims2_def c.dims1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode (nths dims vars2) (nths (digit_encode a.dims0 (digit_decode (nths b.dims0 b.vars1') (nths (digit_encode b.dims0 i) b.vars1'))) (- a.vars1')) = digit_decode (nths dims vars2) (nths (digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 i) (- d.vars1')))) c.vars1')
[PROOF STEP]
apply (rule arg_cong[where f="digit_decode (nths dims vars2)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (digit_encode a.dims0 (digit_decode (nths b.dims0 b.vars1') (nths (digit_encode b.dims0 i) b.vars1'))) (- a.vars1') = nths (digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 i) (- d.vars1')))) c.vars1'
[PROOF STEP]
apply (subst m2eq1[OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode b.dims0 i) b.vars1') (- a.vars1') = nths (digit_encode c.dims0 (digit_decode (nths d.dims0 (- d.vars1')) (nths (digit_encode d.dims0 i) (- d.vars1')))) c.vars1'
[PROOF STEP]
apply (subst m2eq2[OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode b.dims0 i) b.vars1') (- a.vars1') = nths (nths (digit_encode d.dims0 i) (- d.vars1')) c.vars1'
[PROOF STEP]
unfolding b.dims0_def b.vars0_def b.vars1'_def a.vars1'_def a.vars0_def
      d.dims0_def d.vars0_def d.vars1'_def c.vars1'_def c.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (- ind_in_set (vars1 \<union> vars2) ` vars1) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vars1 \<inter> vars2 = {}
 2. card (vars1 \<union> vars2) = length (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)))
 3. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> vars2 = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> vars2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card (vars1 \<union> vars2) = length (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)))
 2. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> vars2) = length (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)))
[PROOF STEP]
apply (auto simp only: length_nths length_digit_encode)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> vars2) = card {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3} \<and> i \<in> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)}
[PROOF STEP]
apply (rule bij_betw_same_card[where f="ind_in_set (vars1 \<union> vars2 \<union> vars3)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars1 \<union> vars2) {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3} \<and> i \<in> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)}
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars1 \<union> vars2) \<and> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3} \<and> i \<in> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars1 \<union> vars2)
 2. ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3} \<and> i \<in> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars1 \<union> vars2)
[PROOF STEP]
apply (rule ind_in_set_inj')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<union> vars2 \<subseteq> vars1 \<union> vars2 \<union> vars3
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3} \<and> i \<in> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> vars1 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
 2. \<And>xa. xa \<in> vars2 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
[PROOF STEP]
using finite_union
[PROOF STATE]
proof (prove)
using this:
finite (vars1 \<union> vars2 \<union> vars3)

goal (2 subgoals):
 1. \<And>xa. xa \<in> vars1 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
 2. \<And>xa. xa \<in> vars2 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
[PROOF STEP]
by (auto simp add: ** intro: ind_in_set_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
 2. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 3. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 2. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
[PROOF STEP]
apply (auto simp only: length_digit_encode length_nths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)}
[PROOF STEP]
by (auto simp add: ** uassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
using nths_assoc_three_B[OF assms(1-2)] uassoc
[PROOF STATE]
proof (prove)
using this:
nths (nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars2)
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))) (ind_in_set (vars1 \<union> vars2) ` vars2) = nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> partial_state.encode2 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' ?i1) = partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' ?i1)

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m3eq: "digit_encode c.dims0 (digit_decode d.dims2 (nths (digit_encode d.dims0 i) (- d.vars1')))
    = nths (digit_encode d.dims0 i) (- d.vars1')" if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode c.dims0 (digit_decode d.dims2 (nths (digit_encode d.dims0 i) (- d.vars1'))) = nths (digit_encode d.dims0 i) (- d.vars1')
[PROOF STEP]
unfolding c.dims0_def c.vars0_def d.dims2_def d.dims0_def d.vars1'_def d.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_encode (nths dims (vars2 \<union> vars3)) (digit_decode (nths dims (vars2 \<union> vars3)) (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1))) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (subst digit_encode_decode)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) \<lhd> nths dims (vars2 \<union> vars3)
 2. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
 2. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 4. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 2. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
[PROOF STEP]
apply (auto simp only: length_digit_encode length_nths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)}
[PROOF STEP]
by (auto simp add: ** uassoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)) \<lhd> nths dims (vars2 \<union> vars3)
 2. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (rule valid_index_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i \<lhd> nths dims (vars1 \<union> (vars2 \<union> vars3))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
apply (rule digit_encode_valid_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < state_sig.d b.dims0

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
unfolding state_sig.d_def b.dims0_def b.vars0_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
using uassoc
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims (vars1 \<union> vars2 \<union> vars3))
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (3 subgoals):
 1. i < prod_list (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars2 \<union> vars3 \<subseteq> vars1 \<union> (vars2 \<union> vars3)
 3. nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1) = nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> digit_encode c.dims0 (digit_decode d.dims2 (nths (digit_encode d.dims0 ?i1) (- d.vars1'))) = nths (digit_encode d.dims0 ?i1) (- d.vars1')

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
have m3index: "partial_state.encode2 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i) =
    partial_state.encode2 b.dims0 b.vars1' i"
    if "i < state_sig.d b.dims0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i) = partial_state.encode2 b.dims0 b.vars1' i
[PROOF STEP]
unfolding partial_state.encode2_def partial_state.dims2_def c.nths_vars2' d.nths_vars2' b.nths_vars2'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode c.dims2 (nths (digit_encode c.dims0 (digit_decode d.dims2 (nths (digit_encode d.dims0 i) (- d.vars1')))) (- c.vars1')) = digit_decode c.dims2 (nths (digit_encode b.dims0 i) (- b.vars1'))
[PROOF STEP]
apply (rule arg_cong[where f="digit_decode c.dims2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (digit_encode c.dims0 (digit_decode d.dims2 (nths (digit_encode d.dims0 i) (- d.vars1')))) (- c.vars1') = nths (digit_encode b.dims0 i) (- b.vars1')
[PROOF STEP]
apply (subst m3eq[OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode d.dims0 i) (- d.vars1')) (- c.vars1') = nths (digit_encode b.dims0 i) (- b.vars1')
[PROOF STEP]
unfolding d.dims0_def d.vars0_def d.vars1'_def c.vars1'_def b.dims0_def b.vars1'_def b.vars0_def c.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (- ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` vars1)) (- ind_in_set (vars2 \<union> vars3) ` vars2) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
 2. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 3. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (- ind_in_set (vars2 \<union> vars3) ` vars2) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
 2. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (- ind_in_set (vars2 \<union> vars3) ` vars2) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = length (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i)
[PROOF STEP]
apply (auto simp only: length_digit_encode length_nths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> (vars2 \<union> vars3)) = card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)}
[PROOF STEP]
by (auto simp add: ** uassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (- ind_in_set (vars2 \<union> vars3) ` vars2) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vars2 \<inter> vars3 = {}
 2. card (vars2 \<union> vars3) = length (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)))
 3. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card (vars2 \<union> vars3) = length (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)))
 2. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars2 \<union> vars3) = length (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)))
[PROOF STEP]
apply (auto simp only: length_nths length_digit_encode)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars2 \<union> vars3) = card {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)} \<and> i \<in> ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)}
[PROOF STEP]
apply (rule bij_betw_same_card[where f="ind_in_set (vars1 \<union> vars2 \<union> vars3)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars2 \<union> vars3) {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)} \<and> i \<in> ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)}
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars2 \<union> vars3) \<and> ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars2 \<union> vars3) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)} \<and> i \<in> ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars2 \<union> vars3)
 2. ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars2 \<union> vars3) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)} \<and> i \<in> ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set (vars1 \<union> vars2 \<union> vars3)) (vars2 \<union> vars3)
[PROOF STEP]
apply (rule ind_in_set_inj')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<union> vars3 \<subseteq> vars1 \<union> vars2 \<union> vars3
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars2 \<union> vars3) = {i. i < card {i. i < length dims \<and> i \<in> vars1 \<union> (vars2 \<union> vars3)} \<and> i \<in> ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3)}
[PROOF STEP]
apply (auto simp add: uassoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> vars2 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
 2. \<And>xa. xa \<in> vars3 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
[PROOF STEP]
using finite_union
[PROOF STATE]
proof (prove)
using this:
finite (vars1 \<union> vars2 \<union> vars3)

goal (2 subgoals):
 1. \<And>xa. xa \<in> vars2 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
 2. \<And>xa. xa \<in> vars3 \<Longrightarrow> ind_in_set (vars1 \<union> vars2 \<union> vars3) xa < card {i. i < length dims \<and> (i \<in> vars1 \<or> i \<in> vars2 \<or> i \<in> vars3)}
[PROOF STEP]
by (auto simp add: ** intro: ind_in_set_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (- ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars1 \<union> vars2))
[PROOF STEP]
apply (subst nths_complement_ind_in_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (vars1 \<union> vars2) \<inter> vars3 = {}
 2. card (vars1 \<union> vars2 \<union> vars3) = length (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i)
 3. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars3)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vars1 \<union> vars2) \<inter> vars3 = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. (vars1 \<union> vars2) \<inter> vars3 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card (vars1 \<union> vars2 \<union> vars3) = length (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i)
 2. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars3)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> vars2 \<union> vars3) = length (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i)
[PROOF STEP]
apply (auto simp only: length_nths length_digit_encode)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (vars1 \<union> vars2 \<union> vars3) = card {i. i < length dims \<and> i \<in> vars1 \<union> vars2 \<union> vars3}
[PROOF STEP]
by (auto simp add: ** uassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars3)
[PROOF STEP]
using nths_assoc_three_C[OF assms(1-2)] uassoc
[PROOF STATE]
proof (prove)
using this:
nths (nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths ?xs (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars3)
vars1 \<union> (vars2 \<union> vars3) = vars1 \<union> vars2 \<union> vars3

goal (1 subgoal):
 1. nths (nths (digit_encode (nths dims (vars1 \<union> (vars2 \<union> vars3))) i) (ind_in_set (vars1 \<union> (vars2 \<union> vars3)) ` (vars2 \<union> vars3))) (ind_in_set (vars2 \<union> vars3) ` vars3) = nths (digit_encode (nths dims (vars1 \<union> vars2 \<union> vars3)) i) (ind_in_set (vars1 \<union> vars2 \<union> vars3) ` vars3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < state_sig.d b.dims0 \<Longrightarrow> partial_state.encode2 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' ?i1) = partial_state.encode2 b.dims0 b.vars1' ?i1

goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)
[PROOF STEP]
unfolding a.ptensor_mat_def b.ptensor_mat_def c.ptensor_mat_def d.ptensor_mat_def partial_state.tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (state_sig.d b.dims0) (state_sig.d b.dims0) (\<lambda>(i, j). mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = mat (state_sig.d d.dims0) (state_sig.d d.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
apply (rule cong_mat)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. state_sig.d b.dims0 = state_sig.d d.dims0
 2. state_sig.d b.dims0 = state_sig.d d.dims0
 3. \<And>i j. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d b.dims0 = state_sig.d d.dims0
[PROOF STEP]
unfolding b.dims0_def d.dims0_def b.vars0_def d.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d (nths dims (vars1 \<union> vars2 \<union> vars3)) = state_sig.d (nths dims (vars1 \<union> (vars2 \<union> vars3)))
[PROOF STEP]
apply (subgoal_tac "vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3) \<Longrightarrow> state_sig.d (nths dims (vars1 \<union> vars2 \<union> vars3)) = state_sig.d (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. state_sig.d b.dims0 = state_sig.d d.dims0
 2. \<And>i j. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d b.dims0 = state_sig.d d.dims0
[PROOF STEP]
unfolding b.dims0_def d.dims0_def b.vars0_def d.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d (nths dims (vars1 \<union> vars2 \<union> vars3)) = state_sig.d (nths dims (vars1 \<union> (vars2 \<union> vars3)))
[PROOF STEP]
apply (subgoal_tac "vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3) \<Longrightarrow> state_sig.d (nths dims (vars1 \<union> vars2 \<union> vars3)) = state_sig.d (nths dims (vars1 \<union> (vars2 \<union> vars3)))
 2. vars1 \<union> vars2 \<union> vars3 = vars1 \<union> (vars2 \<union> vars3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
assume lti: "i < state_sig.d b.dims0" and ltj: "j < state_sig.d b.dims0"
[PROOF STATE]
proof (state)
this:
i < state_sig.d b.dims0
j < state_sig.d b.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have lti': "i < state_sig.d d.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < state_sig.d d.dims0
[PROOF STEP]
using \<open>state_sig.d b.dims0 = state_sig.d d.dims0\<close> lti
[PROOF STATE]
proof (prove)
using this:
state_sig.d b.dims0 = state_sig.d d.dims0
i < state_sig.d b.dims0

goal (1 subgoal):
 1. i < state_sig.d d.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < state_sig.d d.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have ltj': "j < state_sig.d d.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < state_sig.d d.dims0
[PROOF STEP]
using \<open>state_sig.d b.dims0 = state_sig.d d.dims0\<close> ltj
[PROOF STATE]
proof (prove)
using this:
state_sig.d b.dims0 = state_sig.d d.dims0
j < state_sig.d b.dims0

goal (1 subgoal):
 1. j < state_sig.d d.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < state_sig.d d.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have eq1: "partial_state.d2 d.dims0 d.vars1' = state_sig.d c.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.d2 d.dims0 d.vars1' = state_sig.d c.dims0
[PROOF STEP]
unfolding partial_state.d2_def partial_state.dims2_def d.nths_vars2'
          d.dims2_def state_sig.d_def c.dims0_def c.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths dims (vars2 \<union> vars3)) = prod_list (nths dims (vars2 \<union> vars3))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.d2 d.dims0 d.vars1' = state_sig.d c.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have eq2: "partial_state.d1 b.dims0 b.vars1' = state_sig.d a.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.d1 b.dims0 b.vars1' = state_sig.d a.dims0
[PROOF STEP]
unfolding partial_state.d1_def partial_state.dims1_def b.nths_vars1'
          b.dims1_def state_sig.d_def a.dims0_def a.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths dims (vars1 \<union> vars2)) = prod_list (nths dims (vars1 \<union> vars2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.d1 b.dims0 b.vars1' = state_sig.d a.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have lt1: "partial_state.encode2 d.dims0 d.vars1' i < state_sig.d c.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 d.dims0 d.vars1' i < state_sig.d c.dims0
[PROOF STEP]
using partial_state.encode2_lt[OF lti', where vars=d.vars1'] eq1
[PROOF STATE]
proof (prove)
using this:
partial_state.encode2 d.dims0 d.vars1' i < partial_state.d2 d.dims0 d.vars1'
partial_state.d2 d.dims0 d.vars1' = state_sig.d c.dims0

goal (1 subgoal):
 1. partial_state.encode2 d.dims0 d.vars1' i < state_sig.d c.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 d.dims0 d.vars1' i < state_sig.d c.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have lt2: "partial_state.encode2 d.dims0 d.vars1' j < state_sig.d c.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 d.dims0 d.vars1' j < state_sig.d c.dims0
[PROOF STEP]
using partial_state.encode2_lt[OF ltj', where vars=d.vars1'] eq1
[PROOF STATE]
proof (prove)
using this:
partial_state.encode2 d.dims0 d.vars1' j < partial_state.d2 d.dims0 d.vars1'
partial_state.d2 d.dims0 d.vars1' = state_sig.d c.dims0

goal (1 subgoal):
 1. partial_state.encode2 d.dims0 d.vars1' j < state_sig.d c.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 d.dims0 d.vars1' j < state_sig.d c.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have lt3: "partial_state.encode1 b.dims0 b.vars1' i < state_sig.d a.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 b.dims0 b.vars1' i < state_sig.d a.dims0
[PROOF STEP]
using partial_state.encode1_lt[OF lti, where vars=b.vars1'] eq2
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 b.dims0 b.vars1' i < partial_state.d1 b.dims0 b.vars1'
partial_state.d1 b.dims0 b.vars1' = state_sig.d a.dims0

goal (1 subgoal):
 1. partial_state.encode1 b.dims0 b.vars1' i < state_sig.d a.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 b.dims0 b.vars1' i < state_sig.d a.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
have lt4: "partial_state.encode1 b.dims0 b.vars1' j < state_sig.d a.dims0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 b.dims0 b.vars1' j < state_sig.d a.dims0
[PROOF STEP]
using partial_state.encode1_lt[OF ltj, where vars=b.vars1'] eq2
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 b.dims0 b.vars1' j < partial_state.d1 b.dims0 b.vars1'
partial_state.d1 b.dims0 b.vars1' = state_sig.d a.dims0

goal (1 subgoal):
 1. partial_state.encode1 b.dims0 b.vars1' j < state_sig.d a.dims0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 b.dims0 b.vars1' j < state_sig.d a.dims0

goal (1 subgoal):
 1. \<lbrakk>i < state_sig.d b.dims0; j < state_sig.d b.dims0\<rbrakk> \<Longrightarrow> (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))
[PROOF STEP]
apply (auto simp add: lt1 lt2 lt3 lt4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 $$ (partial_state.encode1 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i), partial_state.encode1 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' j)) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' i), partial_state.encode2 a.dims0 a.vars1' (partial_state.encode1 b.dims0 b.vars1' j)) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j) = m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * (m2 $$ (partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i), partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' j)) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i), partial_state.encode2 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' j)))
[PROOF STEP]
apply (simp only: m1index[OF lti] m1index[OF ltj] m2index[OF lti] m2index[OF ltj] m3index[OF lti] m3index[OF ltj])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * m2 $$ (partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i), partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' j)) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j) = m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * (m2 $$ (partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' i), partial_state.encode1 c.dims0 c.vars1' (partial_state.encode2 d.dims0 d.vars1' j)) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case (i, j) of (i, j) \<Rightarrow> mat (state_sig.d a.dims0) (state_sig.d a.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 a.dims0 a.vars1' i, partial_state.encode1 a.dims0 a.vars1' j) * m2 $$ (partial_state.encode2 a.dims0 a.vars1' i, partial_state.encode2 a.dims0 a.vars1' j)) $$ (partial_state.encode1 b.dims0 b.vars1' i, partial_state.encode1 b.dims0 b.vars1' j) * m3 $$ (partial_state.encode2 b.dims0 b.vars1' i, partial_state.encode2 b.dims0 b.vars1' j)) = (case (i, j) of (i, j) \<Rightarrow> m1 $$ (partial_state.encode1 d.dims0 d.vars1' i, partial_state.encode1 d.dims0 d.vars1' j) * mat (state_sig.d c.dims0) (state_sig.d c.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 c.dims0 c.vars1' i, partial_state.encode1 c.dims0 c.vars1' j) * m3 $$ (partial_state.encode2 c.dims0 c.vars1' i, partial_state.encode2 c.dims0 c.vars1' j)) $$ (partial_state.encode2 d.dims0 d.vars1' i, partial_state.encode2 d.dims0 d.vars1' j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
b.ptensor_mat (a.ptensor_mat m1 m2) m3 = d.ptensor_mat m1 (c.ptensor_mat m2 m3)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmat_extension_assoc:
  assumes "vars1 \<inter> vars2 = {}"
    and "(vars1 \<union> vars2) \<inter> vars3 = {}"
    and "vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..< length dims}"
  shows "pmat_extension dims vars1 (vars2 \<union> vars3) m =
         pmat_extension dims (vars1 \<union> vars2) vars3 (pmat_extension dims vars1 vars2 m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2.pmat_extension dims vars1 (vars2 \<union> vars3) m = partial_state2.pmat_extension dims (vars1 \<union> vars2) vars3 (partial_state2.pmat_extension dims vars1 vars2 m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.pmat_extension dims vars1 (vars2 \<union> vars3) m = partial_state2.pmat_extension dims (vars1 \<union> vars2) vars3 (partial_state2.pmat_extension dims vars1 vars2 m)
[PROOF STEP]
interpret a: partial_state2 dims vars1 vars2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars1 vars2
[PROOF STEP]
by (unfold_locales, rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.pmat_extension dims vars1 (vars2 \<union> vars3) m = partial_state2.pmat_extension dims (vars1 \<union> vars2) vars3 (a.pmat_extension m)
[PROOF STEP]
interpret b: partial_state2 dims "vars1 \<union> vars2" vars3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 (vars1 \<union> vars2) vars3
[PROOF STEP]
by (unfold_locales, rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.pmat_extension dims vars1 (vars2 \<union> vars3) m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
interpret c: partial_state2 dims vars2 vars3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars2 vars3
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(vars1 \<union> vars2) \<inter> vars3 = {}

goal (1 subgoal):
 1. vars2 \<inter> vars3 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.pmat_extension dims vars1 (vars2 \<union> vars3) m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
interpret d: partial_state2 dims vars1 "vars2 \<union> vars3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars1 (vars2 \<union> vars3)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}
(vars1 \<union> vars2) \<inter> vars3 = {}
vars1 \<union> vars2 \<union> vars3 \<subseteq> {0..<length dims}

goal (1 subgoal):
 1. vars1 \<inter> (vars2 \<union> vars3) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d.pmat_extension m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
have "a.d2 = c.d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a.d2 = c.d1
[PROOF STEP]
by (simp add: c.d1_def a.d2_def c.dims1_def a.dims2_def)
[PROOF STATE]
proof (state)
this:
a.d2 = c.d1

goal (1 subgoal):
 1. d.pmat_extension m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
have "c.d0 = d.d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.d0 = d.d2
[PROOF STEP]
by (simp add: c.d0_def d.d2_def c.dims0_def d.dims2_def c.vars0_def)
[PROOF STATE]
proof (state)
this:
c.d0 = d.d2

goal (1 subgoal):
 1. d.pmat_extension m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d.pmat_extension m = b.pmat_extension (a.pmat_extension m)
[PROOF STEP]
unfolding a.pmat_extension_def b.pmat_extension_def d.pmat_extension_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d.ptensor_mat m (1\<^sub>m d.d2) = b.ptensor_mat (a.ptensor_mat m (1\<^sub>m a.d2)) (1\<^sub>m c.d2)
[PROOF STEP]
apply (simp add: ptensor_mat_assoc[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d.ptensor_mat m (1\<^sub>m d.d2) = d.ptensor_mat m (c.ptensor_mat (1\<^sub>m a.d2) (1\<^sub>m c.d2))
[PROOF STEP]
apply (simp add: \<open>a.d2 = c.d1\<close> c.ptensor_mat_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d.ptensor_mat m (1\<^sub>m d.d2) = d.ptensor_mat m (1\<^sub>m c.d0)
[PROOF STEP]
by (simp add: \<open>c.d0 = d.d2\<close>)
[PROOF STATE]
proof (state)
this:
d.pmat_extension m = b.pmat_extension (a.pmat_extension m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma well_com_Utrans_P:
  assumes "U \<in> carrier_mat (prod_list (nths dims vars)) (prod_list (nths dims vars))"
    and "unitary U"
  shows "well_com (Utrans_P vars U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
have 1: "mat_extension dims vars U \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_extension dims vars U \<in> carrier_mat d d
[PROOF STEP]
by (rule partial_state.mat_extension_carrier)
[PROOF STATE]
proof (state)
this:
mat_extension dims vars U \<in> carrier_mat d d

goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
have 2: "unitary (mat_extension dims vars U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (mat_extension dims vars U)
[PROOF STEP]
apply (rule partial_state.mat_extension_unitary)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. U \<in> carrier_mat (partial_state.d1 dims vars) (partial_state.d1 dims vars)
 2. unitary U
[PROOF STEP]
unfolding partial_state.d1_def partial_state.dims1_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. U \<in> carrier_mat (prod_list (nths dims vars)) (prod_list (nths dims vars))
 2. unitary U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat (prod_list (nths dims vars)) (prod_list (nths dims vars))
unitary U

goal (2 subgoals):
 1. U \<in> carrier_mat (prod_list (nths dims vars)) (prod_list (nths dims vars))
 2. unitary U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unitary (mat_extension dims vars U)

goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
show "well_com (Utrans_P vars U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
using 1 2 Utrans_P_def
[PROOF STATE]
proof (prove)
using this:
mat_extension dims vars U \<in> carrier_mat d d
unitary (mat_extension dims vars U)
Utrans_P ?vars ?U = Utrans (mat_extension dims ?vars ?U)

goal (1 subgoal):
 1. well_com (Utrans_P vars U)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com (Utrans_P vars U)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" \<comment>\<open>Proof also found by sledgehammer\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T1: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E X))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>
[PROOF STEP]
by (metis A2 U1)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T2: "\<lfloor>\<P> \<G>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<G>\<^bold>\<in>\<P>\<rfloor>
[PROOF STEP]
by (metis A3 G_def)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<G>\<^bold>\<in>\<P>\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using T1 T2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>
\<lfloor>\<G>\<^bold>\<in>\<P>\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T5: "\<lfloor>(\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by (metis A2 G_def T2 U1)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using T3
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops  \<comment>\<open>Model found\<close>


[STATEMENT]
lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>