theory Adequacy
imports "ResourcedAdequacy" "Denotational-Related"
begin
theorem adequacy:
assumes "\e\\<^bsub>\\\\<^esub> \ \"
shows "\ \ v. \ : e \\<^bsub>S\<^esub> \ : v"
proof-
have "\\\ \\\<^sup>* \\\\" by (rule heaps_similar)
hence "\e\\<^bsub>\\\\<^esub> \\ (\\e\\<^bsub>\\\\\<^esub>)\C\<^sup>\" by (rule denotational_semantics_similar)
from bot_or_not_bot[OF this] assms
have "(\\e\\<^bsub>\\\\\<^esub>)\C\<^sup>\ \ \" by metis
thus ?thesis by (rule resourced_adequacy)
qed
end