equal
deleted
inserted
replaced
548 proof - |
548 proof - |
549 -- {* Since the counts of @{term th'} are balanced, the subtree |
549 -- {* Since the counts of @{term th'} are balanced, the subtree |
550 of it contains only itself, so, its @{term cp}-value |
550 of it contains only itself, so, its @{term cp}-value |
551 equals its @{term preced}-value: *} |
551 equals its @{term preced}-value: *} |
552 have "?L = cp (t@s) th'" |
552 have "?L = cp (t@s) th'" |
553 by (unfold cp_eq_cpreced cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) |
553 by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) |
554 -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, |
554 -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, |
555 its @{term cp}-value equals @{term "preced th s"}, |
555 its @{term cp}-value equals @{term "preced th s"}, |
556 which equals to @{term "?R"} by simplification: *} |
556 which equals to @{term "?R"} by simplification: *} |
557 also have "... = ?R" |
557 also have "... = ?R" |
558 thm runing_preced_inversion |
558 thm runing_preced_inversion |