773 lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)"

   774 proof -

   775   from moment_plus_split [of i "length s" "t@s"]

   776   have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"

   777     by auto

   778   with app_moment_restm[of t s]

   779   have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp

   780   with moment_app show ?thesis by auto

   781 qed

   782