[STATEMENT]
lemma emp_UNlift01_UNpart1:
assumes l: "length cl = length dl"
and P: "\<And> n. n < length cl \<Longrightarrow> part {..< brn (cl!n)} (P n) \<and> {} \<notin> P n"
and FP: "\<And> n. n < length dl \<Longrightarrow> {} \<notin> F n ` (P n)"
shows "{} \<notin> (UNlift01 cl dl P F) ` (UNpart1 cl dl P)" (is "{} \<notin> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
have R: "?R = UNpart1 dl cl (%n. F n ` (P n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNlift01 cl dl P F ` UNpart1 cl dl P = UNpart1 dl cl (\<lambda>n. F n ` P n)
[PROOF STEP]
apply(rule UNlift01_UNpart1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length cl = length dl
 2. \<And>n. n < length cl \<Longrightarrow> part {..<brn (cl ! n)} (P n) \<and> {} \<notin> P n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length cl = length dl
?n5 < length cl \<Longrightarrow> part {..<brn (cl ! ?n5)} (P ?n5) \<and> {} \<notin> P ?n5
?n5 < length dl \<Longrightarrow> {} \<notin> F ?n5 ` P ?n5

goal (2 subgoals):
 1. length cl = length dl
 2. \<And>n. n < length cl \<Longrightarrow> part {..<brn (cl ! n)} (P n) \<and> {} \<notin> P n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNlift01 cl dl P F ` UNpart1 cl dl P = UNpart1 dl cl (\<lambda>n. F n ` P n)

goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
unfolding R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNpart1 dl cl (\<lambda>n. F n ` P n)
[PROOF STEP]
apply(rule emp_UNpart1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length dl \<Longrightarrow> {} \<notin> F n ` P n
[PROOF STEP]
using FP
[PROOF STATE]
proof (prove)
using this:
?n5 < length dl \<Longrightarrow> {} \<notin> F ?n5 ` P ?n5

goal (1 subgoal):
 1. \<And>n. n < length dl \<Longrightarrow> {} \<notin> F n ` P n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P

goal:
No subgoals!
[PROOF STEP]
qed