(* Title: The Partial Cost Model of the List Update Problem Author: Max Haslbeck *) section "Partial cost model" theory Partial_Cost_Model imports Move_to_Front begin definition t⇩p :: "'a state ⇒ 'a ⇒ answer ⇒ nat" where "t⇩p s q a = (let (mf,sws) = a in index (swaps sws s) q + size sws)" notation (latex) t⇩p ("\<^latex>‹$t^{*}$›") lemma t⇩pt: "t⇩p s q a + 1 = t s q a" unfolding t⇩p_def t_def by(simp add: split_def)