1840     from vat_s.cp_gen_rec[OF this]

  1840     from vat_s.cp_gen_rec[OF this]

  1841     have "?L = 

  1841     have "?L = 

  1842           Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .

  1842           Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .

  1843     also have "... = 

  1843     also have "... = 

  1844           Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"

  1844           Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"

  1845     proof -

  1846     proof -

  1846       from preced_kept have "the_preced s th2 = the_preced s' th2" by simp

  1847       from preced_kept have "the_preced s th2 = the_preced s' th2" by simp

  1847       moreover have "cp_gen s ` RTree.children (tRAG s) x =

  1848       moreover have "cp_gen s ` RTree.children (tRAG s) x =

  1848                      cp_gen s' ` RTree.children (tRAG s') x"

  1849                      cp_gen s' ` RTree.children (tRAG s') x"

  1849       proof -

  1850       proof -

  1998   assumes nd: "(Th th, Th th') \<notin> (child s)^+"

  1999   assumes nd: "(Th th, Th th') \<notin> (child s)^+"

  1999   shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"

  2000   shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"

  2000   by (insert eq_child_left[OF nd] eq_child_right, auto)

  2001   by (insert eq_child_left[OF nd] eq_child_right, auto)

  2001 

  2002 

  2002 lemma eq_cp:

  2003 lemma eq_cp:

  2004   assumes nd: "th \<notin> dependants s th'"

  2004   assumes nd: "th \<notin> dependants s th'"

  2005   shows "cp s th' = cp s' th'"

  2005   shows "cp s th' = cp s' th'"

  2006   apply (unfold cp_eq_cpreced cpreced_def)

  2006   apply (unfold cp_eq_cpreced cpreced_def)

  2007 proof -

  2007 proof -

  2008   have nd': "(Th th, Th th') \<notin> (child s)^+"

  2008   have nd': "(Th th, Th th') \<notin> (child s)^+"

  2046   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  2046   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  2047         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp

  2047         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp

  2048 qed

  2048 qed

  2049 

  2049 

  2050 lemma eq_up:

  2050 lemma eq_up:

  2052   assumes dp1: "th \<in> dependants s th'"

  2051   assumes dp1: "th \<in> dependants s th'"

  2053   and dp2: "th' \<in> dependants s th''"

  2052   and dp2: "th' \<in> dependants s th''"

  2054   and eq_cps: "cp s th' = cp s' th'"

  2053   and eq_cps: "cp s th' = cp s' th'"

  2055   shows "cp s th'' = cp s' th''"

  2054   shows "cp s th'' = cp s' th''"

  2056 proof -

  2055 proof -