[STATEMENT]
lemma not_lnull_sswSts: "\<not> lnull sswSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lnull sswSts
[PROOF STEP]
using deriv_sswSts_weighted_RP
[PROOF STATE]
proof (prove)
using this:
chain (\<leadsto>\<^sub>w) sswSts

goal (1 subgoal):
 1. \<not> lnull sswSts
[PROOF STEP]
by (cases rule: chain.cases) auto