@@ -19,16 +19,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
19
19
// / second one, starting at position offset.
20
20
// /
21
21
// / These axioms are:
22
- // / 1. \f$ {\tt isprefix} \Rightarrow {\tt offset_within_bounds}\f$
23
- // / 2. \f$ \ forall 0 \le qvar<|{\tt prefix}|.\ {\tt isprefix}
24
- // / \Rightarrow s0 [qvar+{\tt offset}]=s2 [qvar] \f$
25
- // / 3. \f$ (\lnot {\tt isprefix} \Rightarrow
26
- // / \lnot {\tt offset_within_bounds}
27
- // / \lor (0 \le witness<|{\tt prefix}|
28
- // / \land {\tt str}[witness+{\tt offset}] \ne {\tt prefix}[witness])\f$
29
- // / where \f$ {\tt offset_within_bounds} \f$ is
30
- // / \f$ offset \ge 0 \land offset \le |str| \land
31
- // / |str| - offset \ge |{\tt prefix}| \f$
22
+ // / 1. isprefix => offset_within_bounds
23
+ // / 2. forall qvar in [0, | prefix|).
24
+ // / isprefix => str [qvar + offset] = prefix [qvar]
25
+ // / 3. ! isprefix => !offset_within_bounds
26
+ // / || 0 <= witness < |prefix|
27
+ // / && str[ witness+offset] != prefix[witness]
28
+ // /
29
+ // / where offset_within_bounds is:
30
+ // / offset >= 0 && offset <= |str| && |str| - offset >= |prefix|
31
+ // /
32
32
// / \param prefix: an array of characters
33
33
// / \param str: an array of characters
34
34
// / \param offset: an integer
0 commit comments