equal
deleted
inserted
replaced
556 proof - |
556 proof - |
557 -- {* Since the counts of @{term th'} are balanced, the subtree |
557 -- {* Since the counts of @{term th'} are balanced, the subtree |
558 of it contains only itself, so, its @{term cp}-value |
558 of it contains only itself, so, its @{term cp}-value |
559 equals its @{term preced}-value: *} |
559 equals its @{term preced}-value: *} |
560 have "?L = cp (t@s) th'" |
560 have "?L = cp (t@s) th'" |
561 by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) |
561 by (simp add: detached_cp_preced eq_pv vat_t.detached_intro) |
562 -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion}, |
562 -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion}, |
563 its @{term cp}-value equals @{term "preced th s"}, |
563 its @{term cp}-value equals @{term "preced th s"}, |
564 which equals to @{term "?R"} by simplification: *} |
564 which equals to @{term "?R"} by simplification: *} |
565 also have "... = ?R" |
565 also have "... = ?R" |
566 thm running_preced_inversion |
566 thm running_preced_inversion |