(NOTE-LIB "rsa")

(DEFINE (^BM^INVERSE J P)
 (IF (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO))))
     (^BM^REMAINDER J (^INT (^BM^CONS (^2) (^BM^ZERO))))
     (^BM^REMAINDER
      (^BM^EXP J (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (EQUAL (^BM^REMAINDER (^BM^TIMES (^BM^INVERSE J P) J) P)
         (^BM^REMAINDER (^BM^EXP J (^BM^SUB1 P)) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES (^BM^INVERSE J P) J) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP N))
   (^BM^NOT (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO))))))
  (EQUAL (^BM^TIMES (^BM^SUB1 N) (^BM^SUB1 N))
         (^BM^PLUS (^INT (^BM^CONS (^1) (^BM^ZERO)))
          (^BM^TIMES N (^BM^SUB1 (^BM^SUB1 N)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP N))
   (^BM^NOT (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO))))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES (^BM^SUB1 N) (^BM^SUB1 N)) N)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME P) (EQUAL (^BM^INVERSE (^BM^SUB1 P) P) (^BM^SUB1 P))))

(LEMMA
 (EQUAL (^BM^DIFFERENCE (^BM^TIMES X X) (^INT (^BM^CONS (^1) (^BM^ZERO))))
        (^BM^TIMES (^BM^ADD1 X) (^BM^SUB1 X))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (EQUAL (^BM^REMAINDER
           (^BM^DIFFERENCE (^BM^TIMES J J) (^INT (^BM^CONS (^1) (^BM^ZERO))))
           P)
          (^INT (^BM^ZERO))))
  (^BM^OR (EQUAL (^BM^REMAINDER (^BM^ADD1 J) P) (^INT (^BM^ZERO)))
   (EQUAL (^BM^REMAINDER (^BM^SUB1 J) P) (^INT (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^LESSP A (^INT (^BM^CONS (^1) (^BM^ZERO)))))
   (EQUAL (^BM^REMAINDER A P) (^INT (^BM^CONS (^1) (^BM^ZERO)))))
  (EQUAL (^BM^REMAINDER (^BM^SUB1 A) P) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO))))
    (EQUAL (^BM^INVERSE J P) J)))
  (^BM^OR (EQUAL (^BM^REMAINDER (^BM^ADD1 J) P) (^INT (^BM^ZERO)))
   (EQUAL (^BM^REMAINDER (^BM^SUB1 J) P) (^INT (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP J (^BM^SUB1 P))
    (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) J)))
  (^BM^NOT (EQUAL (^BM^INVERSE J P) J))))

(LEMMA
 (EQUAL (^BM^SUB1
         (^BM^TIMES (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))
          (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))))
        (^BM^TIMES (^BM^DIFFERENCE P (^INT (^BM^CONS (^3) (^BM^ZERO))))
         (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO)))))
  (EQUAL (^BM^INVERSE (^BM^INVERSE J P) P) (^BM^REMAINDER J P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ZEROP I) (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) P))
  (EQUAL (^BM^INVERSE I P) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO)))))
  (^BM^NOT (^BM^ZEROP (^BM^INVERSE J P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO))))
    (EQUAL (^BM^INVERSE J P) (^BM^SUB1 P))))
  (EQUAL (^BM^REMAINDER J P) (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) P)
  (^BM^LEQ (^BM^INVERSE J P) (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP J (^BM^SUB1 P)))
  (^BM^LESSP (^BM^INVERSE J P) (^BM^SUB1 P))))

(DEFINE (^BM^INVERSE-LIST I P)
 (IF (^BM^ZEROP I)
     (^NIL)
     (IF (EQUAL I (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^NIL))
         (IF (^BM^MEMBER I (^BM^INVERSE-LIST (^BM^SUB1 I) P))
             (^BM^INVERSE-LIST (^BM^SUB1 I) P)
             (^BM^CONS I
              (^BM^CONS (^BM^INVERSE I P)
               (^BM^INVERSE-LIST (^BM^SUB1 I) P)))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP I (^BM^SUB1 P)))
  (^BM^ALL-NON-ZEROP (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP I (^BM^SUB1 P))
    (EQUAL J (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))
  (^BM^ALL-LESSEQP (^BM^INVERSE-LIST I P) J)))

(LEMMA (^BM^SUBSETP (^BM^POSITIVES N) (^BM^INVERSE-LIST N P)))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) P)
  (EQUAL (^BM^INVERSE (^INT (^BM^CONS (^1) (^BM^ZERO))) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER I P) (^INT (^BM^ZERO))))
    (^BM^AND (^BM^LESSP I P) (^BM^MEMBER J (^BM^INVERSE-LIST I P)))))
  (^BM^MEMBER (^BM^INVERSE J P) (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER I P) (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NOT (EQUAL (^BM^REMAINDER J P) (^INT (^BM^ZERO))))
     (^BM^AND (^BM^LESSP I P)
      (^BM^AND (^BM^LESSP J P)
       (^BM^MEMBER (^BM^INVERSE J P) (^BM^INVERSE-LIST I P)))))))
  (^BM^MEMBER J (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP I (^BM^SUB1 P))
    (^BM^ALL-DISTINCT (^BM^INVERSE-LIST (^BM^SUB1 I) P))))
  (^BM^ALL-DISTINCT (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP I (^BM^SUB1 P)))
  (^BM^ALL-DISTINCT (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES
  (EQUAL (^BM^REMAINDER (^BM^TIMES A B) P) (^INT (^BM^CONS (^1) (^BM^ZERO))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES A (^BM^TIMES B C)) P) (^BM^REMAINDER C P))))

(LEMMA
 (^BM^IMPLIES
  (EQUAL (^BM^REMAINDER (^BM^TIMES I (^BM^INVERSE I P)) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^INVERSE-LIST I P)) P)
         (^BM^REMAINDER (^BM^TIMES-LIST (^BM^INVERSE-LIST (^BM^SUB1 I) P)) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^NOT (EQUAL (^BM^REMAINDER I P) (^INT (^BM^ZERO)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^INVERSE-LIST I P)) P)
         (^BM^REMAINDER (^BM^TIMES-LIST (^BM^INVERSE-LIST (^BM^SUB1 I) P)) P))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ I (^INT (^BM^CONS (^1) (^BM^ZERO))))
  (EQUAL (^BM^TIMES-LIST (^BM^INVERSE-LIST I P))
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP I P))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^INVERSE-LIST I P)) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^MEMBER A S) (^BM^NOT (EQUAL A X)))
  (^BM^MEMBER A (^BM^DELETE X S))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^SUBSETP R S) (^BM^NOT (^BM^MEMBER X R)))
  (^BM^SUBSETP R (^BM^DELETE X S))))

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

(LEMMA (^BM^IMPLIES (^BM^LESSP N M) (^BM^NOT (^BM^MEMBER M (^BM^POSITIVES N)))))

(LEMMA
 (^BM^IMPLIES (^BM^SUBSETP (^BM^POSITIVES N) L)
  (^BM^SUBSETP (^BM^POSITIVES (^BM^SUB1 N)) (^BM^DELETE N L))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ZEROP N) (^BM^AND (^BM^ALL-LESSEQP L N) (^BM^ALL-NON-ZEROP L)))
  (^BM^NOT (^BM^LISTP L))))

(DEFINE (^BM^PIGEONHOLE2-INDUCTION L N)
 (IF (^BM^ZEROP N)
     (^BM^TRUE)
     (^BM^PIGEONHOLE2-INDUCTION (^BM^DELETE N L) (^BM^SUB1 N))))

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (EQUAL I (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))))
  (^BM^PERM (^BM^POSITIVES I) (^BM^INVERSE-LIST I P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (EQUAL I (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))))
  (EQUAL (^BM^TIMES-LIST (^BM^INVERSE-LIST I P)) (^BM^FACT I))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (EQUAL I (^BM^DIFFERENCE P (^INT (^BM^CONS (^2) (^BM^ZERO))))))
  (EQUAL (^BM^REMAINDER (^BM^FACT I) P) (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES (^BM^PRIME P)
  (EQUAL (^BM^REMAINDER (^BM^FACT (^BM^SUB1 P)) P) (^BM^SUB1 P))))