(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^OPPOSITE-COLOR X Y)
 (^BM^OR (^BM^AND (^BM^NUMBERP X) (^BM^NOT (^BM^NUMBERP Y)))
  (^BM^AND (^BM^NUMBERP Y) (^BM^NOT (^BM^NUMBERP X)))))

(DEFINE (^BM^ALTERNATING-COLORS X)
 (IF (^BM^OR (^BM^NLISTP X) (^BM^NLISTP (^BM^CDR X)))
     (^BM^TRUE)
     (^BM^AND (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR (^BM^CDR X)))
      (^BM^ALTERNATING-COLORS (^BM^CDR X)))))

(DEFINE (^BM^PAIRED-COLORS X)
 (IF (^BM^OR (^BM^NLISTP X) (^BM^NLISTP (^BM^CDR X)))
     (^BM^TRUE)
     (^BM^AND (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR (^BM^CDR X)))
      (^BM^PAIRED-COLORS (^BM^CDR (^BM^CDR X))))))

(DEFINE (^BM^PLISTP X)
 (IF (^BM^NLISTP X) (EQUAL X (^NIL)) (^BM^PLISTP (^BM^CDR X))))

(DEFINE (^BM^SHUFFLEP X Y Z)
 (IF (^BM^NLISTP Z)
     (^BM^AND (EQUAL X (^NIL)) (^BM^AND (EQUAL Y (^NIL)) (EQUAL Z (^NIL))))
     (IF (^BM^NLISTP X)
         (^BM^AND (EQUAL X (^NIL)) (^BM^AND (EQUAL Y Z) (^BM^PLISTP Y)))
         (IF (^BM^NLISTP Y)
             (^BM^AND (EQUAL Y (^NIL)) (^BM^AND (EQUAL X Z) (^BM^PLISTP X)))
             (^BM^OR
              (^BM^AND (EQUAL (^BM^CAR X) (^BM^CAR Z))
               (^BM^SHUFFLEP (^BM^CDR X) Y (^BM^CDR Z)))
              (^BM^AND (EQUAL (^BM^CAR Y) (^BM^CAR Z))
               (^BM^SHUFFLEP X (^BM^CDR Y) (^BM^CDR Z))))))))

(DEFINE (^BM^EVEN-LENGTH L)
 (IF (^BM^NLISTP L)
     (^BM^TRUE)
     (IF (^BM^NLISTP (^BM^CDR L))
         (^BM^FALSE)
         (^BM^EVEN-LENGTH (^BM^CDR (^BM^CDR L))))))

(LEMMA (^BM^IMPLIES (^BM^ALTERNATING-COLORS X) (^BM^PAIRED-COLORS X)))

(DEFINE (^BM^SILLY X Y Z)
 (IF (^BM^NLISTP Z)
     (^BM^TRUE)
     (^BM^CONS (^BM^SILLY (^BM^CDR (^BM^CDR X)) Y (^BM^CDR (^BM^CDR Z)))
      (^BM^CONS (^BM^SILLY (^BM^CDR X) (^BM^CDR Y) (^BM^CDR (^BM^CDR Z)))
       (^BM^CONS (^BM^SILLY X (^BM^CDR (^BM^CDR Y)) (^BM^CDR (^BM^CDR Z)))
        (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^SHUFFLEP X Y Z)
   (^BM^AND (^BM^ALTERNATING-COLORS X)
    (^BM^AND (^BM^ALTERNATING-COLORS Y)
     (^BM^AND (^BM^LISTP X)
      (^BM^AND (^BM^LISTP Y) (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR Y)))))))
  (^BM^PAIRED-COLORS Z)))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PLISTP D) (^BM^PLISTP C))
  (^BM^SHUFFLEP C D (^BM^APPEND C D))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PLISTP D) (^BM^PLISTP C))
  (^BM^SHUFFLEP C D (^BM^APPEND D C))))

(LEMMA
 (EQUAL (^BM^CDR (^BM^APPEND C D))
        (IF (^BM^LISTP C) (^BM^APPEND (^BM^CDR C) D) (^BM^CDR D))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PLISTP W) (^BM^SHUFFLEP X Y Z))
  (^BM^SHUFFLEP X (^BM^APPEND Y W) (^BM^APPEND Z W))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PLISTP W) (^BM^SHUFFLEP X Y Z))
  (^BM^SHUFFLEP (^BM^APPEND X W) Y (^BM^APPEND Z W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP X) (^BM^AND (^BM^LISTP Y) (^BM^SHUFFLEP X Y Z)))
  (^BM^OR
   (^BM^SHUFFLEP (^BM^APPEND (^BM^CDR X) (^BM^CONS (^BM^CAR X) (^NIL))) Y
    (^BM^APPEND (^BM^CDR Z) (^BM^CONS (^BM^CAR Z) (^NIL))))
   (^BM^SHUFFLEP X (^BM^APPEND (^BM^CDR Y) (^BM^CONS (^BM^CAR Y) (^NIL)))
    (^BM^APPEND (^BM^CDR Z) (^BM^CONS (^BM^CAR Z) (^NIL)))))))

(LEMMA
 (EQUAL (^BM^CAR (^BM^APPEND X Y)) (IF (^BM^LISTP X) (^BM^CAR X) (^BM^CAR Y))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALTERNATING-COLORS (^BM^APPEND C (^BM^CONS D (^NIL))))
   (^BM^NOT (^BM^OPPOSITE-COLOR D E)))
  (^BM^ALTERNATING-COLORS (^BM^APPEND C (^BM^CONS E (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP L)
   (^BM^AND (^BM^EVEN-LENGTH L) (^BM^ALTERNATING-COLORS L)))
  (^BM^ALTERNATING-COLORS
   (^BM^APPEND (^BM^CDR L) (^BM^CONS (^BM^CAR L) (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALTERNATING-COLORS C)
   (^BM^AND (^BM^NUMBERP (^BM^CAR C))
    (^BM^AND (^BM^EVEN-LENGTH C) (^BM^NUMBERP V))))
  (^BM^ALTERNATING-COLORS (^BM^APPEND C (^BM^CONS V (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALTERNATING-COLORS C)
   (^BM^AND (^BM^NOT (^BM^NUMBERP (^BM^CAR C)))
    (^BM^AND (^BM^EVEN-LENGTH C) (^BM^NOT (^BM^NUMBERP V)))))
  (^BM^ALTERNATING-COLORS (^BM^APPEND C (^BM^CONS V (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^SHUFFLEP X Y Z)
   (^BM^AND (^BM^ALTERNATING-COLORS X)
    (^BM^AND (^BM^ALTERNATING-COLORS Y)
     (^BM^AND (^BM^EVEN-LENGTH X)
      (^BM^AND (^BM^EVEN-LENGTH Y)
       (^BM^NOT (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR Y))))))))
  (^BM^PAIRED-COLORS (^BM^APPEND (^BM^CDR Z) (^BM^CONS (^BM^CAR Z) (^NIL))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALTERNATING-COLORS (^BM^APPEND X Y))
   (^BM^AND (^BM^EVEN-LENGTH (^BM^APPEND X Y))
    (^BM^NOT (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR Y)))))
  (^BM^AND (^BM^EVEN-LENGTH X) (^BM^EVEN-LENGTH Y))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ALTERNATING-COLORS X))
  (^BM^NOT (^BM^ALTERNATING-COLORS (^BM^APPEND X Y)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ALTERNATING-COLORS Y))
  (^BM^NOT (^BM^ALTERNATING-COLORS (^BM^APPEND X Y)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALTERNATING-COLORS (^BM^APPEND X Y))
   (^BM^AND (^BM^EVEN-LENGTH (^BM^APPEND X Y))
    (^BM^AND (^BM^SHUFFLEP X Y Z) (^BM^AND (^BM^LISTP X) (^BM^LISTP Y)))))
  (IF (^BM^OPPOSITE-COLOR (^BM^CAR X) (^BM^CAR Y))
      (^BM^PAIRED-COLORS Z)
      (^BM^PAIRED-COLORS
       (^BM^APPEND (^BM^CDR Z) (^BM^CONS (^BM^CAR Z) (^NIL)))))))