#|
Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "mc20-2" using the compiled version.

; some general theorems.  They are used to establish properties of string
; functions.

Theorem: ilessp-lessp ((x ∈ N) ∧ (y ∈ N)) → (ilessp (x, y) = (x < y))

Theorem: idifference-numberp (idifference (x, y) ∈ N) = (¬ ilessp (x, y))

Theorem: idifference-equal-0 (idifference (x, y) = 0) = (fix-int (x) = fix-int (y))

Event: Enable get-nth-0.

Event: Enable put-nth-0.

; the upper bound of strlen.

Theorem: strlen-ub stringp (i, n, lst) → (strlen (i, n, lst) < n)

; the lower bound of strlen.

Theorem: strlen-lb strlen (i, n, lst) ≮ i

Theorem: strlen-01 (strlen (i, 0, lst) = i) ∧ (strlen (i, 1, lst)

= if (i < 1) ∧ (get-nth (0, lst) ≠ 0) then 1

else i endif)

∧ (strlen (1, n, lst) ≠ 0)

Theorem: strlen-ii strlen (i, i, lst) = i

Theorem: strlen-ii1 strlen (i, 1 + i, lst) = if get-nth (i, lst) = 0 then i

else 1 + i endif

; some properties of strlen.
; lst[j] =\= 0, if i <= j < strlen(lst).

Theorem: strlen-non0p ((i ≤ j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ 0)

; lst[strlen] == 0!

Theorem: strlen-0p stringp (i, n, lst) → (get-nth (strlen (i, n, lst), lst) = 0)

; some properties of strcpy.

Theorem: strcpy-get-1 (j < i) → (get-nth (j , strcpy (i, lst1 , n2 , lst2 )) = get-nth (j , lst1 ))

; strlen(strcpy(lst1, lst2)) == strlen(lst2).

Theorem: strcpy-strlen strlen (i, n2 , strcpy (i, lst1 , n2 , lst2 )) = strlen (i, n2 , lst2 )

;  if i <= j <= strlen(lst2), lst1[j] == lst2[j].

Theorem: strcpy-cpy (stringp (i, n2 , lst2 ) ∧ (i ≤ j ) ∧ (j ≤ strlen (i, n2 , lst2 ))) → (get-nth (j , strcpy (i, lst1 , n2 , lst2 )) = get-nth (j , lst2 ))

;  if lst2 is a string, then lst1' is also a string.

Theorem: strcpy-stringp stringp (i, n2 , lst2 ) → stringp (i, n2 , strcpy (i, lst1 , n2 , lst2 ))

; some properties of strcmp.
; (strcmp lst lst) == 0.

Theorem: strcmp-id strcmp (i, n, lst, lst) = 0

; (strcmp lst1 lst2) < 0 ==> (strcmp lst2 lst1) >= 0.

Theorem: strcmp-antisym negativep (strcmp (i, n, lst1 , lst2 )) = (0 < strcmp (i, n, lst2 , lst1 ))

; the transitivity of strcmp.

Theorem: strcmp-trans-1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ lst-of-chrp (lst3 ) ∧ (strcmp (i, n, lst1 , lst2 ) ∈ N) ∧ (strcmp (i, n, lst2 , lst3 ) ∈ N)) → (strcmp (i, n, lst1 , lst3 ) ∈ N)

; (strcpy lst1 lst2) == lst2.

Theorem: strcmp-strcpy strcmp (i, n, lst2 , strcpy (i, lst1 , n, lst2 )) = 0

; if (strcmp lst1 lst2) == 0, all i <= j < (strlen lst1) lst1[j] == lst2[j].

Theorem: strcmp-thm1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (strcmp (i, n, lst1 , lst2 ) = 0) ∧ (i ≤ j ) ∧ (j < strlen (i, n, lst1 ))) → (get-nth (j , lst1 ) = get-nth (j , lst2 ))

Definition: strcmp-sk (n1 , lst1 , lst2 ) ↔ ∃ j (∀ i ((i < j ) → (get-nth (i, lst1 ) = get-nth (i, lst2 )))

∧ (strcmp (0, n1 , lst1 , lst2 ) = idifference (get-nth (j , lst1 ), get-nth (j , lst2 ))))

Definition: strcmp-j (i, n1 , lst1 , lst2 ) = if i < n1

then if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if get-nth (i, lst1 ) = null then fix (i)

else strcmp-j (1 + i, n1 , lst1 , lst2 ) endif else fix (i) endif

else fix (i) endif

Theorem: strcmp-j-1 ((i < strcmp-j (i1 , n1 , lst1 , lst2 )) ∧ (i1 ≤ i)) → (get-nth (i, lst1 ) = get-nth (i, lst2 ))

Theorem: strcmp-j-2 (strcmp (i1 , n1 , lst1 , lst2 ) ≠ 0) → (strcmp (i1 , n1 , lst1 , lst2 )

= idifference (get-nth (strcmp-j (i1 , n1 , lst1 , lst2 ), lst1 ), get-nth (strcmp-j (i1 , n1 , lst1 , lst2 ), lst2 )))

Theorem: strcmp-thm2 (strcmp (0, n1 , lst1 , lst2 ) ≠ 0) → strcmp-sk (n1 , lst1 , lst2 )

Event: Disable strcmp-j-1.

Event: Disable strcmp-j-2.

; some properties of strcat.

Theorem: strcpy1-get-1 (j < i1 ) → (get-nth (j , strcpy1 (i1 , lst1 , i2 , n2 , lst2 )) = get-nth (j , lst1 ))

Definition: strlen1 (i, n, lst) = if i < n

then if get-nth (i, lst) = null then 0

else 1 + strlen1 (1 + i, n, lst) endif else 0 endif Theorem: strlen1-strlen strlen1 (i, n, lst) = (strlen (i, n, lst) − i)

Event: Disable strlen1-strlen.

Theorem: strcpy1-get-2 ((i1 + strlen1 (i2 , n2 , lst2 )) < j ) → (get-nth (j , strcpy1 (i1 , lst1 , i2 , n2 , lst2 )) = get-nth (j , lst1 ))

Theorem: get-nth-plus-0 (j ∉ N) → (get-nth (i + j , lst) = get-nth (i, lst))

Theorem: plus-sub1-add1 ((x + (1 + y)) − 1) = (x + y)

Theorem: strcpy1-get-3 ((i1 ≤ j ) ∧ (j < (i1 + strlen1 (i2 , n2 , lst2 )))) → (get-nth (j , strcpy1 (i1 , lst1 , i2 , n2 , lst2 ))

= get-nth (i2 + (j − i1 ), lst2 ))

; all 0 <= j < (strlen lst1) lst1'[j] == lst1[j].

Theorem: strcat-get-1 (j < strlen (0, n1 , lst1 )) → (get-nth (j , strcat (n1 , lst1 , n2 , lst2 )) = get-nth (j , lst1 ))

; all (strlen lst1) <= j < (strlen lst1)+(strlen lst2) lst1'[j] == lst2[j].

Theorem: strcat-get-2 (stringp (0, n1 , lst1 ) ∧ (strlen (0, n1 , lst1 ) ≤ j ) ∧ (j < (strlen (0, n1 , lst1 ) + strlen (0, n2 , lst2 )))) → (get-nth (j , strcat (n1 , lst1 , n2 , lst2 ))

= get-nth (j − strlen (0, n1 , lst1 ), lst2 ))

; some properties about strchr.
; lst[strchr] == ch,  if strchr returns non-f.

Theorem: strchr-thm1 strchr (i, n, lst, ch) → (get-nth (strchr (i, n, lst, ch), lst) = ch)

; all i <= j < strchr, lst[j] =\= ch.  i.e. strchr is the first one.

Theorem: strchr-thm2 ((i ≤ j ) ∧ (j < strchr (i, n, lst, ch))) → (get-nth (j , lst) ≠ ch)

; all i <= j < strlen, lst[j] =\= ch, if strchr returns f.

Theorem: strchr-thm3 ((¬ strchr (i, n, lst, ch)) ∧ (i ≤ j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ ch)

; ch is not equal to the null character, if strchr returns f.

Theorem: strchr-thm4 (stringp (i, n, lst) ∧ (¬ strchr (i, n, lst, ch))) → (ch ≠ 0)

; strcpy and strchr.

Theorem: strcpy-strchr strchr (i, n, strcpy (i, lst1 , n, lst2 ), ch) = strchr (i, n, lst2 , ch)

; some properties about memset.
; lemmas about memset1.

Theorem: memset1-get-1 (j < i) → (get-nth (j , memset1 (i, n, lst, ch)) = get-nth (j , lst))

; all i <= j < i+n, lst'[j] == ch.

Theorem: memset1-thm1 ((i ≤ j ) ∧ (j < (i + n))) → (get-nth (j , memset1 (i, n, lst, ch)) = ch) Theorem: memset1-thm2 (((i + n) ≤ j ) ∧ (n ≄ 0)) → (get-nth (j , memset1 (i, n, lst, ch)) = get-nth (j , lst))

; all i <= j < n, lst'[j] == ch.

Theorem: memset-thm1 ((i ≤ j ) ∧ (j < n)) → (get-nth (j , memset (n, lst, ch)) = ch)

; all j >= n, lst'[j] == lst[j].

Theorem: memset-thm2 ((n ≤ j ) ∧ (n ∈ N)) → (get-nth (j , memset (n, lst, ch)) = get-nth (j , lst))

; some properties about memchr.

Theorem: memchr1-thm1 memchr1 (i, n, lst, ch) → (get-nth (memchr1 (i, n, lst, ch), lst) = ch)

; lst[memchr] == ch,  if memchr returns non-f.

Theorem: memchr-thm1 memchr (n, lst, ch) → (get-nth (memchr (n, lst, ch), lst) = ch) Theorem: memchr1-thm2 ((i ≤ j ) ∧ (j < memchr1 (i, n, lst, ch))) → (get-nth (j , lst) ≠ ch)

; all j < memchr, lst[j] =\= ch.  i.e. memchr is the first one.

Theorem: memchr-thm2 (j < memchr (n, lst, ch)) → (get-nth (j , lst) ≠ ch) Theorem: memchr1-thm3 ((¬ memchr1 (i, n, lst, ch)) ∧ (i ≤ j ) ∧ (j < (i + n))) → (get-nth (j , lst) ≠ ch)

; all j < n, lst[j] =\= ch, if memchr returns f.

Theorem: memchr-thm3 ((¬ memchr (n, lst, ch)) ∧ (j < n)) → (get-nth (j , lst) ≠ ch)

; some properties about strrchr.

Theorem: strrchr-la1 (j ∈ N) → strrchr (i, n, lst, ch, j ) Theorem: strrchr-strchr-la (¬ strchr (i, n, lst, ch)) → (strrchr (i, n, lst, ch, j ) = j ) Theorem: strrchr-la2 strchr (i, n, lst, ch) → (get-nth (strrchr (i, n, lst, ch, j ), lst) = ch)

; strrchr finds ch in the string.

Theorem: strrchr-thm1 strrchr (i, n, lst, ch, f) → (get-nth (strrchr (i, n, lst, ch, f), lst) = ch) Theorem: strchr-get ((i ≤ j ) ∧ (j < strlen (i, n, lst))) → strchr (i, n, lst, get-nth (j , lst)) Theorem: strrchr-la3 (strchr (i, n, lst, ch) ∧ (strrchr (i, n, lst, ch, k) < j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ ch)

; strrchr returns the last one.

Theorem: strrchr-thm2 (strrchr (i, n, lst, ch, f) ∧ (strrchr (i, n, lst, ch, f) < j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ ch)

; no means none.

Theorem: strrchr-thm3 ((¬ strrchr (i, n, lst, ch, k)) ∧ (i ≤ j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ ch)

; ch is not equal to the null character, if strrchr returns f.

Theorem: strrchr-thm4 (stringp (i, n, lst) ∧ (¬ strrchr (i, n, lst, ch, k))) → (ch ≠ 0)

; some properties about memcmp.

Theorem: memcmp1-id memcmp1 (i, n, lst, lst) = 0

Theorem: memcmp-id memcmp (n, lst, lst) = 0

Theorem: memcmp1-thm1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (memcmp1 (i, n, lst1 , lst2 ) = 0) ∧ (i ≤ j ) ∧ (j < (i + n))) → (get-nth (j , lst1 ) = get-nth (j , lst2 ))

Theorem: memcmp-thm1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (memcmp (n, lst1 , lst2 ) = 0) ∧ (j < n)) → (get-nth (j , lst1 ) = get-nth (j , lst2 ))

Definition: memcmp-sk (n, lst1 , lst2 ) ↔ ∃ j (∀ i ((i < j ) → (get-nth (i, lst1 ) = get-nth (i, lst2 )))

∧ (memcmp (n, lst1 , lst2 ) = idifference (get-nth (j , lst1 ), get-nth (j , lst2 ))))

Definition: memcmp-j (i, n, lst1 , lst2 ) = if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if (n − 1) = 0 then fix (i)

else memcmp-j (1 + i, n − 1, lst1 , lst2 ) endif else fix (i) endif

Theorem: memcmp-j-1 ((i < memcmp-j (i1 , n1 , lst1 , lst2 )) ∧ (i1 ≤ i)) → (get-nth (i, lst1 ) = get-nth (i, lst2 ))

Theorem: memcmp-j-2 (memcmp1 (i1 , n1 , lst1 , lst2 ) ≠ 0) → (memcmp1 (i1 , n1 , lst1 , lst2 )

= idifference (get-nth (memcmp-j (i1 , n1 , lst1 , lst2 ), lst1 ), get-nth (memcmp-j (i1 , n1 , lst1 , lst2 ), lst2 )))

Theorem: memcmp-thm2 (memcmp (n, lst1 , lst2 ) ≠ 0) → memcmp-sk (n, lst1 , lst2 )

Event: Disable memcmp-j-1.

Event: Disable memcmp-j-2.

; some properties about strncat.

Theorem: strcpy2-get-1 (j < i1 ) → (get-nth (j , strcpy2 (i1 , lst1 , i2 , n2 , lst2 )) = get-nth (j , lst1 ))

Theorem: strlen1-ii strlen1 (i, i, lst) = 0

Theorem: strcpy2-get-2 ((i1 ≤ j ) ∧ (j < (i1 + strlen1 (i2 , i2 + n2 , lst2 )))) → (get-nth (j , strcpy2 (i1 , lst1 , i2 , n2 , lst2 ))

= get-nth ((i2 + j ) − i1 , lst2 ))

; all j < (strlen lst1), lst'[j] == lst1[j].

Theorem: strncat-get-1 (j < strlen (0, n1 , lst1 )) → (get-nth (j , strncat (n1 , lst1 , n2 , lst2 )) = get-nth (j , lst1 ))

; all (strlen lst1) <= j < (strlen lst1)+(strlen lst2),
; lst'[j] == lst2[j-(strlen lst1)].

Theorem: strncat-get-2 (stringp (0, n1 , lst1 ) ∧ (strlen (0, n1 , lst1 ) ≤ j ) ∧ (j < (strlen (0, n1 , lst1 ) + strlen (0, n2 , lst2 )))) → (get-nth (j , strncat (n1 , lst1 , n2 , lst2 ))

= get-nth (j − strlen (0, n1 , lst1 ), lst2 ))

; some properties about strncpy.

Theorem: zero-list1-la (j < i) → (get-nth (j , zero-list1 (i, n, lst)) = get-nth (j , lst))

Theorem: zero-list1-get ((i ≤ j ) ∧ (j < ((i + n) − 1))) → (get-nth (j , zero-list1 (i, n, lst)) = 0)

Theorem: zero-list-get ((i ≤ j ) ∧ (j < (i + n))) → (get-nth (j , zero-list (i, n, lst)) = 0)

Theorem: strncpy1-get (j < i) → (get-nth (j , strncpy1 (i, n, lst1 , lst2 )) = get-nth (j , lst1 ))

Event: Disable zero-list.

Theorem: strncpy1-strlen strlen (i, i + n, strncpy1 (i, n, lst1 , lst2 )) = strlen (i, i + n, lst2 )

Theorem: strcpy-0 strncpy (0, lst1 , lst2 ) = lst1

; the length of (strncpy lst1 lst2) equals the length of lst2.

Theorem: strncpy-strlen strlen (0, n, strncpy (n, lst1 , lst2 )) = if n ≃ 0 then strlen (0, n, lst1 )

else strlen (0, n, lst2 ) endif

Theorem: strncpy1-cpy ((i ≤ j ) ∧ (j < strlen (i, i + n, lst2 ))) → (get-nth (j , strncpy1 (i, n, lst1 , lst2 )) = get-nth (j , lst2 ))

; all j < (strlen lst2), lst'[j] == lst2[j].

Theorem: strncpy-cpy (j < strlen (0, n, lst2 )) → (get-nth (j , strncpy (n, lst1 , lst2 )) = get-nth (j , lst2 ))

Theorem: strncpy1-0s ((strlen (i, i + n, lst2 ) ≤ j ) ∧ (j < (i + n))) → (get-nth (j , strncpy1 (i, n, lst1 , lst2 )) = 0)

; all (strlen lst2) <= j < n, lst'[j] == 0.

Theorem: strncpy-0s ((strlen (0, n, lst2 ) ≤ j ) ∧ (j < n)) → (get-nth (j , strncpy (n, lst1 , lst2 )) = 0)

; some properties about strncmp.

Theorem: strncmp1-id strncmp1 (i, n, lst, lst) = 0

Theorem: strncmp-id strncmp (n, lst, lst) = 0

Theorem: strncmp1-thm1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (strncmp1 (i, n, lst1 , lst2 ) = 0) ∧ (i ≤ j ) ∧ (j < strlen (i, i + n, lst1 ))) → (get-nth (j , lst1 ) = get-nth (j , lst2 ))

Theorem: strncmp-thm1 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (strncmp (n, lst1 , lst2 ) = 0) ∧ (j < strlen (0, n, lst1 ))) → (get-nth (j , lst1 ) = get-nth (j , lst2 ))

Definition: strncmp-j (i, n, lst1 , lst2 ) = if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if get-nth (i, lst1 ) = 0 then fix (i) elseif (n − 1) = 0 then fix (i) else strncmp-j (1 + i, n − 1, lst1 , lst2 ) endif

else fix (i) endif

Definition: strncmp-sk (n, lst1 , lst2 ) ↔ ∃ j (∀ i ((i < j ) → (get-nth (i, lst1 ) = get-nth (i, lst2 )))

∧ (strncmp (n, lst1 , lst2 ) = idifference (get-nth (j , lst1 ), get-nth (j , lst2 ))))

Theorem: strncmp-j-1 ((i < strncmp-j (i1 , n1 , lst1 , lst2 )) ∧ (i1 ≤ i)) → (get-nth (i, lst1 ) = get-nth (i, lst2 ))

Theorem: strncmp-j-2 (strncmp1 (i1 , n1 , lst1 , lst2 ) ≠ 0) → (strncmp1 (i1 , n1 , lst1 , lst2 )

= idifference (get-nth (strncmp-j (i1 , n1 , lst1 , lst2 ), lst1 ), get-nth (strncmp-j (i1 , n1 , lst1 , lst2 ), lst2 )))

Theorem: strncmp-thm2 (strncmp (n, lst1 , lst2 ) ≠ 0) → strncmp-sk (n, lst1 , lst2 )

Event: Disable strncmp-j-1.

Event: Disable strncmp-j-2.

; some properties about strpbrk.

Theorem: strpbrk-thm1 let j be strpbrk (i1 , n1 , lst1 , n2 , lst2 ) in j → strchr1 (0, n2 , lst2 , get-nth (j , lst1 )) endlet

Theorem: strpbrk-thm2 ((i1 ≤ j ) ∧ (j < strpbrk (i1 , n1 , lst1 , n2 , lst2 ))) → (¬ strchr1 (0, n2 , lst2 , get-nth (j , lst1 )))

Theorem: strpbrk-thm3 ((¬ strpbrk (i1 , n1 , lst1 , n2 , lst2 )) ∧ (i1 ≤ j ) ∧ (j < strlen (i1 , n1 , lst1 ))) → (¬ strchr1 (0, n2 , lst2 , get-nth (j , lst1 )))

; strchr1, which is used to specify several string functions, is a variant
; of strchr.  strchr1 does not have the `thm4' of strchr.

Theorem: strchr1-thm1 strchr1 (i, n, lst, ch) → (get-nth (strchr1 (i, n, lst, ch), lst) = ch)

Theorem: strchr1-thm2 ((i ≤ j ) ∧ (j < strchr1 (i, n, lst, ch))) → (get-nth (j , lst) ≠ ch)

Theorem: strchr1-thm3 ((¬ strchr1 (i, n, lst, ch)) ∧ (i ≤ j ) ∧ (j < strlen (i, n, lst))) → (get-nth (j , lst) ≠ ch)

; some properties of strcspn.

Theorem: strcspn-thm1 let j be strcspn (i1 , n1 , lst1 , n2 , lst2 ) in j → strchr (0, n2 , lst2 , get-nth (j , lst1 )) endlet

Theorem: strcspn-thm2 ((i1 ≤ j ) ∧ (j < strcspn (i1 , n1 , lst1 , n2 , lst2 ))) → (¬ strchr (0, n2 , lst2 , get-nth (j , lst1 )))

Theorem: strcspn-thm3 ((¬ strcspn (i1 , n1 , lst1 , n2 , lst2 )) ∧ (i1 ≤ j ) ∧ (j < strlen (i1 , n1 , lst1 ))) → (¬ strchr (0, n2 , lst2 , get-nth (j , lst1 )))

; some properties of strspn.

Theorem: strspn-thm1 let j be strspn (i1 , n1 , lst1 , n2 , lst2 ) in j → (¬ strchr1 (0, n2 , lst2 , get-nth (j , lst1 ))) endlet

Theorem: strspn-thm2 ((i1 ≤ j ) ∧ (j < strspn (i1 , n1 , lst1 , n2 , lst2 ))) → strchr1 (0, n2 , lst2 , get-nth (j , lst1 ))

Theorem: strspn-thm3 ((¬ strspn (i1 , n1 , lst1 , n2 , lst2 )) ∧ (i1 ≤ j ) ∧ (j < strlen (i1 , n1 , lst1 ))) → strchr1 (0, n2 , lst2 , get-nth (j , lst1 ))

; a generalized defn for strncmp.

Definition: strncmp2 (i, n, lst1 , j , lst2 ) = if n ≃ 0 then 0

elseif get-nth (i, lst1 ) = get-nth (j , lst2 )

then if get-nth (i, lst1 ) = 0 then 0

else strncmp2 (1 + i, n − 1, lst1 , 1 + j , lst2 ) endif else idifference (get-nth (i, lst1 ), get-nth (j , lst2 )) endif

Theorem: strncmp2-non-numberp (i ∉ N) → (strncmp2 (i, n, lst1 , j , lst2 ) = strncmp2 (0, n, lst1 , j , lst2 ))

Theorem: strncmp2-0 strncmp2 (i, 0, lst1 , j , lst2 ) = 0

Theorem: strncmp1-strncmp2 (n ≄ 0) → (strncmp1 (i, n, lst1 , lst2 ) = strncmp2 (i, n, lst1 , i, lst2 ))

Theorem: strncmp-strncmp2 strncmp (n, lst1 , lst2 ) = strncmp2 (0, n, lst1 , 0, lst2 )

Theorem: strncmp2-mcdr-1 strncmp2 (i1 , n, mcdr (j , lst1 ), i2 , lst2 ) = strncmp2 (i1 + j , n, lst1 , i2 , lst2 )

Theorem: strncmp2-mcdr-2 strncmp2 (i1 , n, lst1 , i2 , mcdr (j , lst2 )) = strncmp2 (i1 , n, lst1 , i2 + j , lst2 )

; a lemma of strlen and mcdr.

Theorem: strlen-cdr (i ∈ N) → (strlen (i, n − 1, mcdr (1, lst)) = (strlen (1 + i, n, lst) − 1))

Theorem: strlen-mcdr (i ∈ N) → (strlen (i, n, mcdr (k, lst)) = (strlen (i + k, k + n, lst) − k))

; some properties of strstr.
; a lemma for strstr-thm1.

Theorem: strstr1-thm1 let j be strstr1 (i, n1 , lst1 , n2 , lst2 , len) in ((j ∈ N) ∧ (n = (1 + len))) → (strncmp2 (j , n, lst1 , 0, lst2 ) = 0) endlet

; all 0 <= i < (strlen lst2), lst1[j+i] == lst2[i], if strstr == j =\= 0.

Theorem: strstr-thm1 let j be strstr (n1 , lst1 , n2 , lst2 ) in (j ∈ N) → (strncmp (strlen (0, n2 , lst2 ), mcdr (j , lst1 ), lst2 ) = 0) endlet

; a few lemmas about strchr1.

Theorem: strchr1-nth ((i ≤ j ) ∧ (j < strlen (i, n, lst))) → (strchr1 (i, n, lst, get-nth (j , lst)) ∈ N)

Theorem: strlen-strchr1-nth ((i ≤ j ) ∧ (j < strlen (i, n, lst))) → (strlen (1 + strchr1 (i, n, lst, get-nth (j , lst)), n, lst)

= strlen (i, n, lst))

Theorem: strlen-strchr1 (strchr1 (i, n, lst, 0) ∈ N) → (strchr1 (i, n, lst, 0) ≮ strlen (i, n, lst))

Theorem: strchr1-ch0 ¬ strchr1 (i, n, lst, 0)

Theorem: strchr1-nth-first ((strchr1 (i, n, lst, get-nth (j , lst)) ∈ N) ∧ (i ≤ j )) → (j ≮ strchr1 (i, n, lst, get-nth (j , lst)))

; a lemma for strstr-thm2.

Theorem: strstr1-thm2 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (i ≤ j ) ∧ (j < strstr1 (i, n1 , lst1 , n2 , lst2 , len)) ∧ (n = (1 + len))) → (strncmp2 (j , n, lst1 , 0, lst2 ) ≠ 0)

; all j < (strstr lst1 lst2), (strncmp (mcdr j lst1) lst2) =\= 0.

Theorem: strstr-thm2 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (j < strstr (n1 , lst1 , n2 , lst2 )) ∧ (n2 ≄ 0)) → (strncmp (strlen (0, n2 , lst2 ), mcdr (j , lst1 ), lst2 ) ≠ 0)

; a lemma for strstr-thm3.

Theorem: strstr1-thm3 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (¬ strstr1 (i, n1 , lst1 , n2 , lst2 , len)) ∧ (i ≤ j ) ∧ (j < strlen (i, n1 , lst1 )) ∧ (n = (1 + len))) → (strncmp2 (j , n, lst1 , 0, lst2 ) ≠ 0)

; all j < (strlen lst1), (strncmp (mcdr j lst1) lst2) =\= 0.

Theorem: strstr-thm3 (lst-of-chrp (lst1 ) ∧ lst-of-chrp (lst2 ) ∧ (¬ strstr (n1 , lst1 , n2 , lst2 )) ∧ (j < strlen (0, n1 , lst1 )) ∧ (n2 ≄ 0)) → (strncmp (strlen (0, n2 , lst2 ), mcdr (j , lst1 ), lst2 ) ≠ 0)

; some properties of strtok.

Theorem: strtok-thm1 let i be strspn (0, n1 , lst1 , n2 , lst2 ) in ((nat-to-uint (s1 ) ≠ 0) ∧ (get-nth (i, lst1 ) = 0)) → ((strtok-tok (s1 , last, n1 , lst1 , n2 , lst2 ) = 0)

∧ (strtok-last (s1 , last, n1 , lst1 , n2 , lst2 ) = 0) ∧ (strtok-lst (n1 , lst1 , n2 , lst2 ) = lst1 )) endlet

Theorem: strtok-thm2 let i be strspn (0, n1 , lst1 , n2 , lst2 ) in ((nat-to-uint (s1 ) ≠ 0) ∧ (get-nth (i, lst1 ) ≠ 0) ∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ), lst1 ) = 0) ∧ stringp (0, n1 , lst1 ) ∧ (n1 ∈ N)) → ((strtok-tok (s1 , last, n1 , lst1 , n2 , lst2 )

= add (32, s1 , strspn* (0, 0, n1 , lst1 , n2 , lst2 ))) ∧ (strtok-last (s1 , last, n1 , lst1 , n2 , lst2 ) = 0) ∧ (strtok-lst (n1 , lst1 , n2 , lst2 ) = lst1 )) endlet

Theorem: strspn-strchr1 strspn (i1 , n1 , lst1 , n2 , lst2 ) → (¬ strchr1 (0, n2 , lst2 , get-nth (strspn (i1 , n1 , lst1 , n2 , lst2 ), lst1 )))

Theorem: strchr-strchr1 (ch ≠ 0) → (strchr (i, n, lst, ch) = strchr1 (i, n, lst, ch))

Theorem: strspn-true (stringp (i, n1 , lst1 ) ∧ stringp (0, n2 , lst2 )) → strspn (i, n1 , lst1 , n2 , lst2 )

Theorem: strtok-thm3 let i* be strspn* (0, 0, n1 , lst1 , n2 , lst2 ),

i be strspn (0, n1 , lst1 , n2 , lst2 ) in ((nat-to-uint (s1 ) ≠ 0) ∧ (get-nth (i, lst1 ) ≠ 0) ∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ), lst1 ) ≠ 0) ∧ stringp (0, n1 , lst1 ) ∧ stringp (0, n2 , lst2 ) ∧ (n1 ∈ N)) → ((strtok-tok (s1 , last, n1 , lst1 , n2 , lst2 )

= add (32, s1 , strspn* (0, 0, n1 , lst1 , n2 , lst2 ))) ∧ (strtok-last (s1 , last, n1 , lst1 , n2 , lst2 )

= add (32, s1 , add (32, strcspn* (i* , i, n1 , lst1 , n2 , lst2 ), 1)))

∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ),

strtok-lst (n1 , lst1 , n2 , lst2 )) = 0)) endlet

Theorem: strtok-thm4 (strtok-tok (0, 0, n1 , lst1 , n2 , lst2 ) = 0) ∧ (strtok-last (0, 0, n1 , lst1 , n2 , lst2 ) = 0)

Theorem: strtok-thm5 let i be strspn (0, n1 , lst1 , n2 , lst2 ) in ((nat-to-uint (last) ≠ 0) ∧ (get-nth (i, lst1 ) ≠ 0) ∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ), lst1 ) = 0) ∧ stringp (0, n1 , lst1 ) ∧ (n1 ∈ N)) → ((strtok-tok (0, last, n1 , lst1 , n2 , lst2 )

= add (32, last, strspn* (0, 0, n1 , lst1 , n2 , lst2 ))) ∧ (strtok-last (0, last, n1 , lst1 , n2 , lst2 ) = 0) ∧ (strtok-lst (n1 , lst1 , n2 , lst2 ) = lst1 )) endlet

Theorem: strtok-thm6 let i* be strspn* (0, 0, n1 , lst1 , n2 , lst2 ),

i be strspn (0, n1 , lst1 , n2 , lst2 ) in ((nat-to-uint (last) ≠ 0) ∧ (get-nth (i, lst1 ) ≠ 0) ∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ), lst1 ) ≠ 0) ∧ stringp (0, n1 , lst1 ) ∧ stringp (0, n2 , lst2 ) ∧ (n1 ∈ N)) → ((strtok-tok (0, last, n1 , lst1 , n2 , lst2 )

= add (32, last, strspn* (0, 0, n1 , lst1 , n2 , lst2 )))

∧ (strtok-last (0, last, n1 , lst1 , n2 , lst2 )

= add (32, last, add (32, strcspn* (i* , i, n1 , lst1 , n2 , lst2 ), 1)))

∧ (get-nth (strcspn (i, n1 , lst1 , n2 , lst2 ),

strtok-lst (n1 , lst1 , n2 , lst2 )) = 0)) endlet

Event: Disable strchr-strchr1.

; some properties of memmove.
; memmove is equivalent to lstmov.

Theorem: mmov1-lst-cpy mmov1-lst (i, lst1 , lst2 , n) = lstcpy (i, lst1 , i, lst2 , n)

Theorem: mmovn-mmov1-lst mmovn-lst (h, lst1 , lst2 , i, n) = mmov1-lst (i, lst1 , lst2 , h ∗ n)

Theorem: lstcpy-nonnumberp (i1 ∉ N) → ((lstcpy (i1 , lst1 , i2 , lst2 , n) = lstcpy (0, lst1 , i2 , lst2 , n))

∧ (lstcpy (i2 , lst1 , i1 , lst2 , n) = lstcpy (i2 , lst1 , 0, lst2 , n)))

Theorem: lstcpy-lstcpy-0 lstcpy (h1 , lstcpy (0, lst1 , 0, lst2 , h1 ), h1 , lst2 , h2 ) = lstcpy (0, lst1 , 0, lst2 , h1 + h2 )

Theorem: mmov1-lst1-cpy (n ≤ i) → (mmov1-lst1 (i, lst1 , lst2 , n) = lstcpy (i − n, lst1 , i − n, lst2 , n))

Theorem: lstcpy-lstcpy-1 ((j1 = (h1 + i1 )) ∧ (j2 = (h1 + i2 ))) → (lstcpy (i1 , lstcpy (j1 , lst1 , j2 , lst2 , h2 ), i2 , lst2 , h1 )

= lstcpy (i1 , lst1 , i2 , lst2 , h1 + h2 ))

Theorem: times-lessp-dual (x < y) → ((x < (y ∗ z)) = (z ≄ 0))

Theorem: mmovn-lst1-mmov1-lst ((h ∗ n) ≤ i) → (mmovn-lst1 (h, lst1 , lst2 , i, n)

= mmov1-lst (i − (h ∗ n), lst1 , lst2 , h ∗ n))

Theorem: quotient-shrink-fast-1 (x < (y ∗ (x ÷ y))) = f

Theorem: memmove-mmov1-lst memmove (str1 , str2 , n, lst1 , lst2 ) = if n ≃ 0 then lst1

elseif nat-to-uint (str1 ) = nat-to-uint (str2 ) then lst2 else mmov1-lst (0, lst1 , lst2 , n) endif

; for k < i, lstcpy(lst1,lst2)[k] == lst1[k].

Theorem: lstcpy-get-1 (k < i) → (get-nth (k, lstcpy (i, lst1 , j , lst2 , n)) = get-nth (k, lst1 ))

; for i <= i1 < i+n, lstcpy(lst1,lst2)[i1] == lst2[i1].

Theorem: lstcpy-get-2 ((i ≤ i1 ) ∧ (i1 < (i + n))) → (get-nth (i1 , lstcpy (i, lst1 , j , lst2 , n))

= get-nth ((j + i1 ) − i, lst2 ))

; for 0 <= i < n, mmov1-lst(lst1,lst2)[i] == lst2[i].

Theorem: mmov1-lst-thm1 (i1 < n) → (get-nth (i1 , mmov1-lst (0, lst1 , lst2 , n)) = get-nth (i1 , lst2 ))

; for 0 <= i < n, memmove(lst1,lst2,n)[i] == lst2[i].

Theorem: memmove-thm1 (i < n) → (get-nth (i, memmove (str1 , str2 , n, lst1 , lst2 )) = get-nth (i, lst2 ))

Index

add, 16–18

exists, 4, 8, 11

fix-int, 1 forall, 4, 8, 11

get-nth, 2–19 get-nth-plus-0, 5

idifference, 1, 4, 8, 9, 11–13 idifference-equal-0, 1 idifference-numberp, 1 ilessp, 1 ilessp-lessp, 1

lst-of-chrp, 3, 8, 11, 15, 16 lstcpy, 18, 19 lstcpy-get-1, 19 lstcpy-get-2, 19 lstcpy-lstcpy-0, 18 lstcpy-lstcpy-1, 18 lstcpy-nonnumberp, 18

mcdr, 14–16 memchr, 7 memchr-thm1, 7 memchr-thm2, 7 memchr-thm3, 7 memchr1, 6, 7 memchr1-thm1, 6 memchr1-thm2, 7 memchr1-thm3, 7 memcmp, 8, 9 memcmp-id, 8 memcmp-j, 9 memcmp-j-1, 9 memcmp-j-2, 9 memcmp-sk, 8, 9 memcmp-thm1, 8 memcmp-thm2, 9 memcmp1, 8, 9 memcmp1-id, 8 memcmp1-thm1, 8 memmove, 19 memmove-mmov1-lst, 19 memmove-thm1, 19 memset, 6 memset-thm1, 6 memset-thm2, 6 memset1, 6 memset1-get-1, 6 memset1-thm1, 6 memset1-thm2, 6 mmov1-lst, 18, 19 mmov1-lst-cpy, 18 mmov1-lst-thm1, 19 mmov1-lst1, 18 mmov1-lst1-cpy, 18 mmovn-lst, 18 mmovn-lst1, 18 mmovn-lst1-mmov1-lst, 18 mmovn-mmov1-lst, 18

nat-to-uint, 16, 17, 19 null, 4

plus-sub1-add1, 5

quotient-shrink-fast-1, 19

strcat, 5 strcat-get-1, 5 strcat-get-2, 5 strchr, 5–7, 13, 16 strchr-get, 7 strchr-strchr1, 16 strchr-thm1, 5 strchr-thm2, 5 strchr-thm3, 6 strchr-thm4, 6 strchr1, 12–16 strchr1-ch0, 15 strchr1-nth, 14 strchr1-nth-first, 15 strchr1-thm1, 12 strchr1-thm2, 12 strchr1-thm3, 12 strcmp, 3, 4 strcmp-antisym, 3 strcmp-id, 3 strcmp-j, 4 strcmp-j-1, 4 strcmp-j-2, 4 strcmp-sk, 4 strcmp-strcpy, 3 strcmp-thm1, 3 strcmp-thm2, 4 strcmp-trans-1, 3 strcpy, 2, 3, 6 strcpy-0, 10 strcpy-cpy, 3 strcpy-get-1, 2 strcpy-strchr, 6 strcpy-stringp, 3 strcpy-strlen, 2 strcpy1, 4, 5 strcpy1-get-1, 4 strcpy1-get-2, 5 strcpy1-get-3, 5 strcpy2, 9 strcpy2-get-1, 9 strcpy2-get-2, 9 strcspn, 13, 16–18 strcspn*, 17, 18 strcspn-thm1, 13 strcspn-thm2, 13 strcspn-thm3, 13 stringp, 2, 3, 5, 6, 8, 10, 16, 17 strlen, 2, 3, 5–16 strlen-01, 2 strlen-0p, 2 strlen-cdr, 14 strlen-ii, 2 strlen-ii1, 2 strlen-lb, 2 strlen-mcdr, 14 strlen-non0p, 2 strlen-strchr1, 15 strlen-strchr1-nth, 15 strlen-ub, 2 strlen1, 4, 5, 9 strlen1-ii, 9 strlen1-strlen, 5 strncat, 9, 10 strncat-get-1, 9 strncat-get-2, 10 strncmp, 11, 12, 14–16 strncmp-id, 11 strncmp-j, 11, 12 strncmp-j-1, 12 strncmp-j-2, 12 strncmp-sk, 11, 12 strncmp-strncmp2, 14 strncmp-thm1, 11 strncmp-thm2, 12 strncmp1, 11, 12, 14 strncmp1-id, 11 strncmp1-strncmp2, 14 strncmp1-thm1, 11 strncmp2, 13–15 strncmp2-0, 14 strncmp2-mcdr-1, 14 strncmp2-mcdr-2, 14 strncmp2-non-numberp, 13 strncpy, 10, 11 strncpy-0s, 11 strncpy-cpy, 10 strncpy-strlen, 10 strncpy1, 10, 11 strncpy1-0s, 11 strncpy1-cpy, 10 strncpy1-get, 10 strncpy1-strlen, 10 strpbrk, 12 strpbrk-thm1, 12 strpbrk-thm2, 12 strpbrk-thm3, 12 strrchr, 7, 8 strrchr-la1, 7 strrchr-la2, 7 strrchr-la3, 7 strrchr-strchr-la, 7 strrchr-thm1, 7 strrchr-thm2, 8 strrchr-thm3, 8 strrchr-thm4, 8 strspn, 13, 16, 17 strspn*, 16, 17 strspn-strchr1, 16 strspn-thm1, 13 strspn-thm2, 13 strspn-thm3, 13 strspn-true, 16 strstr, 14–16 strstr-thm1, 14 strstr-thm2, 15 strstr-thm3, 16 strstr1, 14, 15 strstr1-thm1, 14 strstr1-thm2, 15 strstr1-thm3, 15 strtok-last, 16–18 strtok-lst, 16–18 strtok-thm1, 16 strtok-thm2, 16 strtok-thm3, 16 strtok-thm4, 17 strtok-thm5, 17 strtok-thm6, 17 strtok-tok, 16, 17

times-lessp-dual, 18

zero-list, 10 zero-list-get, 10 zero-list1, 10 zero-list1-get, 10 zero-list1-la, 10