[STATEMENT]
lemma existence_safe_trans:
assumes Pst_in: "Ps \<noteq> []" "set Ps \<subseteq> progs" "t \<in> tests" and
 o0: "o\<^sub>0 \<in> out (Ps!0) t" and
 des: "\<forall>n < (length Ps) - 1. deselect (Ps!n) o\<^sub>0 (Ps!(Suc n))"
shows "\<exists>o\<^sub>n \<in> out (last Ps) t. equiv_out o\<^sub>0 o\<^sub>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o\<^sub>0 o\<^sub>n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. \<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o\<^sub>0 o\<^sub>n
[PROOF STEP]
proof(induct "length Ps" arbitrary: Ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ps. \<lbrakk>0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
 2. \<And>x Ps. \<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (2 subgoals):
 1. \<And>Ps. \<lbrakk>0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
 2. \<And>x Ps. \<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
with Pst_in
[PROOF STATE]
proof (chain)
picking this:
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
0 = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
0 = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. \<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a

goal (1 subgoal):
 1. \<And>x Ps. \<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Ps. \<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = length ?Ps; ?Ps \<noteq> []; set ?Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (?Ps ! 0) t; \<forall>n<length ?Ps - 1. deselect (?Ps ! n) o\<^sub>0 (?Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last ?Ps) t) (equiv_out o\<^sub>0)
Suc x = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. \<And>x Ps. \<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = length ?Ps; ?Ps \<noteq> []; set ?Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (?Ps ! 0) t; \<forall>n<length ?Ps - 1. deselect (?Ps ! n) o\<^sub>0 (?Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last ?Ps) t) (equiv_out o\<^sub>0)
Suc x = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = length ?Ps; ?Ps \<noteq> []; set ?Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (?Ps ! 0) t; \<forall>n<length ?Ps - 1. deselect (?Ps ! n) o\<^sub>0 (?Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last ?Ps) t) (equiv_out o\<^sub>0)
Suc x = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
proof(induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>Ps. \<lbrakk>0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc 0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
 2. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
case z: 0
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 = length ?Ps; ?Ps \<noteq> []; set ?Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (?Ps ! 0) t; \<forall>n<length ?Ps - 1. deselect (?Ps ! n) o\<^sub>0 (?Ps ! Suc n)\<rbrakk> \<Longrightarrow> \<exists>a\<in>out (last ?Ps) t. equiv_out o\<^sub>0 a
Suc 0 = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (2 subgoals):
 1. \<lbrakk>\<And>Ps. \<lbrakk>0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc 0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
 2. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
from z.prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
Suc 0 = length Ps
Ps \<noteq> []
[PROOF STEP]
have "Ps ! (length Ps - 2) = last Ps"
[PROOF STATE]
proof (prove)
using this:
Suc 0 = length Ps
Ps \<noteq> []

goal (1 subgoal):
 1. Ps ! (length Ps - 2) = last Ps
[PROOF STEP]
by (simp add: last_conv_nth numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
Ps ! (length Ps - 2) = last Ps

goal (2 subgoals):
 1. \<lbrakk>\<And>Ps. \<lbrakk>0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc 0 = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
 2. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
with equiv_out_refl z.prems(2,6)
[PROOF STATE]
proof (chain)
picking this:
equiv_out ?a ?a
Suc 0 = length Ps
o\<^sub>0 \<in> out (Ps ! 0) t
Ps ! (length Ps - 2) = last Ps
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
equiv_out ?a ?a
Suc 0 = length Ps
o\<^sub>0 \<in> out (Ps ! 0) t
Ps ! (length Ps - 2) = last Ps

goal (1 subgoal):
 1. \<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
case Suc':(Suc x')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>Ps. \<lbrakk>x' = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> \<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a; Suc x' = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> \<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a
\<lbrakk>Suc x' = length ?Ps; ?Ps \<noteq> []; set ?Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (?Ps ! 0) t; \<forall>n<length ?Ps - 1. deselect (?Ps ! n) o\<^sub>0 (?Ps ! Suc n)\<rbrakk> \<Longrightarrow> \<exists>a\<in>out (last ?Ps) t. equiv_out o\<^sub>0 a
Suc (Suc x') = length Ps
Ps \<noteq> []
set Ps \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (Ps ! 0) t
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
let ?Ps = "take (Suc x') Ps"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have len': "Suc x' = length (take (Suc x') Ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc x' = length (take (Suc x') Ps)
[PROOF STEP]
using Suc'.prems(2)
[PROOF STATE]
proof (prove)
using this:
Suc (Suc x') = length Ps

goal (1 subgoal):
 1. Suc x' = length (take (Suc x') Ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc x' = length (take (Suc x') Ps)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc x' = length (take (Suc x') Ps)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have nmt': "take (Suc x') Ps \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc x') Ps \<noteq> []
[PROOF STEP]
using len'
[PROOF STATE]
proof (prove)
using this:
Suc x' = length (take (Suc x') Ps)

goal (1 subgoal):
 1. take (Suc x') Ps \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (Suc x') Ps \<noteq> []

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
take (Suc x') Ps \<noteq> []

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have sub': "set (take (Suc x') Ps) \<subseteq> progs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (take (Suc x') Ps) \<subseteq> progs
[PROOF STEP]
using Suc.prems(2)
[PROOF STATE]
proof (prove)
using this:
set Ps \<subseteq> progs

goal (1 subgoal):
 1. set (take (Suc x') Ps) \<subseteq> progs
[PROOF STEP]
by (meson order_trans set_take_subset)
[PROOF STATE]
proof (state)
this:
set (take (Suc x') Ps) \<subseteq> progs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (take (Suc x') Ps) \<subseteq> progs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have "t \<in> tests"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> tests
[PROOF STEP]
using Pst_in(3)
[PROOF STATE]
proof (prove)
using this:
t \<in> tests

goal (1 subgoal):
 1. t \<in> tests
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<in> tests

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<in> tests

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have "o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t
[PROOF STEP]
using Suc.prems(4)
[PROOF STATE]
proof (prove)
using this:
o\<^sub>0 \<in> out (Ps ! 0) t

goal (1 subgoal):
 1. o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have "\<forall>n<length (take (Suc x') Ps) - 1.
     deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n<length (take (Suc x') Ps) - 1. deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! Suc n)
[PROOF STEP]
using Suc.prems(5) len'
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)
Suc x' = length (take (Suc x') Ps)

goal (1 subgoal):
 1. \<forall>n<length (take (Suc x') Ps) - 1. deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n<length (take (Suc x') Ps) - 1. deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! Suc n)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc x' = length (take (Suc x') Ps)
take (Suc x') Ps \<noteq> []
set (take (Suc x') Ps) \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t
\<forall>n<length (take (Suc x') Ps) - 1. deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! Suc n)
[PROOF STEP]
have "\<exists>o'\<in>out (last ?Ps) t. equiv_out o\<^sub>0 o'"
[PROOF STATE]
proof (prove)
using this:
Suc x' = length (take (Suc x') Ps)
take (Suc x') Ps \<noteq> []
set (take (Suc x') Ps) \<subseteq> progs
t \<in> tests
o\<^sub>0 \<in> out (take (Suc x') Ps ! 0) t
\<forall>n<length (take (Suc x') Ps) - 1. deselect (take (Suc x') Ps ! n) o\<^sub>0 (take (Suc x') Ps ! Suc n)

goal (1 subgoal):
 1. \<exists>o'\<in>out (last (take (Suc x') Ps)) t. equiv_out o\<^sub>0 o'
[PROOF STEP]
by(rule Suc'.prems(1)[of ?Ps])
[PROOF STATE]
proof (state)
this:
\<exists>o'\<in>out (last (take (Suc x') Ps)) t. equiv_out o\<^sub>0 o'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>o'\<in>out (last (take (Suc x') Ps)) t. equiv_out o\<^sub>0 o'
[PROOF STEP]
obtain o' where o': "o' \<in> out (last ?Ps) t" and eo: "equiv_out o\<^sub>0 o'"
[PROOF STATE]
proof (prove)
using this:
\<exists>o'\<in>out (last (take (Suc x') Ps)) t. equiv_out o\<^sub>0 o'

goal (1 subgoal):
 1. (\<And>o'. \<lbrakk>o' \<in> out (last (take (Suc x') Ps)) t; equiv_out o\<^sub>0 o'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarify
[PROOF STATE]
proof (state)
this:
o' \<in> out (last (take (Suc x') Ps)) t
equiv_out o\<^sub>0 o'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
from Suc.prems(1) Suc'.prems(2) len' nmt'
[PROOF STATE]
proof (chain)
picking this:
Ps \<noteq> []
Suc (Suc x') = length Ps
Suc x' = length (take (Suc x') Ps)
take (Suc x') Ps \<noteq> []
[PROOF STEP]
have "last (take (Suc x') Ps) = Ps!x'" "last Ps = Ps!(Suc x')"
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
Suc (Suc x') = length Ps
Suc x' = length (take (Suc x') Ps)
take (Suc x') Ps \<noteq> []

goal (1 subgoal):
 1. last (take (Suc x') Ps) = Ps ! x' &&& last Ps = Ps ! Suc x'
[PROOF STEP]
by (metis diff_Suc_1 last_conv_nth lessI nth_take)+
[PROOF STATE]
proof (state)
this:
last (take (Suc x') Ps) = Ps ! x'
last Ps = Ps ! Suc x'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last (take (Suc x') Ps) = Ps ! x'
last Ps = Ps ! Suc x'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have "x' < length Ps - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' < length Ps - 1
[PROOF STEP]
using Suc'.prems(2)
[PROOF STATE]
proof (prove)
using this:
Suc (Suc x') = length Ps

goal (1 subgoal):
 1. x' < length Ps - 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
x' < length Ps - 1

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last (take (Suc x') Ps) = Ps ! x'
last Ps = Ps ! Suc x'
x' < length Ps - 1
[PROOF STEP]
have des':"deselect (last (take (Suc x') Ps)) o\<^sub>0 (last Ps)"
[PROOF STATE]
proof (prove)
using this:
last (take (Suc x') Ps) = Ps ! x'
last Ps = Ps ! Suc x'
x' < length Ps - 1

goal (1 subgoal):
 1. deselect (last (take (Suc x') Ps)) o\<^sub>0 (last Ps)
[PROOF STEP]
using Suc.prems(5)
[PROOF STATE]
proof (prove)
using this:
last (take (Suc x') Ps) = Ps ! x'
last Ps = Ps ! Suc x'
x' < length Ps - 1
\<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)

goal (1 subgoal):
 1. deselect (last (take (Suc x') Ps)) o\<^sub>0 (last Ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deselect (last (take (Suc x') Ps)) o\<^sub>0 (last Ps)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
from Suc.prems(1,2) sub' nmt' last_in_set
[PROOF STATE]
proof (chain)
picking this:
Ps \<noteq> []
set Ps \<subseteq> progs
set (take (Suc x') Ps) \<subseteq> progs
take (Suc x') Ps \<noteq> []
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as
[PROOF STEP]
have Ps_in: "last (take (Suc x') Ps) \<in> progs" "last Ps \<in> progs"
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
set Ps \<subseteq> progs
set (take (Suc x') Ps) \<subseteq> progs
take (Suc x') Ps \<noteq> []
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

goal (1 subgoal):
 1. last (take (Suc x') Ps) \<in> progs &&& last Ps \<in> progs
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
last (take (Suc x') Ps) \<in> progs
last Ps \<in> progs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
have "\<exists>o\<^sub>n \<in> out (last Ps) t. equiv_out o' o\<^sub>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o' o\<^sub>n
[PROOF STEP]
by(rule existence_safe[where P="last (take (Suc x') Ps)" and P'="last Ps" and t=t,
                    OF Ps_in Pst_in(3) o' equiv_out_deselect[OF eo des']])
[PROOF STATE]
proof (state)
this:
\<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o' o\<^sub>n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o' o\<^sub>n
[PROOF STEP]
obtain o\<^sub>n where oN: "o\<^sub>n \<in> out (last Ps) t" and eo': "equiv_out o' o\<^sub>n"
[PROOF STATE]
proof (prove)
using this:
\<exists>o\<^sub>n\<in>out (last Ps) t. equiv_out o' o\<^sub>n

goal (1 subgoal):
 1. (\<And>o\<^sub>n. \<lbrakk>o\<^sub>n \<in> out (last Ps) t; equiv_out o' o\<^sub>n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarify
[PROOF STATE]
proof (state)
this:
o\<^sub>n \<in> out (last Ps) t
equiv_out o' o\<^sub>n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
o\<^sub>n \<in> out (last Ps) t
equiv_out o' o\<^sub>n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
from eo eo'
[PROOF STATE]
proof (chain)
picking this:
equiv_out o\<^sub>0 o'
equiv_out o' o\<^sub>n
[PROOF STEP]
have "equiv_out o\<^sub>0 o\<^sub>n"
[PROOF STATE]
proof (prove)
using this:
equiv_out o\<^sub>0 o'
equiv_out o' o\<^sub>n

goal (1 subgoal):
 1. equiv_out o\<^sub>0 o\<^sub>n
[PROOF STEP]
by(rule equiv_out_trans)
[PROOF STATE]
proof (state)
this:
equiv_out o\<^sub>0 o\<^sub>n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<And>Ps. \<lbrakk>x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); \<And>Ps. \<lbrakk>Suc x = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0); Suc (Suc x) = length Ps; Ps \<noteq> []; set Ps \<subseteq> progs; t \<in> tests; o\<^sub>0 \<in> out (Ps ! 0) t; \<forall>n<length Ps - 1. deselect (Ps ! n) o\<^sub>0 (Ps ! Suc n)\<rbrakk> \<Longrightarrow> Bex (out (last Ps) t) (equiv_out o\<^sub>0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
o\<^sub>n \<in> out (last Ps) t
equiv_out o' o\<^sub>n
equiv_out o\<^sub>0 o\<^sub>n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
o\<^sub>n \<in> out (last Ps) t
equiv_out o' o\<^sub>n
equiv_out o\<^sub>0 o\<^sub>n

goal (1 subgoal):
 1. \<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>out (last Ps) t. equiv_out o\<^sub>0 a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Bex (out (last Ps) t) (equiv_out o\<^sub>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cond_seq_left_distr:
  "out\<alpha> \<sharp> b \<Longrightarrow> ((P \<triangleleft> b \<triangleright> Q) ;; R) = ((P ;; R) \<triangleleft> b \<triangleright> (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> b \<Longrightarrow> (P \<triangleleft> b \<triangleright> Q) ;; R = P ;; R \<triangleleft> b \<triangleright> Q ;; R
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma cond_seq_right_distr:
  "in\<alpha> \<sharp> b \<Longrightarrow> (P ;; (Q \<triangleleft> b \<triangleright> R)) = ((P ;; Q) \<triangleleft> b \<triangleright> (P ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in\<alpha> \<sharp> b \<Longrightarrow> P ;; (Q \<triangleleft> b \<triangleright> R) = P ;; Q \<triangleleft> b \<triangleright> P ;; R
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma rcond_rassume_expand: "P \<triangleleft> b \<triangleright>\<^sub>r Q = ([b]\<^sup>\<top> ;; P) \<sqinter> ([(\<not> b)]\<^sup>\<top> ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<triangleleft> b \<triangleright>\<^sub>r Q = (?[b] ;; P) \<sqinter> (?[\<not> b] ;; Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem precond_equiv:
  "P = (P ;; true) \<longleftrightarrow> (out\<alpha> \<sharp> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P = P ;; true) = (out\<alpha> \<sharp> P)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem postcond_equiv:
  "P = (true ;; P) \<longleftrightarrow> (in\<alpha> \<sharp> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P = true ;; P) = (in\<alpha> \<sharp> P)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma precond_right_unit: "out\<alpha> \<sharp> p \<Longrightarrow> (p ;; true) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> p \<Longrightarrow> p ;; true = p
[PROOF STEP]
by (metis precond_equiv)


[STATEMENT]
lemma postcond_left_unit: "in\<alpha> \<sharp> p \<Longrightarrow> (true ;; p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in\<alpha> \<sharp> p \<Longrightarrow> true ;; p = p
[PROOF STEP]
by (metis postcond_equiv)


[STATEMENT]
theorem precond_left_zero:
  assumes "out\<alpha> \<sharp> p" "p \<noteq> false"
  shows "(true ;; p) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. true ;; p = true
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
out\<alpha> \<sharp> p
\<not> p = false

goal (1 subgoal):
 1. true ;; p = true
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem feasibile_iff_true_right_zero:
  "P ;; true = true \<longleftrightarrow> `\<exists> out\<alpha> \<bullet> P`"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P ;; true = true) = `\<exists> out\<alpha> \<bullet> P`
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_assoc: "(P ;; Q) ;; R = P ;; (Q ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P ;; Q) ;; R = P ;; Q ;; R
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_left_unit [simp]:
  "II ;; P = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. II ;; P = P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_right_unit [simp]:
  "P ;; II = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; II = P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_left_zero [simp]:
  "false ;; P = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false ;; P = false
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma seqr_right_zero [simp]:
  "P ;; false = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; false = false
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma impl_seqr_mono: "\<lbrakk> `P \<Rightarrow> Q`; `R \<Rightarrow> S` \<rbrakk> \<Longrightarrow> `(P ;; R) \<Rightarrow> (Q ;; S)`"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>`P \<Rightarrow> Q`; `R \<Rightarrow> S`\<rbrakk> \<Longrightarrow> `P ;; R \<Rightarrow> Q ;; S`
[PROOF STEP]
by (pred_blast)


[STATEMENT]
lemma seqr_mono:
  "\<lbrakk> P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<rbrakk> \<Longrightarrow> (P\<^sub>1 ;; Q\<^sub>1) \<sqsubseteq> (P\<^sub>2 ;; Q\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2\<rbrakk> \<Longrightarrow> P\<^sub>1 ;; Q\<^sub>1 \<sqsubseteq> P\<^sub>2 ;; Q\<^sub>2
[PROOF STEP]
by (rel_blast)


[STATEMENT]
lemma seqr_monotonic:
  "\<lbrakk> mono P; mono Q \<rbrakk> \<Longrightarrow> mono (\<lambda> X. P X ;; Q X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono P; mono Q\<rbrakk> \<Longrightarrow> mono (\<lambda>X. P X ;; Q X)
[PROOF STEP]
by (simp add: mono_def, rel_blast)


[STATEMENT]
lemma Monotonic_seqr_tail [closure]:
  assumes "Monotonic F"
  shows "Monotonic (\<lambda> X. P ;; F(X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotonic (\<lambda>X. P ;; F X)
[PROOF STEP]
by (simp add: assms monoD monoI seqr_mono)


[STATEMENT]
lemma seqr_exists_left:
  "((\<exists> $x \<bullet> P) ;; Q) = (\<exists> $x \<bullet> (P ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists> $x \<bullet> P) ;; Q = (\<exists> $x \<bullet> P ;; Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_exists_right:
  "(P ;; (\<exists> $x\<acute> \<bullet> Q)) = (\<exists> $x\<acute> \<bullet> (P ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<exists> $x\<acute> \<bullet> Q) = (\<exists> $x\<acute> \<bullet> P ;; Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_or_distl:
  "((P \<or> Q) ;; R) = ((P ;; R) \<or> (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<or> Q) ;; R = (P ;; R \<or> Q ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_or_distr:
  "(P ;; (Q \<or> R)) = ((P ;; Q) \<or> (P ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (Q \<or> R) = (P ;; Q \<or> P ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_inf_distl:
  "((P \<sqinter> Q) ;; R) = ((P ;; R) \<sqinter> (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sqinter> Q ;; R = (P ;; R) \<sqinter> (Q ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_inf_distr:
  "(P ;; (Q \<sqinter> R)) = ((P ;; Q) \<sqinter> (P ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; Q \<sqinter> R = (P ;; Q) \<sqinter> (P ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_and_distr_ufunc:
  "ufunctional P \<Longrightarrow> (P ;; (Q \<and> R)) = ((P ;; Q) \<and> (P ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufunctional P \<Longrightarrow> P ;; (Q \<and> R) = (P ;; Q \<and> P ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_and_distl_uinj:
  "uinj R \<Longrightarrow> ((P \<and> Q) ;; R) = ((P ;; R) \<and> (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uinj R \<Longrightarrow> (P \<and> Q) ;; R = (P ;; R \<and> Q ;; R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_unfold:
  "(P ;; Q) = (\<^bold>\<exists> v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/$\<^bold>v\<acute>\<rbrakk> \<and> Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$\<^bold>v\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; Q = (\<^bold>\<exists> v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/$\<^bold>v\<acute>\<rbrakk> \<and> Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$\<^bold>v\<rbrakk>)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_middle:
  assumes "vwb_lens x"
  shows "(P ;; Q) = (\<^bold>\<exists> v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; Q = (\<^bold>\<exists> v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x

goal (1 subgoal):
 1. P ;; Q = (\<^bold>\<exists> v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>)
[PROOF STEP]
by (rel_auto', metis vwb_lens_wb wb_lens.source_stability)


[STATEMENT]
lemma seqr_left_one_point:
  assumes "vwb_lens x"
  shows "((P \<and> $x\<acute> =\<^sub>u \<guillemotleft>v\<guillemotright>) ;; Q) = (P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and> $x\<acute> =\<^sub>u \<guillemotleft>v\<guillemotright>) ;; Q = P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x

goal (1 subgoal):
 1. (P \<and> $x\<acute> =\<^sub>u \<guillemotleft>v\<guillemotright>) ;; Q = P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>
[PROOF STEP]
by (rel_auto, metis vwb_lens_wb wb_lens.get_put)


[STATEMENT]
lemma seqr_right_one_point:
  assumes "vwb_lens x"
  shows "(P ;; ($x =\<^sub>u \<guillemotleft>v\<guillemotright> \<and> Q)) = (P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ($x =\<^sub>u \<guillemotleft>v\<guillemotright> \<and> Q) = P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x

goal (1 subgoal):
 1. P ;; ($x =\<^sub>u \<guillemotleft>v\<guillemotright> \<and> Q) = P\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<acute>\<rbrakk> ;; Q\<lbrakk>\<guillemotleft>v\<guillemotright>/$x\<rbrakk>
[PROOF STEP]
by (rel_auto, metis vwb_lens_wb wb_lens.get_put)


[STATEMENT]
lemma seqr_left_one_point_true:
  assumes "vwb_lens x"
  shows "((P \<and> $x\<acute>) ;; Q) = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and> $x\<acute>) ;; Q = P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk>
[PROOF STEP]
by (metis assms seqr_left_one_point true_alt_def upred_eq_true)


[STATEMENT]
lemma seqr_left_one_point_false:
  assumes "vwb_lens x"
  shows "((P \<and> \<not>$x\<acute>) ;; Q) = (P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and> \<not> $x\<acute>) ;; Q = P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>
[PROOF STEP]
by (metis assms false_alt_def seqr_left_one_point upred_eq_false)


[STATEMENT]
lemma seqr_right_one_point_true:
  assumes "vwb_lens x"
  shows "(P ;; ($x \<and> Q)) = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ($x \<and> Q) = P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk>
[PROOF STEP]
by (metis assms seqr_right_one_point true_alt_def upred_eq_true)


[STATEMENT]
lemma seqr_right_one_point_false:
  assumes "vwb_lens x"
  shows "(P ;; (\<not>$x \<and> Q)) = (P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<not> $x \<and> Q) = P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>
[PROOF STEP]
by (metis assms false_alt_def seqr_right_one_point upred_eq_false)


[STATEMENT]
lemma seqr_insert_ident_left:
  assumes "vwb_lens x" "$x\<acute> \<sharp> P" "$x \<sharp> Q"
  shows "(($x\<acute> =\<^sub>u $x \<and> P) ;; Q) = (P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($x\<acute> =\<^sub>u $x \<and> P) ;; Q = P ;; Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x
$x\<acute> \<sharp> P
$x \<sharp> Q

goal (1 subgoal):
 1. ($x\<acute> =\<^sub>u $x \<and> P) ;; Q = P ;; Q
[PROOF STEP]
by (rel_simp, meson vwb_lens_wb wb_lens_weak weak_lens.put_get)


[STATEMENT]
lemma seqr_insert_ident_right:
  assumes "vwb_lens x" "$x\<acute> \<sharp> P" "$x \<sharp> Q"
  shows "(P ;; ($x\<acute> =\<^sub>u $x \<and> Q)) = (P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ($x\<acute> =\<^sub>u $x \<and> Q) = P ;; Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x
$x\<acute> \<sharp> P
$x \<sharp> Q

goal (1 subgoal):
 1. P ;; ($x\<acute> =\<^sub>u $x \<and> Q) = P ;; Q
[PROOF STEP]
by (rel_simp, metis (no_types, opaque_lifting) vwb_lens_def wb_lens_def weak_lens.put_get)


[STATEMENT]
lemma seq_var_ident_lift:
  assumes "vwb_lens x" "$x\<acute> \<sharp> P" "$x \<sharp> Q"
  shows "(($x\<acute> =\<^sub>u $x \<and> P) ;; ($x\<acute> =\<^sub>u $x \<and> Q)) = ($x\<acute> =\<^sub>u $x \<and> (P ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($x\<acute> =\<^sub>u $x \<and> P) ;; ($x\<acute> =\<^sub>u $x \<and> Q) = ($x\<acute> =\<^sub>u $x \<and> P ;; Q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x
$x\<acute> \<sharp> P
$x \<sharp> Q

goal (1 subgoal):
 1. ($x\<acute> =\<^sub>u $x \<and> P) ;; ($x\<acute> =\<^sub>u $x \<and> Q) = ($x\<acute> =\<^sub>u $x \<and> P ;; Q)
[PROOF STEP]
by (rel_auto', metis (no_types, lifting) vwb_lens_wb wb_lens_weak weak_lens.put_get)


[STATEMENT]
lemma seqr_bool_split:
  assumes "vwb_lens x"
  shows "P ;; Q = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk> \<or> P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; Q = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk> \<or> P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x

goal (1 subgoal):
 1. P ;; Q = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; Q\<lbrakk>true/$x\<rbrakk> \<or> P\<lbrakk>false/$x\<acute>\<rbrakk> ;; Q\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
by (subst seqr_middle[of x], simp_all)


[STATEMENT]
lemma cond_inter_var_split:
  assumes "vwb_lens x"
  shows "(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
have "(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R)
[PROOF STEP]
by (simp add: cond_def seqr_or_distl)
[PROOF STATE]
proof (state)
this:
(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
have "... = ((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not>$x\<acute>) ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R) = ((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not> $x\<acute>) ;; R)
[PROOF STEP]
by (rel_auto)
[PROOF STATE]
proof (state)
this:
(($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R) = ((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not> $x\<acute>) ;; R)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(($x\<acute> \<and> P) ;; R \<or> (\<not> $x\<acute> \<and> Q) ;; R) = ((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not> $x\<acute>) ;; R)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
have "... = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not> $x\<acute>) ;; R) = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
by (simp add: seqr_left_one_point_true seqr_left_one_point_false assms)
[PROOF STATE]
proof (state)
this:
((P \<and> $x\<acute>) ;; R \<or> (Q \<and> \<not> $x\<acute>) ;; R) = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)

goal (1 subgoal):
 1. (P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(P \<triangleleft> $x\<acute> \<triangleright> Q) ;; R = (P\<lbrakk>true/$x\<acute>\<rbrakk> ;; R\<lbrakk>true/$x\<rbrakk> \<or> Q\<lbrakk>false/$x\<acute>\<rbrakk> ;; R\<lbrakk>false/$x\<rbrakk>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem seqr_pre_transfer: "in\<alpha> \<sharp> q \<Longrightarrow> ((P \<and> q) ;; R) = (P ;; (q\<^sup>- \<and> R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in\<alpha> \<sharp> q \<Longrightarrow> (P \<and> q) ;; R = P ;; (q\<^sup>- \<and> R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem seqr_pre_transfer':
  "((P \<and> \<lceil>q\<rceil>\<^sub>>) ;; R) = (P ;; (\<lceil>q\<rceil>\<^sub>< \<and> R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and> \<lceil>q\<rceil>\<^sub>>) ;; R = P ;; (\<lceil>q\<rceil>\<^sub>< \<and> R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem seqr_post_out: "in\<alpha> \<sharp> r \<Longrightarrow> (P ;; (Q \<and> r)) = ((P ;; Q) \<and> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in\<alpha> \<sharp> r \<Longrightarrow> P ;; (Q \<and> r) = (P ;; Q \<and> r)
[PROOF STEP]
by (rel_blast)


[STATEMENT]
lemma seqr_post_var_out:
  fixes x :: "(bool \<Longrightarrow> '\<alpha>)"
  shows "(P ;; (Q \<and> $x\<acute>)) = ((P ;; Q) \<and> $x\<acute>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (Q \<and> $x\<acute>) = (P ;; Q \<and> $x\<acute>)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_pre_out: "out\<alpha> \<sharp> p \<Longrightarrow> ((p \<and> Q) ;; R) = (p \<and> (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> p \<Longrightarrow> (p \<and> Q) ;; R = (p \<and> Q ;; R)
[PROOF STEP]
by (rel_blast)


[STATEMENT]
lemma seqr_pre_var_out:
  fixes x :: "(bool \<Longrightarrow> '\<alpha>)"
  shows "(($x \<and> P) ;; Q) = ($x \<and> (P ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($x \<and> P) ;; Q = ($x \<and> P ;; Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_true_lemma:
  "(P = (\<not> ((\<not> P) ;; true))) = (P = (P ;; true))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P = (\<not> (\<not> P) ;; true)) = (P = P ;; true)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma seqr_to_conj: "\<lbrakk> out\<alpha> \<sharp> P; in\<alpha> \<sharp> Q \<rbrakk> \<Longrightarrow> (P ;; Q) = (P \<and> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>out\<alpha> \<sharp> P; in\<alpha> \<sharp> Q\<rbrakk> \<Longrightarrow> P ;; Q = (P \<and> Q)
[PROOF STEP]
by (metis postcond_left_unit seqr_pre_out utp_pred_laws.inf_top.right_neutral)


[STATEMENT]
lemma shEx_lift_seq_1 [uquant_lift]:
  "((\<^bold>\<exists> x \<bullet> P x) ;; Q) = (\<^bold>\<exists> x \<bullet> (P x ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ushEx P ;; Q = (\<^bold>\<exists> x \<bullet> P x ;; Q)
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma shEx_mem_lift_seq_1 [uquant_lift]:
  assumes "out\<alpha> \<sharp> A"
  shows "((\<^bold>\<exists> x \<in> A \<bullet> P x) ;; Q) = (\<^bold>\<exists> x \<in> A \<bullet> (P x ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P x) ;; Q = (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P x ;; Q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
out\<alpha> \<sharp> A

goal (1 subgoal):
 1. (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P x) ;; Q = (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P x ;; Q)
[PROOF STEP]
by rel_blast


[STATEMENT]
lemma shEx_lift_seq_2 [uquant_lift]:
  "(P ;; (\<^bold>\<exists> x \<bullet> Q x)) = (\<^bold>\<exists> x \<bullet> (P ;; Q x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ushEx Q = (\<^bold>\<exists> x \<bullet> P ;; Q x)
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma shEx_mem_lift_seq_2 [uquant_lift]:
  assumes "in\<alpha> \<sharp> A"
  shows "(P ;; (\<^bold>\<exists> x \<in> A \<bullet> Q x)) = (\<^bold>\<exists> x \<in> A \<bullet> (P ;; Q x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> Q x) = (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P ;; Q x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
in\<alpha> \<sharp> A

goal (1 subgoal):
 1. P ;; (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> Q x) = (\<^bold>\<exists> x \<bullet> \<guillemotleft>x\<guillemotright> \<in>\<^sub>u A \<and> P ;; Q x)
[PROOF STEP]
by rel_blast


[STATEMENT]
lemma iter_seqr_nil [simp]: "(;; i : [] \<bullet> P(i)) = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seqr_iter [] P = II
[PROOF STEP]
by (simp add: seqr_iter_def)


[STATEMENT]
lemma iter_seqr_cons [simp]: "(;; i : (x # xs) \<bullet> P(i)) = P(x) ;; (;; i : xs \<bullet> P(i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seqr_iter (x # xs) P = P x ;; seqr_iter xs P
[PROOF STEP]
by (simp add: seqr_iter_def)


[STATEMENT]
lemma seq_Sup_distl: "P ;; (\<Sqinter> A) = (\<Sqinter> Q\<in>A. P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; \<Or>A = \<Or>((;;) P ` A)
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma seq_Sup_distr: "(\<Sqinter> A) ;; Q = (\<Sqinter> P\<in>A. P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>A ;; Q = \<Or>((\<lambda>P. P ;; Q) ` A)
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma seq_UINF_distl: "P ;; (\<Sqinter> Q\<in>A \<bullet> F(Q)) = (\<Sqinter> Q\<in>A \<bullet> P ;; F(Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<Sqinter> Q \<in> A \<bullet> F Q) = (\<Sqinter> Q \<in> A \<bullet> P ;; F Q)
[PROOF STEP]
by (simp add: UINF_as_Sup_collect seq_Sup_distl)


[STATEMENT]
lemma seq_UINF_distl': "P ;; (\<Sqinter> Q \<bullet> F(Q)) = (\<Sqinter> Q \<bullet> P ;; F(Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<Sqinter> Q \<bullet> F Q) = (\<Sqinter> Q \<bullet> P ;; F Q)
[PROOF STEP]
by (metis UINF_mem_UNIV seq_UINF_distl)


[STATEMENT]
lemma seq_UINF_distr: "(\<Sqinter> P\<in>A \<bullet> F(P)) ;; Q = (\<Sqinter> P\<in>A \<bullet> F(P) ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter> P \<in> A \<bullet> F P) ;; Q = (\<Sqinter> P \<in> A \<bullet> F P ;; Q)
[PROOF STEP]
by (simp add: UINF_as_Sup_collect seq_Sup_distr)


[STATEMENT]
lemma seq_UINF_distr': "(\<Sqinter> P \<bullet> F(P)) ;; Q = (\<Sqinter> P \<bullet> F(P) ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter> P \<bullet> F P) ;; Q = (\<Sqinter> P \<bullet> F P ;; Q)
[PROOF STEP]
by (metis UINF_mem_UNIV seq_UINF_distr)


[STATEMENT]
lemma seq_SUP_distl: "P ;; (\<Sqinter>i\<in>A. Q(i)) = (\<Sqinter>i\<in>A. P ;; Q(i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; \<Or>(Q ` A) = \<Or>((\<lambda>i. P ;; Q i) ` A)
[PROOF STEP]
by (metis image_image seq_Sup_distl)


[STATEMENT]
lemma seq_SUP_distr: "(\<Sqinter>i\<in>A. P(i)) ;; Q = (\<Sqinter>i\<in>A. P(i) ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>(P ` A) ;; Q = \<Or>((\<lambda>i. P i ;; Q) ` A)
[PROOF STEP]
by (simp add: seq_Sup_distr)


[STATEMENT]
lemma cond_skip: "out\<alpha> \<sharp> b \<Longrightarrow> (b \<and> II) = (II \<and> b\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> b \<Longrightarrow> (b \<and> II) = (II \<and> b\<^sup>-)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma pre_skip_post: "(\<lceil>b\<rceil>\<^sub>< \<and> II) = (II \<and> \<lceil>b\<rceil>\<^sub>>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lceil>b\<rceil>\<^sub>< \<and> II) = (II \<and> \<lceil>b\<rceil>\<^sub>>)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma skip_var:
  fixes x :: "(bool \<Longrightarrow> '\<alpha>)"
  shows "($x \<and> II) = (II \<and> $x\<acute>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($x \<and> II) = (II \<and> $x\<acute>)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma skip_r_unfold:
  "vwb_lens x \<Longrightarrow> II = ($x\<acute> =\<^sub>u $x \<and> II\<restriction>\<^sub>\<alpha>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> II = ($x\<acute> =\<^sub>u $x \<and> II \<restriction>\<^sub>\<alpha> x)
[PROOF STEP]
by (rel_simp, metis mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put)


[STATEMENT]
lemma skip_r_alpha_eq:
  "II = ($\<^bold>v\<acute> =\<^sub>u $\<^bold>v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. II = ($\<^bold>v\<acute> =\<^sub>u $\<^bold>v)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma skip_ra_unfold:
  "II\<^bsub>x;y\<^esub> = ($x\<acute> =\<^sub>u $x \<and> II\<^bsub>y\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. II\<^bsub>x +\<^sub>L y\<^esub> = ($x\<acute> =\<^sub>u $x \<and> II\<^bsub>y\<^esub>)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma skip_res_as_ra:
  "\<lbrakk> vwb_lens y; x +\<^sub>L y \<approx>\<^sub>L 1\<^sub>L; x \<bowtie> y \<rbrakk> \<Longrightarrow> II\<restriction>\<^sub>\<alpha>x = II\<^bsub>y\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens y; x +\<^sub>L y \<approx>\<^sub>L \<Sigma>; x \<bowtie> y\<rbrakk> \<Longrightarrow> II \<restriction>\<^sub>\<alpha> x = II\<^bsub>y\<^esub>
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b Z Za v va. \<lbrakk>vwb_lens y; x \<bowtie> y; vwb_lens Z; vwb_lens Za; \<forall>xa. (get\<^bsub>x\<^esub> xa, get\<^bsub>y\<^esub> xa) = get\<^bsub>Z\<^esub> xa; \<forall>xa a b. put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> xa b) a = put\<^bsub>Z\<^esub> xa (a, b); \<forall>x. x = get\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x); \<forall>x xa. xa = put\<^bsub>Z\<^esub> x (put\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x) xa); put\<^bsub>x\<^esub> b va = put\<^bsub>x\<^esub> a v\<rbrakk> \<Longrightarrow> get\<^bsub>y\<^esub> b = get\<^bsub>y\<^esub> a
 2. \<And>a b Z Za. \<lbrakk>vwb_lens y; x \<bowtie> y; vwb_lens Z; vwb_lens Za; \<forall>xa. (get\<^bsub>x\<^esub> xa, get\<^bsub>y\<^esub> xa) = get\<^bsub>Z\<^esub> xa; \<forall>xa a b. put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> xa b) a = put\<^bsub>Z\<^esub> xa (a, b); \<forall>x. x = get\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x); \<forall>x xa. xa = put\<^bsub>Z\<^esub> x (put\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x) xa); get\<^bsub>y\<^esub> b = get\<^bsub>y\<^esub> a\<rbrakk> \<Longrightarrow> \<exists>v va. put\<^bsub>x\<^esub> b va = put\<^bsub>x\<^esub> a v
[PROOF STEP]
apply (metis (no_types, lifting) lens_indep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b Z Za. \<lbrakk>vwb_lens y; x \<bowtie> y; vwb_lens Z; vwb_lens Za; \<forall>xa. (get\<^bsub>x\<^esub> xa, get\<^bsub>y\<^esub> xa) = get\<^bsub>Z\<^esub> xa; \<forall>xa a b. put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> xa b) a = put\<^bsub>Z\<^esub> xa (a, b); \<forall>x. x = get\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x); \<forall>x xa. xa = put\<^bsub>Z\<^esub> x (put\<^bsub>Za\<^esub> (get\<^bsub>Z\<^esub> x) xa); get\<^bsub>y\<^esub> b = get\<^bsub>y\<^esub> a\<rbrakk> \<Longrightarrow> \<exists>v va. put\<^bsub>x\<^esub> b va = put\<^bsub>x\<^esub> a v
[PROOF STEP]
apply (metis vwb_lens.put_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma assigns_subst [usubst]:
  "\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> \<langle>\<rho>\<rangle>\<^sub>a = \<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> \<langle>\<rho>\<rangle>\<^sub>a = \<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assigns_r_comp: "(\<langle>\<sigma>\<rangle>\<^sub>a ;; P) = (\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<sigma>\<rangle>\<^sub>a ;; P = \<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assigns_r_feasible:
  "(\<langle>\<sigma>\<rangle>\<^sub>a ;; true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<sigma>\<rangle>\<^sub>a ;; true = true
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assign_subst [usubst]:
  "\<lbrakk> mwb_lens x; mwb_lens y \<rbrakk> \<Longrightarrow> [$x \<mapsto>\<^sub>s \<lceil>u\<rceil>\<^sub><] \<dagger> (y := v) = (x, y) := (u, [x \<mapsto>\<^sub>s u] \<dagger> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mwb_lens x; mwb_lens y\<rbrakk> \<Longrightarrow> (y := v)\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk> = x, y := u, v\<lbrakk>u/x\<rbrakk>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assign_vacuous_skip:
  assumes "vwb_lens x"
  shows "(x := &x) = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := &x = II
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwb_lens x

goal (1 subgoal):
 1. x := &x = II
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma assign_vacuous_assume:
  assumes "mwb_lens x"
  shows "[(&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>)]\<^sup>\<top> ;; (x := &x) = [(&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>)]\<^sup>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?[&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>] ;; x := &x = ?[&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mwb_lens x

goal (1 subgoal):
 1. ?[&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>] ;; x := &x = ?[&\<^bold>v \<in>\<^sub>u \<guillemotleft>\<S>\<^bsub>x\<^esub>\<guillemotright>]
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma assign_simultaneous:
  assumes "vwb_lens y" "x \<bowtie> y"
  shows "(x,y) := (e, &y) = (x := e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x, y := e, &y = x := e
[PROOF STEP]
by (simp add: assms usubst_upd_comm usubst_upd_var_id)


[STATEMENT]
lemma assigns_idem: "mwb_lens x \<Longrightarrow> (x,x) := (u,v) = (x := v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mwb_lens x \<Longrightarrow> x, x := u, v = x := v
[PROOF STEP]
by (simp add: usubst)


[STATEMENT]
lemma assigns_comp: "(\<langle>f\<rangle>\<^sub>a ;; \<langle>g\<rangle>\<^sub>a) = \<langle>g \<circ> f\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>f\<rangle>\<^sub>a ;; \<langle>g\<rangle>\<^sub>a = \<langle>g \<circ> f\<rangle>\<^sub>a
[PROOF STEP]
by (simp add: assigns_r_comp usubst)


[STATEMENT]
lemma assigns_cond: "(\<langle>f\<rangle>\<^sub>a \<triangleleft> b \<triangleright>\<^sub>r \<langle>g\<rangle>\<^sub>a) = \<langle>f \<triangleleft> b \<triangleright>\<^sub>s g\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>f\<rangle>\<^sub>a \<triangleleft> b \<triangleright>\<^sub>r \<langle>g\<rangle>\<^sub>a = \<langle>f \<triangleleft> b \<triangleright>\<^sub>s g\<rangle>\<^sub>a
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assigns_r_conv:
  "bij f \<Longrightarrow> \<langle>f\<rangle>\<^sub>a\<^sup>- = \<langle>inv f\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> \<langle>f\<rangle>\<^sub>a\<^sup>- = \<langle>inv f\<rangle>\<^sub>a
[PROOF STEP]
by (rel_auto, simp_all add: bij_is_inj bij_is_surj surj_f_inv_f)


[STATEMENT]
lemma assign_pred_transfer:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  assumes "$x \<sharp> b" "out\<alpha> \<sharp> b"
  shows "(b \<and> x := v) = (x := v \<and> b\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<and> x := v) = (x := v \<and> b\<^sup>-)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
$x \<sharp> b
out\<alpha> \<sharp> b

goal (1 subgoal):
 1. (b \<and> x := v) = (x := v \<and> b\<^sup>-)
[PROOF STEP]
by (rel_blast)


[STATEMENT]
lemma assign_r_comp: "x := u ;; P = P\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := u ;; P = P\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>
[PROOF STEP]
by (simp add: assigns_r_comp usubst alpha)


[STATEMENT]
lemma assign_test: "mwb_lens x \<Longrightarrow> (x := \<guillemotleft>u\<guillemotright> ;; x := \<guillemotleft>v\<guillemotright>) = (x := \<guillemotleft>v\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mwb_lens x \<Longrightarrow> x := \<guillemotleft>u\<guillemotright> ;; x := \<guillemotleft>v\<guillemotright> = x := \<guillemotleft>v\<guillemotright>
[PROOF STEP]
by (simp add: assigns_comp usubst)


[STATEMENT]
lemma assign_twice: "\<lbrakk> mwb_lens x; x \<sharp> f \<rbrakk> \<Longrightarrow> (x := e ;; x := f) = (x := f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mwb_lens x; x \<sharp> f\<rbrakk> \<Longrightarrow> x := e ;; x := f = x := f
[PROOF STEP]
by (simp add: assigns_comp usubst unrest)


[STATEMENT]
lemma assign_commute:
  assumes "x \<bowtie> y" "x \<sharp> f" "y \<sharp> e"
  shows "(x := e ;; y := f) = (y := f ;; x := e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := e ;; y := f = y := f ;; x := e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<bowtie> y
x \<sharp> f
y \<sharp> e

goal (1 subgoal):
 1. x := e ;; y := f = y := f ;; x := e
[PROOF STEP]
by (rel_simp, simp_all add: lens_indep_comm)


[STATEMENT]
lemma assign_cond:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  assumes "out\<alpha> \<sharp> b"
  shows "(x := e ;; (P \<triangleleft> b \<triangleright> Q)) = ((x := e ;; P) \<triangleleft> (b\<lbrakk>\<lceil>e\<rceil>\<^sub></$x\<rbrakk>) \<triangleright> (x := e ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := e ;; (P \<triangleleft> b \<triangleright> Q) = x := e ;; P \<triangleleft> b\<lbrakk>\<lceil>e\<rceil>\<^sub></$x\<rbrakk> \<triangleright> x := e ;; Q
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assign_rcond:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  shows "(x := e ;; (P \<triangleleft> b \<triangleright>\<^sub>r Q)) = ((x := e ;; P) \<triangleleft> (b\<lbrakk>e/x\<rbrakk>) \<triangleright>\<^sub>r (x := e ;; Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := e ;; (P \<triangleleft> b \<triangleright>\<^sub>r Q) = x := e ;; P \<triangleleft> b\<lbrakk>e/x\<rbrakk> \<triangleright>\<^sub>r x := e ;; Q
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assign_r_alt_def:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  shows "x := v = II\<lbrakk>\<lceil>v\<rceil>\<^sub></$x\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x := v = II\<lbrakk>\<lceil>v\<rceil>\<^sub></$x\<rbrakk>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assigns_r_ufunc: "ufunctional \<langle>f\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufunctional \<langle>f\<rangle>\<^sub>a
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assigns_r_uinj: "inj f \<Longrightarrow> uinj \<langle>f\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f \<Longrightarrow> uinj \<langle>f\<rangle>\<^sub>a
[PROOF STEP]
by (rel_simp, simp add: inj_eq)


[STATEMENT]
lemma assigns_r_swap_uinj:
  "\<lbrakk> vwb_lens x; vwb_lens y; x \<bowtie> y \<rbrakk> \<Longrightarrow> uinj ((x,y) := (&y,&x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; vwb_lens y; x \<bowtie> y\<rbrakk> \<Longrightarrow> uinj (x, y := &y, &x)
[PROOF STEP]
by (metis assigns_r_uinj pr_var_def swap_usubst_inj)


[STATEMENT]
lemma assign_unfold:
  "vwb_lens x \<Longrightarrow> (x := v) = ($x\<acute> =\<^sub>u \<lceil>v\<rceil>\<^sub>< \<and> II\<restriction>\<^sub>\<alpha>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> x := v = ($x\<acute> =\<^sub>u \<lceil>v\<rceil>\<^sub>< \<and> II \<restriction>\<^sub>\<alpha> x)
[PROOF STEP]
apply (rel_auto, auto simp add: comp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b va vaa. \<lbrakk>vwb_lens x; get\<^bsub>x\<^esub> b = \<lbrakk>v\<rbrakk>\<^sub>e a; put\<^bsub>x\<^esub> b vaa = put\<^bsub>x\<^esub> a va\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> a (\<lbrakk>v\<rbrakk>\<^sub>e a)
[PROOF STEP]
using vwb_lens.put_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vwb_lens ?x; get\<^bsub>?x\<^esub> ?\<sigma> = ?k; put\<^bsub>?x\<^esub> ?\<sigma> ?u = put\<^bsub>?x\<^esub> ?\<rho> ?v\<rbrakk> \<Longrightarrow> put\<^bsub>?x\<^esub> ?\<rho> ?k = ?\<sigma>

goal (1 subgoal):
 1. \<And>a b va vaa. \<lbrakk>vwb_lens x; get\<^bsub>x\<^esub> b = \<lbrakk>v\<rbrakk>\<^sub>e a; put\<^bsub>x\<^esub> b vaa = put\<^bsub>x\<^esub> a va\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> a (\<lbrakk>v\<rbrakk>\<^sub>e a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma nd_assign_comp:
  "x \<bowtie> y \<Longrightarrow> x := * ;; y := * = x,y := *"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<bowtie> y \<Longrightarrow> x := * ;; y := * = x +\<^sub>L y := *
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xa xaa. x \<bowtie> y \<Longrightarrow> \<exists>aa b. put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> a xa) xaa = put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a b) aa
 2. \<And>a aa ba. x \<bowtie> y \<Longrightarrow> \<exists>ya. (\<exists>xa. ya = put\<^bsub>x\<^esub> a xa) \<and> (\<exists>xa. put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a ba) aa = put\<^bsub>y\<^esub> ya xa)
[PROOF STEP]
using lens_indep_comm
[PROOF STATE]
proof (prove)
using this:
?x \<bowtie> ?y \<Longrightarrow> put\<^bsub>?x\<^esub> (put\<^bsub>?y\<^esub> ?\<sigma> ?v) ?u = put\<^bsub>?y\<^esub> (put\<^bsub>?x\<^esub> ?\<sigma> ?u) ?v

goal (2 subgoals):
 1. \<And>a xa xaa. x \<bowtie> y \<Longrightarrow> \<exists>aa b. put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> a xa) xaa = put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a b) aa
 2. \<And>a aa ba. x \<bowtie> y \<Longrightarrow> \<exists>ya. (\<exists>xa. ya = put\<^bsub>x\<^esub> a xa) \<and> (\<exists>xa. put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a ba) aa = put\<^bsub>y\<^esub> ya xa)
[PROOF STEP]
by fastforce+


[STATEMENT]
lemma nd_assign_assign:
  "\<lbrakk> vwb_lens x; x \<sharp> e \<rbrakk> \<Longrightarrow> x := * ;; x := e = x := e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; x \<sharp> e\<rbrakk> \<Longrightarrow> x := * ;; x := e = x := e
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma convr_invol [simp]: "p\<^sup>-\<^sup>- = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sup>-\<^sup>- = p
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma lit_convr [simp]: "\<guillemotleft>v\<guillemotright>\<^sup>- = \<guillemotleft>v\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>v\<guillemotright>\<^sup>- = \<guillemotleft>v\<guillemotright>
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma uivar_convr [simp]:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  shows "($x)\<^sup>- = $x\<acute>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $x\<^sup>- = $x\<acute>
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma uovar_convr [simp]:
  fixes x :: "('a \<Longrightarrow> '\<alpha>)"
  shows "($x\<acute>)\<^sup>- = $x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $x\<acute>\<^sup>- = $x
[PROOF STEP]
by pred_auto


[STATEMENT]
lemma uop_convr [simp]: "(uop f u)\<^sup>- = uop f (u\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uop f u\<^sup>- = uop f (u\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma bop_convr [simp]: "(bop f u v)\<^sup>- = bop f (u\<^sup>-) (v\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bop f u v\<^sup>- = bop f (u\<^sup>-) (v\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma eq_convr [simp]: "(p =\<^sub>u q)\<^sup>- = (p\<^sup>- =\<^sub>u q\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p =\<^sub>u q)\<^sup>- = (p\<^sup>- =\<^sub>u q\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma not_convr [simp]: "(\<not> p)\<^sup>- = (\<not> p\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> p)\<^sup>- = (\<not> p\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma disj_convr [simp]: "(p \<or> q)\<^sup>- = (q\<^sup>- \<or> p\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<or> q)\<^sup>- = (q\<^sup>- \<or> p\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma conj_convr [simp]: "(p \<and> q)\<^sup>- = (q\<^sup>- \<and> p\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<and> q)\<^sup>- = (q\<^sup>- \<and> p\<^sup>-)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma seqr_convr [simp]: "(p ;; q)\<^sup>- = (q\<^sup>- ;; p\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p ;; q)\<^sup>- = q\<^sup>- ;; p\<^sup>-
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma pre_convr [simp]: "\<lceil>p\<rceil>\<^sub><\<^sup>- = \<lceil>p\<rceil>\<^sub>>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>p\<rceil>\<^sub><\<^sup>- = \<lceil>p\<rceil>\<^sub>>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma post_convr [simp]: "\<lceil>p\<rceil>\<^sub>>\<^sup>- = \<lceil>p\<rceil>\<^sub><"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>p\<rceil>\<^sub>>\<^sup>- = \<lceil>p\<rceil>\<^sub><
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assume_false: "[false]\<^sup>\<top> = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?[false] = false
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assume_true: "[true]\<^sup>\<top> = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?[true] = II
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assume_seq: "[b]\<^sup>\<top> ;; [c]\<^sup>\<top> = [(b \<and> c)]\<^sup>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?[b] ;; ?[c] = ?[b \<and> c]
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assert_false: "{false}\<^sub>\<bottom> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {false}\<^sub>\<bottom> = true
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assert_true: "{true}\<^sub>\<bottom> = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {true}\<^sub>\<bottom> = II
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assert_seq: "{b}\<^sub>\<bottom> ;; {c}\<^sub>\<bottom> = {(b \<and> c)}\<^sub>\<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b}\<^sub>\<bottom> ;; {c}\<^sub>\<bottom> = {b \<and> c}\<^sub>\<bottom>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_all [frame]: "\<Sigma>:[P] = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<Sigma>}:[P] = P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_none [frame]:
  "\<emptyset>:[P] = (P \<and> II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<emptyset>}:[P] = (P \<and> II)
[PROOF STEP]
by (rel_auto)