(NOTE-LIB "proveall")

(DEFINE (^BM^CRYPT M E N)
 (IF (^BM^ZEROP E)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (IF (^BM^EVEN E)
         (^BM^REMAINDER
          (^BM^SQUARE
           (^BM^CRYPT M (^BM^QUOTIENT E (^INT (^BM^CONS (^2) (^BM^ZERO)))) N))
          N)
         (^BM^REMAINDER
          (^BM^TIMES M
           (^BM^REMAINDER
            (^BM^SQUARE
             (^BM^CRYPT M (^BM^QUOTIENT E (^INT (^BM^CONS (^2) (^BM^ZERO))))
              N))
            N))
          N))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^TIMES X (^BM^REMAINDER Y N)) N)
        (^BM^REMAINDER (^BM^TIMES X Y) N)))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^TIMES A (^BM^TIMES B (^BM^REMAINDER Y N))) N)
        (^BM^REMAINDER (^BM^TIMES A (^BM^TIMES B Y)) N)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO)))))
  (EQUAL (^BM^CRYPT M E N) (^BM^REMAINDER (^BM^EXP M E) N))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^TIMES (^BM^REMAINDER A N) B) N)
        (^BM^REMAINDER (^BM^TIMES A B) N)))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER Y A) (^BM^REMAINDER Z A))
  (EQUAL (EQUAL (^BM^REMAINDER (^BM^TIMES X Y) A)
                (^BM^REMAINDER (^BM^TIMES X Z) A))
         (^BM^TRUE))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^EXP (^BM^REMAINDER A N) I) N)
        (^BM^REMAINDER (^BM^EXP A I) N)))

(LEMMA
 (^BM^IMPLIES
  (EQUAL (^BM^REMAINDER (^BM^EXP M J) P) (^INT (^BM^CONS (^1) (^BM^ZERO))))
  (EQUAL (^BM^REMAINDER (^BM^EXP M (^BM^TIMES I J)) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(DEFINE (^BM^PDIFFERENCE A B)
 (IF (^BM^LESSP A B) (^BM^DIFFERENCE B A) (^BM^DIFFERENCE A B)))

(LEMMA
 (EQUAL (^BM^TIMES M (^BM^PDIFFERENCE A B))
        (^BM^PDIFFERENCE (^BM^TIMES M A) (^BM^TIMES M B))))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER (^BM^PDIFFERENCE A B) P) (^INT (^BM^ZERO)))
  (EQUAL (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P)) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P))
  (EQUAL (^BM^REMAINDER (^BM^PDIFFERENCE A B) P) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND
   (EQUAL (^BM^REMAINDER (^BM^TIMES M A) P) (^BM^REMAINDER (^BM^TIMES M B) P))
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO))))
    (^BM^PRIME P)))
  (EQUAL (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P)) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO)))
  (EQUAL (^BM^REMAINDER (^BM^TIMES Y X) (^BM^TIMES Y Z)) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (EQUAL (^BM^REMAINDER X P) (^INT (^BM^ZERO)))
   (^BM^AND (EQUAL (^BM^REMAINDER X Q) (^INT (^BM^ZERO)))
    (^BM^AND (^BM^PRIME P) (^BM^AND (^BM^PRIME Q) (^BM^NOT (EQUAL P Q))))))
  (EQUAL (^BM^REMAINDER X (^BM^TIMES P Q)) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P))
      (EQUAL (^BM^REMAINDER A Q) (^BM^REMAINDER B Q))))))
  (EQUAL (^BM^REMAINDER A (^BM^TIMES P Q)) (^BM^REMAINDER B (^BM^TIMES P Q)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P))
      (^BM^AND (EQUAL (^BM^REMAINDER A Q) (^BM^REMAINDER B Q))
       (^BM^AND (^BM^NUMBERP B) (^BM^LESSP B (^BM^TIMES P Q))))))))
  (EQUAL (EQUAL (^BM^REMAINDER A (^BM^TIMES P Q)) B) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO)))))
  (EQUAL (EQUAL (^BM^REMAINDER (^BM^TIMES M X) P)
                (^BM^REMAINDER (^BM^TIMES M Y) P))
         (EQUAL (^BM^REMAINDER X P) (^BM^REMAINDER Y P)))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME P)
  (EQUAL (EQUAL (^BM^REMAINDER (^BM^TIMES M X) P) (^BM^REMAINDER M P))
         (^BM^OR (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO)))
          (EQUAL (^BM^REMAINDER X P) (^INT (^BM^CONS (^1) (^BM^ZERO))))))))

(DEFINE (^BM^ALL-DISTINCT L)
 (IF (^BM^NLISTP L)
     (^BM^TRUE)
     (^BM^AND (^BM^NOT (^BM^MEMBER (^BM^CAR L) (^BM^CDR L)))
      (^BM^ALL-DISTINCT (^BM^CDR L)))))

(DEFINE (^BM^ALL-LESSEQP L N)
 (IF (^BM^NLISTP L)
     (^BM^TRUE)
     (^BM^AND (^BM^NOT (^BM^LESSP N (^BM^CAR L)))
      (^BM^ALL-LESSEQP (^BM^CDR L) N))))

(DEFINE (^BM^ALL-NON-ZEROP L)
 (IF (^BM^NLISTP L)
     (^BM^TRUE)
     (^BM^AND (^BM^NOT (^BM^ZEROP (^BM^CAR L)))
      (^BM^ALL-NON-ZEROP (^BM^CDR L)))))

(DEFINE (^BM^POSITIVES N)
 (IF (^BM^ZEROP N) (^NIL) (^BM^CONS N (^BM^POSITIVES (^BM^SUB1 N)))))

(LEMMA (EQUAL (^BM^LISTP (^BM^POSITIVES N)) (^BM^NOT (^BM^ZEROP N))))

(LEMMA
 (EQUAL (^BM^CAR (^BM^POSITIVES N)) (IF (^BM^ZEROP N) (^INT (^BM^ZERO)) N)))

(LEMMA
 (EQUAL (^BM^MEMBER X (^BM^POSITIVES N))
        (IF (^BM^ZEROP X) (^BM^FALSE) (^BM^LESSP X (^BM^ADD1 N)))))

(LEMMA (^BM^IMPLIES (^BM^ALL-NON-ZEROP L) (^BM^ALL-NON-ZEROP (^BM^DELETE X L))))

(LEMMA (^BM^IMPLIES (^BM^ALL-DISTINCT L) (^BM^ALL-DISTINCT (^BM^DELETE X L))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^ALL-DISTINCT L) (^BM^ALL-LESSEQP L (^BM^ADD1 N)))
  (^BM^ALL-LESSEQP (^BM^DELETE (^BM^ADD1 N) L) N)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^MEMBER (^BM^ADD1 N) X))
   (^BM^ALL-LESSEQP X (^BM^ADD1 N)))
  (^BM^ALL-LESSEQP X N)))

(LEMMA (^BM^IMPLIES (^BM^AND (^BM^PERM A B) (^BM^MEMBER X A)) (^BM^MEMBER X B)))

(DEFINE (^BM^PIGEON-HOLE-INDUCTION L)
 (IF (^BM^LISTP L)
     (IF (^BM^MEMBER (^BM^LENGTH L) L)
         (^BM^PIGEON-HOLE-INDUCTION (^BM^DELETE (^BM^LENGTH L) L))
         (^BM^PIGEON-HOLE-INDUCTION (^BM^CDR L)))
     (^BM^TRUE)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALL-NON-ZEROP L)
   (^BM^AND (^BM^ALL-DISTINCT L) (^BM^ALL-LESSEQP L (^BM^LENGTH L))))
  (^BM^PERM (^BM^POSITIVES (^BM^LENGTH L)) L)))

(LEMMA
 (^BM^IMPLIES (^BM^PERM L1 L2) (EQUAL (^BM^TIMES-LIST L1) (^BM^TIMES-LIST L2))))

(LEMMA (EQUAL (^BM^TIMES-LIST (^BM^POSITIVES N)) (^BM^FACT N)))

(LEMMA
 (^BM^IMPLIES (^BM^PERM (^BM^POSITIVES N) L)
  (EQUAL (^BM^TIMES-LIST L) (^BM^FACT N))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP N P))
  (^BM^NOT (EQUAL (^BM^REMAINDER (^BM^FACT N) P) (^INT (^BM^ZERO))))))

(DEFINE (^BM^S N M P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^REMAINDER (^BM^TIMES M N) P) (^BM^S (^BM^SUB1 N) M P))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^S N M P)) P)
        (^BM^REMAINDER (^BM^TIMES (^BM^FACT N) (^BM^EXP M N)) P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP N1) (^BM^AND (^BM^LESSP N2 N1) (^BM^LESSP N1 P)))))
  (^BM^NOT (^BM^MEMBER (^BM^REMAINDER (^BM^TIMES M N1) P) (^BM^S N2 M P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO))))
    (^BM^LESSP N P)))
  (^BM^ALL-DISTINCT (^BM^S N M P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO))))
    (^BM^LESSP N P)))
  (^BM^ALL-NON-ZEROP (^BM^S N M P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (^BM^ALL-LESSEQP (^BM^S N M P) (^BM^SUB1 P))))

(LEMMA (EQUAL (^BM^LENGTH (^BM^S N M P)) (^BM^FIX N)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER M P) (^INT (^BM^ZERO)))))
  (EQUAL (^BM^REMAINDER (^BM^EXP M (^BM^SUB1 P)) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME P)
  (EQUAL (^BM^REMAINDER (^BM^TIMES M (^BM^EXP M (^BM^TIMES K (^BM^SUB1 P)))) P)
         (^BM^REMAINDER M P))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME P)
  (EQUAL (^BM^REMAINDER
          (^BM^TIMES M
           (^BM^EXP M (^BM^TIMES K (^BM^TIMES (^BM^SUB1 P) (^BM^SUB1 Q)))))
          P)
         (^BM^REMAINDER M P))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME Q)
  (EQUAL (^BM^REMAINDER
          (^BM^TIMES M
           (^BM^EXP M (^BM^TIMES K (^BM^TIMES (^BM^SUB1 P) (^BM^SUB1 Q)))))
          Q)
         (^BM^REMAINDER M Q))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (^BM^NUMBERP M)
      (^BM^AND (^BM^LESSP M (^BM^TIMES P Q))
       (EQUAL (^BM^REMAINDER ED (^BM^TIMES (^BM^SUB1 P) (^BM^SUB1 Q)))
              (^INT (^BM^CONS (^1) (^BM^ZERO)))))))))
  (EQUAL (^BM^REMAINDER (^BM^EXP M ED) (^BM^TIMES P Q)) M)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (EQUAL N (^BM^TIMES P Q))
      (^BM^AND (^BM^NUMBERP M)
       (^BM^AND (^BM^LESSP M N)
        (EQUAL (^BM^REMAINDER (^BM^TIMES E D)
                (^BM^TIMES (^BM^SUB1 P) (^BM^SUB1 Q)))
               (^INT (^BM^CONS (^1) (^BM^ZERO))))))))))
  (EQUAL (^BM^CRYPT (^BM^CRYPT M E N) D N) M)))