[STATEMENT]
lemma d_sinpoly_cospoly:
    "(sinpoly (Suc n) has_field_derivative cospoly n x) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
 2. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
 2. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
[PROOF STEP]
by (simp add: sinpoly_def cospoly_def)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)

goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc n) has_real_derivative cospoly n x) (at x)

goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
proof (cases "n=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
 2. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
 2. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
by (simp add: sinpoly_def sin_coeff_def cospoly_def)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have xn: "x ^ (n - Suc 0) * x = x ^ n"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. x ^ (n - Suc 0) * x = x ^ n
[PROOF STEP]
by (metis Suc_pred mult.commute not_gr0 power_Suc)
[PROOF STATE]
proof (state)
this:
x ^ (n - Suc 0) * x = x ^ n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
using Suc False
[PROOF STATE]
proof (prove)
using this:
(sinpoly (Suc n) has_real_derivative cospoly n x) (at x)
n \<noteq> 0

goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
apply (simp add: sinpoly_Suc [of "Suc n"] cospoly_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>a. sinpoly (Suc n) a + sin_coeff (Suc n) * (a * a ^ n)) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k) + cos_coeff n * x ^ n) (at x)
[PROOF STEP]
apply (intro derivative_eq_intros | simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> (x ^ n + real n * x ^ (n - Suc 0) * x) * sin_coeff (Suc n) = cos_coeff n * x ^ n
[PROOF STEP]
apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def divide_simps del: fact_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. (if even k then (- 1) ^ (k div 2) / fact k else 0) * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> even n \<longrightarrow> (x ^ n + real n * x ^ n) * fact n = x ^ n * fact (Suc n)
[PROOF STEP]
apply (simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simple_fw_remdups_Rev: "simple_fw (remdups_rev rs) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw (remdups_rev rs) p = simple_fw rs p
[PROOF STEP]
apply(induction rs p rule: simple_fw.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_. simple_fw (remdups_rev []) uu_ = simple_fw [] uu_
 2. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Accept # rs)) p = simple_fw (SimpleRule m simple_action.Accept # rs) p
 3. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Drop # rs)) p = simple_fw (SimpleRule m simple_action.Drop # rs) p
[PROOF STEP]
apply(simp add: remdups_rev_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Accept # rs)) p = simple_fw (SimpleRule m simple_action.Accept # rs) p
 2. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Drop # rs)) p = simple_fw (SimpleRule m simple_action.Drop # rs) p
[PROOF STEP]
apply(simp_all add: remdups_rev_fst remdups_rev_removeAll simple_fw_not_matches_removeAll)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pseudo_mod_zero[simp]:
"pseudo_mod 0 f = (0::'a :: {idom} poly)"
"pseudo_mod f 0 = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_mod 0 f = 0 &&& pseudo_mod f 0 = f
[PROOF STEP]
unfolding pseudo_mod_def snd_pseudo_mod_smult_left[of 0 _ f,simplified]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 &&& snd (pseudo_divmod f 0) = f
[PROOF STEP]
unfolding pseudo_divmod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 &&& snd (if 0 = 0 then (0, f) else pseudo_divmod_main (lead_coeff 0) 0 f 0 (degree f) (1 + length (coeffs f) - length (coeffs 0))) = f
[PROOF STEP]
by auto


[STATEMENT]
lemma fundamental_theorem_eq_5: assumes i: "3 \<le> i" "i \<le> k" "n i < j" "j < n (i - 1) - 1"
  shows "R j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from BT_lemma_2_23[OF i]
[PROOF STATE]
proof (chain)
picking this:
subresultant j (F (i - 2)) (F (i - 1)) = 0
[PROOF STEP]
have id1: "subresultant j (F (i - 2)) (F (i - 1)) = 0"
[PROOF STATE]
proof (prove)
using this:
subresultant j (F (i - 2)) (F (i - 1)) = 0

goal (1 subgoal):
 1. subresultant j (F (i - 2)) (F (i - 1)) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subresultant j (F (i - 2)) (F (i - 1)) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "n (i - 1) \<le> n 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (i - 1) \<le> n 2
[PROOF STEP]
by (rule n_ge_trans, insert i, auto)
[PROOF STATE]
proof (state)
this:
n (i - 1) \<le> n 2

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with n_gt[of "i - 1"] i
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>2 \<le> i - 1; i - 1 < k\<rbrakk> \<Longrightarrow> n (Suc (i - 1)) < n (i - 1)
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) \<le> n 2
[PROOF STEP]
have "n (i - 1) - 1 < n 2"
    and lt: "j < n (i - 1)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> i - 1; i - 1 < k\<rbrakk> \<Longrightarrow> n (Suc (i - 1)) < n (i - 1)
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) \<le> n 2

goal (1 subgoal):
 1. n (i - 1) - 1 < n 2 &&& j < n (i - 1)
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)
[PROOF STEP]
have "R j = subresultant j G1 G2"
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. R j = subresultant j G1 G2
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. (if j = n 2 then sdiv_poly (Polynomial.smult (lead_coeff G2 ^ \<delta> 1) G2) (lead_coeff G2) else subresultant j G1 G2) = subresultant j G1 G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R j = subresultant j G1 G2

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from arg_cong[OF this, of ffp, unfolded to_fract_hom.subresultant_hom, folded F1 F2]
[PROOF STATE]
proof (chain)
picking this:
ffp (R j) = subresultant j (F 1) (F 2)
[PROOF STEP]
have id2: "ffp (R j) = subresultant j (F 1) (F 2)"
[PROOF STATE]
proof (prove)
using this:
ffp (R j) = subresultant j (F 1) (F 2)

goal (1 subgoal):
 1. ffp (R j) = subresultant j (F 1) (F 2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ffp (R j) = subresultant j (F 1) (F 2)

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
[PROOF STEP]
have "3 \<le> i" "i \<le> k + 1"
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1

goal (1 subgoal):
 1. 3 \<le> i &&& i \<le> k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
3 \<le> i
i \<le> k + 1

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
note eq_30 = BT_eq_30[OF this lt]
[PROOF STATE]
proof (state)
this:
Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2)) = Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1)))

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
let ?c3 = "\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
let ?c2 = "\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) *
                  (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "?c3 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0
[PROOF STEP]
by (rule nonzero_alphaprod, insert i, auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with arg_cong[OF eq_30, of "smult (inverse ?c3)"]
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2))) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1))))
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0
[PROOF STEP]
have id3: "subresultant j (F 1) (F 2) = smult (inverse ?c3 * ?c2)
     (subresultant j (F (i - 2)) (F (i - 1)))"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2))) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1))))
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0

goal (1 subgoal):
 1. subresultant j (F 1) (F 2) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) (subresultant j (F (i - 2)) (F (i - 1)))
[PROOF STEP]
by (auto intro: poly_eqI)
[PROOF STATE]
proof (state)
this:
subresultant j (F 1) (F 2) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) (subresultant j (F (i - 2)) (F (i - 1)))

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "ffp (R j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffp (R j) = 0
[PROOF STEP]
unfolding id1 id2 id3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffp (R j) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ffp (R j) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
R j = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma floor_div_pos_int:
  fixes r :: "'a :: floor_ceiling"
  assumes n: "n > 0"
  shows "\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?of_int = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define rhs where "rhs = \<lfloor>r\<rfloor> div n"
[PROOF STATE]
proof (state)
this:
rhs = \<lfloor>r\<rfloor> div n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?n = "?of_int n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define m where "m = \<lfloor>r\<rfloor> mod n"
[PROOF STATE]
proof (state)
this:
m = \<lfloor>r\<rfloor> mod n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?m = "?of_int m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
from div_mult_mod_eq[of "floor r" n]
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>
[PROOF STEP]
have dm: "rhs * n + m = \<lfloor>r\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. rhs * n + m = \<lfloor>r\<rfloor>
[PROOF STEP]
unfolding rhs_def m_def
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rhs * n + m = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have mn: "m < n" and m0: "m \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n &&& 0 \<le> m
[PROOF STEP]
using n m_def
[PROOF STATE]
proof (prove)
using this:
0 < n
m = \<lfloor>r\<rfloor> mod n

goal (1 subgoal):
 1. m < n &&& 0 \<le> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < n
0 \<le> m

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define e where "e = r - ?of_int \<lfloor>r\<rfloor>"
[PROOF STATE]
proof (state)
this:
e = r - of_int \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have e0: "e \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> e
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> r - of_int \<lfloor>r\<rfloor>
[PROOF STEP]
by (metis diff_self eq_iff floor_diff_of_int zero_le_floor)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have e1: "e < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e < (1::'a)
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r - of_int \<lfloor>r\<rfloor> < (1::'a)
[PROOF STEP]
by (metis diff_self dual_order.refl floor_diff_of_int floor_le_zero)
[PROOF STATE]
proof (state)
this:
e < (1::'a)

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "r = ?of_int \<lfloor>r\<rfloor> + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = of_int \<lfloor>r\<rfloor> + e
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = of_int \<lfloor>r\<rfloor> + (r - of_int \<lfloor>r\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = of_int \<lfloor>r\<rfloor> + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r = of_int \<lfloor>r\<rfloor> + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "\<lfloor>r\<rfloor> = rhs * n + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r\<rfloor> = rhs * n + m
[PROOF STEP]
using dm
[PROOF STATE]
proof (prove)
using this:
rhs * n + m = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r\<rfloor> = rhs * n + m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r\<rfloor> = rhs * n + m

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r = of_int (rhs * n + m) + e
[PROOF STEP]
have "r = ?of_int (rhs * n + m) + e"
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. r = of_int (rhs * n + m) + e
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
hence "r / ?n = ?of_int (rhs * n) / ?n + (e + ?m) / ?n"
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e
0 < n

goal (1 subgoal):
 1. r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "?of_int (rhs * n) / ?n = ?of_int rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (rhs * n) / of_int n = of_int rhs
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. of_int (rhs * n) / of_int n = of_int rhs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int (rhs * n) / of_int n = of_int rhs

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r / of_int n = of_int rhs + (e + of_int m) / of_int n
[PROOF STEP]
have *: "r / ?of_int n = (e + ?of_int m) / ?of_int n + ?of_int rhs"
[PROOF STATE]
proof (prove)
using this:
r / of_int n = of_int rhs + (e + of_int m) / of_int n

goal (1 subgoal):
 1. r / of_int n = (e + of_int m) / of_int n + of_int rhs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r / of_int n = (e + of_int m) / of_int n + of_int rhs

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "?l = rhs + floor ((e + ?m) / ?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(e + of_int m) / of_int n + of_int rhs\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "floor ((e + ?m) / ?n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(e + of_int m) / of_int n\<rfloor> = 0
[PROOF STEP]
proof (rule floor_unique)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_int 0 \<le> (e + of_int m) / of_int n
 2. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
show "?of_int 0 \<le> (e + ?m) / ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int 0 \<le> (e + of_int m) / of_int n
[PROOF STEP]
using e0 m0 n
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> e
0 \<le> m
0 < n

goal (1 subgoal):
 1. of_int 0 \<le> (e + of_int m) / of_int n
[PROOF STEP]
by (metis add_increasing2 divide_nonneg_pos of_int_0 of_int_0_le_iff of_int_0_less_iff)
[PROOF STATE]
proof (state)
this:
of_int 0 \<le> (e + of_int m) / of_int n

goal (1 subgoal):
 1. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
show "(e + ?m) / ?n < ?of_int 0 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have n': "?n > 0" "?n \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (0::'a) < of_int n &&& (0::'a) \<le> of_int n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(0::'a) < of_int n
(0::'a) \<le> of_int n

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (e + of_int m) / of_int n < of_int 0 + (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "(e + ?m) / ?n \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
\<not> (e + of_int m) / of_int n < of_int 0 + (1::'a)

goal (1 subgoal):
 1. (1::'a) \<le> (e + of_int m) / of_int n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
from mult_right_mono[OF this n'(2)]
[PROOF STATE]
proof (chain)
picking this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n
[PROOF STEP]
have "?n \<le> e + ?m"
[PROOF STATE]
proof (prove)
using this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n

goal (1 subgoal):
 1. of_int n \<le> e + of_int m
[PROOF STEP]
using n'(1)
[PROOF STATE]
proof (prove)
using this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n
(0::'a) < of_int n

goal (1 subgoal):
 1. of_int n \<le> e + of_int m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int m

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int m

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
have "?m \<le> ?n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int m \<le> of_int n - (1::'a)
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. of_int m \<le> of_int n - (1::'a)
[PROOF STEP]
by (metis of_int_1 of_int_diff of_int_le_iff zle_diff1_eq)
[PROOF STATE]
proof (state)
this:
of_int m \<le> of_int n - (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> e + x \<le> e + y) \<Longrightarrow> of_int n \<le> e + (of_int n - (1::'a))
[PROOF STEP]
have "?n \<le> e + ?n - 1"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> e + x \<le> e + y) \<Longrightarrow> of_int n \<le> e + (of_int n - (1::'a))

goal (1 subgoal):
 1. of_int n \<le> e + of_int n - (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int n - (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
with e1
[PROOF STATE]
proof (chain)
picking this:
e < (1::'a)
of_int n \<le> e + of_int n - (1::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
e < (1::'a)
of_int n \<le> e + of_int n - (1::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(e + of_int m) / of_int n < of_int 0 + (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lfloor>(e + of_int m) / of_int n\<rfloor> = 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>r / of_int n\<rfloor> = rhs + 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r / of_int n\<rfloor> = rhs + 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
unfolding rhs_def
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n + 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_der_stack_lt: "k \<in> set (der_stack i\<^sub>0) \<Longrightarrow> k<i\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> set (local.der_stack i\<^sub>0) \<Longrightarrow> k < i\<^sub>0
[PROOF STEP]
apply (induction i\<^sub>0 rule: der_stack.induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < local.the_left i; k \<in> set (local.der_stack i)\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
apply (subst (asm) der_stack.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < local.the_left i; k \<in> set (if local.has_left i then local.the_left i # local.der_stack (local.the_left i) else [])\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>k < local.the_left i; local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
using less_trans the_leftI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
local.has_left ?j \<Longrightarrow> local.the_left ?j < ?j \<and> xs ! local.the_left ?j < xs ! ?j

goal (1 subgoal):
 1. \<And>i. \<lbrakk>k < local.the_left i; local.has_left i; k \<in> set (local.der_stack (local.the_left i))\<rbrakk> \<Longrightarrow> k < i
[PROOF STEP]
by blast


[STATEMENT]
theorem algo_impl_correct': "
  <array_assn int_assn xs xsi>
    all_left_impl xsi
  <\<lambda>lfi. \<exists>\<^sub>Alf. array_assn int_assn xs xsi
        * array_assn (option_assn id_assn) lf lfi
        * \<up>(all_left_spec xs lf)>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <array_assn int_assn xs xsi> all_left_impl xsi <\<lambda>r. \<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf r * \<up> (all_left_spec xs lf)>\<^sub>t
[PROOF STEP]
apply (rule cons_rule[OF _ _ algo_impl_correct[to_hnr, THEN hn_refineD, unfolded autoref_tag_defs]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. array_assn int_assn xs xsi \<Longrightarrow>\<^sub>A hn_ctxt (fst (array_assn int_assn, array_assn int_assn)) ?x2 xsi
 2. \<And>x. hn_ctxt (snd (array_assn int_assn, array_assn int_assn)) ?x2 xsi * (\<exists>\<^sub>Axa. array_assn (option_assn nat_assn) xa x * \<up> (RETURN xa \<le> (SPEC \<circ> all_left_spec) ?x2)) * true \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf x * \<up> (all_left_spec xs lf)) * true
 3. nofail ((SPEC \<circ> all_left_spec) ?x2)
[PROOF STEP]
apply (simp add: hn_ctxt_def, rule ent_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. hn_ctxt (snd (array_assn int_assn, array_assn int_assn)) xs xsi * (\<exists>\<^sub>Axa. array_assn (option_assn nat_assn) xa x * \<up> (RETURN xa \<le> (SPEC \<circ> all_left_spec) xs)) * true \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf x * \<up> (all_left_spec xs lf)) * true
 2. nofail ((SPEC \<circ> all_left_spec) xs)
[PROOF STEP]
by (auto simp: hn_ctxt_def)


[STATEMENT]
lemma rbd_Id_pres: "bd\<^sub>\<R> Id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd\<^sub>\<R> Id = id
[PROOF STEP]
unfolding rbd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bd\<^sub>\<F> \<circ> \<F>) Id = id
[PROOF STEP]
by simp


[STATEMENT]
lemma iffd_iffb_demorgan: "Sup_pres \<phi> \<Longrightarrow> fd\<^sup>-\<^sub>\<F> \<phi> = (fb\<^sup>-\<^sub>\<F> \<circ> \<partial>\<^sub>F) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_pres \<phi> \<Longrightarrow> fd\<^sup>-\<^sub>\<F> \<phi> = (fb\<^sup>-\<^sub>\<F> \<circ> \<partial>\<^sub>F) \<phi>
[PROOF STEP]
by (smt Sup_pres_Inf_pres comp_apply iffb_ifbd_dual iffd_def map_dual_dual)


[STATEMENT]
lemma [iff]: "is_Ref Null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Ref Null
[PROOF STEP]
by (simp add: is_Ref_def2)


[STATEMENT]
lemma \<G>_semantics':
  "\<G> \<phi> w = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<G> \<phi> w = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}
[PROOF STEP]
unfolding \<G>_semantics
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<psi> \<in> subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>} = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}
[PROOF STEP]
by auto


[STATEMENT]
lemma foldl_rule_aux:
  fixes I :: "'\<sigma> \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes initial: "I \<sigma>0 l0"
  assumes step: "!!l1 l2 x \<sigma>. \<lbrakk> l0=l1@x#l2; I \<sigma> (x#l2) \<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2"
  shows "I (foldl f \<sigma>0 l0) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (foldl f \<sigma>0 l0) []
[PROOF STEP]
using initial step
[PROOF STATE]
proof (prove)
using this:
I \<sigma>0 l0
\<lbrakk>l0 = ?l1.0 @ ?x # ?l2.0; I ?\<sigma> (?x # ?l2.0)\<rbrakk> \<Longrightarrow> I (f ?\<sigma> ?x) ?l2.0

goal (1 subgoal):
 1. I (foldl f \<sigma>0 l0) []
[PROOF STEP]
apply (induct l0 arbitrary: \<sigma>0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>0. \<lbrakk>I \<sigma>0 []; \<And>l1 x l2 \<sigma>. \<lbrakk>[] = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 []) []
 2. \<And>a l0 \<sigma>0. \<lbrakk>\<And>\<sigma>0. \<lbrakk>I \<sigma>0 l0; \<And>l1 x l2 \<sigma>. \<lbrakk>l0 = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 l0) []; I \<sigma>0 (a # l0); \<And>l1 x l2 \<sigma>. \<lbrakk>a # l0 = l1 @ x # l2; I \<sigma> (x # l2)\<rbrakk> \<Longrightarrow> I (f \<sigma> x) l2\<rbrakk> \<Longrightarrow> I (foldl f \<sigma>0 (a # l0)) []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in linorder) sorted_wrt_rev_linord [simp] :
  "sorted_wrt (\<ge>) l \<longleftrightarrow> sorted (rev l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) l = sorted (rev l)
[PROOF STEP]
by (simp add: sorted_wrt_rev)


[STATEMENT]
lemma drop_takeWhile:
    assumes "i\<le>length (takeWhile P l)"
    shows "drop i (takeWhile P l) = takeWhile P (drop i l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop i (takeWhile P l) = takeWhile P (drop i l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> length (takeWhile P l)

goal (1 subgoal):
 1. drop i (takeWhile P l) = takeWhile P (drop i l)
[PROOF STEP]
proof (induction l arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<le> length (takeWhile P []) \<Longrightarrow> drop i (takeWhile P []) = takeWhile P (drop i [])
 2. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
i \<le> length (takeWhile P [])

goal (2 subgoals):
 1. \<And>i. i \<le> length (takeWhile P []) \<Longrightarrow> drop i (takeWhile P []) = takeWhile P (drop i [])
 2. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i \<le> length (takeWhile P [])

goal (1 subgoal):
 1. drop i (takeWhile P []) = takeWhile P (drop i [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
drop i (takeWhile P []) = takeWhile P (drop i [])

goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
case (Cons x l)
[PROOF STATE]
proof (state)
this:
?i \<le> length (takeWhile P l) \<Longrightarrow> drop ?i (takeWhile P l) = takeWhile P (drop ?i l)
i \<le> length (takeWhile P (x # l))

goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?i \<le> length (takeWhile P l) \<Longrightarrow> drop ?i (takeWhile P l) = takeWhile P (drop ?i l)
i \<le> length (takeWhile P (x # l))

goal (1 subgoal):
 1. drop i (takeWhile P (x # l)) = takeWhile P (drop i (x # l))
[PROOF STEP]
by (cases i) auto
[PROOF STATE]
proof (state)
this:
drop i (takeWhile P (x # l)) = takeWhile P (drop i (x # l))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ccpo_Sup_mono:
  assumes C: "Complete_Partial_Order.chain (\<le>) A"
    "Complete_Partial_Order.chain (\<le>) B"
  assumes B: "\<forall>x\<in>A. \<exists>y\<in>B. x\<le>y"
  shows "Sup A \<le> Sup B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup A \<le> Sup B
[PROOF STEP]
proof (rule ccpo_Sup_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
assume "x\<in>A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
with B
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>A. \<exists>y\<in>B. x \<le> y
x \<in> A
[PROOF STEP]
obtain y where I: "y\<in>B" and L: "x\<le>y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<exists>y\<in>B. x \<le> y
x \<in> A

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> B; x \<le> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> B
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
note L
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
from I ccpo_Sup_upper
[PROOF STATE]
proof (chain)
picking this:
y \<in> B
\<lbrakk>Complete_Partial_Order.chain (\<le>) ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?A
[PROOF STEP]
have "y\<le>Sup B"
[PROOF STATE]
proof (prove)
using this:
y \<in> B
\<lbrakk>Complete_Partial_Order.chain (\<le>) ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?A

goal (1 subgoal):
 1. y \<le> Sup B
[PROOF STEP]
by (blast intro: C)
[PROOF STATE]
proof (state)
this:
y \<le> Sup B

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<le> Sup B
[PROOF STEP]
show "x\<le>Sup B"
[PROOF STATE]
proof (prove)
using this:
x \<le> Sup B

goal (1 subgoal):
 1. x \<le> Sup B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<le> Sup B

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) A
[PROOF STEP]
qed (rule C)


[STATEMENT]
lemma phl_cons2: "w \<le> x \<Longrightarrow> z \<cdot> y \<le> y \<cdot> w \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> x; z \<cdot> y \<le> y \<cdot> w\<rbrakk> \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x
[PROOF STEP]
using local.order_trans mult_isol
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y

goal (1 subgoal):
 1. \<lbrakk>w \<le> x; z \<cdot> y \<le> y \<cdot> w\<rbrakk> \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x
[PROOF STEP]
by blast


[STATEMENT]
lemma af_letter\<^sub>G_lifted_semantics:
  "\<up>afletter\<^sub>G \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>G \<phi> \<psi> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>afletter\<^sub>G \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>G \<phi> \<psi> \<nu>)
[PROOF STEP]
by (metis af_letter\<^sub>G_lifted_def Rep_inverse af_letter\<^sub>G_def af_letter_congruent Abs_eq)


[STATEMENT]
theorem WF1_general:
  assumes h1: "|~ P \<and> N \<longrightarrow> \<circle>P \<or> \<circle>Q"
      and h2: "|~ P \<and> N \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circle>Q"
      and h3: "\<turnstile> P \<and> N \<longrightarrow> Enabled \<langle>A\<rangle>_v"
      and h4: "|~ P \<and> Unchanged w \<longrightarrow> \<circle>P"
  shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
have "\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)
[PROOF STEP]
proof (rule STL4)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
have "\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v
[PROOF STEP]
by (rule lift_imp_trans[OF h3[THEN STL4] E3])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
hence "\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v

goal (1 subgoal):
 1. \<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
by (auto simp: WeakF_def STL5[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
with ax1[of "TEMP \<diamond>\<langle>A\<rangle>_v"]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>\<diamond>\<langle>A\<rangle>_v \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
show "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>\<diamond>\<langle>A\<rangle>_v \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
hence "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)
[PROOF STEP]
by (simp add: STL5[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
with AA22[OF h1 h2 h4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v) \<longrightarrow> P \<leadsto> Q
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v) \<longrightarrow> P \<leadsto> Q
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem SF2:
  assumes h1: "|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g"
      and h2: "|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B"
      and h3: "\<turnstile> P \<and> Enabled \<langle>M\<rangle>_g \<longrightarrow> Enabled \<langle>A\<rangle>_f"
      and h4: "\<turnstile> \<box>[N \<and> \<not>B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
  shows "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have 1: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
have A: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
                 \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
[PROOF STEP]
unfolding STL6[int_rewrite]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>\<box>[\<not> M]_g
[PROOF STEP]
(* important to do this before STL5 is applied *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>\<box>[\<not> M]_g
[PROOF STEP]
by (auto simp: STL5[int_rewrite] dualization_rew)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
have B: "\<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow>
                 \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))
[PROOF STEP]
by (rule SE2)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from lift_imp_trans[OF A B]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
              \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
[PROOF STEP]
by (simp add: STL5[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g
[PROOF STEP]
have "|~ [N]_f \<longrightarrow> [\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f"
[PROOF STATE]
proof (prove)
using this:
|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g

goal (1 subgoal):
 1. |~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f
[PROOF STEP]
by (auto simp: actrans_def angle_actrans_def)
[PROOF STATE]
proof (state)
this:
|~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
hence "\<turnstile> \<box>[[N]_f]_f \<longrightarrow> \<box>[[\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f]_f"
[PROOF STATE]
proof (prove)
using this:
|~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f

goal (1 subgoal):
 1. \<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f]_f
[PROOF STEP]
by (rule M2)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from lift_imp_trans[OF this ax4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g]_f \<longrightarrow> \<box>[_actrans (N \<and> \<not> B) f]_f
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> \<box>[\<not>M]_g \<longrightarrow> \<box>[N \<and> \<not>B]_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g]_f \<longrightarrow> \<box>[_actrans (N \<and> \<not> B) f]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f
[PROOF STEP]
by (force intro: T4[unlift_rule])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
with h4
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N \<and> \<not> B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f
[PROOF STEP]
have "\<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N \<and> \<not> B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f

goal (1 subgoal):
 1. \<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from STL4_eve[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<diamond>\<box>P
[PROOF STEP]
have "\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)) \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have 2: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have "\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
using h3[THEN STL4_eve, THEN STL4]
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<longrightarrow> \<box>\<diamond>Enabled \<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
by (auto simp: StrongF_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
with E28
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>\<box>?F \<and> \<box>\<diamond>?G \<longrightarrow> \<box>\<diamond>(?F \<and> ?G)
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
have A: "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>?F \<and> \<box>\<diamond>?G \<longrightarrow> \<box>\<diamond>(?F \<and> ?G)
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have B: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from M1[of P f]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>P \<longrightarrow> \<box>[P \<and> \<circle>P]_f
[PROOF STEP]
have "\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>P \<longrightarrow> \<box>[P \<and> \<circle>P]_f

goal (1 subgoal):
 1. \<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (force intro: AA29[unlift_rule])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
hence "\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (rule STL4_eve[OF STL4])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
hence "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (simp add: STL6[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
with AA29[of N f A]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
have B1: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B
[PROOF STEP]
have "|~ \<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B

goal (1 subgoal):
 1. |~ \<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f
[PROOF STEP]
by (auto simp: angle_actrans_sem[unlifted])
[PROOF STATE]
proof (state)
this:
|~ \<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from B1 this[THEN AA25, THEN STL4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have "\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by (rule h1[THEN AA25, THEN STL4])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from A B
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
by (auto simp: StrongF_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_transfer_operator_mono:
  assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
have "AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
by (rule AE_symmetric[OF real_transfer_operator_diff], auto simp add: assms)
[PROOF STATE]
proof (state)
this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
have "AE x in M. real_transfer_operator (\<lambda>x. g x - f x) x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
by (rule real_transfer_operator_pos, auto simp add: assms(1))
[PROOF STATE]
proof (state)
this:
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
have "AE x in M. real_transfer_operator g x - real_transfer_operator f x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma typings_append:
  assumes "CT;\<Gamma> \<turnstile>+ es : Cs"
  and "CT;\<Gamma> \<turnstile> e : C"
  shows "CT;\<Gamma> \<turnstile>+ (es@[e]) : (Cs@[C])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
have "length es = length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length es = length Cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. length es = length Cs
[PROOF STEP]
by(simp_all add:typings_lengths)
[PROOF STATE]
proof (state)
this:
length es = length Cs

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
thus "CT;\<Gamma> \<turnstile>+ (es@[e]) : (Cs@[C])"
[PROOF STATE]
proof (prove)
using this:
length es = length Cs

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length es = length Cs
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
proof(induct "es" "Cs" rule:list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ []:[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ [] : []
[PROOF STEP]
by(simp add:typings_typing.ts_nil)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ [] : []

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ [] : []

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
have "CT;\<Gamma> \<turnstile> e : C"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile> e : C

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ [] : []
CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
show "CT;\<Gamma> \<turnstile>+ ([]@[e]) : ([]@[C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ [] : []
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
[PROOF STEP]
by (auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
fix x xs y ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
assume "length xs = length ys"
      and IH: "\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])"
      and x_xs_typs: "CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)"
      and e_typ: "CT;\<Gamma> \<turnstile> e : C"
[PROOF STATE]
proof (state)
this:
length xs = length ys
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
from x_xs_typs
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)
[PROOF STEP]
have x_typ: "CT;\<Gamma> \<turnstile> x : y" and "CT;\<Gamma> \<turnstile>+ xs : ys"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile> x : y &&& CT;\<Gamma> \<turnstile>+ xs : ys
[PROOF STEP]
by(auto elim:typings.cases)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
with IH e_typ
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile> e : C
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ (xs@[e]) : (ys@[C])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile> e : C
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
with x_typ
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ ((x#xs)@[e]) : ((y#ys)@[C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
by (auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
thus "CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
by(auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_projection_on_eqI:
  fixes  M :: \<open>'a::complex_inner set\<close>
  assumes a1: \<open>closed_csubspace M\<close> and a2: \<open>h - x \<in> orthogonal_complement M\<close> and a3: \<open>x \<in> M\<close>
    and a4: \<open>is_projection_on \<pi> M\<close>
  shows \<open>\<pi> h = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> h = x
[PROOF STEP]
by (meson a1 a2 a3 a4 closed_csubspace.subspace csubspace_is_convex is_projection_on_def smallest_dist_is_ortho smallest_dist_unique)


[STATEMENT]
lemma ani_mult_left_upper_bound:
  "ani(x * y) \<le> ani(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani (x * y) \<le> ani x
[PROOF STEP]
by (simp add: an_mult_left_upper_bound ani_def mult_left_isotone)


[STATEMENT]
lemma ani_omega:
  "ani(x)\<^sup>\<omega> = ani(x) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani x\<^sup>\<omega> = ani x * L
[PROOF STEP]
by (simp add: L_left_zero ani_def mult_L_omega mult_assoc)


[STATEMENT]
lemma get_M_Mshadow_root_preserved4  [simp]:
  "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
   \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x))
   \<Longrightarrow> preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
[PROOF STEP]
apply(cases "cast shadow_root_ptr \<noteq> document_ptr")[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); cast shadow_root_ptr \<noteq> document_ptr\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
 2. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); \<not> cast shadow_root_ptr \<noteq> document_ptr\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
      DocumentMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)


[STATEMENT]
lemma horn_infer1_union:
  "horn.infer1 (\<H>\<^sub>1 \<union> \<H>\<^sub>2) x B = horn.infer1 \<H>\<^sub>1 x B \<union> horn.infer1 \<H>\<^sub>2 x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horn.infer1 (\<H>\<^sub>1 \<union> \<H>\<^sub>2) x B = horn.infer1 \<H>\<^sub>1 x B \<union> horn.infer1 \<H>\<^sub>2 x B
[PROOF STEP]
by (auto simp: horn.infer1_def)