[STATEMENT]
lemma cat_Rel_is_iso_arrI[intro]:
  assumes "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
    and "v11 (T\<lparr>ArrVal\<rparr>)"
    and "\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A"
    and "\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B"
  shows "T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
proof(rule is_iso_arrI[where ?g = \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<close>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
interpret T: arr_Rel \<alpha> T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> T
[PROOF STEP]
by (intro cat_Rel_is_arrD[OF assms(1)])+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
interpret Rel: category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule T.category_cat_Rel)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
interpret v11: v11 \<open>T\<lparr>ArrVal\<rparr>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
interpret is_iso_functor \<alpha> \<open>op_cat (cat_Rel \<alpha>)\<close> \<open>cat_Rel \<alpha>\<close> \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (simp add: T.cf_dag_Rel_is_iso_functor)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
show "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
show "is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T
[PROOF STEP]
proof(intro is_inverseI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : ?b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> ?a
 2. T : ?a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> ?b
 3. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
show dag_T: "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_op_simps cat_Rel_cs_simps
            cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A

goal (3 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
 3. T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
show T: "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (2 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
 2. T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
from T T.arr_Rel_axioms v11.v11_axioms assms(3)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)
\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
[PROOF STEP]
show
      "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)
\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_Rel_cs_simps
            cs_intro: cat_cs_intros cat_Rel_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
from T T.arr_Rel_axioms v11.v11_axioms assms(4)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)
\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
show
      "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)
\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B

goal (1 subgoal):
 1. T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_Rel_cs_simps
            cs_intro: cat_cs_intros cat_Rel_cs_intros
        )
[PROOF STATE]
proof (state)
this:
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_inverse (cat_Rel \<alpha>) (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_Rel_is_iso_arrD[dest]:
  assumes "T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B"
  shows "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
    and "v11 (T\<lparr>ArrVal\<rparr>)"
    and "\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A"
    and "\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B &&& v11 (T\<lparr>ArrVal\<rparr>)) &&& \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A &&& \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
 2. v11 (T\<lparr>ArrVal\<rparr>)
 3. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 4. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
show T: "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
by (simp add: is_iso_arr_def)
[PROOF STATE]
proof (state)
this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
interpret T: arr_Rel \<alpha> T
    rewrites [simp]: "T\<lparr>ArrDom\<rparr> = A" and [simp]: "T\<lparr>ArrCod\<rparr> = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> T &&& T\<lparr>ArrDom\<rparr> = A &&& T\<lparr>ArrCod\<rparr> = B
[PROOF STEP]
by (intro cat_Rel_is_arrD[OF T])+
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
interpret is_iso_functor \<alpha> \<open>op_cat (cat_Rel \<alpha>)\<close> \<open>cat_Rel \<alpha>\<close> \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (simp add: T.cf_dag_Rel_is_iso_functor)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from is_iso_arrD[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
\<exists>g. is_inverse (cat_Rel \<alpha>) g T
[PROOF STEP]
obtain S where
    "is_inverse (cat_Rel \<alpha>) S T"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
\<exists>g. is_inverse (cat_Rel \<alpha>) g T

goal (1 subgoal):
 1. (\<And>S. is_inverse (cat_Rel \<alpha>) S T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
is_inverse (cat_Rel \<alpha>) S T

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from is_inverseD[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. S : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a \<and> T : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<and> S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> \<and> T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
obtain A' B' where "S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'"
    and "T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'"
    and "S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>"
    and "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. S : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a \<and> T : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<and> S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> \<and> T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. (\<And>B' A'. \<lbrakk>S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'; T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'; S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>; T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
with T
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>
[PROOF STEP]
have "A' = A" "B' = B"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>

goal (1 subgoal):
 1. A' = A &&& B' = B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' = A
B' = B

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>
A' = A
B' = B
[PROOF STEP]
have S: "S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
    and ST: "S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>"
    and TS: "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S : B' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A'
T : A' \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B'
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A'\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B'\<rparr>
A' = A
B' = B

goal (1 subgoal):
 1. S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A &&& S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr> &&& T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from S T ST TS
[PROOF STATE]
proof (chain)
picking this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
have S_def: "S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>
[PROOF STEP]
by (rule is_iso_arr_dag)
[PROOF STATE]
proof (state)
this:
S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
interpret S: arr_Rel \<alpha> \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<close>
    rewrites "(\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)\<lparr>ArrDom\<rparr> = B"
      and "(\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)\<lparr>ArrCod\<rparr> = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>) &&& \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr> = B &&& \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr> = A
[PROOF STEP]
by (fold S_def, insert S, all\<open>elim cat_Rel_is_arrE\<close>)
      (simp_all add: cat_Rel_components)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from T.arr_Rel_axioms S_def
[PROOF STATE]
proof (chain)
picking this:
arr_Rel \<alpha> T
S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>
[PROOF STEP]
have S_T: "S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> T
S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
by (simp add: cf_dag_Rel_ArrMap_app converse_Rel_components(1))
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from S
[PROOF STATE]
proof (chain)
picking this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
have A: "A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>" and B: "B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> &&& B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
from B TS A ST
[PROOF STATE]
proof (chain)
picking this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
have
    "(T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr>"
    "(S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. (T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr> &&& (S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>
[PROOF STEP]
unfolding cat_Rel_Comp_app[OF S T] cat_Rel_Comp_app[OF T S]
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
T \<circ>\<^sub>R\<^sub>e\<^sub>l S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
S \<circ>\<^sub>R\<^sub>e\<^sub>l T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. (T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr> &&& (S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>
[PROOF STEP]
unfolding cat_Rel_components
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> Vset \<alpha>
T \<circ>\<^sub>R\<^sub>e\<^sub>l S = VLambda (Vset \<alpha>) id_Rel\<lparr>B\<rparr>
A \<in>\<^sub>\<circ> Vset \<alpha>
S \<circ>\<^sub>R\<^sub>e\<^sub>l T = VLambda (Vset \<alpha>) id_Rel\<lparr>A\<rparr>

goal (1 subgoal):
 1. (T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr> &&& (S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr>
(S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr>
(S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>
[PROOF STEP]
have val_ST: "S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A"
    and val_TS: "T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B"
[PROOF STATE]
proof (prove)
using this:
(T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = id_Rel B\<lparr>ArrVal\<rparr>
(S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = id_Rel A\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A &&& T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
[PROOF STEP]
unfolding comp_Rel_components id_Rel_components
[PROOF STATE]
proof (prove)
using this:
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A &&& T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B

goal (3 subgoals):
 1. v11 (T\<lparr>ArrVal\<rparr>)
 2. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 3. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
show "v11 (T\<lparr>ArrVal\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
proof(rule v11I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (T\<lparr>ArrVal\<rparr>)
 2. vsv ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
show "vsv (T\<lparr>ArrVal\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
proof(rule vsvI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
assume prems: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>" "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
from prems(1) S_T
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
have "\<langle>b, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
with prems(2) val_TS
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
have "\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on B"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on B

goal (2 subgoals):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on B
[PROOF STEP]
show "b = c"
[PROOF STATE]
proof (prove)
using this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on B

goal (1 subgoal):
 1. b = c
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
b = c

goal (1 subgoal):
 1. vbrelation (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
qed (auto simp: T.ArrVal.vbrelation_axioms)
[PROOF STATE]
proof (state)
this:
vsv (T\<lparr>ArrVal\<rparr>)

goal (1 subgoal):
 1. vsv ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
show "vsv ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
proof(rule vsvI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
assume prems: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>" "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>"
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
with S_T
[PROOF STATE]
proof (chain)
picking this:
S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
have "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>" and "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> &&& \<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
have "\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>" and "\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> &&& \<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
have "\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A
[PROOF STEP]
using val_ST
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A

goal (1 subgoal):
 1. \<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A

goal (2 subgoals):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A
[PROOF STEP]
show "b = c"
[PROOF STATE]
proof (prove)
using this:
\<langle>b, c\<rangle> \<in>\<^sub>\<circ> vid_on A

goal (1 subgoal):
 1. b = c
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
b = c

goal (1 subgoal):
 1. vbrelation ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
vsv ((T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v11 (T\<lparr>ArrVal\<rparr>)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
 2. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
show "\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> A
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> A
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> A
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
with val_ST
[PROOF STATE]
proof (chain)
picking this:
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A
a \<in>\<^sub>\<circ> A
[PROOF STEP]
have "\<langle>a, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A
a \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. \<langle>a, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> A
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> A
[PROOF STEP]
qed (use T.arr_Rel_ArrVal_vdomain in auto)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
show "\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> B
 2. \<And>x. x \<in>\<^sub>\<circ> B \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> B
 2. \<And>x. x \<in>\<^sub>\<circ> B \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> B

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> B
 2. \<And>x. x \<in>\<^sub>\<circ> B \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
with val_TS
[PROOF STATE]
proof (chain)
picking this:
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
b \<in>\<^sub>\<circ> B
[PROOF STEP]
have "\<langle>b, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
b \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<langle>b, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>b, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> B
 2. \<And>x. x \<in>\<^sub>\<circ> B \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>b, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
show "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>b, b\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> B
[PROOF STEP]
qed (use T.arr_Rel_ArrVal_vrange in auto)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_Rel_is_iso_arr:
  "T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B \<longleftrightarrow>
    T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B \<and>
    v11 (T\<lparr>ArrVal\<rparr>) \<and>
    \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A \<and>
    \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B = (T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B \<and> v11 (T\<lparr>ArrVal\<rparr>) \<and> \<D>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = A \<and> \<R>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>) = B)
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_Rel_the_inverse[cat_Rel_cs_simps]:
  assumes "T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B"
  shows "T\<inverse>\<^sub>C\<^bsub>cat_Rel \<alpha>\<^esub> = T\<inverse>\<^sub>R\<^sub>e\<^sub>l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<inverse>\<^sub>C\<^bsub>cat_Rel \<alpha>\<^esub> = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
unfolding the_inverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE g. is_inverse (cat_Rel \<alpha>) g T) = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
proof(rule the_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T
 2. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
have T: "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (2 subgoals):
 1. is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T
 2. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
interpret T: arr_Rel \<alpha> T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> T
[PROOF STEP]
by (intro cat_Rel_is_arrD[OF T])+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T
 2. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
interpret Rel: category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule T.category_cat_Rel)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T
 2. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
from assms T T.arr_Rel_axioms cat_Rel_is_iso_arrD(2)[OF assms]
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)
[PROOF STEP]
show inv_T_T: "is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_Rel \<alpha>\<^esub> B
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> T
v11 (T\<lparr>ArrVal\<rparr>)

goal (1 subgoal):
 1. is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T
[PROOF STEP]
by (intro is_inverseI[where a=A and b=B])
      (
        cs_concl
          cs_simp: cat_cs_simps cat_Rel_cs_simps
          cs_intro: cat_Rel_cs_intros cat_cs_intros
      )+
[PROOF STATE]
proof (state)
this:
is_inverse (cat_Rel \<alpha>) (T\<inverse>\<^sub>R\<^sub>e\<^sub>l) T

goal (1 subgoal):
 1. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
assume "is_inverse (cat_Rel \<alpha>) S T"
[PROOF STATE]
proof (state)
this:
is_inverse (cat_Rel \<alpha>) S T

goal (1 subgoal):
 1. \<And>g. is_inverse (cat_Rel \<alpha>) g T \<Longrightarrow> g = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_inverse (cat_Rel \<alpha>) S T
[PROOF STEP]
show "S = T\<inverse>\<^sub>R\<^sub>e\<^sub>l"
[PROOF STATE]
proof (prove)
using this:
is_inverse (cat_Rel \<alpha>) S T

goal (1 subgoal):
 1. S = T\<inverse>\<^sub>R\<^sub>e\<^sub>l
[PROOF STEP]
by (rule category.cat_is_inverse_eq[OF Rel.category_axioms _ inv_T_T])
[PROOF STATE]
proof (state)
this:
S = T\<inverse>\<^sub>R\<^sub>e\<^sub>l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_Exec_one: "f_Exec_Comp trans_fun [m] c = trans_fun m c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp trans_fun [m] c = trans_fun m c
[PROOF STEP]
by simp


[STATEMENT]
lemma f_Exec_Stream_length[rule_format, simp]:"
  \<forall>c. length (f_Exec_Comp_Stream trans_fun xs c) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. length (f_Exec_Comp_Stream trans_fun xs c) = length xs
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma f_Exec_Stream_empty_conv:"
  (f_Exec_Comp_Stream trans_fun xs c = []) = (xs = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f_Exec_Comp_Stream trans_fun xs c = []) = (xs = [])
[PROOF STEP]
by (simp add: length_0_conv[symmetric] del: length_0_conv)


[STATEMENT]
lemma f_Exec_Stream_not_empty_conv:"
  (f_Exec_Comp_Stream trans_fun xs c \<noteq> []) = (xs \<noteq> [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f_Exec_Comp_Stream trans_fun xs c \<noteq> []) = (xs \<noteq> [])
[PROOF STEP]
by (simp add: f_Exec_Stream_empty_conv)


[STATEMENT]
lemma f_Exec_eq_f_Exec_Stream_last[rule_format]:"
  \<forall>c. f_Exec_Comp trans_fun xs c = last (c # (f_Exec_Comp_Stream trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. f_Exec_Comp trans_fun xs c = last (c # f_Exec_Comp_Stream trans_fun xs c)
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma f_Exec_Stream_nth: "
  \<And>n c. n < length xs \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c ! n = f_Exec_Comp trans_fun (xs \<down> Suc n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. n < length xs \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = f_Exec_Comp trans_fun (xs \<down> Suc n) c
[PROOF STEP]
apply (induct xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs n c. \<lbrakk>\<And>n c. n < length xs \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = f_Exec_Comp trans_fun (xs \<down> Suc n) c; n < length (a # xs)\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun (a # xs) c ! n = f_Exec_Comp trans_fun ((a # xs) \<down> Suc n) c
[PROOF STEP]
apply (simp add: nth_Cons')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_nth2: "
  n \<le> length xs \<Longrightarrow>
  (c # f_Exec_Comp_Stream trans_fun xs c) ! n = f_Exec_Comp trans_fun (xs \<down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> (c # f_Exec_Comp_Stream trans_fun xs c) ! n = f_Exec_Comp trans_fun (xs \<down> n) c
[PROOF STEP]
by (simp add: nth_Cons' f_Exec_Stream_nth)


[STATEMENT]
lemma f_Exec_N_all:"
  length xs \<le> n \<Longrightarrow>
    f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp trans_fun xs c
[PROOF STEP]
by (simp add: f_Exec_Comp_N_def)


[STATEMENT]
lemma f_Exec_Stream_append[rule_format]:"\<forall>c.
  f_Exec_Comp_Stream trans_fun (xs @ ys) c =
    (f_Exec_Comp_Stream trans_fun xs c) @
    (f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. f_Exec_Comp_Stream trans_fun (xs @ ys) c = f_Exec_Comp_Stream trans_fun xs c @ f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c)
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma f_Exec_Stream_snoc: "
  f_Exec_Comp_Stream trans_fun (xs @ [x]) c =
    f_Exec_Comp_Stream trans_fun xs c @
    [trans_fun x (f_Exec_Comp trans_fun xs c)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream trans_fun (xs @ [x]) c = f_Exec_Comp_Stream trans_fun xs c @ [trans_fun x (f_Exec_Comp trans_fun xs c)]
[PROOF STEP]
by (simp add: f_Exec_Stream_append)


[STATEMENT]
lemma f_Exec_snoc: "
  f_Exec_Comp trans_fun (xs @ [x]) c =
  trans_fun x (f_Exec_Comp trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp trans_fun (xs @ [x]) c = trans_fun x (f_Exec_Comp trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_append)


[STATEMENT]
lemma f_Exec_N_append[rule_format]:"
  f_Exec_Comp_N trans_fun (a + b) xs c =
  f_Exec_Comp_N trans_fun b (xs \<up> a) (f_Exec_Comp_N trans_fun a xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_N trans_fun (a + b) xs c = f_Exec_Comp_N trans_fun b (xs \<up> a) (f_Exec_Comp_N trans_fun a xs c)
[PROOF STEP]
apply (simp add: f_Exec_Comp_N_def f_Exec_append[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp trans_fun (xs \<down> (a + b)) c = f_Exec_Comp trans_fun (xs \<down> a @ xs \<up> a \<down> b) c
[PROOF STEP]
apply (simp add: take_drop add.commute[of b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp trans_fun (xs \<down> (a + b)) c = f_Exec_Comp trans_fun (xs \<down> a @ xs \<down> (a + b) \<up> a) c
[PROOF STEP]
apply (rule subst[of "xs \<down> (a + b) \<down> a" "xs \<down> a" ], simp add: min_eqL)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp trans_fun (xs \<down> (a + b)) c = f_Exec_Comp trans_fun (xs \<down> (a + b) \<down> a @ xs \<down> (a + b) \<up> a) c
[PROOF STEP]
apply (subst append_take_drop_id, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem f_Exec_Stream_take:"
  (f_Exec_Comp_Stream trans_fun xs c) \<down> n =
  f_Exec_Comp_Stream trans_fun (xs \<down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream trans_fun xs c \<down> n = f_Exec_Comp_Stream trans_fun (xs \<down> n) c
[PROOF STEP]
apply (case_tac "length xs \<le> n", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> length xs \<le> n \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c \<down> n = f_Exec_Comp_Stream trans_fun (xs \<down> n) c
[PROOF STEP]
apply (rule subst[OF append_take_drop_id, of _ n xs])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> length xs \<le> n \<Longrightarrow> f_Exec_Comp_Stream trans_fun (xs \<down> n @ xs \<up> n) c \<down> n = f_Exec_Comp_Stream trans_fun ((xs \<down> n @ xs \<up> n) \<down> n) c
[PROOF STEP]
apply (simp add: f_Exec_Stream_append del: append_take_drop_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem f_Exec_Stream_drop:"
  (f_Exec_Comp_Stream trans_fun xs c) \<up> n =
  f_Exec_Comp_Stream trans_fun (xs \<up> n)
    (f_Exec_Comp trans_fun (xs \<down> n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream trans_fun xs c \<up> n = f_Exec_Comp_Stream trans_fun (xs \<up> n) (f_Exec_Comp trans_fun (xs \<down> n) c)
[PROOF STEP]
apply (case_tac "length xs \<le> n", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> length xs \<le> n \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c \<up> n = f_Exec_Comp_Stream trans_fun (xs \<up> n) (f_Exec_Comp trans_fun (xs \<down> n) c)
[PROOF STEP]
apply (rule subst[OF append_take_drop_id, of _ n xs])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> length xs \<le> n \<Longrightarrow> f_Exec_Comp_Stream trans_fun (xs \<down> n @ xs \<up> n) c \<up> n = f_Exec_Comp_Stream trans_fun ((xs \<down> n @ xs \<up> n) \<up> n) (f_Exec_Comp trans_fun ((xs \<down> n @ xs \<up> n) \<down> n) c)
[PROOF STEP]
apply (simp add: f_Exec_Stream_append del: append_take_drop_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_nth: "
  i_Exec_Comp_Stream trans_fun input c n = f_Exec_Comp trans_fun (input \<Down> Suc n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c n = f_Exec_Comp trans_fun (input \<Down> Suc n) c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_def)


[STATEMENT]
lemma i_Exec_Stream_nth_Suc: "
  i_Exec_Comp_Stream trans_fun input c (Suc n) =
  trans_fun (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c (Suc n) = trans_fun (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c n)
[PROOF STEP]
by (simp add: i_Exec_Stream_nth i_take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma i_Exec_Stream_nth_Suc_first: "
  i_Exec_Comp_Stream trans_fun input c (Suc n) =
  (i_Exec_Comp_Stream trans_fun (input \<Up> Suc 0) (trans_fun (input 0) c) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c (Suc n) = i_Exec_Comp_Stream trans_fun (input \<Up> Suc 0) (trans_fun (input 0) c) n
[PROOF STEP]
by (simp add: i_Exec_Stream_nth i_take_Suc)


[STATEMENT]
lemma f_Exec_Stream_nth_eq_i_Exec_Stream_nth: "
  n < n' \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun (input \<Down> n') c ! n =
  i_Exec_Comp_Stream trans_fun input c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < n' \<Longrightarrow> f_Exec_Comp_Stream trans_fun (input \<Down> n') c ! n = i_Exec_Comp_Stream trans_fun input c n
[PROOF STEP]
by (simp add: f_Exec_Stream_nth i_Exec_Stream_nth min_eqR)


[STATEMENT]
lemma i_Exec_Stream_append: "
  i_Exec_Comp_Stream trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream trans_fun xs c \<frown>
  i_Exec_Comp_Stream trans_fun input (f_Exec_Comp trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream trans_fun xs c \<frown> i_Exec_Comp_Stream trans_fun input (f_Exec_Comp trans_fun xs c)
[PROOF STEP]
by (simp add: ilist_eq_iff i_Exec_Stream_nth f_Exec_Stream_nth f_Exec_append i_append_nth Suc_diff_le)


[STATEMENT]
lemma i_Exec_Stream_append_last_Cons: "
  i_Exec_Comp_Stream trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream trans_fun xs c \<frown>
  i_Exec_Comp_Stream trans_fun input (
    last (c # f_Exec_Comp_Stream trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream trans_fun xs c \<frown> i_Exec_Comp_Stream trans_fun input (last (c # f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
by (simp add: f_Exec_eq_f_Exec_Stream_last i_Exec_Stream_append)


[STATEMENT]
lemma i_Exec_Stream_append_last: "
  xs \<noteq> [] \<Longrightarrow>
  i_Exec_Comp_Stream trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream trans_fun xs c \<frown>
  i_Exec_Comp_Stream trans_fun input (
    last (f_Exec_Comp_Stream trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> i_Exec_Comp_Stream trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream trans_fun xs c \<frown> i_Exec_Comp_Stream trans_fun input (last (f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
by (simp add: f_Exec_Stream_empty_conv i_Exec_Stream_append_last_Cons)


[STATEMENT]
lemma i_Exec_Stream_append_if: "
  i_Exec_Comp_Stream trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream trans_fun xs c \<frown>
  i_Exec_Comp_Stream trans_fun input (
    if xs = [] then c
    else last (f_Exec_Comp_Stream trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream trans_fun xs c \<frown> i_Exec_Comp_Stream trans_fun input (if xs = [] then c else last (f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
by (simp add: i_Exec_Stream_append_last)


[STATEMENT]
theorem i_Exec_Stream_take:"
  (i_Exec_Comp_Stream trans_fun input c) \<Down> n =
  f_Exec_Comp_Stream trans_fun (input \<Down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c \<Down> n = f_Exec_Comp_Stream trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: list_eq_iff f_Exec_Stream_nth i_Exec_Stream_nth min_eqR)


[STATEMENT]
theorem i_Exec_Stream_drop:"
  (i_Exec_Comp_Stream trans_fun input c) \<Up> n =
  i_Exec_Comp_Stream trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c \<Up> n = i_Exec_Comp_Stream trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n) c)
[PROOF STEP]
apply (rule subst[OF i_append_i_take_i_drop_id, of _ n input])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun (input \<Down> n \<frown> input \<Up> n) c \<Up> n = i_Exec_Comp_Stream trans_fun ((input \<Down> n \<frown> input \<Up> n) \<Up> n) (f_Exec_Comp trans_fun ((input \<Down> n \<frown> input \<Up> n) \<Down> n) c)
[PROOF STEP]
apply (simp add: i_Exec_Stream_append  i_drop_def del: i_append_i_take_i_drop_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_expand_aggregate_map_take: "
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag \<down> n =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs \<down> n) \<odot>\<^sub>f k) c)) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag \<down> n = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<down> n \<odot> k) c)) k ag
[PROOF STEP]
by (simp add: f_aggregate_take_mult[symmetric] take_map f_Exec_Stream_take f_expand_take_mult)


[STATEMENT]
lemma i_Exec_Stream_expand_aggregate_map_take: "
  0 < k \<Longrightarrow>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) c)) k ag \<Down> n =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((input \<Down> n) \<odot>\<^sub>f k) c)) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) c) k ag \<Down> n = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (input \<Down> n \<odot> k) c)) k ag
[PROOF STEP]
by (simp add: i_aggregate_i_take_mult[symmetric] i_Exec_Stream_take i_expand_i_take_mult)


[STATEMENT]
lemma f_Exec_Stream_expand_aggregate_map_drop: "
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag \<up> n =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs \<up> n) \<odot>\<^sub>f k) (
    f_Exec_Comp trans_fun ((xs \<down> n) \<odot>\<^sub>f k) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag \<up> n = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<up> n \<odot> k) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c))) k ag
[PROOF STEP]
by (simp add: f_aggregate_drop_mult[symmetric] drop_map f_Exec_Stream_drop f_expand_take_mult f_expand_drop_mult)


[STATEMENT]
lemma i_Exec_Stream_expand_aggregate_map_drop: "
  0 < k \<Longrightarrow>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) c)) k ag \<Up> n =
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun ((input \<Up> n) \<odot>\<^sub>i k) (
    f_Exec_Comp trans_fun ((input \<Down> n) \<odot>\<^sub>f k) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) c) k ag \<Up> n = i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<Up> n \<odot> k) (f_Exec_Comp trans_fun (input \<Down> n \<odot> k) c)) k ag
[PROOF STEP]
by (simp add: i_aggregate_i_drop_mult[symmetric] i_Exec_Stream_drop i_expand_i_take_mult i_expand_i_drop_mult)


[STATEMENT]
lemma f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth: "
  \<lbrakk> 0 < k; n < n' \<rbrakk> \<Longrightarrow>
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (input \<Down> n' \<odot>\<^sub>f k) c)) k ag ! n =
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) c)) k ag n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < n'\<rbrakk> \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun (input \<Down> n' \<odot> k) c)) k ag ! n = i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) c) k ag n
[PROOF STEP]
apply (simp add: f_aggregate_nth i_aggregate_nth f_Exec_Stream_take f_Exec_Stream_drop i_Exec_Stream_take i_Exec_Stream_drop drop_map take_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < n'\<rbrakk> \<Longrightarrow> ag (map f (f_Exec_Comp_Stream trans_fun (input \<Down> n' \<odot> k \<up> (n * k) \<down> k) (f_Exec_Comp trans_fun (input \<Down> n' \<odot> k \<down> (n * k)) c))) = ag (map f (f_Exec_Comp_Stream trans_fun (input \<odot> k \<Up> (n * k) \<Down> k) (f_Exec_Comp trans_fun (input \<odot> k \<Down> (n * k)) c)))
[PROOF STEP]
apply (simp add: f_expand_take_mod i_expand_i_take_mod f_expand_drop_mod i_expand_i_drop_mod i_drop_i_take_1 drop_take_1 min_eqR)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_expand_shrink_last_map_nth_eq_f_Exec_Comp: "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c) \<div>\<^bsub>fl\<^esub> k ! n =
  f (f_Exec_Comp trans_fun ((xs \<down> Suc n) \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c) \<div>\<^sub>l k ! n = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (simp add: f_shrink_last_map f_shrink_last_length f_shrink_last_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (n * k + k - Suc 0)) = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (subgoal_tac "n * k + k - Suc 0 < length xs * k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; n < length xs; n * k + k - Suc 0 < length xs * k\<rbrakk> \<Longrightarrow> f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (n * k + k - Suc 0)) = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
 2. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> n * k + k - Suc 0 < length xs * k
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> n * k + k - Suc 0 < length xs * k
 2. \<lbrakk>0 < k; n < length xs; n * k + k - Suc 0 < length xs * k\<rbrakk> \<Longrightarrow> f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (n * k + k - Suc 0)) = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (drule Suc_leI[of n])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> n * k + k - Suc 0 < length xs * k
 2. \<lbrakk>0 < k; n < length xs; n * k + k - Suc 0 < length xs * k\<rbrakk> \<Longrightarrow> f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (n * k + k - Suc 0)) = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (drule mult_le_mono1[of _ _ k], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs; n * k + k - Suc 0 < length xs * k\<rbrakk> \<Longrightarrow> f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (n * k + k - Suc 0)) = f (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (simp add: f_Exec_Stream_nth add.commute[of k] f_expand_take_mult[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_expand_aggregate_map_nth: "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag ! n =
  ag (map f (f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>\<^bsup>k - Suc 0\<^esup>)
    (f_Exec_Comp trans_fun (xs \<down> n \<odot>\<^sub>f k) c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag ! n = ag (map f (f_Exec_Comp_Stream trans_fun (xs ! n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c)))
[PROOF STEP]
apply (simp add: f_aggregate_nth take_map drop_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> ag (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c \<up> (n * k) \<down> k)) = ag (f (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c)) # map f (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c))))
[PROOF STEP]
apply (simp add: take_map drop_map f_Exec_Stream_drop f_Exec_Stream_take f_expand_take_mod f_expand_drop_mod drop_take_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_expand_snoc: "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c \<up> (n * k) \<down> k =
  f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>\<^bsup>k - Suc 0\<^esup>)
    (f_Exec_Comp trans_fun (xs \<down> n \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun (xs \<odot> k) c \<up> (n * k) \<down> k = f_Exec_Comp_Stream trans_fun (xs ! n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c)
[PROOF STEP]
by (simp add: f_Exec_Stream_drop f_Exec_Stream_take f_expand_take_mod f_expand_drop_mod drop_take_1)


[STATEMENT]
lemma f_Exec_Stream_expand_map_aggregate_append: "
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ ys) \<odot>\<^sub>f k) c)) k ag =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag @
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (ys \<odot>\<^sub>f k) (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ ys) \<odot> k) c)) k ag = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag @ f_aggregate (map f (f_Exec_Comp_Stream trans_fun (ys \<odot> k) (f_Exec_Comp trans_fun (xs \<odot> k) c))) k ag
[PROOF STEP]
by (simp add: f_Exec_Stream_append f_aggregate_append_mod)


[STATEMENT]
lemma i_Exec_Stream_expand_map_aggregate_append: "
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun ((xs \<frown> input) \<odot>\<^sub>i k) c)) k ag =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag \<frown>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun ((xs \<frown> input) \<odot> k) c) k ag = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag \<frown> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) (f_Exec_Comp trans_fun (xs \<odot> k) c)) k ag
[PROOF STEP]
by (simp add: i_expand_i_append i_Exec_Stream_append i_aggregate_i_append_mod)


[STATEMENT]
lemma f_Exec_Stream_expand_map_aggregate_Cons: "
  0 < k \<Longrightarrow>
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((x # xs) \<odot>\<^sub>f k) c)) k ag =
  ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c)) #
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) (
    f_Exec_Comp trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((x # xs) \<odot> k) c)) k ag = ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) # f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))) k ag
[PROOF STEP]
apply (subst append_eq_Cons[of x xs, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun (([x] @ xs) \<odot> k) c)) k ag = ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) # f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))) k ag
[PROOF STEP]
apply (subst f_Exec_Stream_expand_map_aggregate_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun ([x] \<odot> k) c)) k ag @ f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun ([x] \<odot> k) c))) k ag = ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) # f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))) k ag
[PROOF STEP]
apply (simp add: f_aggregate_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_expand_map_aggregate_snoc: "
  0 < k \<Longrightarrow>
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ [x]) \<odot>\<^sub>f k) c)) k ag =
  f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) k ag @
  [ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c)))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ [x]) \<odot> k) c)) k ag = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag @ [ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<odot> k) c)))]
[PROOF STEP]
apply (subst f_Exec_Stream_expand_map_aggregate_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag @ f_aggregate (map f (f_Exec_Comp_Stream trans_fun ([x] \<odot> k) (f_Exec_Comp trans_fun (xs \<odot> k) c))) k ag = f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c)) k ag @ [ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<odot> k) c)))]
[PROOF STEP]
apply (simp add: f_aggregate_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_expand_map_aggregate_Cons: "
  0 < k \<Longrightarrow>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (([x] \<frown> input) \<odot>\<^sub>i k) c)) k ag =
  [ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c))] \<frown>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) (
    f_Exec_Comp trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c))) k ag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (([x] \<frown> input) \<odot> k) c) k ag = [ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))] \<frown> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) k ag
[PROOF STEP]
apply (subst i_Exec_Stream_expand_map_aggregate_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_aggregate (map f (f_Exec_Comp_Stream trans_fun ([x] \<odot> k) c)) k ag \<frown> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) (f_Exec_Comp trans_fun ([x] \<odot> k) c)) k ag = [ag (map f (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))] \<frown> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) k ag
[PROOF STEP]
apply (simp add: f_aggregate_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_N_eq_f_Exec_Stream_nth:"
  n \<le> length xs \<Longrightarrow>
  f_Exec_Comp_N trans_fun n xs c = (c # f_Exec_Comp_Stream trans_fun xs c) ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> f_Exec_Comp_N trans_fun n xs c = (c # f_Exec_Comp_Stream trans_fun xs c) ! n
[PROOF STEP]
by (simp add: f_Exec_Comp_N_def f_Exec_Stream_nth2)


[STATEMENT]
theorem f_Exec_Stream_causal: "
  xs \<down> n = ys \<down> n \<Longrightarrow>
  (f_Exec_Comp_Stream trans_fun xs c) \<down> n = (f_Exec_Comp_Stream trans_fun ys c) \<down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<down> n = ys \<down> n \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c \<down> n = f_Exec_Comp_Stream trans_fun ys c \<down> n
[PROOF STEP]
by (simp add: f_Exec_Stream_take)


[STATEMENT]
theorem i_Exec_Stream_causal: "
  input1 \<Down> n = input2 \<Down> n \<Longrightarrow>
  (i_Exec_Comp_Stream trans_fun input1 c) \<Down> n = (i_Exec_Comp_Stream trans_fun input2 c) \<Down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. input1 \<Down> n = input2 \<Down> n \<Longrightarrow> i_Exec_Comp_Stream trans_fun input1 c \<Down> n = i_Exec_Comp_Stream trans_fun input2 c \<Down> n
[PROOF STEP]
by (simp add: i_Exec_Stream_take)


[STATEMENT]
lemma f_Exec_Stream_Init_length[rule_format, simp]:"
  \<forall>c. length (f_Exec_Comp_Stream_Init trans_fun xs c) = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. length (f_Exec_Comp_Stream_Init trans_fun xs c) = Suc (length xs)
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma f_Exec_Stream_Init_not_empty:"
  (f_Exec_Comp_Stream_Init trans_fun xs c \<noteq> [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun xs c \<noteq> []
[PROOF STEP]
by (simp add: length_0_conv[symmetric] del: length_0_conv)


[STATEMENT]
lemma f_Exec_eq_f_Exec_Stream_Init_last[rule_format]:"
  \<forall>c. f_Exec_Comp trans_fun xs c = last (f_Exec_Comp_Stream_Init trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. f_Exec_Comp trans_fun xs c = last (f_Exec_Comp_Stream_Init trans_fun xs c)
[PROOF STEP]
by (induct xs, simp_all add: f_Exec_Stream_Init_not_empty)


[STATEMENT]
lemma f_Exec_Stream_Init_eq_f_Exec_Stream_Cons[rule_format]: "
  \<forall>c. f_Exec_Comp_Stream_Init trans_fun xs c = c # f_Exec_Comp_Stream trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. f_Exec_Comp_Stream_Init trans_fun xs c = c # f_Exec_Comp_Stream trans_fun xs c
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma f_Exec_N_eq_last_f_Exec_Stream_Init_take:"
  f_Exec_Comp_N trans_fun n xs c =
  last (f_Exec_Comp_Stream_Init trans_fun (xs \<down> n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_N trans_fun n xs c = last (f_Exec_Comp_Stream_Init trans_fun (xs \<down> n) c)
[PROOF STEP]
by (simp add: f_Exec_Comp_N_def f_Exec_eq_f_Exec_Stream_Init_last)


[STATEMENT]
lemma f_Exec_Stream_Init_nth: "
  n \<le> length xs \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c ! n = f_Exec_Comp trans_fun (xs \<down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c ! n = f_Exec_Comp trans_fun (xs \<down> n) c
[PROOF STEP]
apply (subst f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> (c # f_Exec_Comp_Stream trans_fun xs c) ! n = f_Exec_Comp trans_fun (xs \<down> n) c
[PROOF STEP]
apply (case_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n \<le> length xs; n = Suc nat\<rbrakk> \<Longrightarrow> (c # f_Exec_Comp_Stream trans_fun xs c) ! n = f_Exec_Comp trans_fun (xs \<down> n) c
[PROOF STEP]
apply (simp add: f_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Init_nth_0: "f_Exec_Comp_Stream_Init trans_fun xs c ! 0 = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun xs c ! 0 = c
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_nth)


[STATEMENT]
lemma f_Exec_Stream_Init_hd: "hd (f_Exec_Comp_Stream_Init trans_fun xs c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (f_Exec_Comp_Stream_Init trans_fun xs c) = c
[PROOF STEP]
by (simp add: hd_conv_nth f_Exec_Stream_Init_not_empty f_Exec_Stream_Init_nth_0)


[STATEMENT]
lemma f_Exec_Stream_Init_nth_Suc_eq_f_Exec_Stream_nth: "
  f_Exec_Comp_Stream_Init trans_fun xs c ! (Suc n) = f_Exec_Comp_Stream trans_fun xs c ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n = f_Exec_Comp_Stream trans_fun xs c ! n
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)


[STATEMENT]
lemma f_Exec_Stream_Init_append:"
  f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c =
    (f_Exec_Comp_Stream_Init trans_fun xs c) @
    tl (f_Exec_Comp_Stream_Init trans_fun ys (f_Exec_Comp trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c = f_Exec_Comp_Stream_Init trans_fun xs c @ tl (f_Exec_Comp_Stream_Init trans_fun ys (f_Exec_Comp trans_fun xs c))
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_append)


[STATEMENT]
lemma f_Exec_Stream_Init_f_Exec_Stream_append:"
  f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c =
    (f_Exec_Comp_Stream_Init trans_fun xs c) @
    (f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c = f_Exec_Comp_Stream_Init trans_fun xs c @ f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_append)


[STATEMENT]
lemma f_Exec_Stream_Init_take:"
  (f_Exec_Comp_Stream_Init trans_fun xs c) \<down> Suc n =
  f_Exec_Comp_Stream_Init trans_fun (xs \<down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun xs c \<down> Suc n = f_Exec_Comp_Stream_Init trans_fun (xs \<down> n) c
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_take)


[STATEMENT]
lemma f_Exec_Stream_Init_drop:"
  n \<le> length xs \<Longrightarrow>
  (f_Exec_Comp_Stream_Init trans_fun xs c) \<up> n =
  f_Exec_Comp_Stream_Init trans_fun (xs \<up> n)
    (f_Exec_Comp trans_fun (xs \<down> n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<up> n = f_Exec_Comp_Stream_Init trans_fun (xs \<up> n) (f_Exec_Comp trans_fun (xs \<down> n) c)
[PROOF STEP]
apply (case_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n \<le> length xs; n = Suc nat\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<up> n = f_Exec_Comp_Stream_Init trans_fun (xs \<up> n) (f_Exec_Comp trans_fun (xs \<down> n) c)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> length xs; n = Suc nat\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun (xs \<up> nat) (f_Exec_Comp trans_fun (xs \<down> nat) c) = f_Exec_Comp trans_fun (xs \<down> Suc nat) c # f_Exec_Comp_Stream trans_fun (xs \<up> Suc nat) (f_Exec_Comp trans_fun (xs \<down> Suc nat) c)
[PROOF STEP]
apply (simp add: take_Suc_conv_app_nth f_Exec_append Cons_nth_drop_Suc[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Init_drop_geq_not_valid:"
  length xs \<le> n \<Longrightarrow>
  (f_Exec_Comp_Stream_Init trans_fun xs c) \<up> Suc n \<noteq>
  f_Exec_Comp_Stream_Init trans_fun arbitrary_input arbitrary_comp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<up> Suc n \<noteq> f_Exec_Comp_Stream_Init trans_fun arbitrary_input arbitrary_comp
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_not_empty[symmetric])


[STATEMENT]
lemma i_Exec_Stream_Init_nth: "
  i_Exec_Comp_Stream_Init trans_fun input c n = f_Exec_Comp trans_fun (input \<Down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c n = f_Exec_Comp trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Init_def)


[STATEMENT]
lemma i_Exec_Stream_Init_nth_0: "
  i_Exec_Comp_Stream_Init trans_fun input c 0 = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c 0 = c
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth)


[STATEMENT]
lemma i_Exec_Stream_Init_nth_Suc_eq_i_Exec_Stream_nth: "
  i_Exec_Comp_Stream_Init trans_fun input c (Suc n) = i_Exec_Comp_Stream trans_fun input c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c (Suc n) = i_Exec_Comp_Stream trans_fun input c n
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth i_Exec_Stream_nth)


[STATEMENT]
lemma i_Exec_Stream_Init_eq_i_Exec_Stream_Cons: "
  i_Exec_Comp_Stream_Init trans_fun input c = [c] \<frown> i_Exec_Comp_Stream trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c = [c] \<frown> i_Exec_Comp_Stream trans_fun input c
[PROOF STEP]
by (simp add: ilist_eq_iff i_Exec_Stream_Init_nth i_append_nth i_Exec_Stream_nth)


[STATEMENT]
lemma i_Exec_Stream_Init_append:"
  i_Exec_Comp_Stream_Init trans_fun (input1 \<frown> input2) c =
    (f_Exec_Comp_Stream_Init trans_fun input1 c) \<frown>
    ((i_Exec_Comp_Stream_Init trans_fun input2 (f_Exec_Comp trans_fun input1 c)) \<Up> Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun (input1 \<frown> input2) c = f_Exec_Comp_Stream_Init trans_fun input1 c \<frown> i_Exec_Comp_Stream_Init trans_fun input2 (f_Exec_Comp trans_fun input1 c) \<Up> Suc 0
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_append)


[STATEMENT]
lemma i_Exec_Stream_Init_i_Exec_Stream_append:"
  i_Exec_Comp_Stream_Init trans_fun (input1 \<frown> input2) c =
    (f_Exec_Comp_Stream_Init trans_fun input1 c) \<frown>
    (i_Exec_Comp_Stream trans_fun input2 (f_Exec_Comp trans_fun input1 c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun (input1 \<frown> input2) c = f_Exec_Comp_Stream_Init trans_fun input1 c \<frown> i_Exec_Comp_Stream trans_fun input2 (f_Exec_Comp trans_fun input1 c)
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_append)


[STATEMENT]
lemma i_Exec_Stream_Init_take:"
  (i_Exec_Comp_Stream_Init trans_fun input c) \<Down> Suc n =
  f_Exec_Comp_Stream_Init trans_fun (input \<Down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c \<Down> Suc n = f_Exec_Comp_Stream_Init trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_take)


[STATEMENT]
lemma i_Exec_Stream_Init_drop:"
  (i_Exec_Comp_Stream_Init trans_fun input c) \<Up> n =
  i_Exec_Comp_Stream_Init trans_fun (input \<Up> n)
    (f_Exec_Comp trans_fun (input \<Down> n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c \<Up> n = i_Exec_Comp_Stream_Init trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n) c)
[PROOF STEP]
apply (case_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> i_Exec_Comp_Stream_Init trans_fun input c \<Up> n = i_Exec_Comp_Stream_Init trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n) c)
[PROOF STEP]
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> i_Exec_Comp_Stream trans_fun (input \<Up> nat) (f_Exec_Comp trans_fun (input \<Down> nat) c) = [f_Exec_Comp trans_fun (input \<Down> Suc nat) c] \<frown> i_Exec_Comp_Stream trans_fun (input \<Up> Suc nat) (f_Exec_Comp trans_fun (input \<Down> Suc nat) c)
[PROOF STEP]
apply (simp add: ilist_eq_iff i_take_Suc_conv_app_nth f_Exec_append i_Exec_Stream_nth i_append_nth i_take_first i_take_drop_eq_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<forall>x>0. trans_fun (input (nat + x)) (f_Exec_Comp trans_fun (map input [nat..<nat + x]) (f_Exec_Comp trans_fun (input \<Down> nat) c)) = trans_fun (input (nat + x)) (f_Exec_Comp trans_fun (map input [Suc nat..<nat + x]) (trans_fun (input nat) (f_Exec_Comp trans_fun (input \<Down> nat) c)))
[PROOF STEP]
apply (simp add: upt_conv_Cons)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem f_Exec_Stream_Init_strictly_causal: "
  xs \<down> n = ys \<down> n \<Longrightarrow>
  (f_Exec_Comp_Stream_Init trans_fun xs c) \<down> Suc n = (f_Exec_Comp_Stream_Init trans_fun ys c) \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<down> n = ys \<down> n \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<down> Suc n = f_Exec_Comp_Stream_Init trans_fun ys c \<down> Suc n
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_take)


[STATEMENT]
theorem i_Exec_Stream_Init_strictly_causal: "
  input1 \<Down> n = input2 \<Down> n \<Longrightarrow>
  (i_Exec_Comp_Stream_Init trans_fun input1 c) \<Down> Suc n = (i_Exec_Comp_Stream_Init trans_fun input2 c) \<Down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. input1 \<Down> n = input2 \<Down> n \<Longrightarrow> i_Exec_Comp_Stream_Init trans_fun input1 c \<Down> Suc n = i_Exec_Comp_Stream_Init trans_fun input2 c \<Down> Suc n
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_take)


[STATEMENT]
theorem f_Exec_N_eq_f_Exec_Stream_Init_nth:"
  n \<le> length xs \<Longrightarrow>
  f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp_Stream_Init trans_fun xs c ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp_Stream_Init trans_fun xs c ! n
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_N_eq_f_Exec_Stream_nth)


[STATEMENT]
lemma list_Previous_nth: "xs\<^bsup>\<leftarrow>' init\<^esup> n = (case n of 0 \<Rightarrow> init | Suc n' \<Rightarrow> xs ! n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^bsup>\<leftarrow>' init\<^esup> n = (case n of 0 \<Rightarrow> init | Suc n' \<Rightarrow> xs ! n')
[PROOF STEP]
by (simp add: list_Previous_def)


[STATEMENT]
lemma ilist_Previous_nth: "f\<^bsup>\<leftarrow> init\<^esup> n = (case n of 0 \<Rightarrow> init | Suc n' \<Rightarrow> f n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^bsup>\<leftarrow> init\<^esup> n = (case n of 0 \<Rightarrow> init | Suc n' \<Rightarrow> f n')
[PROOF STEP]
by (simp add: ilist_Previous_def)


[STATEMENT]
lemma list_Previous_nth_if: "xs\<^bsup>\<leftarrow>' init\<^esup> n = (if n = 0 then init else xs ! (n - Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^bsup>\<leftarrow>' init\<^esup> n = (if n = 0 then init else xs ! (n - Suc 0))
[PROOF STEP]
by (case_tac n, simp_all add: list_Previous_nth)


[STATEMENT]
lemma ilist_Previous_nth_if: "f\<^bsup>\<leftarrow> init\<^esup> n = (if n = 0 then init else f (n - Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^bsup>\<leftarrow> init\<^esup> n = (if n = 0 then init else f (n - Suc 0))
[PROOF STEP]
by (case_tac n, simp_all add: ilist_Previous_nth)


[STATEMENT]
lemma list_Previous_Cons: "xs\<^bsup>\<leftarrow>' init\<^esup> n = (init # xs) ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^bsup>\<leftarrow>' init\<^esup> n = (init # xs) ! n
[PROOF STEP]
by (case_tac n, simp_all add: list_Previous_nth)


[STATEMENT]
lemma ilist_Previous_Cons: "f\<^bsup>\<leftarrow> init\<^esup> n = ([init] \<frown> f) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^bsup>\<leftarrow> init\<^esup> n = ([init] \<frown> f) n
[PROOF STEP]
by (case_tac n, simp_all add: ilist_Previous_nth)


[STATEMENT]
lemma list_Previous_0: "xs\<^bsup>\<leftarrow>' init\<^esup> 0 = init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^bsup>\<leftarrow>' init\<^esup> 0 = init
[PROOF STEP]
by (simp add: list_Previous_def)


[STATEMENT]
lemma ilist_Previous_0: "f\<^bsup>\<leftarrow> init\<^esup> 0 = init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^bsup>\<leftarrow> init\<^esup> 0 = init
[PROOF STEP]
by (simp add: ilist_Previous_def)


[STATEMENT]
lemma list_Previous_gr0: "0 < n \<Longrightarrow> xs\<^bsup>\<leftarrow>' init\<^esup> n = xs ! (n - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> xs\<^bsup>\<leftarrow>' init\<^esup> n = xs ! (n - Suc 0)
[PROOF STEP]
by (case_tac n, simp_all add: list_Previous_nth)


[STATEMENT]
lemma ilist_Previous_gr0: "0 < n \<Longrightarrow> f\<^bsup>\<leftarrow> init\<^esup> n = f (n - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f\<^bsup>\<leftarrow> init\<^esup> n = f (n - Suc 0)
[PROOF STEP]
by (case_tac n, simp_all add: ilist_Previous_nth)


[STATEMENT]
lemma list_Previous_Suc: "xs\<^bsup>\<leftarrow>' init\<^esup> (Suc n) = xs ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^bsup>\<leftarrow>' init\<^esup> Suc n = xs ! n
[PROOF STEP]
by (simp add: list_Previous_def)


[STATEMENT]
lemma ilist_Previous_Suc: "f\<^bsup>\<leftarrow> init\<^esup> (Suc n) = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^bsup>\<leftarrow> init\<^esup> Suc n = f n
[PROOF STEP]
by (simp add: ilist_Previous_def)


[STATEMENT]
lemma f_Exec_Stream_Previous_f_Exec_Stream_Init: "
  f_Exec_Comp_Stream_Init trans_fun xs c ! n =
  (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Init trans_fun xs c ! n = (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons list_Previous_Cons)


[STATEMENT]
lemma i_Exec_Stream_Previous_i_Exec_Stream_Init: "
  i_Exec_Comp_Stream_Init trans_fun input c n =
  (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c n = (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons ilist_Previous_Cons)


[STATEMENT]
lemma f_Exec_Stream_hd: "
  0 < length xs \<Longrightarrow> hd (f_Exec_Comp_Stream trans_fun xs c) = trans_fun (hd xs) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> hd (f_Exec_Comp_Stream trans_fun xs c) = trans_fun (hd xs) c
[PROOF STEP]
by (case_tac xs, simp+)


[STATEMENT]
lemma f_Exec_Stream_nth_0: "
  0 < length xs \<Longrightarrow> (f_Exec_Comp_Stream trans_fun xs c) ! 0= trans_fun (xs ! 0) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! 0 = trans_fun (xs ! 0) c
[PROOF STEP]
by (case_tac xs, simp+)


[STATEMENT]
lemma f_Exec_Stream_nth_gr0_calc: "
  \<lbrakk> n < length xs; 0 < n \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c ! n =
  trans_fun (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; 0 < n\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = trans_fun (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! (n - 1))
[PROOF STEP]
by (simp add: f_Exec_Stream_nth take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma f_Exec_Stream_nth_calc_Previous: "
  n < length xs \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c ! n =
  trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n)
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; n = 0\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n)
 2. \<And>nat. \<lbrakk>n < length xs; n = Suc nat\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n)
[PROOF STEP]
apply (simp add: list_Previous_0 f_Exec_Stream_nth_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n < length xs; n = Suc nat\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c ! n = trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n)
[PROOF STEP]
apply (simp add: list_Previous_def f_Exec_Stream_nth_gr0_calc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_nth_0: "
  (i_Exec_Comp_Stream trans_fun input c) 0 = trans_fun (input 0) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c 0 = trans_fun (input 0) c
[PROOF STEP]
by (simp add: i_Exec_Stream_nth i_take_first)