[STATEMENT]
lemma is_final_dstate_imp_not_weighted_RP: "is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'
[PROOF STEP]
using wrp.final_weighted_RP
[PROOF STATE]
proof (prove)
using this:
\<not> ({#}, {#}, ?Q, ?n) \<leadsto>\<^sub>w ?St

goal (1 subgoal):
 1. is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'
[PROOF STEP]
by (cases St) (auto intro: wrp.final_weighted_RP simp: is_final_dstate.simps)