[STATEMENT]
lemma (in Corps) ring_n_distinct_prime_divisors:"distinct_pds K n P \<Longrightarrow>
       Ring (Sr K {x. x\<in>carrier K \<and> (\<forall>j\<le> n. 0 \<le> ((\<nu>\<^bsub> K (P j)\<^esub>) x))})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m) \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule Ring.Sr_ring, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (subst sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<subseteq> carrier K \<and> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<subseteq> carrier K
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rbrakk> \<Longrightarrow> x \<in> carrier K
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (simp add:Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) 1\<^sub>r
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) 1\<^sub>r
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp,
        simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}; y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x); y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y)\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x); y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y); aGroup K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = y in aGroup.ag_mOp_closed[of "K"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = x and y = "-\<^sub>a y" in aGroup.ag_pOp_closed[of "K"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rotate_tac -4, frule_tac a = j in forall_spec, assumption,
        rotate_tac -3,
        drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac v = "\<nu>\<^bsub>K (P j)\<^esub>" and x = x and y = "-\<^sub>a y" in amin_le_plus,
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a y)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (simp add:val_minus_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) x" and y = "(\<nu>\<^bsub>K (P j)\<^esub>) y" in amin_ge1[of "0"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y
 2. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y); 0 \<le> amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 3. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y); 0 \<le> amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule_tac j = "amin ((\<nu>\<^bsub>K (P j)\<^esub>) x) ((\<nu>\<^bsub>K (P j)\<^esub>) y)" and k = "(\<nu>\<^bsub>K (P j)\<^esub>) (x \<plusminus> -\<^sub>a y)" in ale_trans[of "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (simp add:Ring.ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply (rule allI, rule impI,
       cut_tac P = "P j" in representative_of_pd_valuation, simp,
       subst val_t2p [where v="\<nu>\<^bsub>K P j\<^esub>"], assumption+,
       rule aadd_two_pos, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_1I: "execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> Predicate.eval (exec_1 P t \<sigma>) (ta, \<sigma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> pred.eval (exec_1 P t \<sigma>) (ta, \<sigma>')
[PROOF STEP]
by(erule execute.exec_1.cases)(simp add: exec_1_def exec_def)


[STATEMENT]
lemma acceptI[intro?]: "\<lbrakk>is_run r; w = L o r\<rbrakk> \<Longrightarrow> accept w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_run r; w = L \<circ> r\<rbrakk> \<Longrightarrow> accept w
[PROOF STEP]
by (auto simp: accept_def)


[STATEMENT]
lemma no_black_refs_eq_imp:
  "eq_imp (\<lambda>r'. (\<lambda>s. (\<Union>p. WL p s)) \<^bold>\<otimes> sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')))
          no_black_refs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (\<Union>p. WL p s, sys_fM s, map_option obj_mark (sys_heap s r'))) no_black_refs
[PROOF STEP]
apply (clarsimp simp add: eq_imp_def no_black_refs_def black_def grey_def all_conj_distrib fun_eq_iff set_eq_iff split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
[PROOF STEP]
apply (subgoal_tac "\<forall>x. marked x s \<longleftrightarrow> marked x s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
 2. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (drule_tac x=x in spec)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>sys_fM s = sys_fM s'; (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (auto split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma HC_contrapos_np:
  "\<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
by (meson HC_intros(12) HC_intros(13) HC_mono MP sup_ge2  HC_contrapos_nn[of \<Gamma> F "Not G"])


[STATEMENT]
lemma cmfi:"m O f^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O f\<inverse> \<subseteq> b
[PROOF STEP]
apply (r_compose r1:m r2:f r3:b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u. \<lbrakk>x \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; k \<parallel> y; y \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1)


[STATEMENT]
lemma (in arelations) cmd:"m O d \<subseteq> s \<union> ov \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O d \<subseteq> s \<union> ov \<union> d
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
fix x::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
assume a:"x \<in> m O d"
[PROOF STATE]
proof (state)
this:
x \<in> m O d

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> m O d
[PROOF STEP]
obtain p q z where x:"x =(p,q)" and 1:"(p,z) \<in> m" and 2:"(z,q) \<in> d"
[PROOF STATE]
proof (prove)
using this:
x \<in> m O d

goal (1 subgoal):
 1. (\<And>p q z. \<lbrakk>x = (p, q); (p, z) \<in> m; (z, q) \<in> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> d

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> d
[PROOF STEP]
obtain k l u v  where pz:"p\<parallel>z" and kq:"k\<parallel>q" and kl:"k\<parallel>l" and lz:"l\<parallel>z" and zu:"z\<parallel>u" and uv:"u\<parallel>v" and qv:"q\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> d

goal (1 subgoal):
 1. (\<And>k l u v. \<lbrakk>p \<parallel> z; k \<parallel> q; k \<parallel> l; l \<parallel> z; z \<parallel> u; u \<parallel> v; q \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using m d
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> d
((?p, ?q) \<in> m) = ?p \<parallel> ?q
((?p, ?q) \<in> d) = (\<exists>k l u v. k \<parallel> l \<and> l \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. (\<And>k l u v. \<lbrakk>p \<parallel> z; k \<parallel> q; k \<parallel> l; l \<parallel> z; z \<parallel> u; u \<parallel> v; q \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> z
k \<parallel> q
k \<parallel> l
l \<parallel> z
z \<parallel> u
u \<parallel> v
q \<parallel> v

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
obtain k' where kpp:"k'\<parallel>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. k' \<parallel> p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3 meets_wd pz
[PROOF STATE]
proof (prove)
using this:
\<I> ?p \<Longrightarrow> \<exists>q r. q \<parallel> ?p \<and> ?p \<parallel> r
?p \<parallel> ?q \<Longrightarrow> \<I> ?p \<and> \<I> ?q
p \<parallel> z

goal (1 subgoal):
 1. (\<And>k'. k' \<parallel> p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<parallel> p

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from pz zu uv
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> z
z \<parallel> u
u \<parallel> v
[PROOF STEP]
obtain zu where pzu:"p\<parallel>zu" and zuv:"zu\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> z
z \<parallel> u
u \<parallel> v

goal (1 subgoal):
 1. (\<And>zu. \<lbrakk>p \<parallel> zu; zu \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
p \<parallel> z
z \<parallel> u
u \<parallel> v
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>zu. \<lbrakk>p \<parallel> zu; zu \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> zu
zu \<parallel> v

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from kpp kq
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> p
k \<parallel> q
[PROOF STEP]
have "k'\<parallel>q \<oplus> ((\<exists>t. k'\<parallel>t \<and> t\<parallel>q) \<oplus> (\<exists>t. k\<parallel>t \<and> t\<parallel>p))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> p
k \<parallel> q

goal (1 subgoal):
 1. k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> p
k \<parallel> q
\<lbrakk>?p \<parallel> ?q; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?p \<parallel> ?s \<oplus> ((\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?s) \<oplus> (\<exists>t. ?r \<parallel> t \<and> t \<parallel> ?q))

goal (1 subgoal):
 1. k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
have "(?A\<and>\<not>?B\<and>\<not>?C)\<or>(\<not>?A\<and>?B\<and>\<not>?C)\<or>(\<not>?A\<and>\<not>?B\<and>?C)"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))

goal (1 subgoal):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
using local.meets_atrans xor_distr_L[of ?A ?B ?C]
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p))
\<lbrakk>?p \<parallel> ?q; ?q \<parallel> ?r\<rbrakk> \<Longrightarrow> \<not> ?p \<parallel> ?r
k' \<parallel> q \<oplus> ((\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)) = (k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)) \<or> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. \<And>x. x \<in> m O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus "x \<in> s \<union> ov \<union> d"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<or> \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 3. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 3. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
assume "(?A\<and>\<not>?B\<and>\<not>?C)"
[PROOF STATE]
proof (state)
this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)

goal (3 subgoals):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 3. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
have "?A"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. k' \<parallel> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' \<parallel> q

goal (3 subgoals):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 3. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q
[PROOF STEP]
have "(p,q) \<in> s"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q

goal (1 subgoal):
 1. (p, q) \<in> s
[PROOF STEP]
using  s qv kpp pzu zuv
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)
q \<parallel> v
k' \<parallel> p
p \<parallel> zu
zu \<parallel> v

goal (1 subgoal):
 1. (p, q) \<in> s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> s

goal (3 subgoals):
 1. k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 3. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s
x = (p, q)

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> ov \<union> d

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
assume "(\<not>?A\<and>?B\<and>\<not>?C)"
[PROOF STATE]
proof (state)
this:
\<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
have "?B"
[PROOF STATE]
proof (prove)
using this:
\<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. \<exists>t. k' \<parallel> t \<and> t \<parallel> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> q

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> q
[PROOF STEP]
obtain t where kpt:"k'\<parallel>t" and tq:"t\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> q

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>k' \<parallel> t; t \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<parallel> t
t \<parallel> q

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k' \<parallel> t
t \<parallel> q

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from kq kl tq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q
k \<parallel> l
t \<parallel> q
[PROOF STEP]
have "t\<parallel>l"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
k \<parallel> l
t \<parallel> q

goal (1 subgoal):
 1. t \<parallel> l
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
k \<parallel> l
t \<parallel> q
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. t \<parallel> l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<parallel> l

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<parallel> l

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from lz pz pzu
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
p \<parallel> z
p \<parallel> zu
[PROOF STEP]
have "l\<parallel>zu"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
p \<parallel> z
p \<parallel> zu

goal (1 subgoal):
 1. l \<parallel> zu
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
p \<parallel> z
p \<parallel> zu
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. l \<parallel> zu
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<parallel> zu

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> t
t \<parallel> q
t \<parallel> l
l \<parallel> zu
[PROOF STEP]
have "(p,q) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> t
t \<parallel> q
t \<parallel> l
l \<parallel> zu

goal (1 subgoal):
 1. (p, q) \<in> ov
[PROOF STEP]
using ov kpp qv pzu zuv
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> t
t \<parallel> q
t \<parallel> l
l \<parallel> zu
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)
k' \<parallel> p
q \<parallel> v
p \<parallel> zu
zu \<parallel> v

goal (1 subgoal):
 1. (p, q) \<in> ov
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> ov

goal (2 subgoals):
 1. \<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 2. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov
x = (p, q)

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> ov \<union> d

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> k' \<parallel> q \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
assume "(\<not>?A\<and>\<not>?B\<and>?C)"
[PROOF STATE]
proof (state)
this:
\<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
have "?C"
[PROOF STATE]
proof (prove)
using this:
\<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p)

goal (1 subgoal):
 1. \<exists>t. k \<parallel> t \<and> t \<parallel> p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. k \<parallel> t \<and> t \<parallel> p

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. k \<parallel> t \<and> t \<parallel> p
[PROOF STEP]
obtain t where kt:"k\<parallel>t" and tp:"t\<parallel>p"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. k \<parallel> t \<and> t \<parallel> p

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>k \<parallel> t; t \<parallel> p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<parallel> t
t \<parallel> p

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
with kq pzu zuv qv
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q
p \<parallel> zu
zu \<parallel> v
q \<parallel> v
k \<parallel> t
t \<parallel> p
[PROOF STEP]
have "(p,q)\<in>d"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
p \<parallel> zu
zu \<parallel> v
q \<parallel> v
k \<parallel> t
t \<parallel> p

goal (1 subgoal):
 1. (p, q) \<in> d
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
p \<parallel> zu
zu \<parallel> v
q \<parallel> v
k \<parallel> t
t \<parallel> p
((?p, ?q) \<in> d) = (\<exists>k l u v. k \<parallel> l \<and> l \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. (p, q) \<in> d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> d

goal (1 subgoal):
 1. \<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> d

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> d
x = (p, q)

goal (1 subgoal):
 1. x \<in> s \<union> ov \<union> d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> ov \<union> d

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> k' \<parallel> q \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> ov \<union> d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdsi:"d O s^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using csdi
[PROOF STATE]
proof (prove)
using this:
s O d\<inverse> \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. d O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma pcorresI2[intro]:
  fixes A::"'a prog" and B::"'b prog"
  assumes withG: "\<And>Q s. \<lbrakk> unitary Q; G s \<rbrakk> \<Longrightarrow> wp A Q (\<phi> s)= wp B (Q o \<phi>) s"
      and wA: "well_def A"
      and wB: "well_def B"
  shows "pcorres \<phi> G A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G A B
[PROOF STEP]
proof(rule pcorresI, rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
fix Q::"'a \<Rightarrow> real" and s::'b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
hence uQ\<phi>: "unitary (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. unitary (Q \<circ> \<phi>)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
show "(\<guillemotleft>G\<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft>G\<guillemotright> && wp B (Q \<circ> \<phi>)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
proof(cases "G s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
note this
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
from well_def_wp_healthy[OF wA] uQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp A)
unitary Q
[PROOF STEP]
have "0 \<le> wp A Q (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp A)
unitary Q

goal (1 subgoal):
 1. 0 \<le> wp A Q (\<phi> s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> wp A Q (\<phi> s)

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> wp A Q (\<phi> s)

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
from well_def_wp_healthy[OF wB] uQ\<phi>
[PROOF STATE]
proof (chain)
picking this:
healthy (wp B)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have "0 \<le> wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp B)
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. 0 \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> wp B (Q \<circ> \<phi>) s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
G s
0 \<le> wp A Q (\<phi> s)
0 \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
G s
0 \<le> wp A Q (\<phi> s)
0 \<le> wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
using uQ
[PROOF STATE]
proof (prove)
using this:
G s
0 \<le> wp A Q (\<phi> s)
0 \<le> wp B (Q \<circ> \<phi>) s
unitary Q

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
by(simp add:exp_conj_def withG)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
note this
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
from well_def_wp_healthy[OF wA] uQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp A)
unitary Q
[PROOF STEP]
have "wp A Q (\<phi> s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
healthy (wp A)
unitary Q

goal (1 subgoal):
 1. wp A Q (\<phi> s) \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) \<le> 1

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) \<le> 1

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
from well_def_wp_healthy[OF wB] uQ\<phi>
[PROOF STATE]
proof (chain)
picking this:
healthy (wp B)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have "wp B (Q o \<phi>) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
healthy (wp B)
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp B (Q \<circ> \<phi>) s \<le> 1
[PROOF STEP]
by(blast dest!:healthy_bounded_byD intro:sound_nneg)
[PROOF STATE]
proof (state)
this:
wp B (Q \<circ> \<phi>) s \<le> 1

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> G s
wp A Q (\<phi> s) \<le> 1
wp B (Q \<circ> \<phi>) s \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> G s
wp A Q (\<phi> s) \<le> 1
wp B (Q \<circ> \<phi>) s \<le> 1

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DNI_CoP1: "Fr_1b \<F> \<Longrightarrow> DNI \<^bold>\<not> \<Longrightarrow> CoP1 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1b \<F>; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
using CoP1_def2 CoPw
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> = (CoPw ?\<eta> \<and> DNI ?\<eta>)
Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1b \<F>; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma two_not_one: "2 \<noteq> (1::'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2::'a) \<noteq> (1::'a)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
assume "2 = (1::'a)"
[PROOF STATE]
proof (state)
this:
(2::'a) = (1::'a)

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "2 - 1 = 1 - (1::'a)"
[PROOF STATE]
proof (prove)
using this:
(2::'a) = (1::'a)

goal (1 subgoal):
 1. (2::'a) - (1::'a) = (1::'a) - (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(2::'a) - (1::'a) = (1::'a) - (1::'a)

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "1 = (0::'a)"
[PROOF STATE]
proof (prove)
using this:
(2::'a) - (1::'a) = (1::'a) - (1::'a)

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

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using one_neq_zero
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)
(1::'a) \<noteq> (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_complement_partition_finite [simp]:
  "finite (UNIV :: 'a set) \<Longrightarrow> infinite_complement_partition = (UNIV :: 'a set set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> infinite_complement_partition = UNIV
[PROOF STEP]
by(auto intro: finite_subset finite_complement_partition)


[STATEMENT]
lemma tkt_thread_eq:
    assumes R: "A.reachable (c,n,ts)"
    assumes A: "t<N" "has_ticket (ts t) k"
    shows "tkt_thread ts k = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tkt_thread ts k = t
[PROOF STEP]
using has_ticket_unique[OF R]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t

goal (1 subgoal):
 1. tkt_thread ts k = t
[PROOF STEP]
unfolding tkt_thread_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t

goal (1 subgoal):
 1. (THE t. t < N \<and> has_ticket (ts t) k) = t
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t
t < N
has_ticket (ts t) k

goal (1 subgoal):
 1. (THE t. t < N \<and> has_ticket (ts t) k) = t
[PROOF STEP]
by auto


[STATEMENT]
lemma linepath_translate_right: "linepath (a + c) (b + c) = (\<lambda>x. x + c) \<circ> linepath a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linepath (a + c) (b + c) = (\<lambda>x. x + c) \<circ> linepath a b
[PROOF STEP]
by (auto simp: fun_eq_iff linepath_def algebra_simps)


[STATEMENT]
lemma ent_ex_inst2: "\<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
using ent_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P \<Longrightarrow>\<^sub>A ?Q; ?Q \<Longrightarrow>\<^sub>A ?R\<rbrakk> \<Longrightarrow> ?P \<Longrightarrow>\<^sub>A ?R

goal (1 subgoal):
 1. \<exists>\<^sub>Ax y. P x y \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P x y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
by blast


[STATEMENT]
lemma diamond_associative:
  "|x * y>z = |x>(y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y > z = | x > (y * z)
[PROOF STEP]
by (simp add: diamond_def mult_assoc)


[STATEMENT]
lemma has_branch: "\<exists>b. branch b T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. branch b T
[PROOF STEP]
proof (induction T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
case (Leaf)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
have "branch [] Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch [] Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch [] Leaf

goal (2 subgoals):
 1. \<exists>b. branch b Leaf
 2. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch [] Leaf
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch [] Leaf

goal (1 subgoal):
 1. \<exists>b. branch b Leaf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b Leaf

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2
[PROOF STEP]
obtain b where "branch b T\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>b. branch b T\<^sub>1
\<exists>b. branch b T\<^sub>2

goal (1 subgoal):
 1. (\<And>b. branch b T\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch b T\<^sub>1

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b T\<^sub>1
[PROOF STEP]
have "branch (Left#b) (Branching T\<^sub>1 T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
branch b T\<^sub>1

goal (1 subgoal):
 1. branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2. \<lbrakk>\<exists>b. branch b T1; \<exists>b. branch b T2\<rbrakk> \<Longrightarrow> \<exists>b. branch b (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch (Left # b) (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<exists>b. branch b (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. branch b (Branching T\<^sub>1 T\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_qAFresh_or_in_ordLess_var:
assumes Var: "|V| <o |UNIV :: 'var set|" and "|XS| <o |UNIV :: 'var set|" and "\<forall> X \<in> XS. qGood X"
shows "|{x| x X. (x \<in> V \<or> (X \<in> XS \<and> \<not> qAFresh xs x X))}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
define J and K where "J \<equiv> {x| x X. (x \<in> V \<or> (X \<in> XS \<and> \<not> qAFresh xs x X))}"
  and "K \<equiv> {x| x X. X \<in> XS \<and> \<not> qAFresh xs x X}"
[PROOF STATE]
proof (state)
this:
J \<equiv> {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}
K \<equiv> {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
have "J \<subseteq> K \<union> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> K \<union> V
[PROOF STEP]
unfolding J_def K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)} \<subseteq> {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X} \<union> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
J \<subseteq> K \<union> V

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
hence "|J| \<le>o |K \<union> V|"
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> K \<union> V

goal (1 subgoal):
 1. |J| \<le>o |K \<union> V|
[PROOF STEP]
using card_of_mono1
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> K \<union> V
?A \<subseteq> ?B \<Longrightarrow> |?A| \<le>o |?B|

goal (1 subgoal):
 1. |J| \<le>o |K \<union> V|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
have "|K| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using assms non_qAFresh_ordLess_var
[PROOF STATE]
proof (prove)
using this:
|V| <o |UNIV|
|XS| <o |UNIV|
Ball XS qGood
\<lbrakk>Ball ?XS qGood; |?XS| <o |UNIV|\<rbrakk> \<Longrightarrow> |{uu_. \<exists>x X. uu_ = x \<and> X \<in> ?XS \<and> \<not> qAFresh ?xs x X}| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
hence "|K \<union> V| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|

goal (1 subgoal):
 1. |K \<union> V| <o |UNIV|
[PROOF STEP]
using Var var_infinite_INNER card_of_Un_ordLess_infinite
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|
|V| <o |UNIV|
infinite UNIV
\<lbrakk>infinite ?C; |?A| <o |?C|; |?B| <o |?C|\<rbrakk> \<Longrightarrow> |?A \<union> ?B| <o |?C|

goal (1 subgoal):
 1. |K \<union> V| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|K \<union> V| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
|K \<union> V| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|
[PROOF STEP]
have "|J| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|

goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
using ordLeq_ordLess_trans
[PROOF STATE]
proof (prove)
using this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|
\<lbrakk>?r \<le>o ?r'; ?r' <o ?r''\<rbrakk> \<Longrightarrow> ?r <o ?r''

goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
|J| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
|J| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
unfolding J_def
[PROOF STATE]
proof (prove)
using this:
|{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
|{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_is_arrE:
  assumes "gf : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd"
  obtains g f a b c d
    where "gf = [g, f]\<^sub>\<circ>"
      and "ab = [a, b]\<^sub>\<circ>"
      and "cd = [c, d]\<^sub>\<circ>"
      and "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c"
      and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from dg_prod_is_arrD[OF assms[unfolded dg_prod_2_def]]
[PROOF STATE]
proof (chain)
picking this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>
[PROOF STEP]
have [simp]: "vsv gf" "\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>" "vsv ab" "\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>" "vsv cd" "\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>"
    and gf_app:
      "\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> : ab\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = 0 then \<AA> else \<BB>\<^esub> cd\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>

goal (1 subgoal):
 1. ((vsv gf &&& \<D>\<^sub>\<circ> gf = 2\<^sub>\<nat> &&& vsv ab) &&& \<D>\<^sub>\<circ> ab = 2\<^sub>\<nat> &&& vsv cd &&& \<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>) &&& (\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> : ab\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>i\<rparr>)
[PROOF STEP]
by (auto simp: two)
[PROOF STATE]
proof (state)
this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "gf = [vpfst gf, vpsnd gf]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "ab = [vpfst ab, vpsnd ab]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "cd = [vpfst cd, vpsnd cd]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
have "vpfst gf : vpfst ab \<mapsto>\<^bsub>\<AA>\<^esub> vpfst cd"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
have "vpsnd gf : vpsnd ab \<mapsto>\<^bsub>\<BB>\<^esub> vpsnd cd"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
\<lbrakk>gf = [?g, ?f]\<^sub>\<circ>; ab = [?a, ?b]\<^sub>\<circ>; cd = [?c, ?d]\<^sub>\<circ>; ?g : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?c; ?f : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?d\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<oo>_Shuffle[simp]:
  "\<oo> (Shuffle r s) = (\<oo> r \<and> \<oo> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Shuffle r s) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
unfolding Shuffle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times_Plus (ShuffleLR r s)) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
by simp