Lines Matching refs:function
32 (* Relationship between checkDeltaC function
66 (* Intermediate lemmas to reason about recursive function bounds *)
156 (* Relationship between cmVal function and valid_cha_shift specification *)
172 (* Proving bounds on cmVal function with valid input *)
203 (* Relationship between checkDeltaS function
272 (* Intermediate lemmas to reason about recursive function bounds *)
369 (* Relationship between smVal function and valid_suf_shift specification *)
390 (* Proving bounds on smVal function with valid input *)
680 (* Final proof that the bmSearch function correctly searches
825 (* Final proof that the bmSearchString function correctly searches