[STATEMENT]
lemma lr_appFLv:
  assumes lr: "logical_relation R"
  assumes f: "(\<lambda>i::'i::type. f) \<in> R"
  assumes args: "set args \<subseteq> R"
  shows "appFLv f args \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv f args \<in> R
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv f args \<in> R
[PROOF STEP]
using args
[PROOF STATE]
proof (prove)
using this:
set args \<subseteq> R

goal (1 subgoal):
 1. appFLv f args \<in> R
[PROOF STEP]
proof(induct args rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> R \<Longrightarrow> appFLv f [] \<in> R
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R; set (xs @ [x]) \<subseteq> R\<rbrakk> \<Longrightarrow> appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> R

goal (2 subgoals):
 1. set [] \<subseteq> R \<Longrightarrow> appFLv f [] \<in> R
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R; set (xs @ [x]) \<subseteq> R\<rbrakk> \<Longrightarrow> appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>i. f) \<in> R
set [] \<subseteq> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i. f) \<in> R
set [] \<subseteq> R

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

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R; set (xs @ [x]) \<subseteq> R\<rbrakk> \<Longrightarrow> appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R; set (xs @ [x]) \<subseteq> R\<rbrakk> \<Longrightarrow> appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R
set (xs @ [x]) \<subseteq> R

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R; set (xs @ [x]) \<subseteq> R\<rbrakk> \<Longrightarrow> appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R
set (xs @ [x]) \<subseteq> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R
set (xs @ [x]) \<subseteq> R

goal (1 subgoal):
 1. appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
using lr_l2r(1)[OF _ _ lr, where fs="\<lambda>i. (foldl (\<lambda>f x. appF\<cdot>f\<cdot>(x i)) f xs)" and xs=x]
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> R \<Longrightarrow> appFLv f xs \<in> R
set (xs @ [x]) \<subseteq> R
\<lbrakk>appFLv f xs \<in> R; x \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(appFLv f xs j)\<cdot>(x j)) \<in> R

goal (1 subgoal):
 1. appFLv f (xs @ [x]) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
appFLv f (xs @ [x]) \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma POR_simps [simp]:
  "(ValTT por y) = ValTT"
  "(x por ValTT) = ValTT"
  "(ValFF por ValFF) = ValFF"
  "(ValFF por \<bottom>) = \<bottom>"
  "(ValFF por ValN\<cdot>n) = \<bottom>"
  "(ValFF por ValF\<cdot>f) = \<bottom>"
  "(\<bottom> por ValFF) = \<bottom>"
  "(ValN\<cdot>n por ValFF) = \<bottom>"
  "(ValF\<cdot>f por ValFF) = \<bottom>"
  "(\<bottom> por \<bottom>) = \<bottom>"
  "(\<bottom> por ValN\<cdot>n) = \<bottom>"
  "(\<bottom> por ValF\<cdot>f) = \<bottom>"
  "(ValN\<cdot>n por \<bottom>) = \<bottom>"
  "(ValF\<cdot>f por \<bottom>) = \<bottom>"
  "(ValN\<cdot>m por ValN\<cdot>n) = \<bottom>"
  "(ValN\<cdot>n por ValF\<cdot>f) = \<bottom>"
  "(ValF\<cdot>f por ValN\<cdot>n) = \<bottom>"
  "(ValF\<cdot>f por ValF\<cdot>g) = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((ValTT por y) = ValTT &&& (x por ValTT) = ValTT) &&& (ValFF por ValFF) = ValFF &&& (ValFF por \<bottom>) = \<bottom>) &&& ((ValFF por ValN\<cdot>n) = \<bottom> &&& (ValFF por ValF\<cdot>f) = \<bottom>) &&& (\<bottom> por ValFF) = \<bottom> &&& (ValN\<cdot>n por ValFF) = \<bottom> &&& (ValF\<cdot>f por ValFF) = \<bottom>) &&& (((\<bottom> por \<bottom>) = \<bottom> &&& (\<bottom> por ValN\<cdot>n) = \<bottom>) &&& (\<bottom> por ValF\<cdot>f) = \<bottom> &&& (ValN\<cdot>n por \<bottom>) = \<bottom>) &&& ((ValF\<cdot>f por \<bottom>) = \<bottom> &&& (ValN\<cdot>m por ValN\<cdot>n) = \<bottom>) &&& (ValN\<cdot>n por ValF\<cdot>f) = \<bottom> &&& (ValF\<cdot>f por ValN\<cdot>n) = \<bottom> &&& (ValF\<cdot>f por ValF\<cdot>g) = \<bottom>
[PROOF STEP]
unfolding por_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((if ValTT = ValTT then ValTT else if y = ValTT then ValTT else if ValTT = ValFF \<and> y = ValFF then ValFF else \<bottom>) = ValTT &&& (if x = ValTT then ValTT else if ValTT = ValTT then ValTT else if x = ValFF \<and> ValTT = ValFF then ValFF else \<bottom>) = ValTT) &&& (if ValFF = ValTT then ValTT else if ValFF = ValTT then ValTT else if ValFF = ValFF \<and> ValFF = ValFF then ValFF else \<bottom>) = ValFF &&& (if ValFF = ValTT then ValTT else if \<bottom> = ValTT then ValTT else if ValFF = ValFF \<and> \<bottom> = ValFF then ValFF else \<bottom>) = \<bottom>) &&& ((if ValFF = ValTT then ValTT else if ValN\<cdot>n = ValTT then ValTT else if ValFF = ValFF \<and> ValN\<cdot>n = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValFF = ValTT then ValTT else if ValF\<cdot>f = ValTT then ValTT else if ValFF = ValFF \<and> ValF\<cdot>f = ValFF then ValFF else \<bottom>) = \<bottom>) &&& (if \<bottom> = ValTT then ValTT else if ValFF = ValTT then ValTT else if \<bottom> = ValFF \<and> ValFF = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValN\<cdot>n = ValTT then ValTT else if ValFF = ValTT then ValTT else if ValN\<cdot>n = ValFF \<and> ValFF = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValF\<cdot>f = ValTT then ValTT else if ValFF = ValTT then ValTT else if ValF\<cdot>f = ValFF \<and> ValFF = ValFF then ValFF else \<bottom>) = \<bottom>) &&& (((if \<bottom> = ValTT then ValTT else if \<bottom> = ValTT then ValTT else if \<bottom> = ValFF \<and> \<bottom> = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if \<bottom> = ValTT then ValTT else if ValN\<cdot>n = ValTT then ValTT else if \<bottom> = ValFF \<and> ValN\<cdot>n = ValFF then ValFF else \<bottom>) = \<bottom>) &&& (if \<bottom> = ValTT then ValTT else if ValF\<cdot>f = ValTT then ValTT else if \<bottom> = ValFF \<and> ValF\<cdot>f = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValN\<cdot>n = ValTT then ValTT else if \<bottom> = ValTT then ValTT else if ValN\<cdot>n = ValFF \<and> \<bottom> = ValFF then ValFF else \<bottom>) = \<bottom>) &&& ((if ValF\<cdot>f = ValTT then ValTT else if \<bottom> = ValTT then ValTT else if ValF\<cdot>f = ValFF \<and> \<bottom> = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValN\<cdot>m = ValTT then ValTT else if ValN\<cdot>n = ValTT then ValTT else if ValN\<cdot>m = ValFF \<and> ValN\<cdot>n = ValFF then ValFF else \<bottom>) = \<bottom>) &&& (if ValN\<cdot>n = ValTT then ValTT else if ValF\<cdot>f = ValTT then ValTT else if ValN\<cdot>n = ValFF \<and> ValF\<cdot>f = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValF\<cdot>f = ValTT then ValTT else if ValN\<cdot>n = ValTT then ValTT else if ValF\<cdot>f = ValFF \<and> ValN\<cdot>n = ValFF then ValFF else \<bottom>) = \<bottom> &&& (if ValF\<cdot>f = ValTT then ValTT else if ValF\<cdot>g = ValTT then ValTT else if ValF\<cdot>f = ValFF \<and> ValF\<cdot>g = ValFF then ValFF else \<bottom>) = \<bottom>
[PROOF STEP]
by simp_all


[STATEMENT]
lemma POR_sym: "(x por y) = (y por x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x por y) = (y por x)
[PROOF STEP]
unfolding por_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = ValTT then ValTT else if y = ValTT then ValTT else if x = ValFF \<and> y = ValFF then ValFF else \<bottom>) = (if y = ValTT then ValTT else if x = ValTT then ValTT else if y = ValFF \<and> x = ValFF then ValFF else \<bottom>)
[PROOF STEP]
by simp


[STATEMENT]
lemma ValTT_below_iff [simp]: "ValTT \<sqsubseteq> x \<longleftrightarrow> x = ValTT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ValTT \<sqsubseteq> x) = (x = ValTT)
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma ValFF_below_iff [simp]: "ValFF \<sqsubseteq> x \<longleftrightarrow> x = ValFF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ValFF \<sqsubseteq> x) = (x = ValFF)
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma monofun_por: "monofun (\<lambda>x. x por y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monofun (\<lambda>x. x por y)
[PROOF STEP]
unfolding por_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monofun (\<lambda>x. if x = ValTT then ValTT else if y = ValTT then ValTT else if x = ValFF \<and> y = ValFF then ValFF else \<bottom>)
[PROOF STEP]
by (rule monofunI) auto


[STATEMENT]
lemma mic2mic: "max_in_chain i Y \<Longrightarrow> max_in_chain i (\<lambda>i. f (Y i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_in_chain i Y \<Longrightarrow> max_in_chain i (\<lambda>i. f (Y i))
[PROOF STEP]
unfolding max_in_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<ge>i. Y i = Y j \<Longrightarrow> \<forall>j\<ge>i. f (Y i) = f (Y j)
[PROOF STEP]
by simp


[STATEMENT]
lemma cont_por1: "cont (\<lambda>x. x por y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. x por y)
[PROOF STEP]
apply (rule contI2[OF monofun_por])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (case_tac "Lub Y")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); Lub Y = \<bottom>\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); Lub Y = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); Lub Y = ValTT\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); Lub Y = ValFF\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); Lub Y = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> ((\<Squnion>i. Y i) por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 4. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (cases y)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>; y = \<bottom>\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>; y = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>; y = ValTT\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>; y = ValFF\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = \<bottom>; y = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (\<bottom> por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 6. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 7. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 8. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 9. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 3. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (cases y)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun; y = \<bottom>\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y cfun cfuna. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun; y = ValF\<cdot>cfuna\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun; y = ValTT\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun; y = ValFF\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y cfun nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValF\<cdot>cfun; y = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValF\<cdot>cfun por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 6. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 7. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 8. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (frule compact_imp_max_in_chain)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT\<rbrakk> \<Longrightarrow> compact (\<Squnion>i. Y i)
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; \<exists>i. max_in_chain i Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 3. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; \<exists>i. max_in_chain i Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (frule mic2mic[where f="\<lambda>x. x por y"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (\<Squnion>i. Y i por y) = ValTT
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (subst iffD1[OF maxinch_is_thelub])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. Y i por y)
 2. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> max_in_chain (?i18 Y i) (\<lambda>i. Y i por y)
 3. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (Y (?i18 Y i) por y) = ValTT
 4. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValTT; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (Y i por y) = ValTT
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (simp_all add: maxinch_is_thelub)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (frule compact_imp_max_in_chain)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF\<rbrakk> \<Longrightarrow> compact (\<Squnion>i. Y i)
 2. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; \<exists>i. max_in_chain i Y\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; \<exists>i. max_in_chain i Y\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (frule mic2mic[where f="\<lambda>x. x por y"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (subst iffD1[OF maxinch_is_thelub])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. Y i por y)
 2. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> max_in_chain (?i29 Y i) (\<lambda>i. Y i por y)
 3. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (Y (?i29 Y i) por y)
 4. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y i. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValFF; max_in_chain i Y; max_in_chain i (\<lambda>i. Y i por y)\<rbrakk> \<Longrightarrow> (ValFF por y) \<sqsubseteq> (Y i por y)
 2. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (simp_all add: maxinch_is_thelub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply (cases y)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat; y = \<bottom>\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 2. \<And>Y nat cfun. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat; y = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 3. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat; y = ValTT\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 4. \<And>Y nat. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat; y = ValFF\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
 5. \<And>Y nat nata. \<lbrakk>chain Y; chain (\<lambda>i. Y i por y); (\<Squnion>x. Y x) = ValN\<cdot>nat; y = ValN\<cdot>nata\<rbrakk> \<Longrightarrow> (ValN\<cdot>nat por y) \<sqsubseteq> (\<Squnion>i. Y i por y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cont_por[cont2cont, simp]:
  assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)"
  shows "cont (\<lambda>x. f x por g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. f x por g x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cont (\<lambda>x. f x por g x)
[PROOF STEP]
have A: "\<And>f y. cont f \<Longrightarrow> cont (\<lambda>x. f x por y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y. cont f \<Longrightarrow> cont (\<lambda>x. f x por y)
[PROOF STEP]
by (rule cont_apply) (simp_all add: cont_por1)
[PROOF STATE]
proof (state)
this:
cont ?f \<Longrightarrow> cont (\<lambda>x. ?f x por ?y)

goal (1 subgoal):
 1. cont (\<lambda>x. f x por g x)
[PROOF STEP]
from A[OF f] A[OF g]
[PROOF STATE]
proof (chain)
picking this:
cont (\<lambda>x. f x por ?y)
cont (\<lambda>x. g x por ?y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>x. f x por ?y)
cont (\<lambda>x. g x por ?y)

goal (1 subgoal):
 1. cont (\<lambda>x. f x por g x)
[PROOF STEP]
by (auto simp: cont_por1 POR_sym intro: cont_apply[OF f])
[PROOF STATE]
proof (state)
this:
cont (\<lambda>x. f x por g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adm_POR_base_lf_rep:
  "adm (\<lambda>x. x \<in> POR_base_lf_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_base_lf_rep r)
[PROOF STEP]
unfolding POR_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f One = \<bottom>} \<union> {f. f Two = \<bottom>}))
[PROOF STEP]
using adm_below_monic_exists[OF _ below_monic_fun_K[where f="ValN"], where P="\<lambda>_. True", simplified]
[PROOF STATE]
proof (prove)
using this:
adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValN\<cdot>y))

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f One = \<bottom>} \<union> {f. f Two = \<bottom>}))
[PROOF STEP]
by (auto intro!: adm_disj simp: cont_fun)


[STATEMENT]
lemma mono_POR_base_lf_rep:
  "mono POR_base_lf_rep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono POR_base_lf_rep
[PROOF STEP]
unfolding POR_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>(mR, pR). {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f One = \<bottom>} \<union> {f. f Two = \<bottom>})
[PROOF STEP]
by (blast intro!: monoI)


[STATEMENT]
lemma adm_fn:
  shows "adm (\<lambda>x. x \<in> fn_lf_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> fn_lf_rep r)
[PROOF STEP]
unfolding fn_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<lambda>i. ValF\<cdot>(fs i) |fs. \<forall>xs\<in>unlr (undual mR). (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr pR}))
[PROOF STEP]
using adm_below_monic_exists[OF _ below_monic_fun_K[where f="ValF"], where P="\<lambda>_. True", simplified]
[PROOF STATE]
proof (prove)
using this:
adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValF\<cdot>y))

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<lambda>i. ValF\<cdot>(fs i) |fs. \<forall>xs\<in>unlr (undual mR). (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr pR}))
[PROOF STEP]
apply (clarsimp simp: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValF\<cdot>y)) \<Longrightarrow> adm (\<lambda>x. \<exists>fs. x = (\<lambda>i. ValF\<cdot>(fs i)) \<and> (\<forall>xs\<in>unlr (undual (fst r)). (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (snd r)))
[PROOF STEP]
apply (rule adm_below_monic_exists)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValF\<cdot>y)) \<Longrightarrow> adm (\<lambda>y. \<forall>xs\<in>unlr (undual (fst r)). (\<lambda>j. y j\<cdot>(xs j)) \<in> unlr (snd r))
 2. adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValF\<cdot>y)) \<Longrightarrow> below_monic (\<lambda>y i. ValF\<cdot>(y i))
 3. adm (\<lambda>x. \<exists>y. x = (\<lambda>_. ValF\<cdot>y)) \<Longrightarrow> cont (\<lambda>y i. ValF\<cdot>(y i))
[PROOF STEP]
apply (auto simp: cont_fun below_monic_indexed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono_fn_lf_rep:
  "mono fn_lf_rep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono fn_lf_rep
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> fn_lf_rep x \<subseteq> fn_lf_rep y
[PROOF STEP]
fix x y :: "('a \<Rightarrow> ValD) admS dual \<times> ('a \<Rightarrow> ValD) admS"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> fn_lf_rep x \<subseteq> fn_lf_rep y
[PROOF STEP]
obtain x1 x2 y1 y2 where [simp]: "x = (x1, x2)" "y = (y1, y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 y1 y2. \<lbrakk>x = (x1, x2); y = (y1, y2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x, cases y)
[PROOF STATE]
proof (state)
this:
x = (x1, x2)
y = (y1, y2)

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> fn_lf_rep x \<subseteq> fn_lf_rep y
[PROOF STEP]
assume "x \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> fn_lf_rep x \<subseteq> fn_lf_rep y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> y
[PROOF STEP]
show "fn_lf_rep x \<subseteq> fn_lf_rep y"
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. fn_lf_rep x \<subseteq> fn_lf_rep y
[PROOF STEP]
by (simp add: fn_lf_rep_def) (use dual_less_eq_iff less_eq_admS_def in blast)
[PROOF STATE]
proof (state)
this:
fn_lf_rep x \<subseteq> fn_lf_rep y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma admS_POR_lf [intro, simp]:
  "POR_lf_rep r \<in> admS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. POR_lf_rep r \<in> admS
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bottom> \<in> POR_lf_rep r
 2. adm (\<lambda>x. x \<in> POR_lf_rep r)
[PROOF STEP]
show "\<bottom> \<in> POR_lf_rep r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> POR_lf_rep r
[PROOF STEP]
unfolding POR_lf_rep_def POR_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> (case r of (mR, pR) \<Rightarrow> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f One = \<bottom>} \<union> {f. f Two = \<bottom>}) \<union> fn_lf_rep r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bottom> \<in> POR_lf_rep r

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_lf_rep r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_lf_rep r)
[PROOF STEP]
show "adm (\<lambda>x. x \<in> POR_lf_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_lf_rep r)
[PROOF STEP]
unfolding POR_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_base_lf_rep r \<union> fn_lf_rep r)
[PROOF STEP]
using adm_POR_base_lf_rep[of r] adm_fn[of r]
[PROOF STATE]
proof (prove)
using this:
adm (\<lambda>x. x \<in> POR_base_lf_rep r)
adm (\<lambda>x. x \<in> fn_lf_rep r)

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> POR_base_lf_rep r \<union> fn_lf_rep r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adm (\<lambda>x. x \<in> POR_lf_rep r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_POR_lf:
  "mono POR_lf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono POR_lf
[PROOF STEP]
apply (rule monoI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> POR_lf x \<le> POR_lf y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> POR_lf_rep x \<subseteq> POR_lf_rep y
[PROOF STEP]
unfolding POR_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> POR_base_lf_rep x \<union> fn_lf_rep x \<subseteq> POR_base_lf_rep y \<union> fn_lf_rep y
[PROOF STEP]
using mono_fn_lf_rep mono_POR_base_lf_rep
[PROOF STATE]
proof (prove)
using this:
mono fn_lf_rep
mono POR_base_lf_rep

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> POR_base_lf_rep x \<union> fn_lf_rep x \<subseteq> POR_base_lf_rep y \<union> fn_lf_rep y
[PROOF STEP]
apply (blast dest: monoD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_inv_POR_lf:
  assumes "eRSV e R' S'"
  shows "eRSV (ValD_copy_rec\<cdot>e) (dual (POR_lf (dual S', undual R'))) (POR_lf (R', S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eRSV (ValD_copy_rec\<cdot>e) (dual (POR_lf (dual S', undual R'))) (POR_lf (R', S'))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eRSV (ValD_copy_rec\<cdot>e) (dual (POR_lf (dual S', undual R'))) (POR_lf (R', S'))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> POR_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_lf_rep (R', S')
[PROOF STEP]
apply (simp add: POR_lf_rep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> POR_base_lf_rep (dual S', undual R') \<or> d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. d \<in> POR_base_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
 2. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. d \<in> POR_base_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S')
 2. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (auto simp: POR_base_lf_rep_def eta_cfun cfcomp1 cfun_eq_iff)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> POR_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eRSV e R' S'

goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (clarsimp simp: fn_lf_rep_def eta_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> \<exists>fsa. (\<lambda>x. ValF\<cdot>(cfun_map\<cdot>e\<cdot>e\<cdot>(fs x))) = (\<lambda>i. ValF\<cdot>(fsa i)) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. fsa j\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply (simp add: cfcomp1 cfun_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> \<exists>fsa. (\<lambda>x. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs x\<cdot>(e\<cdot>xa)))) = (\<lambda>i. ValF\<cdot>(fsa i)) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. fsa j\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply (rule_tac x="\<lambda>i. \<Lambda> xa. e\<cdot>(fs i\<cdot>(e\<cdot>xa))" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> (\<lambda>x. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs x\<cdot>(e\<cdot>xa)))) = (\<lambda>i. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs i\<cdot>(e\<cdot>xa)))) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. (\<Lambda> xa. e\<cdot>(fs j\<cdot>(e\<cdot>xa)))\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PORI [intro, simp]:
  "(\<lambda>i. ValTT) \<in> unlr POR.delta"
  "(\<lambda>i. ValFF) \<in> unlr POR.delta"
  "(\<lambda>i. ValN\<cdot>n) \<in> unlr POR.delta"
  "f One = \<bottom> \<Longrightarrow> f \<in> unlr POR.delta"
  "f Two = \<bottom> \<Longrightarrow> f \<in> unlr POR.delta"
  "\<lbrakk> \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> unlr POR.delta \<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> unlr POR.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>i. ValTT) \<in> unlr POR.delta &&& (\<lambda>i. ValFF) \<in> unlr POR.delta &&& (\<lambda>i. ValN\<cdot>n) \<in> unlr POR.delta) &&& (f One = \<bottom> \<Longrightarrow> f \<in> unlr POR.delta) &&& (f Two = \<bottom> \<Longrightarrow> f \<in> unlr POR.delta) &&& ((\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> unlr POR.delta)
[PROOF STEP]
by (subst POR.delta_sol, simp, subst POR_lf_rep_def,
      fastforce simp: POR_base_lf_rep_def fn_lf_rep_def eta_cfun cfcomp1)+


[STATEMENT]
lemma PORE:
  "\<lbrakk> a \<in> unlr POR.delta;
     (a = (\<lambda>i. ValTT) \<Longrightarrow> P);
     (a = (\<lambda>i. ValFF) \<Longrightarrow> P);
     (\<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P);
     (a One = \<bottom> \<Longrightarrow> P);
     (a Two = \<bottom> \<Longrightarrow> P);
     (\<And>fs. \<lbrakk> a = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> unlr POR.delta \<rbrakk> \<Longrightarrow> P)
   \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> unlr POR.delta; a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a One = \<bottom> \<Longrightarrow> P; a Two = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (subst (asm) POR.delta_sol)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> unlr (POR_lf (dual POR.delta, POR.delta)); a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a One = \<bottom> \<Longrightarrow> P; a Two = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> POR_lf_rep (dual POR.delta, POR.delta); a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a One = \<bottom> \<Longrightarrow> P; a Two = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (subst (asm) POR_lf_rep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> POR_base_lf_rep (dual POR.delta, POR.delta) \<union> fn_lf_rep (dual POR.delta, POR.delta); a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a One = \<bottom> \<Longrightarrow> P; a Two = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (fastforce simp: POR_base_lf_rep_def fn_lf_rep_def eta_cfun)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma POR_strict_appI:
  assumes "xs \<in> unlr POR.delta"
  assumes "\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta"
  shows "(\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in> unlr POR.delta
?xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(?xs j)) \<in> unlr POR.delta

goal (1 subgoal):
 1. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
by - (erule PORE; simp)


[STATEMENT]
lemma logical_relation_POR:
  "logical_relation (unlr POR.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. logical_relation (unlr POR.delta)
[PROOF STEP]
apply (rule logical_relationI)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr POR.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 9. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
(* Strict application *)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr POR.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 9. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr POR.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 9. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (cut_tac fs="\<lambda>i. appF\<cdot>(fs i)" and xs=xs in POR_strict_appI)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> xs \<in> unlr POR.delta
 2. \<And>fs xs xsa. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta; xsa \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xsa j)) \<in> unlr POR.delta
 3. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta; (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr POR.delta
 4. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr POR.delta
 6. \<And>fs. (\<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 9. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 10. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
A total of 11 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>fs xs xsa. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta; xsa \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xsa j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 4. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (auto elim: PORE)[1]
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
(* FIXME fixD *)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (erule PORE)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>xs. xs = (\<lambda>i. ValTT) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>xs. xs = (\<lambda>i. ValFF) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>xs n. xs = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 4. \<And>xs. xs One = \<bottom> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs Two = \<bottom> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs fs. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr POR.delta
 7. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 9. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 10. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
A total of 11 subgoals...
[PROOF STEP]
apply (simp_all add: fixD_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. fix\<cdot>(fs j)) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (subst fix_argument_promote_fun)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<mu> x. (\<lambda>xa. fs xa\<cdot>(x xa))) \<in> unlr POR.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (rule_tac F="\<Lambda> f. (\<lambda>x. fs x\<cdot>(f x))" in fix_ind)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> adm (\<lambda>a. a \<in> unlr POR.delta)
 2. \<And>xs fs. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> \<bottom> \<in> unlr POR.delta
 3. \<And>xs fs x. \<lbrakk>xs = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta; x \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. fs x\<cdot>(f x)))\<cdot>x \<in> unlr POR.delta
 4. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 6. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 7. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 8. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (simp_all split: nat.split add: cont_fun)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr POR.delta; xs \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr POR.delta
 2. \<And>cs ts es. \<lbrakk>cs \<in> unlr POR.delta; ts \<in> unlr POR.delta; es \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr POR.delta
 3. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr POR.delta
 4. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr POR.delta
 5. \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr POR.delta
[PROOF STEP]
apply (auto elim: PORE simp: cond_def isZero_def pred_def succ_def eta_cfun split: nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PCF_consts_rel_POR:
  "PCF_consts_rel (unlr POR.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_consts_rel (unlr POR.delta)
[PROOF STEP]
by (rule PCF_consts_relI) simp_all


[STATEMENT]
lemma PCF_lr_POR_delta: "PCF_lr (unlr POR.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_lr (unlr POR.delta)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_lr (unlr POR.delta)
[PROOF STEP]
using logical_relation_POR PCF_consts_rel_POR
[PROOF STATE]
proof (prove)
using this:
logical_relation (unlr POR.delta)
PCF_consts_rel (unlr POR.delta)

goal (1 subgoal):
 1. PCF_lr (unlr POR.delta)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma lr_POR_arg1_rel: "POR_arg1_rel \<in> unlr POR.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. POR_arg1_rel \<in> unlr POR.delta
[PROOF STEP]
unfolding POR_arg1_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of One \<Rightarrow> ValTT | Two \<Rightarrow> \<bottom> | Three \<Rightarrow> ValFF) \<in> unlr POR.delta
[PROOF STEP]
by auto


[STATEMENT]
lemma lr_POR_arg2_rel: "POR_arg2_rel \<in> unlr POR.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. POR_arg2_rel \<in> unlr POR.delta
[PROOF STEP]
unfolding POR_arg2_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of One \<Rightarrow> \<bottom> | Two \<Rightarrow> ValTT | Three \<Rightarrow> ValFF) \<in> unlr POR.delta
[PROOF STEP]
by auto


[STATEMENT]
lemma lr_POR_result_rel: "POR_result_rel \<notin> unlr POR.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. POR_result_rel \<notin> unlr POR.delta
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. POR_result_rel \<notin> unlr POR.delta
[PROOF STEP]
unfolding POR_result_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) \<notin> unlr POR.delta
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) \<in> unlr POR.delta \<Longrightarrow> False
[PROOF STEP]
apply (erule PORE)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = (\<lambda>i. ValTT) \<Longrightarrow> False
 2. (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = (\<lambda>i. ValFF) \<Longrightarrow> False
 3. \<And>n. (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> False
 4. (case One of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = \<bottom> \<Longrightarrow> False
 5. (case Two of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = \<bottom> \<Longrightarrow> False
 6. \<And>fs. \<lbrakk>(\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT) = (\<lambda>i. ValF\<cdot>(fs i)); \<And>xs. xs \<in> unlr POR.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr POR.delta\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto iff: fun_eq_iff split: Three.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem POR_sat:
  "appFLv (ValF\<cdot>(\<Lambda> x. ValF\<cdot>(\<Lambda> y. x por y))) [POR_arg1_rel, POR_arg2_rel] = POR_result_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv (ValF\<cdot>(\<Lambda> x. ValF\<cdot>(\<Lambda> y. x por y))) [POR_arg1_rel, POR_arg2_rel] = POR_result_rel
[PROOF STEP]
unfolding POR_arg1_rel_def POR_arg2_rel_def POR_result_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv (ValF\<cdot>(\<Lambda> x. ValF\<cdot>(\<Lambda> y. x por y))) [\<lambda>i. case i of One \<Rightarrow> ValTT | Two \<Rightarrow> \<bottom> | Three \<Rightarrow> ValFF, \<lambda>i. case i of One \<Rightarrow> \<bottom> | Two \<Rightarrow> ValTT | Three \<Rightarrow> ValFF] = (\<lambda>i. case i of Three \<Rightarrow> ValFF | _ \<Rightarrow> ValTT)
[PROOF STEP]
by (simp add: fun_eq_iff split: Three.splits)


[STATEMENT]
theorem POR_is_not_definable:
  shows "\<not>(\<exists>f. definable f \<and> appFLv f [POR_arg1_rel, POR_arg2_rel] = POR_result_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>f. definable f \<and> appFLv f [POR_arg1_rel, POR_arg2_rel] = POR_result_rel
[PROOF STEP]
apply (rule not_definable[where R="unlr POR.delta"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PCF_lr (unlr POR.delta)
 2. set [POR_arg1_rel, POR_arg2_rel] \<subseteq> unlr POR.delta
 3. POR_result_rel \<notin> unlr POR.delta
[PROOF STEP]
using lr_POR_arg1_rel lr_POR_arg2_rel lr_POR_result_rel PCF_lr_POR_delta
[PROOF STATE]
proof (prove)
using this:
POR_arg1_rel \<in> unlr POR.delta
POR_arg2_rel \<in> unlr POR.delta
POR_result_rel \<notin> unlr POR.delta
PCF_lr (unlr POR.delta)

goal (3 subgoals):
 1. PCF_lr (unlr POR.delta)
 2. set [POR_arg1_rel, POR_arg2_rel] \<subseteq> unlr POR.delta
 3. POR_result_rel \<notin> unlr POR.delta
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma plotkin_exists_simps [simp]:
  "plotkin_exists \<bottom> = \<bottom>"
  "plotkin_exists (ValF\<cdot>\<bottom>) = \<bottom>"
  "plotkin_exists (ValF\<cdot>(\<Lambda> _. ValFF)) = ValFF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plotkin_exists \<bottom> = \<bottom> &&& plotkin_exists (ValF\<cdot>\<bottom>) = \<bottom> &&& plotkin_exists (ValF\<cdot>(\<Lambda> uu_. ValFF)) = ValFF
[PROOF STEP]
unfolding plotkin_exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if appF\<cdot>\<bottom>\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>\<bottom>\<cdot>n = ValTT then ValTT else \<bottom>) = \<bottom> &&& (if appF\<cdot>(ValF\<cdot>\<bottom>)\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(ValF\<cdot>\<bottom>)\<cdot>n = ValTT then ValTT else \<bottom>) = \<bottom> &&& (if appF\<cdot>(ValF\<cdot>(\<Lambda> uu_. ValFF))\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(ValF\<cdot>(\<Lambda> uu_. ValFF))\<cdot>n = ValTT then ValTT else \<bottom>) = ValFF
[PROOF STEP]
by simp_all


[STATEMENT]
lemma plotkin_exists_tt [simp]:
  "appF\<cdot>f\<cdot>(ValN\<cdot>n) = ValTT \<Longrightarrow> plotkin_exists f = ValTT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appF\<cdot>f\<cdot>(ValN\<cdot>n) = ValTT \<Longrightarrow> plotkin_exists f = ValTT
[PROOF STEP]
unfolding plotkin_exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appF\<cdot>f\<cdot>(ValN\<cdot>n) = ValTT \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) = ValTT
[PROOF STEP]
using monofun_cfun_arg[where f="appF\<cdot>f" and x="\<bottom>"]
[PROOF STATE]
proof (prove)
using this:
\<bottom> \<sqsubseteq> ?y \<Longrightarrow> appF\<cdot>f\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>f\<cdot>?y

goal (1 subgoal):
 1. appF\<cdot>f\<cdot>(ValN\<cdot>n) = ValTT \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) = ValTT
[PROOF STEP]
by auto


[STATEMENT]
lemma monofun_pe:
  "monofun plotkin_exists"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monofun plotkin_exists
[PROOF STEP]
proof(rule monofunI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
assume fg: "(f::ValD) \<sqsubseteq> g"
[PROOF STATE]
proof (state)
this:
f \<sqsubseteq> g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
let ?goal = "plotkin_exists f \<sqsubseteq> plotkin_exists g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
assume fbot: "appF\<cdot>f\<cdot>\<bottom> = ValFF"
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
with fg
[PROOF STATE]
proof (chain)
picking this:
f \<sqsubseteq> g
appF\<cdot>f\<cdot>\<bottom> = ValFF
[PROOF STEP]
have "appF\<cdot>g\<cdot>\<bottom> = ValFF"
[PROOF STATE]
proof (prove)
using this:
f \<sqsubseteq> g
appF\<cdot>f\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>\<bottom> = ValFF
[PROOF STEP]
using monofun_cfun[where f="appF\<cdot>f" and g="appF\<cdot>g" and x="\<bottom>"]
[PROOF STATE]
proof (prove)
using this:
f \<sqsubseteq> g
appF\<cdot>f\<cdot>\<bottom> = ValFF
\<lbrakk>appF\<cdot>f \<sqsubseteq> appF\<cdot>g; \<bottom> \<sqsubseteq> ?y\<rbrakk> \<Longrightarrow> appF\<cdot>f\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>g\<cdot>?y

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>\<bottom> = ValFF
[PROOF STEP]
by (simp add: monofun_cfun_arg)
[PROOF STATE]
proof (state)
this:
appF\<cdot>g\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
with fbot
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>\<bottom> = ValFF
appF\<cdot>g\<cdot>\<bottom> = ValFF
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>\<bottom> = ValFF
appF\<cdot>g\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. plotkin_exists f \<sqsubseteq> plotkin_exists g
[PROOF STEP]
by (simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
assume efn: "\<exists>n. appF\<cdot>f\<cdot>n = ValTT"
[PROOF STATE]
proof (state)
this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT
[PROOF STEP]
obtain n where fn: "appF\<cdot>f\<cdot>n = ValTT"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. (\<And>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>n = ValTT
[PROOF STEP]
have fbot: "appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
using monofun_cfun_arg[where f="appF\<cdot>f" and x="\<bottom>" and y="n"]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>n = ValTT
\<bottom> \<sqsubseteq> n \<Longrightarrow> appF\<cdot>f\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>f\<cdot>n

goal (1 subgoal):
 1. appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
from fg
[PROOF STATE]
proof (chain)
picking this:
f \<sqsubseteq> g
[PROOF STEP]
have "appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n"
[PROOF STATE]
proof (prove)
using this:
f \<sqsubseteq> g

goal (1 subgoal):
 1. appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n
[PROOF STEP]
using monofun_cfun_arg[OF fg, where f=appF]
[PROOF STATE]
proof (prove)
using this:
f \<sqsubseteq> g
appF\<cdot>f \<sqsubseteq> appF\<cdot>g

goal (1 subgoal):
 1. appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n
[PROOF STEP]
by (simp only: cfun_below_iff)
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
with fn
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>n = ValTT
appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n
[PROOF STEP]
have gn: "appF\<cdot>g\<cdot>n = ValTT"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>n = ValTT
appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>n = ValTT
[PROOF STEP]
using ValD.nchotomy[where y="appF\<cdot>g\<cdot>\<bottom>"]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>n = ValTT
appF\<cdot>f\<cdot>n \<sqsubseteq> appF\<cdot>g\<cdot>n
appF\<cdot>g\<cdot>\<bottom> = \<bottom> \<or> (\<exists>cfun. appF\<cdot>g\<cdot>\<bottom> = ValF\<cdot>cfun) \<or> appF\<cdot>g\<cdot>\<bottom> = ValTT \<or> appF\<cdot>g\<cdot>\<bottom> = ValFF \<or> (\<exists>nat. appF\<cdot>g\<cdot>\<bottom> = ValN\<cdot>nat)

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>n = ValTT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
appF\<cdot>g\<cdot>n = ValTT

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>g\<cdot>n = ValTT
[PROOF STEP]
have gbot: "appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>g\<cdot>n = ValTT

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
using monofun_cfun_arg[where f="appF\<cdot>g" and x="\<bottom>" and y="n"]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>g\<cdot>n = ValTT
\<bottom> \<sqsubseteq> n \<Longrightarrow> appF\<cdot>g\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>g\<cdot>n

goal (1 subgoal):
 1. appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
from fn gn fbot gbot
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>n = ValTT
appF\<cdot>g\<cdot>n = ValTT
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>n = ValTT
appF\<cdot>g\<cdot>n = ValTT
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. plotkin_exists f \<sqsubseteq> plotkin_exists g
[PROOF STEP]
apply (unfold plotkin_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>appF\<cdot>f\<cdot>n = ValTT; appF\<cdot>g\<cdot>n = ValTT; appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF; appF\<cdot>g\<cdot>\<bottom> \<noteq> ValFF\<rbrakk> \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (if appF\<cdot>g\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>g\<cdot>n = ValTT then ValTT else \<bottom>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
assume fbot: "appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF" and efn: "\<not>(\<exists>n. appF\<cdot>f\<cdot>n = ValTT)"
[PROOF STATE]
proof (state)
this:
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
\<nexists>n. appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
\<nexists>n. appF\<cdot>f\<cdot>n = ValTT
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF
\<nexists>n. appF\<cdot>f\<cdot>n = ValTT

goal (1 subgoal):
 1. plotkin_exists f \<sqsubseteq> plotkin_exists g
[PROOF STEP]
by (simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF; \<nexists>n. appF\<cdot>f\<cdot>n = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> plotkin_exists x \<sqsubseteq> plotkin_exists y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g
\<lbrakk>appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF; \<nexists>n. appF\<cdot>f\<cdot>n = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g
\<lbrakk>appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF; \<nexists>n. appF\<cdot>f\<cdot>n = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists f \<sqsubseteq> plotkin_exists g

goal (1 subgoal):
 1. plotkin_exists f \<sqsubseteq> plotkin_exists g
[PROOF STEP]
unfolding plotkin_exists_def
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>f\<cdot>\<bottom> = ValFF \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (if appF\<cdot>g\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>g\<cdot>n = ValTT then ValTT else \<bottom>)
\<exists>n. appF\<cdot>f\<cdot>n = ValTT \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (if appF\<cdot>g\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>g\<cdot>n = ValTT then ValTT else \<bottom>)
\<lbrakk>appF\<cdot>f\<cdot>\<bottom> \<noteq> ValFF; \<nexists>n. appF\<cdot>f\<cdot>n = ValTT\<rbrakk> \<Longrightarrow> (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (if appF\<cdot>g\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>g\<cdot>n = ValTT then ValTT else \<bottom>)

goal (1 subgoal):
 1. (if appF\<cdot>f\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>f\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (if appF\<cdot>g\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>g\<cdot>n = ValTT then ValTT else \<bottom>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
plotkin_exists f \<sqsubseteq> plotkin_exists g

goal:
No subgoals!
[PROOF STEP]
qed