[STATEMENT]
lemma eqvtBangRel:
  fixes Rel :: "(pi \<times> pi) set"

  assumes eqvtRel: "eqvt Rel"

  shows "eqvt(bangRel Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (bangRel Rel)
[PROOF STEP]
proof(simp add: eqvt_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b perma. (a, b) \<in> bangRel Rel \<Longrightarrow> (perma \<bullet> a, perma \<bullet> b) \<in> bangRel Rel
[PROOF STEP]
fix P Q perm
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b perma. (a, b) \<in> bangRel Rel \<Longrightarrow> (perma \<bullet> a, perma \<bullet> b) \<in> bangRel Rel
[PROOF STEP]
assume "(P, Q) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>a b perma. (a, b) \<in> bangRel Rel \<Longrightarrow> (perma \<bullet> a, perma \<bullet> b) \<in> bangRel Rel
[PROOF STEP]
thus "((perm::name prm) \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel Rel

goal (1 subgoal):
 1. (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
assume "(P, Q) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
with eqvtRel
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P, Q) \<in> Rel
[PROOF STEP]
have "(perm \<bullet> P, perm \<bullet> Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P, Q) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> P, perm \<bullet> Q) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P, perm \<bullet> Q) \<in> Rel

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
thus "(perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P, perm \<bullet> Q) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel
[PROOF STEP]
by(force intro: BRBang)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> !P, perm \<bullet> !Q) \<in> bangRel Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
fix P Q R T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
assume R: "(R, T) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(R, T) \<in> Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
assume BR: "(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
from eqvtRel R
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(R, T) \<in> Rel
[PROOF STEP]
have "(perm \<bullet> R, perm \<bullet> T) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(R, T) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> R, perm \<bullet> T) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> R, perm \<bullet> T) \<in> Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
with BR
[PROOF STATE]
proof (chain)
picking this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel
(perm \<bullet> R, perm \<bullet> T) \<in> Rel
[PROOF STEP]
show "(perm \<bullet> (R \<parallel> P), perm \<bullet> (T \<parallel> Q)) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel
(perm \<bullet> R, perm \<bullet> T) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel
[PROOF STEP]
by(force intro: BRPar)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> R \<parallel> P, perm \<bullet> T \<parallel> Q) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
assume "(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
thus "(perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel

goal (1 subgoal):
 1. (perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel
[PROOF STEP]
by(force intro: BRRes)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> <\<nu>a>P, perm \<bullet> <\<nu>a>Q) \<in> bangRel Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P, perm \<bullet> Q) \<in> bangRel Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BRBangCases[consumes 1, case_names BRBang]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   F   :: "pi \<Rightarrow> bool"

  assumes "(P, !Q) \<in> bangRel Rel"
  and     "\<And>P. (P, Q) \<in> Rel \<Longrightarrow> F (!P)"

  shows "F P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P, !Q) \<in> bangRel Rel
(?P, Q) \<in> Rel \<Longrightarrow> F (!?P)

goal (1 subgoal):
 1. F P
[PROOF STEP]
by(induct rule: BRBangCases', auto simp add: pi.inject)


[STATEMENT]
lemma BRParCases[consumes 1, case_names BRPar]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   F   :: "pi \<Rightarrow> bool"

  assumes "(P, Q \<parallel> !Q) \<in> bangRel Rel"
  and     "\<And>P R. \<lbrakk>(P, Q) \<in> Rel; (R, !Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> F (P \<parallel> R)"

  shows "F P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P, Q \<parallel> !Q) \<in> bangRel Rel
\<lbrakk>(?P, Q) \<in> Rel; (?R, !Q) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> F (?P \<parallel> ?R)

goal (1 subgoal):
 1. F P
[PROOF STEP]
by(induct rule: BRParCases', auto simp add: pi.inject)


[STATEMENT]
lemma bangRelSubset:
  fixes Rel  :: "(pi \<times> pi) set"
  and   Rel' :: "(pi \<times> pi) set"

  assumes "(P, Q) \<in> bangRel Rel"
  and     "\<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (P, Q) \<in> Rel'"

  shows "(P, Q) \<in> bangRel Rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P, Q) \<in> bangRel Rel'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel Rel
(?P, ?Q) \<in> Rel \<Longrightarrow> (?P, ?Q) \<in> Rel'

goal (1 subgoal):
 1. (P, Q) \<in> bangRel Rel'
[PROOF STEP]
by(induct rule:  bangRel.induct) (auto intro: BRBang BRPar BRRes)


[STATEMENT]
lemma bangRelSymetric:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"

  assumes A:   "(P, Q) \<in> bangRel Rel"
  and     Sym: "\<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (Q, P) \<in> Rel"

  shows "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> bangRel Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel Rel

goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume "(P, Q) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
hence "(Q, P) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> Rel

goal (1 subgoal):
 1. (Q, P) \<in> Rel
[PROOF STEP]
by(rule Sym)
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> Rel

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(!Q, !P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(Q, P) \<in> Rel

goal (1 subgoal):
 1. (!Q, !P) \<in> bangRel Rel
[PROOF STEP]
by(rule BRBang)
[PROOF STATE]
proof (state)
this:
(!Q, !P) \<in> bangRel Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q R T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume RRelT: "(R, T) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(R, T) \<in> Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume IH: "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> bangRel Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
from RRelT
[PROOF STATE]
proof (chain)
picking this:
(R, T) \<in> Rel
[PROOF STEP]
have "(T, R) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(R, T) \<in> Rel

goal (1 subgoal):
 1. (T, R) \<in> Rel
[PROOF STEP]
by(rule Sym)
[PROOF STATE]
proof (state)
this:
(T, R) \<in> Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(T, R) \<in> Rel

goal (1 subgoal):
 1. (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
(T, R) \<in> Rel
(Q, P) \<in> bangRel Rel

goal (1 subgoal):
 1. (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
[PROOF STEP]
by(rule BRPar)
[PROOF STATE]
proof (state)
this:
(T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(Q, P) \<in> bangRel Rel

goal (1 subgoal):
 1. (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
by(rule BRRes)
[PROOF STATE]
proof (state)
this:
(<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> bangRel Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resChainPerm[simp]:
  fixes perm :: "name prm"
  and   lst  :: "name list"
  and   P    :: pi

  shows "perm \<bullet> (resChain lst P) = resChain (perm \<bullet> lst) (perm \<bullet> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> resChain lst P = resChain (perm \<bullet> lst) (perm \<bullet> P)
[PROOF STEP]
by(induct_tac lst, auto)


[STATEMENT]
lemma resChainFresh:
  fixes a   :: name
  and   lst :: "name list"
  and   P   :: pi

  assumes "a \<sharp> (lst, P)"

  shows "a \<sharp> (resChain lst P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> resChain lst P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<sharp> (lst, P)

goal (1 subgoal):
 1. a \<sharp> resChain lst P
[PROOF STEP]
apply(induct_tac lst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<sharp> (lst, P) \<Longrightarrow> a \<sharp> resChain [] P
 2. \<And>aa list. \<lbrakk>a \<sharp> (lst, P); a \<sharp> resChain list P\<rbrakk> \<Longrightarrow> a \<sharp> resChain (aa # list) P
[PROOF STEP]
apply(simp add: fresh_prod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>a \<sharp> (lst, P); a \<sharp> resChain list P\<rbrakk> \<Longrightarrow> a \<sharp> resChain (aa # list) P
[PROOF STEP]
by(simp add: fresh_prod name_fresh_abs)


[STATEMENT]
lemma ValD_case_ID [simp]:
  "ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN = ID
[PROOF STEP]
apply (rule cfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. x = \<bottom> \<Longrightarrow> ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
 2. \<And>x cfun. x = ValF\<cdot>cfun \<Longrightarrow> ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
 3. \<And>x. x = ValTT \<Longrightarrow> ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
 4. \<And>x. x = ValFF \<Longrightarrow> ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
 5. \<And>x nat. x = ValN\<cdot>nat \<Longrightarrow> ValD_case\<cdot>ValF\<cdot>ValTT\<cdot>ValFF\<cdot>ValN\<cdot>x = ID\<cdot>x
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma below_monic_ValN [iff]:
  "below_monic_cfun ValN"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun ValN
[PROOF STEP]
by (rule below_monicI) simp


[STATEMENT]
lemma ValD_copy_rec_strict [simp]:
  "ValD_copy_rec\<cdot>r\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_copy_rec\<cdot>r\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma ValD_copy_strict [simp]:
  "ValD_copy\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_copy\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (subst fix_eq) simp


[STATEMENT]
lemma ValD_copy_ID [simp]:
  "ValD_copy = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
fix x :: ValD
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
fix i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
have "ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x)) = ValD_take i\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x)) = ValD_take i\<cdot>x
[PROOF STEP]
proof (induct i arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. ValD_take 0\<cdot>(ValD_copy\<cdot>(ValD_take 0\<cdot>x)) = ValD_take 0\<cdot>x
 2. \<And>i x. (\<And>x. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x)) = ValD_take i\<cdot>x) \<Longrightarrow> ValD_take (Suc i)\<cdot>(ValD_copy\<cdot>(ValD_take (Suc i)\<cdot>x)) = ValD_take (Suc i)\<cdot>x
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
ValD_take n\<cdot>(ValD_copy\<cdot>(ValD_take n\<cdot>?x)) = ValD_take n\<cdot>?x

goal (2 subgoals):
 1. \<And>x. ValD_take 0\<cdot>(ValD_copy\<cdot>(ValD_take 0\<cdot>x)) = ValD_take 0\<cdot>x
 2. \<And>i x. (\<And>x. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x)) = ValD_take i\<cdot>x) \<Longrightarrow> ValD_take (Suc i)\<cdot>(ValD_copy\<cdot>(ValD_take (Suc i)\<cdot>x)) = ValD_take (Suc i)\<cdot>x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValD_take n\<cdot>(ValD_copy\<cdot>(ValD_take n\<cdot>?x)) = ValD_take n\<cdot>?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ValD_take n\<cdot>(ValD_copy\<cdot>(ValD_take n\<cdot>?x)) = ValD_take n\<cdot>?x

goal (1 subgoal):
 1. ValD_take (Suc n)\<cdot>(ValD_copy\<cdot>(ValD_take (Suc n)\<cdot>x)) = ValD_take (Suc n)\<cdot>x
[PROOF STEP]
by (cases x) (subst fix_eq, simp add: cfun_map_def)+
[PROOF STATE]
proof (state)
this:
ValD_take (Suc n)\<cdot>(ValD_copy\<cdot>(ValD_take (Suc n)\<cdot>x)) = ValD_take (Suc n)\<cdot>x

goal (1 subgoal):
 1. \<And>x. ValD_take 0\<cdot>(ValD_copy\<cdot>(ValD_take 0\<cdot>x)) = ValD_take 0\<cdot>x
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x)) = ValD_take i\<cdot>x

goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ValD_take ?i2\<cdot>(ValD_copy\<cdot>(ValD_take ?i2\<cdot>?x2)) = ValD_take ?i2\<cdot>?x2

goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValD_take ?i2\<cdot>(ValD_copy\<cdot>(ValD_take ?i2\<cdot>?x2)) = ValD_take ?i2\<cdot>?x2
[PROOF STEP]
have "\<And>x :: ValD. (\<Squnion>i. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x))) = (\<Squnion>i. ValD_take i\<cdot>x)"
[PROOF STATE]
proof (prove)
using this:
ValD_take ?i2\<cdot>(ValD_copy\<cdot>(ValD_take ?i2\<cdot>?x2)) = ValD_take ?i2\<cdot>?x2

goal (1 subgoal):
 1. \<And>x. (\<Squnion>i. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>x))) = (\<Squnion>i. ValD_take i\<cdot>x)
[PROOF STEP]
by (blast intro: lub_eq)
[PROOF STATE]
proof (state)
this:
(\<Squnion>i. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>?x))) = (\<Squnion>i. ValD_take i\<cdot>?x)

goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Squnion>i. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>?x))) = (\<Squnion>i. ValD_take i\<cdot>?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>i. ValD_take i\<cdot>(ValD_copy\<cdot>(ValD_take i\<cdot>?x))) = (\<Squnion>i. ValD_take i\<cdot>?x)

goal (1 subgoal):
 1. ValD_copy = ID
[PROOF STEP]
by (simp add: lub_distribs ValD.lub_take cfun_eq_iff)
[PROOF STATE]
proof (state)
this:
ValD_copy = ID

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma env_ext_same: "env_ext\<cdot>v\<cdot>x\<cdot>\<rho>\<cdot>v = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. env_ext\<cdot>v\<cdot>x\<cdot>\<rho>\<cdot>v = x
[PROOF STEP]
by (simp add: env_ext_def)


[STATEMENT]
lemma env_ext_neq: "v \<noteq> v' \<Longrightarrow> env_ext\<cdot>v\<cdot>x\<cdot>\<rho>\<cdot>v' = \<rho>\<cdot>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> v' \<Longrightarrow> env_ext\<cdot>v\<cdot>x\<cdot>\<rho>\<cdot>v' = \<rho>\<cdot>v'
[PROOF STEP]
by (simp add: env_ext_def)


[STATEMENT]
lemma Y: "\<lbrakk>Ycomb\<rbrakk>\<rho> = ValF\<cdot>fixD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> = ValF\<cdot>fixD
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> = ValF\<cdot>fixD
[PROOF STEP]
proof(rule below_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
 2. ValF\<cdot>fixD \<sqsubseteq> \<lbrakk>Ycomb\<rbrakk>\<rho>
[PROOF STEP]
show "ValF\<cdot>fixD \<sqsubseteq> \<lbrakk>Ycomb\<rbrakk>\<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValF\<cdot>fixD \<sqsubseteq> \<lbrakk>Ycomb\<rbrakk>\<rho>
[PROOF STEP]
unfolding fixD_def Ycomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValF\<cdot>(\<Lambda> (ValF\<cdot>f). fix\<cdot>f) \<sqsubseteq> \<lbrakk>AbsN 0 (App (App Y_delta (Var 0)) (App Y_delta (Var 0)))\<rbrakk>\<rho>
[PROOF STEP]
apply (clarsimp simp: cfun_below_iff eta_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. x = \<bottom> \<Longrightarrow> ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
 2. \<And>x cfun. x = ValF\<cdot>cfun \<Longrightarrow> ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
 3. \<And>x. x = ValTT \<Longrightarrow> ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
 4. \<And>x. x = ValFF \<Longrightarrow> ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
 5. \<And>x nat. x = ValN\<cdot>nat \<Longrightarrow> ValD_case\<cdot>fix\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x cfun. x = ValF\<cdot>cfun \<Longrightarrow> fix\<cdot>cfun \<sqsubseteq> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))
[PROOF STEP]
apply (rule fix_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x cfun. x = ValF\<cdot>cfun \<Longrightarrow> cfun\<cdot>(appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))) = appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>(ValF\<cdot>cfun)\<cdot>\<rho>))\<cdot>(ValF\<cdot>cfun))
[PROOF STEP]
by (subst Y_delta_def, simp)
[PROOF STATE]
proof (state)
this:
ValF\<cdot>fixD \<sqsubseteq> \<lbrakk>Ycomb\<rbrakk>\<rho>

goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
fix f \<rho>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
let ?P = "\<lambda>x. x \<sqsubseteq> ID \<and> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
have "?P ValD_copy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (rule fix_ind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>a. a \<sqsubseteq> ID \<and> appF\<cdot>(a\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f))
 2. \<bottom> \<sqsubseteq> ID \<and> appF\<cdot>(\<bottom>\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
 3. \<And>x. x \<sqsubseteq> ID \<and> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f) \<Longrightarrow> ValD_copy_rec\<cdot>x \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bottom> \<sqsubseteq> ID \<and> appF\<cdot>(\<bottom>\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
 2. \<And>x. x \<sqsubseteq> ID \<and> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f) \<Longrightarrow> ValD_copy_rec\<cdot>x \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<sqsubseteq> ID \<and> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f) \<Longrightarrow> ValD_copy_rec\<cdot>x \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x \<sqsubseteq> ID
 2. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (rule cfun_belowI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 2. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (case_tac xa)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = \<bottom>\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 2. \<And>x xa cfun. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 3. \<And>x xa. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValTT\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 4. \<And>x xa. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValFF\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 5. \<And>x xa nat. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> ValD_copy_rec\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>xa
 6. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa cfun. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> cfun_map\<cdot>x\<cdot>x\<cdot>cfun \<sqsubseteq> cfun
 2. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (drule cfun_map_below_ID)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa cfun. \<lbrakk>appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f); xa = ValF\<cdot>cfun; cfun_map\<cdot>x\<cdot>x \<sqsubseteq> ID\<rbrakk> \<Longrightarrow> cfun_map\<cdot>x\<cdot>x\<cdot>cfun \<sqsubseteq> cfun
 2. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (simp add: cfun_below_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)
[PROOF STEP]
apply (simp add: fixD_def eta_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f
[PROOF STEP]
apply (subst Y_delta_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>AbsN 0 (AbsN 1 (App (Var 0) (App (Var 1) (Var 1))))\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f
[PROOF STEP]
apply (subst fix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(ValD_copy_rec\<cdot>x\<cdot>(appF\<cdot>(\<lbrakk>AbsN 0 (AbsN 1 (App (Var 0) (App (Var 1) (Var 1))))\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> f\<cdot>(fix\<cdot>f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> x\<cdot>(f\<cdot>(appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))))) \<sqsubseteq> f\<cdot>(fix\<cdot>f)
[PROOF STEP]
apply (rule cfun_below_ID, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> f\<cdot>(appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))) \<sqsubseteq> f\<cdot>(fix\<cdot>f)
[PROOF STEP]
apply (rule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))) \<sqsubseteq> fix\<cdot>f
[PROOF STEP]
apply (subgoal_tac "appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))
                        \<sqsubseteq> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))) \<sqsubseteq> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))\<rbrakk> \<Longrightarrow> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))) \<sqsubseteq> fix\<cdot>f
 2. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))) \<sqsubseteq> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))
[PROOF STEP]
apply (erule (1) below_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<sqsubseteq> ID; appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f\<rbrakk> \<Longrightarrow> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))) \<sqsubseteq> appF\<cdot>(x\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f))
[PROOF STEP]
apply (simp add: monofun_cfun_arg cfun_below_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>)\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>f)

goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>?f2)

goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>?f2)
[PROOF STEP]
show "\<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD"
[PROOF STATE]
proof (prove)
using this:
ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)) \<sqsubseteq> fixD\<cdot>(ValF\<cdot>?f2)

goal (1 subgoal):
 1. \<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD
[PROOF STEP]
unfolding Ycomb_def fixD_def
[PROOF STATE]
proof (prove)
using this:
ValD_copy \<sqsubseteq> ID \<and> appF\<cdot>(ValD_copy\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>?\<rho>'2)\<cdot>(ValF\<cdot>?f2)) \<sqsubseteq> (\<Lambda> (ValF\<cdot>f). fix\<cdot>f)\<cdot>(ValF\<cdot>?f2)

goal (1 subgoal):
 1. \<lbrakk>AbsN 0 (App (App Y_delta (Var 0)) (App Y_delta (Var 0)))\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>(\<Lambda> (ValF\<cdot>f). fix\<cdot>f)
[PROOF STEP]
apply (clarsimp simp: cfun_below_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f) \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = \<bottom>\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 2. \<And>x cfun. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 3. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValTT\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 4. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValFF\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 5. \<And>x nat. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
[PROOF STEP]
apply (subst Y_delta_def, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x cfun. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValF\<cdot>cfun\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 2. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValTT\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 3. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValFF\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 4. \<And>x nat. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValTT\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 2. \<And>x. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValFF\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
 3. \<And>x nat. \<lbrakk>\<And>\<rho>' f. appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f))\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>\<rho>')\<cdot>(ValF\<cdot>f)) \<sqsubseteq> fix\<cdot>f; x = ValN\<cdot>nat\<rbrakk> \<Longrightarrow> appF\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x)\<cdot>(appF\<cdot>(\<lbrakk>Y_delta\<rbrakk>(env_ext\<cdot>0\<cdot>x\<cdot>\<rho>))\<cdot>x) \<sqsubseteq> ValD_case\<cdot>(Abs_cfun (Rep_cfun fix))\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>x
[PROOF STEP]
apply (subst Y_delta_def, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ycomb\<rbrakk>\<rho> \<sqsubseteq> ValF\<cdot>fixD

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma logical_relationI:
  "\<lbrakk> \<And>fs xs. \<lbrakk> fs \<in> R; xs \<in> R \<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R;
     \<And>fs xs. \<lbrakk> fs \<in> R; xs \<in> R \<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R;
     \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R;
     \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R;
     \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R;
     \<And>cs ts es. \<lbrakk> cs \<in> R; ts \<in> R; es \<in> R \<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R;
     \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R;
     \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R;
     \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R \<rbrakk> \<Longrightarrow> logical_relation R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>fs xs. \<lbrakk>fs \<in> R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R; \<And>fs xs. \<lbrakk>fs \<in> R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R; \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R; \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R; \<And>cs ts es. \<lbrakk>cs \<in> R; ts \<in> R; es \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> logical_relation R
[PROOF STEP]
unfolding logical_relation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>fs xs. \<lbrakk>fs \<in> R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R; \<And>fs xs. \<lbrakk>fs \<in> R; xs \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R; \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R; \<And>fs. (\<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R; \<And>cs ts es. \<lbrakk>cs \<in> R; ts \<in> R; es \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R; \<And>xs. xs \<in> R \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)
[PROOF STEP]
by (simp add: cfcomp1)


[STATEMENT]
lemma lr_l2r:
  "\<lbrakk> fs \<in> R; xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R"
  "\<lbrakk> fs \<in> R; xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R"
  "\<lbrakk> xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R"
  "\<lbrakk> cs \<in> R; ts \<in> R; es \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R"
  "\<lbrakk> xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R"
  "\<lbrakk> xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R"
  "\<lbrakk> xs \<in> R; logical_relation R \<rbrakk> \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>fs \<in> R; xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>fs \<in> R; xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R)) &&& ((\<lbrakk>cs \<in> R; ts \<in> R; es \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) &&& (\<lbrakk>xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R)) &&& (\<lbrakk>xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>xs \<in> R; logical_relation R\<rbrakk> \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)
[PROOF STEP]
unfolding logical_relation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>fs \<in> R; xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>fs \<in> R; xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> R)) &&& ((\<lbrakk>cs \<in> R; ts \<in> R; es \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) &&& (\<lbrakk>xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> R)) &&& (\<lbrakk>xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> R) &&& (\<lbrakk>xs \<in> R; (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)\<rbrakk> \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> R)
[PROOF STEP]
by blast+


[STATEMENT]
lemma lr_r2l:
  "\<lbrakk> logical_relation R; \<forall>xs \<in> R. (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> R \<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>logical_relation R; \<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> R
[PROOF STEP]
unfolding logical_relation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R); \<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> R
[PROOF STEP]
by (simp add: cfcomp1)


[STATEMENT]
lemma lr_r2l_strict:
  "\<lbrakk> logical_relation R; \<forall>xs \<in> R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R \<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(strictify\<cdot>(fs i))) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>logical_relation R; \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(strictify\<cdot>(fs i))) \<in> R
[PROOF STEP]
unfolding logical_relation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs\<in>R. \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. fs j\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> R) \<and> (\<forall>fs. (\<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R) \<longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. fixD\<cdot>(xs j)) \<in> R) \<and> (\<forall>cs\<in>R. \<forall>ts\<in>R. \<forall>es\<in>R. (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. succ\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. pred\<cdot>(xs j)) \<in> R) \<and> (\<forall>xs\<in>R. (\<lambda>j. isZero\<cdot>(xs j)) \<in> R); \<forall>xs\<in>R. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(strictify\<cdot>(fs i))) \<in> R
[PROOF STEP]
by (simp add: cfcomp1)


[STATEMENT]
lemma PCF_consts_rel_simps [simp, elim]:
  "PCF_consts_rel R \<Longrightarrow> \<bottom> \<in> R"
  "PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValTT) \<in> R"
  "PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValFF) \<in> R"
  "PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValN\<cdot>n) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((PCF_consts_rel R \<Longrightarrow> \<bottom> \<in> R) &&& (PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValTT) \<in> R)) &&& (PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValFF) \<in> R) &&& (PCF_consts_rel R \<Longrightarrow> (\<lambda>i. ValN\<cdot>n) \<in> R)
[PROOF STEP]
unfolding PCF_consts_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<bottom> \<in> R \<and> (\<lambda>i. ValTT) \<in> R \<and> (\<lambda>i. ValFF) \<in> R \<and> (\<forall>n. (\<lambda>i. ValN\<cdot>n) \<in> R) \<Longrightarrow> \<bottom> \<in> R) &&& (\<bottom> \<in> R \<and> (\<lambda>i. ValTT) \<in> R \<and> (\<lambda>i. ValFF) \<in> R \<and> (\<forall>n. (\<lambda>i. ValN\<cdot>n) \<in> R) \<Longrightarrow> (\<lambda>i. ValTT) \<in> R)) &&& (\<bottom> \<in> R \<and> (\<lambda>i. ValTT) \<in> R \<and> (\<lambda>i. ValFF) \<in> R \<and> (\<forall>n. (\<lambda>i. ValN\<cdot>n) \<in> R) \<Longrightarrow> (\<lambda>i. ValFF) \<in> R) &&& (\<bottom> \<in> R \<and> (\<lambda>i. ValTT) \<in> R \<and> (\<lambda>i. ValFF) \<in> R \<and> (\<forall>n. (\<lambda>i. ValN\<cdot>n) \<in> R) \<Longrightarrow> (\<lambda>i. ValN\<cdot>n) \<in> R)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma PCF_consts_relI:
  "\<lbrakk> \<bottom> \<in> R;
     (\<lambda>i. ValTT) \<in> R;
     (\<lambda>i. ValFF) \<in> R;
     \<And>n. (\<lambda>i. ValN\<cdot>n) \<in> R \<rbrakk> \<Longrightarrow> PCF_consts_rel R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bottom> \<in> R; (\<lambda>i. ValTT) \<in> R; (\<lambda>i. ValFF) \<in> R; \<And>n. (\<lambda>i. ValN\<cdot>n) \<in> R\<rbrakk> \<Longrightarrow> PCF_consts_rel R
[PROOF STEP]
unfolding PCF_consts_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bottom> \<in> R; (\<lambda>i. ValTT) \<in> R; (\<lambda>i. ValFF) \<in> R; \<And>n. (\<lambda>i. ValN\<cdot>n) \<in> R\<rbrakk> \<Longrightarrow> \<bottom> \<in> R \<and> (\<lambda>i. ValTT) \<in> R \<and> (\<lambda>i. ValFF) \<in> R \<and> (\<forall>n. (\<lambda>i. ValN\<cdot>n) \<in> R)
[PROOF STEP]
by blast