[STATEMENT]
lemma cop_F_CH_CD_on_disjoint:
  assumes "cop_F_closed_inv ds fp"
  assumes "cop_F_range_inv ds fp"
  shows "Xd ` CH fp \<inter> Xd ` (CD_on ds (- RH fp) - fp) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd ` CH fp \<inter> Xd ` (CD_on ds (- Rf CH fp) - fp) = {}
[PROOF STEP]
using %invisible assms CH_range
[PROOF STATE]
proof (prove)
using this:
cop_F_closed_inv ds fp
cop_F_range_inv ds fp
CH ?A \<subseteq> ?A

goal (1 subgoal):
 1. Xd ` CH fp \<inter> Xd ` (CD_on ds (- Rf CH fp) - fp) = {}
[PROOF STEP]
unfolding cop_F_range_inv_def cop_F_closed_inv_def above_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>fp. {b. (x, b) \<in> Pd (Xd x)} \<subseteq> fp
\<forall>x\<in>fp. x \<in> Field (Pd (Xd x)) \<and> Xd x \<in> ds
CH ?A \<subseteq> ?A

goal (1 subgoal):
 1. Xd ` CH fp \<inter> Xd ` (CD_on ds (- Rf CH fp) - fp) = {}
[PROOF STEP]
by (fastforce simp: set_eq_iff mem_CD_on_Cd Cd_greatest greatest_def)


[STATEMENT]
lemma log_floor[simp]: assumes b: "b > 1" and x: "x > 0"
  shows "log_floor b x = \<lfloor>log b x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
obtain y where y: "log_floor b x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. log_floor b x = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
log_floor b x = y

goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
note main = log_floor_sound[OF assms y]
[PROOF STATE]
proof (state)
this:
b ^ y \<le> x
x < b ^ Suc y

goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
from b x
[PROOF STATE]
proof (chain)
picking this:
1 < b
0 < x
[PROOF STEP]
have *: "1 < real_of_int b" "0 < real_of_int (b ^ y)" "0 < real_of_int x"
    and **: "1 < real_of_int b" "0 < real_of_int x" "0 < real_of_int (b ^ Suc y)"
[PROOF STATE]
proof (prove)
using this:
1 < b
0 < x

goal (1 subgoal):
 1. (1 < real_of_int b &&& 0 < real_of_int (b ^ y) &&& 0 < real_of_int x) &&& 1 < real_of_int b &&& 0 < real_of_int x &&& 0 < real_of_int (b ^ Suc y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < real_of_int b
0 < real_of_int (b ^ y)
0 < real_of_int x
1 < real_of_int b
0 < real_of_int x
0 < real_of_int (b ^ Suc y)

goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
unfolding y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int y = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>
[PROOF STEP]
proof (rule sym, rule floor_unique)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)
 2. log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1
[PROOF STEP]
show "real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)
[PROOF STEP]
using main(1)[folded log_le_cancel_iff[OF *, unfolded of_int_le_iff]]
[PROOF STATE]
proof (prove)
using this:
log (real_of_int b) (real_of_int (b ^ y)) \<le> log (real_of_int b) (real_of_int x)

goal (1 subgoal):
 1. real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)
[PROOF STEP]
using log_pow_cancel[of b y] b
[PROOF STATE]
proof (prove)
using this:
log (real_of_int b) (real_of_int (b ^ y)) \<le> log (real_of_int b) (real_of_int x)
\<lbrakk>0 < real_of_int b; real_of_int b \<noteq> 1\<rbrakk> \<Longrightarrow> log (real_of_int b) (real_of_int b ^ y) = real y
1 < b

goal (1 subgoal):
 1. real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (int y) \<le> log (real_of_int b) (real_of_int x)

goal (1 subgoal):
 1. log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1
[PROOF STEP]
show "log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1
[PROOF STEP]
using main(2)[folded log_less_cancel_iff[OF **, unfolded of_int_less_iff]]
[PROOF STATE]
proof (prove)
using this:
log (real_of_int b) (real_of_int x) < log (real_of_int b) (real_of_int (b ^ Suc y))

goal (1 subgoal):
 1. log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1
[PROOF STEP]
using log_pow_cancel[of b "Suc y"] b
[PROOF STATE]
proof (prove)
using this:
log (real_of_int b) (real_of_int x) < log (real_of_int b) (real_of_int (b ^ Suc y))
\<lbrakk>0 < real_of_int b; real_of_int b \<noteq> 1\<rbrakk> \<Longrightarrow> log (real_of_int b) (real_of_int b ^ Suc y) = real (Suc y)
1 < b

goal (1 subgoal):
 1. log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
log (real_of_int b) (real_of_int x) < real_of_int (int y) + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (log_floor b x) = \<lfloor>log (real_of_int b) (real_of_int x)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l2: "eval_ternary_And t1 t2 = TernaryFalse \<Longrightarrow> t1 = TernaryFalse \<or> t2 = TernaryFalse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_ternary_And t1 t2 = TernaryFalse \<Longrightarrow> t1 = TernaryFalse \<or> t2 = TernaryFalse
[PROOF STEP]
using eval_ternary_And.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eval_ternary_And ?x ?xa = ?y; \<lbrakk>?x = TernaryTrue; ?xa = TernaryTrue; ?y = TernaryTrue\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryTrue; ?xa = TernaryFalse; ?y = TernaryFalse\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryFalse; ?xa = TernaryTrue; ?y = TernaryFalse\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryFalse; ?xa = TernaryFalse; ?y = TernaryFalse\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryFalse; ?xa = TernaryUnknown; ?y = TernaryFalse\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryTrue; ?xa = TernaryUnknown; ?y = TernaryUnknown\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryUnknown; ?xa = TernaryFalse; ?y = TernaryFalse\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryUnknown; ?xa = TernaryTrue; ?y = TernaryUnknown\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?x = TernaryUnknown; ?xa = TernaryUnknown; ?y = TernaryUnknown\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. eval_ternary_And t1 t2 = TernaryFalse \<Longrightarrow> t1 = TernaryFalse \<or> t2 = TernaryFalse
[PROOF STEP]
by blast