[STATEMENT]
lemma IfHigh: 
 "\<lbrakk> G \<rhd> c: HighSec; G \<rhd> d:HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d: HighSec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d : HighSec
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d : HighSec
[PROOF STEP]
apply (rule VDMConseq, rule VDMIff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> c : ?A3
 2. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> d : ?B3
 3. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> \<forall>s t. (evalB b (fst s) \<longrightarrow> ?A3 s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> ?B3 s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply (assumption, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> \<forall>s t. (evalB b (fst s) \<longrightarrow> HighSec s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> HighSec s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply (erule thin_rl, erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. (evalB b (fst s) \<longrightarrow> HighSec s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> HighSec s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done