|
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