Check that two lists do not fork in front.
(lists-nofork-p list1 list2) → yes/no
The lists must be considered from right to left w.r.t. forking.
That is, the lists start at
Saying that the two lists do not diverge amounts to saying that the longer one is an extension of the shorter one, or that they are equal if they have the same length. Saying that one is an extension of another is expressed by saying that the shorter one is obtained by removing from (the front of) the longer one a number of elements equal to the difference in lengths.
We prove various properties of this predicate, so that we do not need to open it in proofs that use it.
Function:
(defun lists-nofork-p (list1 list2) (declare (xargs :guard (and (true-listp list1) (true-listp list2)))) (let ((__function__ 'lists-nofork-p)) (declare (ignorable __function__)) (cond ((< (len list1) (len list2)) (equal (nthcdr (- (len list2) (len list1)) list2) list1)) ((> (len list1) (len list2)) (equal (nthcdr (- (len list1) (len list2)) list1) list2)) (t (equal list1 list2)))))
Theorem:
(defthm booleanp-of-lists-nofork-p (b* ((yes/no (lists-nofork-p list1 list2))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm lists-nofork-p-of-same (lists-nofork-p list list))
Theorem:
(defthm lists-nofork-p-of-nil-left (implies (true-listp list) (lists-nofork-p nil list)))
Theorem:
(defthm lists-nofork-p-of-nil-right (implies (true-listp list) (lists-nofork-p list nil)))
Theorem:
(defthm lists-nofork-p-of-append-left (lists-nofork-p (append list1 list2) list2))
Theorem:
(defthm lists-nofork-p-of-append-right (lists-nofork-p list2 (append list1 list2)))
Theorem:
(defthm lists-nofork-p-commutative (equal (lists-nofork-p list1 list2) (lists-nofork-p list2 list1)))