[STATEMENT]
lemma trans_path_non_nil: "ps \<noteq> [] \<Longrightarrow> trans_path (k\<^sub>1,k\<^sub>2) ps \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<noteq> [] \<Longrightarrow> trans_path (k\<^sub>1, k\<^sub>2) ps \<noteq> []
[PROOF STEP]
by (induction ps) auto