[STATEMENT]
lemma ht_phl_seq: "\<lbrace>p\<rbrace> x \<lbrace>r\<rbrace> \<Longrightarrow> \<lbrace>r\<rbrace> y \<lbrace>q\<rbrace> \<Longrightarrow> \<lbrace>p\<rbrace> x \<cdot> y \<lbrace>q\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>p\<rbrace>x\<lbrace>r\<rbrace>; \<lbrace>r\<rbrace>y\<lbrace>q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x \<cdot> y\<lbrace>q\<rbrace>
[PROOF STEP]
by (fact phl_seq)