Finished adding the function symbol for the bound on the plan lengths. Proved its validity with respect to lemma 2 in Charles' paper.