[STATEMENT]
lemma dom_char:
    shows "V.dom = (\<lambda>\<mu>. if V.arr \<mu> then
                          \<lparr>Chn = span_in_category.apex C (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>
                        else V.null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V.dom = (\<lambda>\<mu>. if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<mu>. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
fix \<mu>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<mu>. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
have "\<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null
[PROOF STEP]
by (simp add: V.arr_def V.dom_def)
[PROOF STATE]
proof (state)
this:
\<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null

goal (1 subgoal):
 1. \<And>\<mu>. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null

goal (1 subgoal):
 1. \<And>\<mu>. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
have "V.arr \<mu> \<Longrightarrow> V.dom \<mu> = \<lparr>Chn = span_in_category.apex C (Dom \<mu>),
                                            Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V.arr \<mu> \<Longrightarrow> V.dom \<mu> = \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>
[PROOF STEP]
by (metis V.comp_arr_dom V.comp_ide_self V.ideD(1) V.ide_dom arrow_of_spans_data.cases
            arrow_of_spans_data.select_convs(1-3) ide_char identity_arrow_of_spans.chine_eq_apex
            identity_arrow_of_spans_axioms.intro identity_arrow_of_spans_def seq_char)
[PROOF STATE]
proof (state)
this:
V.arr \<mu> \<Longrightarrow> V.dom \<mu> = \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>

goal (1 subgoal):
 1. \<And>\<mu>. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null
V.arr \<mu> \<Longrightarrow> V.dom \<mu> = \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>
[PROOF STEP]
show "V.dom \<mu> = (if V.arr \<mu> then
                                     \<lparr>Chn = span_in_category.apex C (Dom \<mu>),
                                      Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>
                                  else V.null)"
[PROOF STATE]
proof (prove)
using this:
\<not> V.arr \<mu> \<Longrightarrow> V.dom \<mu> = V.null
V.arr \<mu> \<Longrightarrow> V.dom \<mu> = \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr>

goal (1 subgoal):
 1. V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
V.dom \<mu> = (if V.arr \<mu> then \<lparr>Chn = span_in_category.apex (\<cdot>) (Dom \<mu>), Dom = Dom \<mu>, Cod = Dom \<mu>\<rparr> else V.null)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prj_chine_assoc' [simp]:
    shows "Prj\<^sub>1\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1"
    and "Prj\<^sub>0\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1\<^sub>0"
    and "Prj\<^sub>0 \<cdot> chine_assoc' = Prj\<^sub>0\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prj\<^sub>1\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1 &&& Prj\<^sub>0\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1\<^sub>0 &&& Prj\<^sub>0 \<cdot> chine_assoc' = Prj\<^sub>0\<^sub>0
[PROOF STEP]
using chine_assoc'_props(2-4)
[PROOF STATE]
proof (prove)
using this:
Prj\<^sub>1\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1
Prj\<^sub>0\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1\<^sub>0
Prj\<^sub>0 \<cdot> chine_assoc' = Prj\<^sub>0\<^sub>0

goal (1 subgoal):
 1. Prj\<^sub>1\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1 &&& Prj\<^sub>0\<^sub>1 \<cdot> chine_assoc' = Prj\<^sub>1\<^sub>0 &&& Prj\<^sub>0 \<cdot> chine_assoc' = Prj\<^sub>0\<^sub>0
[PROOF STEP]
by auto


[STATEMENT]
lemma inverse_assoc_assoc':
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "inverse_arrows (assoc\<^sub>S\<^sub>B f g h) (assoc'\<^sub>S\<^sub>B f g h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret f: arrow_of_spans C f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) f
[PROOF STEP]
using assms arr_char ideD(1)
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>
ide ?a \<Longrightarrow> arr ?a

goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret g: arrow_of_spans C g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) g
[PROOF STEP]
using assms arr_char ideD(1)
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>
ide ?a \<Longrightarrow> arr ?a

goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret h: arrow_of_spans C h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) h
[PROOF STEP]
using assms arr_char ideD(1)
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>
ide ?a \<Longrightarrow> arr ?a

goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret fgh: three_composable_arrows_of_spans C prj0 prj1 f g h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. three_composable_arrows_of_spans (\<cdot>) prj0 prj1 f g h
[PROOF STEP]
using assms arr_char
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>

goal (1 subgoal):
 1. three_composable_arrows_of_spans (\<cdot>) prj0 prj1 f g h
[PROOF STEP]
by (unfold_locales, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 f g h, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 f g h, Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret fgh: three_composable_identity_arrows_of_spans C prj0 prj1 f g h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. three_composable_identity_arrows_of_spans (\<cdot>) prj0 prj1 f g h
[PROOF STEP]
using assms ide_char
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
ide ?\<mu> = (arrow_of_spans (\<cdot>) ?\<mu> \<and> C.ide (Chn ?\<mu>))

goal (1 subgoal):
 1. three_composable_identity_arrows_of_spans (\<cdot>) prj0 prj1 f g h
[PROOF STEP]
by unfold_locales blast+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret afgh: arrow_of_spans C \<open>assoc\<^sub>S\<^sub>B f g h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>
[PROOF STEP]
using assms assoc_props(3) arr_char
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
\<lbrakk>ide ?f; ide ?g; ide ?h; src ?f = trg ?g; src ?g = trg ?h\<rbrakk> \<Longrightarrow> \<guillemotleft>\<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc (\<cdot>) prj0 prj1 ?f ?g ?h, Dom = Dom ((?f \<star> ?g) \<star> ?h), Cod = Cod (?f \<star> ?g \<star> ?h)\<rparr> : (?f \<star> ?g) \<star> ?h \<Rightarrow> ?f \<star> ?g \<star> ?h\<guillemotright>
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>

goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
interpret a'fgh: arrow_of_spans C \<open>assoc'\<^sub>S\<^sub>B f g h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
using assms assoc_props(6) arr_char
[PROOF STATE]
proof (prove)
using this:
ide f
ide g
ide h
src f = trg g
src g = trg h
\<lbrakk>ide ?f; ide ?g; ide ?h; src ?f = trg ?g; src ?g = trg ?h\<rbrakk> \<Longrightarrow> \<guillemotleft>\<lparr>Chn = three_composable_identity_arrows_of_spans.chine_assoc' (\<cdot>) prj0 prj1 ?f ?g ?h, Dom = Cod (?f \<star> ?g \<star> ?h), Cod = Dom ((?f \<star> ?g) \<star> ?h)\<rparr> : ?f \<star> ?g \<star> ?h \<Rightarrow> (?f \<star> ?g) \<star> ?h\<guillemotright>
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>

goal (1 subgoal):
 1. arrow_of_spans (\<cdot>) \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
have "inverse_arrows (assoc\<^sub>S\<^sub>B f g h)
                             \<lparr>Chn = C.inv (Chn (assoc\<^sub>S\<^sub>B f g h)),
                              Dom = Cod (assoc\<^sub>S\<^sub>B f g h), Cod = Dom (assoc\<^sub>S\<^sub>B f g h)\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>
[PROOF STEP]
using inverse_arrows [of "assoc\<^sub>S\<^sub>B f g h"] afgh.arrow_of_spans_axioms
                arr_char fgh.chine_assoc_inverse
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>arr \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>; C.iso afgh.chine\<rbrakk> \<Longrightarrow> inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>
arrow_of_spans (\<cdot>) \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>
arr ?\<mu> = arrow_of_spans (\<cdot>) ?\<mu>
C.inverse_arrows fgh.chine_assoc fgh.chine_assoc'

goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>

goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>

goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
have "C.inv (Chn (assoc\<^sub>S\<^sub>B f g h)) = fgh.chine_assoc'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inv afgh.chine = fgh.chine_assoc'
[PROOF STEP]
using fgh.chine_assoc_inverse C.inv_is_inverse C.inverse_arrow_unique
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows fgh.chine_assoc fgh.chine_assoc'
C.iso ?f \<Longrightarrow> C.inverse_arrows ?f (C.inv ?f)
\<lbrakk>C.inverse_arrows ?f ?g; C.inverse_arrows ?f ?g'\<rbrakk> \<Longrightarrow> ?g = ?g'

goal (1 subgoal):
 1. C.inv afgh.chine = fgh.chine_assoc'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C.inv afgh.chine = fgh.chine_assoc'

goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>
C.inv afgh.chine = fgh.chine_assoc'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = C.inv afgh.chine, Dom = Cod \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>, Cod = Dom \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr>\<rparr>
C.inv afgh.chine = fgh.chine_assoc'

goal (1 subgoal):
 1. inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse_arrows \<lparr>Chn = fgh.chine_assoc, Dom = Dom ((f \<star> g) \<star> h), Cod = Cod (f \<star> g \<star> h)\<rparr> \<lparr>Chn = fgh.chine_assoc', Dom = Cod (f \<star> g \<star> h), Cod = Dom ((f \<star> g) \<star> h)\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HSem_subst_var_app:
  assumes fresh: "atom n \<sharp> x"
  shows "\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho> = \<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho> = \<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>
[PROOF STEP]
proof(rule HSem_subst_expr)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
from fresh
[PROOF STATE]
proof (chain)
picking this:
atom n \<sharp> x
[PROOF STEP]
have [simp]: "n \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
atom n \<sharp> x

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

goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
have ne: "(n,e) \<in> set ((x, App e y) # (n, e) # \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n, e) \<in> set ((x, App e y) # (n, e) # \<Gamma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(n, e) \<in> set ((x, App e y) # (n, e) # \<Gamma>)

goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
have "\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n

goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n

goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
have "... = \<lbrakk> e \<rbrakk>\<^bsub>(\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
by (subst HSem_eq, simp)
[PROOF STATE]
proof (state)
this:
(\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal (2 subgoals):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
 2. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
show "\<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal (1 subgoal):
 1. \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App e y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal (1 subgoal):
 1. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
have "\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n

goal (1 subgoal):
 1. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = (\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n

goal (1 subgoal):
 1. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
have "... = \<lbrakk> e \<rbrakk>\<^bsub>(\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
by (subst HSem_eq, simp)
[PROOF STATE]
proof (state)
this:
(\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>) n = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal (1 subgoal):
 1. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
show "\<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> Var n \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> = \<lbrakk> e \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal (1 subgoal):
 1. \<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk> App e y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> App (Var n) y \<rbrakk>\<^bsub>\<lbrace>(x, App (Var n) y) # (n, e) # \<Gamma>\<rbrace>\<rho>\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma successive_step_rev:
  "successive P (xs @ [x]) \<Longrightarrow> \<not> P x \<Longrightarrow> successive P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>successive P (xs @ [x]); \<not> P x\<rbrakk> \<Longrightarrow> successive P xs
[PROOF STEP]
by (induction _ xs rule: list_two_induct) auto


[STATEMENT]
lemma Some_in_opt [iff]: "(Some x \<in> opt A) = (x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> opt A) = (x \<in> A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> opt A) = (x \<in> A)
[PROOF STEP]
by (unfold opt_def) auto


[STATEMENT]
lemma qbs_integrable_pair1:
  assumes "p \<in> monadP_qbs_Px X"
          "q \<in> monadP_qbs_Px Y"
          "f \<in> X \<Otimes>\<^sub>Q Y \<rightarrow>\<^sub>Q \<real>\<^sub>Q"
          "qbs_integrable p (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x,y)\<bar> \<partial>q)"
      and "\<And>x. x \<in> qbs_space X \<Longrightarrow> qbs_integrable q (\<lambda>y. f (x,y))"
    shows "qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
obtain \<alpha> \<mu> where hp:
    "p = qbs_prob_space (X, \<alpha>, \<mu>)" "qbs_prob X \<alpha> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha> \<mu>. \<lbrakk>p = qbs_prob_space (X, \<alpha>, \<mu>); qbs_prob X \<alpha> \<mu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rep_monadP_qbs_Px[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha> \<mu>. p = qbs_prob_space (X, \<alpha>, \<mu>) \<and> qbs_prob X \<alpha> \<mu>

goal (1 subgoal):
 1. (\<And>\<alpha> \<mu>. \<lbrakk>p = qbs_prob_space (X, \<alpha>, \<mu>); qbs_prob X \<alpha> \<mu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = qbs_prob_space (X, \<alpha>, \<mu>)
qbs_prob X \<alpha> \<mu>

goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
obtain \<beta> \<nu> where hq:
   "q = qbs_prob_space (Y, \<beta>, \<nu>)" "qbs_prob Y \<beta> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<beta> \<nu>. \<lbrakk>q = qbs_prob_space (Y, \<beta>, \<nu>); qbs_prob Y \<beta> \<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rep_monadP_qbs_Px[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha> \<mu>. q = qbs_prob_space (Y, \<alpha>, \<mu>) \<and> qbs_prob Y \<alpha> \<mu>

goal (1 subgoal):
 1. (\<And>\<beta> \<nu>. \<lbrakk>q = qbs_prob_space (Y, \<beta>, \<nu>); qbs_prob Y \<beta> \<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q = qbs_prob_space (Y, \<beta>, \<nu>)
qbs_prob Y \<beta> \<nu>

goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
interpret pqp: pair_qbs_probs X \<alpha> \<mu> Y \<beta> \<nu>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_qbs_probs X \<alpha> \<mu> Y \<beta> \<nu>
[PROOF STEP]
by(simp add: pair_qbs_probs_def hp hq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
have "integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>)
[PROOF STEP]
proof(rule pqp.Fubini_integrable)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pqp.P.random_variable real_borel (f \<circ> map_prod \<alpha> \<beta>)
 2. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 3. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
show "f \<circ> map_prod \<alpha> \<beta> \<in> borel_measurable (\<mu> \<Otimes>\<^sub>M \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pqp.P.random_variable real_borel (f \<circ> map_prod \<alpha> \<beta>)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
f \<in> X \<Otimes>\<^sub>Q Y \<rightarrow>\<^sub>Q \<real>\<^sub>Q

goal (1 subgoal):
 1. pqp.P.random_variable real_borel (f \<circ> map_prod \<alpha> \<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pqp.P.random_variable real_borel (f \<circ> map_prod \<alpha> \<beta>)

goal (2 subgoals):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 2. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 2. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
have "(\<lambda>x. LINT y|\<nu>. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x,y)\<bar> \<partial>q) \<circ> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))) = ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>) x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))) = ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>) x
[PROOF STEP]
using qbs_morphism_Pair1'[OF qbs_Mx_to_X(2)[OF pqp.qp1.in_Mx,of x] assms(3)]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>y. f (\<alpha> x, y)) \<in> Y \<rightarrow>\<^sub>Q \<real>\<^sub>Q

goal (1 subgoal):
 1. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))) = ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>) x
[PROOF STEP]
by(auto intro!: pqp.qp2.qbs_prob_integral_def[symmetric] simp: hq(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>

goal (2 subgoals):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 2. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>

goal (2 subgoals):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 2. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
have "integrable \<mu> ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable \<mu> ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>)
[PROOF STEP]
using assms(4) pqp.qp1.qbs_integrable_def
[PROOF STATE]
proof (prove)
using this:
qbs_integrable p (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q)
qbs_integrable (qbs_prob_space (X, \<alpha>, \<mu>)) ?f = (?f \<in> X \<rightarrow>\<^sub>Q \<real>\<^sub>Q \<and> integrable \<mu> (?f \<circ> \<alpha>))

goal (1 subgoal):
 1. integrable \<mu> ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>)
[PROOF STEP]
by (simp add: hp(1))
[PROOF STATE]
proof (state)
this:
integrable \<mu> ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>)

goal (2 subgoals):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
 2. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>
integrable \<mu> ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>)
[PROOF STEP]
show "integrable \<mu> (\<lambda>x. LINT y|\<nu>. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y)))) = (\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>
integrable \<mu> ((\<lambda>x. \<integral>\<^sub>Q y. \<bar>f (x, y)\<bar> \<partial>q) \<circ> \<alpha>)

goal (1 subgoal):
 1. integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integrable \<mu> (\<lambda>x. pqp.qp2.expectation (\<lambda>y. norm ((f \<circ> map_prod \<alpha> \<beta>) (x, y))))

goal (1 subgoal):
 1. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
have "\<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
have "(\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x,y)) \<circ> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x, y)) \<circ> \<beta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x, y)) \<circ> \<beta>

goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x, y)) \<circ> \<beta>

goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
have "qbs_integrable (qbs_prob_space (Y, \<beta>, \<nu>)) (\<lambda>y. f (\<alpha> x, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_integrable (qbs_prob_space (Y, \<beta>, \<nu>)) (\<lambda>y. f (\<alpha> x, y))
[PROOF STEP]
by(auto intro!: assms(5)[simplified hq(1)] simp: qbs_Mx_to_X)
[PROOF STATE]
proof (state)
this:
qbs_integrable (qbs_prob_space (Y, \<beta>, \<nu>)) (\<lambda>y. f (\<alpha> x, y))

goal (1 subgoal):
 1. \<And>x. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x, y)) \<circ> \<beta>
qbs_integrable (qbs_prob_space (Y, \<beta>, \<nu>)) (\<lambda>y. f (\<alpha> x, y))
[PROOF STEP]
show "integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y)) = (\<lambda>y. f (\<alpha> x, y)) \<circ> \<beta>
qbs_integrable (qbs_prob_space (Y, \<beta>, \<nu>)) (\<lambda>y. f (\<alpha> x, y))

goal (1 subgoal):
 1. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
by(simp add: pqp.qp2.qbs_integrable_def)
[PROOF STATE]
proof (state)
this:
integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (?x1, y))

goal (1 subgoal):
 1. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
thus "AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))"
[PROOF STATE]
proof (prove)
using this:
integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (?x1, y))

goal (1 subgoal):
 1. AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in \<mu>. integrable \<nu> (\<lambda>y. (f \<circ> map_prod \<alpha> \<beta>) (x, y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>)

goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>)

goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
using pqp.qbs_prob_pair_measure_integrable'[OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>)
integrable (\<mu> \<Otimes>\<^sub>M \<nu>) (f \<circ> map_prod \<alpha> \<beta>) \<Longrightarrow> qbs_integrable (qbs_prob_space (X, \<alpha>, \<mu>) \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s qbs_prob_space (Y, \<beta>, \<nu>)) f

goal (1 subgoal):
 1. qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f
[PROOF STEP]
by(simp add: hp(1) hq(1))
[PROOF STATE]
proof (state)
this:
qbs_integrable (p \<Otimes>\<^sub>Q\<^sub>m\<^sub>e\<^sub>s q) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_star_trueE: assumes "h\<Turnstile>P*true" obtains h' where "h'\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h'. h' \<Turnstile> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> P * true

goal (1 subgoal):
 1. (\<And>h'. h' \<Turnstile> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: mod_star_trueE')


[STATEMENT]
lemma lex_mirror_point: "lex (mirror_point x0 a) (mirror_point x0 b) \<Longrightarrow> lex b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Counterclockwise_2D_Arbitrary.lex (mirror_point x0 a) (mirror_point x0 b) \<Longrightarrow> Counterclockwise_2D_Arbitrary.lex b a
[PROOF STEP]
by (auto simp: mirror_point_def lex_def)


[STATEMENT]
theorem PfP_implies_ModPon_PfP: "\<lbrakk>H \<turnstile> PfP (Q_Imp x y); H \<turnstile> PfP x\<rbrakk> \<Longrightarrow> H \<turnstile> PfP y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> PfP (Q_Imp x y); H \<turnstile> PfP x\<rbrakk> \<Longrightarrow> H \<turnstile> PfP y
[PROOF STEP]
by (force intro: PfP_inference [of x, THEN cut3] Disj_I1  simp add: ModPonP_def)


[STATEMENT]
lemma is_shadow_root_ptr_kind_simp1 [dest]: "is_document_ptr_kind ptr \<Longrightarrow> \<not>is_shadow_root_ptr_kind ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_document_ptr_kind ptr \<Longrightarrow> \<not> is_shadow_root_ptr_kind ptr
[PROOF STEP]
by (metis document_ptr_no_shadow_root_ptr_cast shadow_root_ptr_casts_commute3)


[STATEMENT]
lemma oexp_\<omega>_Limit: "Limit \<beta> \<Longrightarrow> \<omega>\<up>\<beta> = (\<Squnion>\<xi> \<in> elts \<beta>. \<omega>\<up>\<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit \<beta> \<Longrightarrow> \<omega> \<up> \<beta> = \<Squnion> ((\<up>) \<omega> ` elts \<beta>)
[PROOF STEP]
by (simp add: oexp_Limit)


[STATEMENT]
lemma vote_set_as_Union:
  "vote_set vs Q = (\<Union>a\<in>(Q \<inter> voters vs). vote_set vs {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vote_set vs Q = (\<Union>a\<in>Q \<inter> voters vs. vote_set vs {a})
[PROOF STEP]
by(auto simp add: vote_set_def voters_def)


[STATEMENT]
lemma Inf_subdistr: "\<Sqinter> X \<cdot> y \<le> (\<Sqinter>x \<in> X. x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> X \<cdot> y \<le> (\<Sqinter>x\<in>X. x \<cdot> y)
[PROOF STEP]
by (auto intro!: Inf_greatest Inf_lower mult_isor)


[STATEMENT]
lemma downset_filter:
  assumes "downset xss"
  shows "downset (filter P ` xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. downset (filter P ` xss)
[PROOF STEP]
proof(rule, elim imageE, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>filter P x \<noteq> []; x \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P x) \<in> filter P ` xss
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>filter P x \<noteq> []; x \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P x) \<in> filter P ` xss
[PROOF STEP]
assume "xs \<in> xss"
[PROOF STATE]
proof (state)
this:
xs \<in> xss

goal (1 subgoal):
 1. \<And>x. \<lbrakk>filter P x \<noteq> []; x \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P x) \<in> filter P ` xss
[PROOF STEP]
thus "butlast (filter P xs) \<in> filter P ` xss"
[PROOF STATE]
proof (prove)
using this:
xs \<in> xss

goal (1 subgoal):
 1. butlast (filter P xs) \<in> filter P ` xss
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<in> xss \<Longrightarrow> butlast (filter P []) \<in> filter P ` xss
 2. \<And>x xs. \<lbrakk>xs \<in> xss \<Longrightarrow> butlast (filter P xs) \<in> filter P ` xss; xs @ [x] \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P (xs @ [x])) \<in> filter P ` xss
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<in> xss

goal (2 subgoals):
 1. [] \<in> xss \<Longrightarrow> butlast (filter P []) \<in> filter P ` xss
 2. \<And>x xs. \<lbrakk>xs \<in> xss \<Longrightarrow> butlast (filter P xs) \<in> filter P ` xss; xs @ [x] \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P (xs @ [x])) \<in> filter P ` xss
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] \<in> xss

goal (1 subgoal):
 1. butlast (filter P []) \<in> filter P ` xss
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
butlast (filter P []) \<in> filter P ` xss

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>xs \<in> xss \<Longrightarrow> butlast (filter P xs) \<in> filter P ` xss; xs @ [x] \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P (xs @ [x])) \<in> filter P ` xss
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>xs \<in> xss \<Longrightarrow> butlast (filter P xs) \<in> filter P ` xss; xs @ [x] \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P (xs @ [x])) \<in> filter P ` xss
[PROOF STEP]
case snoc
[PROOF STATE]
proof (state)
this:
xs_ \<in> xss \<Longrightarrow> butlast (filter P xs_) \<in> filter P ` xss
xs_ @ [x_] \<in> xss

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>xs \<in> xss \<Longrightarrow> butlast (filter P xs) \<in> filter P ` xss; xs @ [x] \<in> xss\<rbrakk> \<Longrightarrow> butlast (filter P (xs @ [x])) \<in> filter P ` xss
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs_ \<in> xss \<Longrightarrow> butlast (filter P xs_) \<in> filter P ` xss
xs_ @ [x_] \<in> xss

goal (1 subgoal):
 1. butlast (filter P (xs_ @ [x_])) \<in> filter P ` xss
[PROOF STEP]
using \<open>downset xss\<close>
[PROOF STATE]
proof (prove)
using this:
xs_ \<in> xss \<Longrightarrow> butlast (filter P xs_) \<in> filter P ` xss
xs_ @ [x_] \<in> xss
downset xss

goal (1 subgoal):
 1. butlast (filter P (xs_ @ [x_])) \<in> filter P ` xss
[PROOF STEP]
by (auto intro: snoc.IH)
[PROOF STATE]
proof (state)
this:
butlast (filter P (xs_ @ [x_])) \<in> filter P ` xss

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
butlast (filter P xs) \<in> filter P ` xss

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma floor_half_interval:
  fixes n d :: nat
  assumes "d \<noteq> 0"
  shows "real (n div d) - real (2 * ((n div 2) div d)) = (if odd (n div d) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
have "((n div 2) div d) = (n div (2 * d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n div 2 div d = n div (2 * d)
[PROOF STEP]
by (rule div_mult2_eq[symmetric])
[PROOF STATE]
proof (state)
this:
n div 2 div d = n div (2 * d)

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n div 2 div d = n div (2 * d)

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
have "\<dots> = ((n div d) div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n div (2 * d) = n div d div 2
[PROOF STEP]
by (simp add: mult_ac div_mult2_eq)
[PROOF STATE]
proof (state)
this:
n div (2 * d) = n div d div 2

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n div (2 * d) = n div d div 2

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
have "real (n div d) - real (2 * \<dots>) = (if odd (n div d) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (n div d) - real (2 * (n div d div 2)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
by (cases "odd (n div d)", cases "n div d = 0 ", simp_all)
[PROOF STATE]
proof (state)
this:
real (n div d) - real (2 * (n div d div 2)) = (if odd (n div d) then 1 else 0)

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)

goal (1 subgoal):
 1. real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (n div d) - real (2 * (n div 2 div d)) = (if odd (n div d) then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_norm_le:
  fixes Q :: "'a :: banach \<Rightarrow>\<^sub>L 'a"
  assumes "norm Q  < 1"
  shows "(id_blinfun-Q) o\<^sub>L (\<Sum>i. Q^^i) = id_blinfun"
    "(\<Sum>i. Q^^i) o\<^sub>L (id_blinfun-Q) = id_blinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_blinfun - Q o\<^sub>L (\<Sum>i. Q ^^ i) = id_blinfun &&& (\<Sum>i. Q ^^ i) o\<^sub>L id_blinfun - Q = id_blinfun
[PROOF STEP]
using inv_one_sub_Q[of "id_blinfun - Q"] assms
[PROOF STATE]
proof (prove)
using this:
norm (id_blinfun - (id_blinfun - Q)) < 1 \<Longrightarrow> id_blinfun - Q o\<^sub>L (\<Sum>i. (id_blinfun - (id_blinfun - Q)) ^^ i) = id_blinfun
norm (id_blinfun - (id_blinfun - Q)) < 1 \<Longrightarrow> (\<Sum>i. (id_blinfun - (id_blinfun - Q)) ^^ i) o\<^sub>L id_blinfun - Q = id_blinfun
norm Q < 1

goal (1 subgoal):
 1. id_blinfun - Q o\<^sub>L (\<Sum>i. Q ^^ i) = id_blinfun &&& (\<Sum>i. Q ^^ i) o\<^sub>L id_blinfun - Q = id_blinfun
[PROOF STEP]
by auto


[STATEMENT]
lemma DynCastReds:
  "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C e',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C e',s'\<rangle>
[PROOF STEP]
apply(erule rtrancl_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C e,s\<rangle>
 2. \<And>a b aa ba. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>a,b\<rangle>; ((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C a,b\<rangle>\<rbrakk> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C aa,ba\<rangle>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>a,b\<rangle>; ((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C a,b\<rangle>\<rbrakk> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>Cast C aa,ba\<rangle>
[PROOF STEP]
apply(erule rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>a,b\<rangle>; ((a, b), aa, ba) \<in> Red P E\<rbrakk> \<Longrightarrow> ((Cast C a, b), Cast C aa, ba) \<in> Red P E
[PROOF STEP]
apply (simp add:DynCastRed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ts_c': assumes "x \<noteq> y"
  "v \<in> lang (seq[Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
  "(\<exists>hs. h = [x, x] @ hs) \<or> h = [x] \<or> h = []"
  shows "T_on' (rTS h0) ([x, y], h) v = (length v - 2)
            \<and>  config' (rTS h0) ([x,y], h) v = ([x,y],rev v@h) \<and> (\<exists>hs. (rev v @ h) = [x,x]@hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])
(\<exists>hs. h = [x, x] @ hs) \<or> h = [x] \<or> h = []
[PROOF STEP]
have lenvmod: "length v mod 2 = 1"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])
(\<exists>hs. h = [x, x] @ hs) \<or> h = [x] \<or> h = []

goal (1 subgoal):
 1. length v mod 2 = 1
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
assume "v \<in> ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[x]}"
[PROOF STATE]
proof (state)
this:
v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}
[PROOF STEP]
obtain p q r where pqr: "v=p@q@r" and "p\<in>({[y]} @@ {[x]})"
              and q: "q \<in> star ({[y]} @@ {[x]})" and "r \<in> {[x]}"
[PROOF STATE]
proof (prove)
using this:
v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}

goal (1 subgoal):
 1. (\<And>p q r. \<lbrakk>v = p @ q @ r; p \<in> {[y]} @@ {[x]}; q \<in> star ({[y]} @@ {[x]}); r \<in> {[x]}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis concE)
[PROOF STATE]
proof (state)
this:
v = p @ q @ r
p \<in> {[y]} @@ {[x]}
q \<in> star ({[y]} @@ {[x]})
r \<in> {[x]}

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = p @ q @ r
p \<in> {[y]} @@ {[x]}
q \<in> star ({[y]} @@ {[x]})
r \<in> {[x]}
[PROOF STEP]
have "p = [y,x]" "r=[x]"
[PROOF STATE]
proof (prove)
using this:
v = p @ q @ r
p \<in> {[y]} @@ {[x]}
q \<in> star ({[y]} @@ {[x]})
r \<in> {[x]}

goal (1 subgoal):
 1. p = [y, x] &&& r = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = [y, x]
r = [x]

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
with pqr
[PROOF STATE]
proof (chain)
picking this:
v = p @ q @ r
p = [y, x]
r = [x]
[PROOF STEP]
have a: "length v = 3+length q"
[PROOF STATE]
proof (prove)
using this:
v = p @ q @ r
p = [y, x]
r = [x]

goal (1 subgoal):
 1. length v = 3 + length q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v = 3 + length q

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
q \<in> star ({[y]} @@ {[x]})
[PROOF STEP]
have b: "length q mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
q \<in> star ({[y]} @@ {[x]})

goal (1 subgoal):
 1. length q mod 2 = 0
[PROOF STEP]
apply(induct q rule: star_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length [] mod 2 = 0
 2. \<And>u v. \<lbrakk>u \<in> {[y]} @@ {[x]}; v \<in> star ({[y]} @@ {[x]}); length v mod 2 = 0\<rbrakk> \<Longrightarrow> length (u @ v) mod 2 = 0
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
length q mod 2 = 0

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; v \<in> ({[y]} @@ {[x]}) @@ star ({[y]} @@ {[x]}) @@ {[x]}; (\<exists>hs. h = x # x # hs) \<or> h = [x] \<or> h = []\<rbrakk> \<Longrightarrow> length v mod 2 = Suc 0
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
length v = 3 + length q
length q mod 2 = 0
[PROOF STEP]
show "length v mod 2 = Suc 0"
[PROOF STATE]
proof (prove)
using this:
length v = 3 + length q
length q mod 2 = 0

goal (1 subgoal):
 1. length v mod 2 = Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length v mod 2 = Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length v mod 2 = 1

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
with assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
(\<exists>hs. h = [x, x] @ hs) \<or> h = [x] \<or> h = []
length v mod 2 = 1
[PROOF STEP]
have fall: "(\<exists>hs. h = [x, x] @ hs) \<or> index h y = length h"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
(\<exists>hs. h = [x, x] @ hs) \<or> h = [x] \<or> h = []
length v mod 2 = 1

goal (1 subgoal):
 1. (\<exists>hs. h = [x, x] @ hs) \<or> index h y = length h
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<exists>hs. h = [x, x] @ hs) \<or> index h y = length h

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])
[PROOF STEP]
have "v \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom x])"
[PROOF STATE]
proof (prove)
using this:
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])

goal (1 subgoal):
 1. v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))]) @@ lang (seq [Atom x])
[PROOF STEP]
by (auto simp: conc_def)
[PROOF STATE]
proof (state)
this:
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))]) @@ lang (seq [Atom x])

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))]) @@ lang (seq [Atom x])
[PROOF STEP]
obtain a b where aa: "a \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b \<in> lang (seq[Atom x])"
                      and vab: "v = a @ b"
[PROOF STATE]
proof (prove)
using this:
v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))]) @@ lang (seq [Atom x])

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))]); b \<in> lang (seq [Atom x]); v = a @ b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule concE)
[PROOF STATE]
proof (state)
this:
a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))])
b \<in> lang (seq [Atom x])
v = a @ b

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))])
b \<in> lang (seq [Atom x])
v = a @ b
[PROOF STEP]
have bb: "b=[x]"
[PROOF STATE]
proof (prove)
using this:
a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))])
b \<in> lang (seq [Atom x])
v = a @ b

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

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from aa
[PROOF STATE]
proof (chain)
picking this:
a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))])
[PROOF STEP]
have lena: "length a > 0"
[PROOF STATE]
proof (prove)
using this:
a \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x))])

goal (1 subgoal):
 1. 0 < length a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < length a

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from TS_yxyx'[OF assms(1) aa fall]
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.T_on' (rTS ?h0.0) ([x, y], h) (a @ ?r) = length a - 1 + Partial_Cost_Model.T_on' (rTS ?h0.0) ([x, y], rev a @ h) ?r \<and> (\<exists>hs. rev a @ h = [x, y] @ hs) \<and> Partial_Cost_Model.config' (rTS ?h0.0) ([x, y], h) a = ([x, y], rev a @ h)
[PROOF STEP]
have stars: "T_on' (rTS h0) ([x, y], h) (a @ b) =
    length a - 1 + T_on' (rTS h0) ([x, y],rev a @ h) b"
    and history: "(\<exists>hs. rev a @ h = [x, y] @ hs)"
    and state: "config' (rTS h0) ([x, y], h) a =  ([x, y], rev a @ h)"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS ?h0.0) ([x, y], h) (a @ ?r) = length a - 1 + Partial_Cost_Model.T_on' (rTS ?h0.0) ([x, y], rev a @ h) ?r \<and> (\<exists>hs. rev a @ h = [x, y] @ hs) \<and> Partial_Cost_Model.config' (rTS ?h0.0) ([x, y], h) a = ([x, y], rev a @ h)

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1 + Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b &&& \<exists>hs. rev a @ h = [x, y] @ hs &&& Partial_Cost_Model.config' (rTS h0) ([x, y], h) a = ([x, y], rev a @ h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1 + Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b
\<exists>hs. rev a @ h = [x, y] @ hs
Partial_Cost_Model.config' (rTS h0) ([x, y], h) a = ([x, y], rev a @ h)

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
have suffix: "T_on' (rTS h0) ( [x, y],rev a @ h) b = 0"
          and suState: "config' (rTS h0) ([x, y], rev a @ h) b = ([x,y], rev b @ (rev a @ h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b = 0 &&& Partial_Cost_Model.config' (rTS h0) ([x, y], rev a @ h) b = ([x, y], rev b @ rev a @ h)
[PROOF STEP]
unfolding bb
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) [x] = 0 &&& Partial_Cost_Model.config' (rTS h0) ([x, y], rev a @ h) [x] = ([x, y], rev [x] @ rev a @ h)
[PROOF STEP]
using TS_x'
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS ?h0.0) ([?x, ?y], ?h) [?x] = 0 \<and> Partial_Cost_Model.config' (rTS ?h0.0) ([?x, ?y], ?h) [?x] = ([?x, ?y], rev [?x] @ ?h)

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) [x] = 0 &&& Partial_Cost_Model.config' (rTS h0) ([x, y], rev a @ h) [x] = ([x, y], rev [x] @ rev a @ h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b = 0
Partial_Cost_Model.config' (rTS h0) ([x, y], rev a @ h) b = ([x, y], rev b @ rev a @ h)

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from stars suffix
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1 + Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b
Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b = 0
[PROOF STEP]
have "T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1 + Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b
Partial_Cost_Model.T_on' (rTS h0) ([x, y], rev a @ h) b = 0

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1
[PROOF STEP]
have whatineed: "T_on' (rTS h0) ([x, y], h) v = (length v - 2)"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2
[PROOF STEP]
using vab bb
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) (a @ b) = length a - 1
v = a @ b
b = [x]

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
have conf: "config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)
[PROOF STEP]
by(simp add: vab config'_append2 state suState)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
from history
[PROOF STATE]
proof (chain)
picking this:
\<exists>hs. rev a @ h = [x, y] @ hs
[PROOF STEP]
obtain hs' where "rev a @ h = [x, y] @ hs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>hs. rev a @ h = [x, y] @ hs

goal (1 subgoal):
 1. (\<And>hs'. rev a @ h = [x, y] @ hs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev a @ h = [x, y] @ hs'

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rev a @ h = [x, y] @ hs'
[PROOF STEP]
obtain hs2 where reva: "rev a @ h = x # hs2"
[PROOF STATE]
proof (prove)
using this:
rev a @ h = [x, y] @ hs'

goal (1 subgoal):
 1. (\<And>hs2. rev a @ h = x # hs2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev a @ h = x # hs2

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
using whatineed
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2

goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<Longrightarrow> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)
 2. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<Longrightarrow> \<exists>hs. rev v @ h = x # x # hs
[PROOF STEP]
using conf
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)

goal (2 subgoals):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<Longrightarrow> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h)
 2. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<Longrightarrow> \<exists>hs. rev v @ h = x # x # hs
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<Longrightarrow> \<exists>hs. rev v @ h = x # x # hs
[PROOF STEP]
by(simp add: reva vab bb)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on' (rTS h0) ([x, y], h) v = length v - 2 \<and> Partial_Cost_Model.config' (rTS h0) ([x, y], h) v = ([x, y], rev v @ h) \<and> (\<exists>hs. rev v @ h = [x, x] @ hs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assm2: "Ana (Fun f T) = (K, M) \<Longrightarrow> set M \<subseteq> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ana (Fun f T) = (K, M) \<Longrightarrow> set M \<subseteq> set T
[PROOF STEP]
by (rule Ana.cases[of "Fun f T"]) (auto elim!: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t.elims Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n.elims)


[STATEMENT]
lemma apply_ops_k_next2 [rewrite]:
  "is_rect_list rects \<Longrightarrow> ops = all_ops rects \<Longrightarrow> n < length ops \<Longrightarrow> \<not>is_INS (ops ! n) \<Longrightarrow>
   apply_ops_k rects (n + 1) = apply_ops_k rects n - {op_idx (ops ! n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_rect_list rects; ops = all_ops rects; n < length ops; \<not> is_INS (ops ! n)\<rbrakk> \<Longrightarrow> apply_ops_k rects (n + 1) = apply_ops_k rects n - {op_idx (ops ! n)}
[PROOF STEP]
by auto2


[STATEMENT]
lemma ir_valid_Seq1:
  "ir_valid P (c1;; c2) c' Q \<Longrightarrow> ir_valid P c1 c' (\<lambda>t t'. \<exists>s s'. P s s' \<and> (c1,s) \<Rightarrow> t \<and> (c',s') \<Rightarrow> t' \<and> (\<exists>u. (c2,t) \<Rightarrow> u \<and> Q u t'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ir_valid P (c1;; c2) c' Q \<Longrightarrow> ir_valid P c1 c' (\<lambda>t t'. \<exists>s s'. P s s' \<and> (c1, s) \<Rightarrow> t \<and> (c', s') \<Rightarrow> t' \<and> (\<exists>u. (c2, t) \<Rightarrow> u \<and> Q u t'))
[PROOF STEP]
by(auto simp: ir_valid_def)


[STATEMENT]
lemma [iff]: "P,E,h \<turnstile> Val v : T = (typeof\<^bsub>h\<^esub> v = Some T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E,h \<turnstile> Val v : T) = (typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E,h \<turnstile> Val v : T) = (typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>)
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P,E,h \<turnstile> Val v : T \<Longrightarrow> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>
 2. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<Longrightarrow> P,E,h \<turnstile> Val v : T
[PROOF STEP]
qed (auto elim: WTrt.cases)


[STATEMENT]
lemma tl_hd_x_not_tl_x:
shows "x \<noteq> [] \<and> hd x \<noteq> [] \<longrightarrow> tl (hd x) # tl x \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> [] \<and> hd x \<noteq> [] \<longrightarrow> tl (hd x) # tl x \<noteq> x
[PROOF STEP]
using tl_x_not_x
[PROOF STATE]
proof (prove)
using this:
?x \<noteq> [] \<longrightarrow> tl ?x \<noteq> ?x

goal (1 subgoal):
 1. x \<noteq> [] \<and> hd x \<noteq> [] \<longrightarrow> tl (hd x) # tl x \<noteq> x
[PROOF STEP]
by(induct x,simp,auto)


[STATEMENT]
lemma powr_ln_powr_lower_bound:
  "a > 1 \<Longrightarrow> a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow>
     min (a powr p) (b powr p) * min (ln a powr p') (ln b powr p') \<le> x powr p * ln x powr p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < a; a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> min (a powr p) (b powr p) * min (ln a powr p') (ln b powr p') \<le> x powr p * ln x powr p'
[PROOF STEP]
by (intro mult_mono powr_lower_bound) (auto intro: min.coboundedI1)


[STATEMENT]
lemma height_bplustree_sub:
  "height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. height (Node ((sub, x) # ls) t) = max (height (Node ls t)) (Suc (height sub))
[PROOF STEP]
by simp


[STATEMENT]
theorem n_permutation_enum_correct: "distinct xs \<Longrightarrow> set (n_permutation_enum xs n) = n_permutations (set xs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> set (n_permutation_enum xs n) = n_permutations (set xs) n
[PROOF STEP]
proof standard
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n
 2. distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)
[PROOF STEP]
show "distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n
[PROOF STEP]
by (simp add: n_permutation_enum_correct1)
[PROOF STATE]
proof (state)
this:
distinct xs \<Longrightarrow> set (n_permutation_enum xs n) \<subseteq> n_permutations (set xs) n

goal (1 subgoal):
 1. distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)
[PROOF STEP]
show "distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)
[PROOF STEP]
by (simp add: n_permutation_enum_correct2 subsetI)
[PROOF STATE]
proof (state)
this:
distinct xs \<Longrightarrow> n_permutations (set xs) n \<subseteq> set (n_permutation_enum xs n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_scospan_composable_\<bb>\<bb>[cat_ss_cs_intros]:
  assumes "g = \<bb>\<^sub>S\<^sub>S" and "f = \<bb>\<^sub>S\<^sub>S"
  shows "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g = \<bb>\<^sub>S\<^sub>S
f = \<bb>\<^sub>S\<^sub>S

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
by auto


[STATEMENT]
lemma WhileNoGuard':
  assumes P_I: "P \<subseteq> I"
  assumes deriv_body: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A"
  assumes I_Q: "I \<inter> -b \<subseteq> Q"
  assumes wf: "wf V"
  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b I V (Seq c Skip)) Q,A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P whileAnno b I V (Seq c Skip) Q,A
[PROOF STEP]
apply (rule While [OF P_I _ I_Q wf])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) Seq c Skip ({t. (t, \<sigma>) \<in> V} \<inter> I),A
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) Seq c Skip ({t. (t, \<sigma>) \<in> V} \<inter> I),A
[PROOF STEP]
apply (rule Seq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c (?R5 \<sigma>),A
 2. \<And>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?R5 \<sigma>) Skip ({t. (t, \<sigma>) \<in> V} \<inter> I),A
[PROOF STEP]
apply  (rule deriv_body [rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({t. (t, \<sigma>) \<in> V} \<inter> I) Skip ({t. (t, \<sigma>) \<in> V} \<inter> I),A
[PROOF STEP]
apply (rule hoaret.Skip)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma absn_dist_eta: "(Abs^^n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (Abs ^^ 0) (var_dist (rev [0..<0]) (liftn 0 t 0)) \<leftrightarrow> t
 2. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (Abs ^^ 0) (var_dist (rev [0..<0]) (liftn 0 t 0)) \<leftrightarrow> t
 2. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs ^^ 0) (var_dist (rev [0..<0]) (liftn 0 t 0)) \<leftrightarrow> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Abs ^^ 0) (var_dist (rev [0..<0]) (liftn 0 t 0)) \<leftrightarrow> t

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
let ?dist_range = "\<lambda>a k. var_dist (rev [a..<k]) (liftn k t 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
have append: "rev [0..<Suc n] = rev [1..<Suc n] @ [0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<Suc n] = rev [1..<Suc n] @ [0]
[PROOF STEP]
by (simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
rev [0..<Suc n] = rev [1..<Suc n] @ [0]

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
have dist_last: "?dist_range 0 (Suc n) = ?dist_range 1 (Suc n) \<degree> Var 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0) = var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0) \<degree> Var 0
[PROOF STEP]
unfolding append var_dist_append1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0) \<degree> Var 0 = var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0) \<degree> Var 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0) = var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0) \<degree> Var 0

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
have "\<not> free (?dist_range 1 (Suc n)) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
have "frees (?dist_range 1 (Suc n)) = frees (liftn (Suc n) t 0) \<union> {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) = frees (liftn (Suc n) t 0) \<union> {1..n}
[PROOF STEP]
unfolding var_dist_frees
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees (liftn (Suc n) t 0) \<union> set (rev [1..<Suc n]) = frees (liftn (Suc n) t 0) \<union> {1..n}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) = frees (liftn (Suc n) t 0) \<union> {1..n}

goal (1 subgoal):
 1. \<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) = frees (liftn (Suc n) t 0) \<union> {1..n}
[PROOF STEP]
have "0 \<notin> frees (?dist_range 1 (Suc n))"
[PROOF STATE]
proof (prove)
using this:
frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) = frees (liftn (Suc n) t 0) \<union> {1..n}

goal (1 subgoal):
 1. 0 \<notin> frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<notin> frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0))

goal (1 subgoal):
 1. \<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<notin> frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<notin> frees (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0))

goal (1 subgoal):
 1. \<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0
[PROOF STEP]
have "Abs (?dist_range 0 (Suc n)) \<rightarrow>\<^sub>\<eta> (?dist_range 1 (Suc n))[Var 0/0]"
[PROOF STATE]
proof (prove)
using this:
\<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0

goal (1 subgoal):
 1. Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<rightarrow>\<^sub>\<eta> var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0]
[PROOF STEP]
unfolding dist_last
[PROOF STATE]
proof (prove)
using this:
\<not> free (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)) 0

goal (1 subgoal):
 1. Abs (var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0) \<degree> Var 0) \<rightarrow>\<^sub>\<eta> var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0]
[PROOF STEP]
by (rule eta)
[PROOF STATE]
proof (state)
this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<rightarrow>\<^sub>\<eta> var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0]

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<rightarrow>\<^sub>\<eta> var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0]

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
have "... = var_dist (rev [0..<n]) ((liftn (Suc n) t 0)[Var 0/0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
have "\<forall>v\<in>set (rev [1..<Suc n]). 0 < v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>set (rev [1..<Suc n]). 0 < v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>set (rev [1..<Suc n]). 0 < v

goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>set (rev [1..<Suc n]). 0 < v

goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
have "rev [0..<n] = map (\<lambda>v. v - 1) (rev [1..<Suc n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<n] = map (\<lambda>v. v - 1) (rev [1..<Suc n])
[PROOF STEP]
by (induction n) simp_all
[PROOF STATE]
proof (state)
this:
rev [0..<n] = map (\<lambda>v. v - 1) (rev [1..<Suc n])

goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>set (rev [1..<Suc n]). 0 < v
rev [0..<n] = map (\<lambda>v. v - 1) (rev [1..<Suc n])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>set (rev [1..<Suc n]). 0 < v
rev [0..<n] = map (\<lambda>v. v - 1) (rev [1..<Suc n])

goal (1 subgoal):
 1. var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])
[PROOF STEP]
by (simp only: var_dist_subst_lt)
[PROOF STATE]
proof (state)
this:
var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
var_dist (rev [1..<Suc n]) (liftn (Suc n) t 0)[Var 0/0] = var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0])

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
have "... = ?dist_range 0 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0]) = var_dist (rev [0..<n]) (liftn n t 0)
[PROOF STEP]
using subst_liftn[of 0 n 0 t "Var 0"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> n + 0 \<and> 0 \<le> 0 \<Longrightarrow> liftn (Suc n) t 0[Var 0/0] = liftn n t 0

goal (1 subgoal):
 1. var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0]) = var_dist (rev [0..<n]) (liftn n t 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
var_dist (rev [0..<n]) (liftn (Suc n) t 0[Var 0/0]) = var_dist (rev [0..<n]) (liftn n t 0)

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<rightarrow>\<^sub>\<eta> var_dist (rev [0..<n]) (liftn n t 0)
[PROOF STEP]
have "Abs (?dist_range 0 (Suc n)) \<leftrightarrow> ?dist_range 0 n"
[PROOF STATE]
proof (prove)
using this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<rightarrow>\<^sub>\<eta> var_dist (rev [0..<n]) (liftn n t 0)

goal (1 subgoal):
 1. Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> var_dist (rev [0..<n]) (liftn n t 0)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> var_dist (rev [0..<n]) (liftn n t 0)

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> var_dist (rev [0..<n]) (liftn n t 0)
[PROOF STEP]
have "(Abs^^Suc n) (?dist_range 0 (Suc n)) \<leftrightarrow> (Abs^^n) (?dist_range 0 n)"
[PROOF STATE]
proof (prove)
using this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> var_dist (rev [0..<n]) (liftn n t 0)

goal (1 subgoal):
 1. (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0))
[PROOF STEP]
unfolding funpow_Suc_inside
[PROOF STATE]
proof (prove)
using this:
Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> var_dist (rev [0..<n]) (liftn n t 0)

goal (1 subgoal):
 1. (Abs ^^ n) (Abs (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0))) \<leftrightarrow> (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0))
[PROOF STEP]
by (rule absn_cong)
[PROOF STATE]
proof (state)
this:
(Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0))

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0))

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
from Suc.IH
[PROOF STATE]
proof (chain)
picking this:
(Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t
[PROOF STEP]
have "... \<leftrightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t

goal (1 subgoal):
 1. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t

goal (1 subgoal):
 1. \<And>n. (Abs ^^ n) (var_dist (rev [0..<n]) (liftn n t 0)) \<leftrightarrow> t \<Longrightarrow> (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t

goal (1 subgoal):
 1. (Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(Abs ^^ Suc n) (var_dist (rev [0..<Suc n]) (liftn (Suc n) t 0)) \<leftrightarrow> t

goal:
No subgoals!
[PROOF STEP]
qed