equal
deleted
inserted
replaced
394 neither of these two threads has children with changed @{text cp}-value. |
394 neither of these two threads has children with changed @{text cp}-value. |
395 It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating |
395 It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating |
396 the @{text cp}-values for @{text th} and @{text taker}. |
396 the @{text cp}-values for @{text th} and @{text taker}. |
397 *} |
397 *} |
398 |
398 |
399 lemma "taker \<notin> children (tG (e#s)) th" |
399 lemma t1: "taker \<notin> children (tG (e#s)) th" |
400 by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp |
400 by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp |
401 subtree_ancestorsI taker_ready_es vat_es.root_readys_tG) |
401 subtree_ancestorsI taker_ready_es vat_es.root_readys_tG) |
402 |
402 |
403 |
403 |
404 lemma "th \<notin> children (tG (e#s)) taker" |
404 lemma t2: "th \<notin> children (tG (e#s)) taker" |
405 by (metis children_subtree empty_iff neq_taker_th root_def |
405 by (metis children_subtree empty_iff neq_taker_th root_def |
406 subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG) |
406 subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG) |
407 |
407 |
408 |
408 |
409 end |
409 end |