[STATEMENT]
lemma wf_cdecl_fdecl: 
"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_cdecl G (C, c); f \<in> set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f
[PROOF STEP]
apply (unfold wf_cdecl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case (C, c) of (C, c) \<Rightarrow> \<not> is_iface G C \<and> (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> (\<forall>s. \<forall>im\<in>DeclConcepts.imethds G I s. ? cm:methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not> is_static cm \<and> accmodi im \<le> accmodi cm)) \<and> Ball (set (cfields c)) (wf_fdecl G (pid C)) \<and> unique (cfields c) \<and> Ball (set (methods c)) (wf_mdecl G C) \<and> unique (methods c) \<and> jumpNestingOkS {} (init c) \<and> Ex (da \<lparr>prg = G, cls = C, lcl = Map.empty\<rparr> {} \<langle>init c\<rangle>) \<and> \<lparr>prg = G, cls = C, lcl = Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> (C \<noteq> Object \<longrightarrow> is_acc_class G (pid C) (super c) \<and> (table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) entails \<lambda>new. \<forall>old sig. (G \<turnstile> qmdecl sig new overrides\<^sub>S qmdecl sig old \<longrightarrow> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old) \<and> (G,sig\<turnstile> new hides old \<longrightarrow> accmodi old \<le> accmodi new \<and> is_static old))); f \<in> set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done