[STATEMENT]
lemma pwd_owner_iv_rel_1:
 "\<lbrakk>n \<in> bad_prikey \<inter> bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\<rbrakk> \<Longrightarrow>
    s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)"
      (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<Turnstile> ?t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> bad_prikey \<inter> bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\<rbrakk> \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)
[PROOF STEP]
by (rule rtrancl_into_rtrancl, erule pwd_spy_iii_rel, drule pwd_spy_iii_msg,
 subgoal_tac "(s, ?t) \<in> rel_owner_iv", simp_all add: rel_def pwd_owner_iv_def
 Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B],
 rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto)