[STATEMENT]
lemma Q_denormalize_full:
  assumes "wf_dlverts t1"
      and "\<forall>v \<in> dverts t1. distinct v"
      and "hd (Dtree.root t1) = root"
      and "max_deg t1 \<le> 1"
      and "\<forall>xs \<in> (dverts t1). seq_conform xs"
      and "dom_children t1 T"
    shows "fwd_sub root (dverts t1) (denormalize (normalize_full t1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fwd_sub root (dverts t1) (denormalize (normalize_full t1))
[PROOF STEP]
using P_denormalize_full[OF assms(1-4)] assms(1,4-6) denormalize_full_sublist_preserv
[PROOF STATE]
proof (prove)
using this:
unique_set_r root (dverts t1) (denormalize (normalize_full t1))
wf_dlverts t1
max_deg t1 \<le> 1
Ball (dverts t1) seq_conform
dom_children t1 T
\<lbrakk>sublist ?xs ?v; ?v \<in> dverts ?t1.0; max_deg ?t1.0 \<le> 1\<rbrakk> \<Longrightarrow> sublist ?xs (denormalize (normalize_full ?t1.0))

goal (1 subgoal):
 1. fwd_sub root (dverts t1) (denormalize (normalize_full t1))
[PROOF STEP]
by (auto dest: denormalize_full_fwd simp: fwd_sub_def)