[STATEMENT]
lemma lr_fundamental:
  assumes lr: "PCF_lr R"
  assumes \<rho>: "\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R"
  shows "(\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
using \<rho>
[PROOF STATE]
proof (prove)
using this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
proof(induct M arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Var x\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>M1 M2 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>App M1 M2\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
A total of 13 subgoals...
[PROOF STEP]
case (Var v \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (13 subgoals):
 1. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Var x\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>M1 M2 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>App M1 M2\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
A total of 13 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>Var v\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>Var v\<rbrakk>(\<rho> i)) \<in> R

goal (12 subgoals):
 1. \<And>M1 M2 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>App M1 M2\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>M1 M2 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>App M1 M2\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
A total of 12 subgoals...
[PROOF STEP]
case (App e1 e2 \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e1\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e2\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (12 subgoals):
 1. \<And>M1 M2 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>App M1 M2\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
A total of 12 subgoals...
[PROOF STEP]
with lr lr_l2r(1)[where fs="\<lambda>j. \<lbrakk>e1\<rbrakk>(\<rho> j)" and xs="\<lambda>j. \<lbrakk>e2\<rbrakk>(\<rho> j)"]
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e1\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>e2\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(\<lbrakk>e1\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>e2\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e1\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e2\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e1\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>e2\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(\<lbrakk>e1\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>e2\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e1\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e2\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>App e1 e2\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>App e1 e2\<rbrakk>(\<rho> i)) \<in> R

goal (11 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
A total of 11 subgoals...
[PROOF STEP]
case (AbsN v e)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (11 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsN x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
A total of 11 subgoals...
[PROOF STEP]
with lr
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>AbsN v e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i)))) \<in> R
[PROOF STEP]
apply (erule lr_r2l[where fs="\<lambda>i. \<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i))" and R=R, simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R\<rbrakk> \<Longrightarrow> \<forall>xs\<in>R. (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (cut_tac \<rho>="\<lambda>j. env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j)" in AbsN.hyps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i)\<cdot>va) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (simp add: env_ext_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
using AbsN(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (case_tac "v=va")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v = va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 3. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (simp add: eta_cfun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xs i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>AbsN v e\<rbrakk>(\<rho> i)) \<in> R

goal (10 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (AbsV v e)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (10 subgoals):
 1. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>AbsV x1a M\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 10. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>AbsV v e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(strictify\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i))))) \<in> R
[PROOF STEP]
apply (rule lr_r2l_strict[where fs="\<lambda>i. \<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i))", simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R\<rbrakk> \<Longrightarrow> logical_relation R
 2. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R\<rbrakk> \<Longrightarrow> \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> j)))\<cdot>(xs j)) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R\<rbrakk> \<Longrightarrow> \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> j)))\<cdot>(xs j)) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> j)))\<cdot>(xs j)) \<in> R
[PROOF STEP]
apply (cut_tac fs="\<lambda>i. ValF\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i)))" and xs=xs and R=R in lr_l2r(2))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i)))) \<in> R
 2. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> xs \<in> R
 3. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> logical_relation R
 4. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R; (\<lambda>j. strictify\<cdot>(appF\<cdot>(ValF\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> j)))))\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> j)))\<cdot>(xs j)) \<in> R
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); logical_relation R; PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i)))) \<in> R
[PROOF STEP]
apply (erule lr_r2l[where fs="\<lambda>i. \<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i))" and R=R, simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R\<rbrakk> \<Longrightarrow> \<forall>xs\<in>R. (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xs j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (cut_tac \<rho>="\<lambda>j. env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j)" in AbsV.hyps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i)\<cdot>va) \<in> R
 2. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (simp add: env_ext_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
using AbsV(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (2 subgoals):
 1. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R\<rbrakk> \<Longrightarrow> \<forall>va. (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs xsa va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (case_tac "v=va")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs xsa va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v = va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs xsa va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 3. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply (simp add: eta_cfun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs xsa va. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then xsa i else \<rho> i\<cdot>va) \<in> R
 2. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs xsa. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; adm (\<lambda>x. x \<in> R); PCF_consts_rel R; xs \<in> R; xsa \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(xsa j)\<cdot>(\<rho> j))) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>AbsV v e\<rbrakk>(\<rho> i)) \<in> R

goal (9 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (Fix v e \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (9 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>x1a M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Fix x1a M\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 9. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>Fix v e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. \<mu> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> i))) \<in> R
[PROOF STEP]
apply (subst fix_argument_promote_fun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> x. (\<lambda>xa. (\<Lambda> x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>x\<cdot>(\<rho> xa)))\<cdot>(x xa))) \<in> R
[PROOF STEP]
apply (rule fix_ind[where F="\<Lambda> f. (\<lambda>x. (\<Lambda> xa. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>xa\<cdot>(\<rho> x)))\<cdot>(f x))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>a. a \<in> R)
 2. \<bottom> \<in> R
 3. \<And>x. x \<in> R \<Longrightarrow> (\<Lambda> f. (\<lambda>x. (\<Lambda> xa. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>xa\<cdot>(\<rho> x)))\<cdot>(f x)))\<cdot>x \<in> R
[PROOF STEP]
apply (simp add: lr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bottom> \<in> R
 2. \<And>x. x \<in> R \<Longrightarrow> (\<Lambda> f. (\<lambda>x. (\<Lambda> xa. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>xa\<cdot>(\<rho> x)))\<cdot>(f x)))\<cdot>x \<in> R
[PROOF STEP]
apply (simp add: lr inst_fun_pcpo[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> R \<Longrightarrow> (\<Lambda> f. (\<lambda>x. (\<Lambda> xa. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>xa\<cdot>(\<rho> x)))\<cdot>(f x)))\<cdot>x \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> R \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply (cut_tac \<rho>="\<lambda>i. env_ext\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i)" in Fix.hyps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> R \<Longrightarrow> \<forall>va. (\<lambda>i. env_ext\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i)\<cdot>va) \<in> R
 2. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>(env_ext\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
unfolding env_ext_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> R \<Longrightarrow> \<forall>va. (\<lambda>i. (\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i)\<cdot>va) \<in> R
 2. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
using Fix(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (2 subgoals):
 1. \<And>x. x \<in> R \<Longrightarrow> \<forall>va. (\<lambda>i. (\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i)\<cdot>va) \<in> R
 2. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x va. \<lbrakk>x \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then x i else \<rho> i\<cdot>va) \<in> R
 2. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply (case_tac "v=va")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x va. \<lbrakk>x \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v = va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then x i else \<rho> i\<cdot>va) \<in> R
 2. \<And>x va. \<lbrakk>x \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then x i else \<rho> i\<cdot>va) \<in> R
 3. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply (simp add: eta_cfun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x va. \<lbrakk>x \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R; v \<noteq> va\<rbrakk> \<Longrightarrow> (\<lambda>i. if v = va then x i else \<rho> i\<cdot>va) \<in> R
 2. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> R; (\<lambda>i. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(x i)\<cdot>(\<rho> i))) \<in> R\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. \<lbrakk>e\<rbrakk>((\<Lambda> v x \<rho> v'. if v = v' then x else \<rho>\<cdot>v')\<cdot>v\<cdot>(f x)\<cdot>(\<rho> x))))\<cdot>x \<in> R
[PROOF STEP]
apply (simp add: cont_fun)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>Fix v e\<rbrakk>(\<rho> i)) \<in> R

goal (8 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (Cond i t e \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>ia. \<lbrakk>i\<rbrakk>(?\<rho> ia)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>t\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (8 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>M1 M2 M3 \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M1\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M2\<rbrakk>(\<rho> i)) \<in> R; \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M3\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Cond M1 M2 M3\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 8. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr lr_l2r(4)[where cs="\<lambda>j. \<lbrakk>i\<rbrakk>(\<rho> j)" and ts="\<lambda>j. \<lbrakk>t\<rbrakk>(\<rho> j)" and es="\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)"]
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>i\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>t\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(\<lbrakk>i\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>t\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>ia. \<lbrakk>i\<rbrakk>(?\<rho> ia)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>t\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>i\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>t\<rbrakk>(\<rho> j)) \<in> ?R; (\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(\<lbrakk>i\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>t\<rbrakk>(\<rho> j))\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>ia. \<lbrakk>i\<rbrakk>(?\<rho> ia)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>t\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>ia. \<lbrakk>Cond i t e\<rbrakk>(\<rho> ia)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>ia. \<lbrakk>Cond i t e\<rbrakk>(\<rho> ia)) \<in> R

goal (7 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (Succ e \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (7 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Succ M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 7. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr lr_l2r(5)[where xs="\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)"]
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. succ\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. succ\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>Succ e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>Succ e\<rbrakk>(\<rho> i)) \<in> R

goal (6 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (Pred e \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (6 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>Pred M\<rbrakk>(\<rho> i)) \<in> R
 6. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr lr_l2r(6)[where xs="\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)"]
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. pred\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. pred\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>Pred e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>Pred e\<rbrakk>(\<rho> i)) \<in> R

goal (5 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case (IsZero e \<rho>)
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (5 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
 5. \<And>M \<rho>. \<lbrakk>\<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>M\<rbrakk>(\<rho> i)) \<in> R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<lbrakk>IsZero M\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr lr_l2r(7)[where xs="\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)"]
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. isZero\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<lbrakk>(\<lambda>j. \<lbrakk>e\<rbrakk>(\<rho> j)) \<in> ?R; logical_relation ?R\<rbrakk> \<Longrightarrow> (\<lambda>j. isZero\<cdot>(\<lbrakk>e\<rbrakk>(\<rho> j))) \<in> ?R
\<forall>v. (\<lambda>i. ?\<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>e\<rbrakk>(?\<rho> i)) \<in> R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>IsZero e\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>IsZero e\<rbrakk>(\<rho> i)) \<in> R

goal (4 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
case Diverge
[PROOF STATE]
proof (state)
this:
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (4 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 4. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
with lr
[PROOF STATE]
proof (chain)
picking this:
PCF_lr R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PCF_lr R
\<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R

goal (1 subgoal):
 1. (\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PCF_lr R; \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. \<bottom>) \<in> R
[PROOF STEP]
apply (simp add: inst_fun_pcpo[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>i. \<lbrakk>\<Omega>\<rbrakk>(\<rho> i)) \<in> R

goal (3 subgoals):
 1. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>tt\<rbrakk>(\<rho> i)) \<in> R
 2. \<And>\<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>ff\<rbrakk>(\<rho> i)) \<in> R
 3. \<And>x \<rho>. \<forall>v. (\<lambda>i. \<rho> i\<cdot>v) \<in> R \<Longrightarrow> (\<lambda>i. \<lbrakk>Num x\<rbrakk>(\<rho> i)) \<in> R
[PROOF STEP]
qed (insert lr, simp_all)