(NOTE-LIB "extras" T) Loading ./numbers/extras.lib Finished loading ./numbers/extras.lib Loading ./numbers/extras.o Finished loading ./numbers/extras.o (#./numbers/extras.lib #./numbers/extras) (PROVE-LEMMA IREM-IGCD-ARG1 (REWRITE) (EQUAL (EQUAL (IREM (IGCD A B) C) 0) (AND (EQUAL (IREM A C) 0) (EQUAL (IREM B C) 0))) ((ENABLE IREM-IS-MY-IREM IABS IGCD MY-IREM FIX-INT INTEGERP INEG))) This formula can be simplified, using the abbreviations IREM-IS-MY-IREM and IGCD, to: (EQUAL (EQUAL (MY-IREM (GCD (IABS A) (IABS B)) C) 0) (AND (EQUAL (MY-IREM A C) 0) (EQUAL (MY-IREM B C) 0))), which simplifies, applying EQUAL-GCD-0 and FIX-INT-REMOVER, and opening up the definitions of IABS, INTEGERP, MY-IREM, FIX-INT, and AND, to the following 192 new formulas: Case 192. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, using linear arithmetic, rewriting with the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the definitions of NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 191. (IMPLIES (AND (NOT (NEGATIVEP A)) (EQUAL A 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)), which again simplifies, clearly, to: T. Case 190. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, clearly, to: T. Case 189. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, applying the lemma REMAINDER-GCD-ARG1, and expanding the functions EQUAL and INEG, to: T. Case 188. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)), which again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL, NUMBERP, and INEG, to: T. Case 187. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, clearly, to: T. Case 186. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, clearly, to: T. Case 185. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). However this again simplifies, rewriting with REMAINDER-GCD-ARG1, and unfolding INEG and EQUAL, to: T. Case 184. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NOT (NUMBERP A)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL, NUMBERP, and INEG, to: T. Case 183. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, obviously, to: T. Case 182. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NEGATIVEP C) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, trivially, to: T. Case 181. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NOT (NUMBERP A)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, trivially, to: T. Case 180. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, trivially, to: T. Case 179. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0) T)). This again simplifies, clearly, to: T. Case 178. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 177. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). This again simplifies, obviously, to: T. Case 176. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and opening up the functions EQUAL and INEG, to: T. Case 175. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL, NUMBERP, and INEG, to: T. Case 174. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). This again simplifies, trivially, to: T. Case 173. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and expanding the definition of INEG, to: T. Case 172. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). This again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to: T. Case 171. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). This again simplifies, obviously, to: T. Case 170. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) (NEGATIVE-GUTS C))) 0))). This again simplifies, obviously, to: T. Case 169. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)). This again simplifies, trivially, to: T. Case 168. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0) (NOT (NUMBERP A))) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)). This again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to: T. Case 167. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)), which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, to: T. Case 166. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD 0 B) (NEGATIVE-GUTS C)) 0)) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)). This again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up the functions EQUAL and NUMBERP, to: T. Case 165. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)), which again simplifies, rewriting with REMAINDER-GCD-ARG1, and opening up the definition of EQUAL, to: T. Case 164. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0)) (EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0) T)). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 163. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))). This again simplifies, clearly, to: T. Case 162. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))). However this again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL and NUMBERP, to: T. Case 161. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))). But this again simplifies, rewriting with COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, and expanding the functions EQUAL and INEG, to: T. Case 160. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD 0 B) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))). But this again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up the definitions of EQUAL and NUMBERP, to: T. Case 159. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))), which again simplifies, rewriting with COMMON-DIVISOR-DIVIDES-GCD, and expanding EQUAL, to: T. Case 158. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C)) 0))). But this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 157. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)), which again simplifies, using linear arithmetic, applying REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding NEGATIVEP, NUMBERP, EQUAL, and ZEROP, to: T. Case 156. (IMPLIES (AND (NOT (NEGATIVEP A)) (EQUAL A 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, obviously, to: T. Case 155. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, obviously, to: T. Case 154. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0) (EQUAL (REMAINDER A 0) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). But this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0, and expanding the function ZEROP, to: T. Case 153. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) 0) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding EQUAL, NUMBERP, and ZEROP, to: T. Case 152. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, clearly, to: T. Case 151. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, trivially, to: T. Case 150. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). But this again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and expanding ZEROP, to: T. Case 149. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (NOT (NUMBERP A)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, using linear arithmetic, applying REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the definitions of EQUAL, NUMBERP, and ZEROP, to: T. Case 148. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, clearly, to: T. Case 147. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, clearly, to: T. Case 146. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NOT (NUMBERP A)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, trivially, to: T. Case 145. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, clearly, to: T. Case 144. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0) T)). This again simplifies, clearly, to: T. Case 143. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and expanding the definitions of NEGATIVEP, NUMBERP, EQUAL, ZEROP, and INEG, to: T. Case 142. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (REMAINDER A 0) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). This again simplifies, clearly, to: T. Case 141. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (REMAINDER A 0) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). But this again simplifies, appealing to the lemmas REMAINDER-ZERO, EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and expanding ZEROP and INEG, to: T. Case 140. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) 0) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))), which again simplifies, using linear arithmetic, applying REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and opening up the definitions of EQUAL, NUMBERP, ZEROP, and INEG, to: T. Case 139. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL A 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). This again simplifies, trivially, to: T. Case 138. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). However this again simplifies, rewriting with the lemmas REMAINDER-ZERO, EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and unfolding the functions ZEROP and INEG, to: T. Case 137. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))), which again simplifies, using linear arithmetic, rewriting with the lemmas REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and expanding the functions EQUAL, NUMBERP, ZEROP, and INEG, to: T. Case 136. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL A 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))), which again simplifies, trivially, to: T. Case 135. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0)) 0))). This again simplifies, trivially, to: T. Case 134. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). This again simplifies, clearly, to: T. Case 133. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0) (NOT (NUMBERP A))) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). But this again simplifies, using linear arithmetic, applying REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and unfolding the functions EQUAL, NUMBERP, and ZEROP, to: T. Case 132. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). This again simplifies, rewriting with COMMUTATIVITY-OF-GCD, REMAINDER-ZERO, and EQUAL-GCD-0, and opening up the definition of ZEROP, to: T. Case 131. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD 0 B) 0) 0)) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up the definitions of EQUAL, NUMBERP, and ZEROP, to: T. Case 130. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) 0) 0) (EQUAL (REMAINDER A 0) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). But this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0, and opening up the function ZEROP, to: T. Case 129. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD A B) 0) 0)) (EQUAL (EQUAL (REMAINDER B 0) 0) T)). This again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up the functions NEGATIVEP, NUMBERP, EQUAL, and ZEROP, to: T. Case 128. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0)) (EQUAL A 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B 0) 0))), which again simplifies, trivially, to: T. Case 127. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (REMAINDER B 0) 0))). However this again simplifies, rewriting with the lemma GCD-REMAINDER, and unfolding the functions NUMBERP, REMAINDER, and EQUAL, to: T. Case 126. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (NOT (EQUAL (REMAINDER B 0) 0))), which again simplifies, appealing to the lemmas COMMUTATIVITY-OF-GCD, REMAINDER-ZERO, EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and opening up the definitions of ZEROP and INEG, to: T. Case 125. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD 0 B) 0) 0))) (NOT (EQUAL (REMAINDER B 0) 0))), which again simplifies, applying the lemma GCD-REMAINDER, and unfolding NUMBERP, REMAINDER, and EQUAL, to: T. Case 124. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) 0) 0)) (EQUAL (REMAINDER A 0) 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B 0) 0))), which again simplifies, rewriting with COMMON-DIVISOR-DIVIDES-GCD, and opening up the function EQUAL, to: T. Case 123. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD A B) 0) 0))) (NOT (EQUAL (REMAINDER B 0) 0))). But this again simplifies, rewriting with GCD-REMAINDER, and opening up NEGATIVEP, NUMBERP, REMAINDER, and EQUAL, to: T. Case 122. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). But this again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up the functions NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 121. (IMPLIES (AND (NOT (NEGATIVEP A)) (EQUAL A 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)), which again simplifies, trivially, to: T. Case 120. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, clearly, to: T. Case 119. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0) (EQUAL (REMAINDER A C) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). But this again simplifies, applying REMAINDER-GCD-ARG1, and expanding the definitions of EQUAL and INEG, to: T. Case 118. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) C) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). But this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to: T. Case 117. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, clearly, to: T. Case 116. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, trivially, to: T. Case 115. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). But this again simplifies, applying the lemma REMAINDER-GCD-ARG1, and expanding INEG and EQUAL, to: T. Case 114. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (NOT (NUMBERP A)) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)), which again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to: T. Case 113. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, obviously, to: T. Case 112. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, clearly, to: T. Case 111. (IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NOT (NUMBERP A)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, clearly, to: T. Case 110. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (EQUAL A 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, clearly, to: T. Case 109. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0) (NUMBERP B) (NOT (EQUAL B 0))) (EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0) T)). This again simplifies, obviously, to: T. Case 108. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))). This again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 107. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0)) (EQUAL (REMAINDER A C) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))), which again simplifies, clearly, to: T. Case 106. (IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0)) (EQUAL (REMAINDER A C) 0) (NOT (NUMBERP B)) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (EQUAL B 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))). But this again simplifies, applying REMAINDER-GCD-ARG1, and opening up the functions EQUAL and INEG, to: T. Case 105. (IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) C) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))). However this again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL, NUMBERP, and INEG, to: T. Case 104. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL A 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))), which again simplifies, trivially, to: T. Case 103. (IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))). But this again simplifies, appealing to the lemma REMAINDER-GCD-ARG1, and unfolding INEG, to: T. Case 102. (IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))), which again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to: T. Case 101. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL A 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))), which again simplifies, obviously, to: T. Case 100. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0) (NUMBERP B)) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C)) 0))). This again simplifies, trivially, to: T. Case 99.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0) (EQUAL A 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B C) 0) T)). This again simplifies, obviously, to: T. Case 98.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0) (NOT (NUMBERP A))) (EQUAL (EQUAL (REMAINDER B C) 0) T)). However this again simplifies, using linear arithmetic, rewriting with the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL and NUMBERP, to: T. Case 97.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (EQUAL (EQUAL (REMAINDER B C) 0) T)), which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, to: T. Case 96.(IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD 0 B) C) 0)) (EQUAL (EQUAL (REMAINDER B C) 0) T)). But this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL and NUMBERP, to: T. Case 95.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) C) 0) (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0))) (EQUAL (EQUAL (REMAINDER B C) 0) T)). But this again simplifies, applying REMAINDER-GCD-ARG1, and opening up EQUAL, to: T. Case 94.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD A B) C) 0)) (EQUAL (EQUAL (REMAINDER B C) 0) T)). This again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 93.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0)) (EQUAL A 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B C) 0))). This again simplifies, clearly, to: T. Case 92.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0)) (NOT (NUMBERP A))) (NOT (EQUAL (REMAINDER B C) 0))). But this again simplifies, using linear arithmetic, rewriting with the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL and NUMBERP, to: T. Case 91.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (NOT (EQUAL (REMAINDER B C) 0))), which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, and unfolding the functions EQUAL and INEG, to: T. Case 90.(IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD 0 B) C) 0))) (NOT (EQUAL (REMAINDER B C) 0))). However this again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL and NUMBERP, to: T. Case 89.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) C) 0)) (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0))) (NOT (EQUAL (REMAINDER B C) 0))), which again simplifies, appealing to the lemma COMMON-DIVISOR-DIVIDES-GCD, and unfolding the definition of EQUAL, to: T. Case 88.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD A B) C) 0))) (NOT (EQUAL (REMAINDER B C) 0))), which again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 87.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL B 0))), which again simplifies, obviously, to: T. Case 86.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0))) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 85.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (EQUAL A 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0))) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 84.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0)). This again simplifies, applying REMAINDER-GCD-ARG1, to: T. Case 83.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 82.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). But this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the definitions of EQUAL and NUMBERP, to: T. Case 81.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD A 0) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0)), which again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to: T. Case 80.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD A 0) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0))). However this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to: T. Case 79.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0)), which again simplifies, rewriting with REMAINDER-GCD-ARG1, to: T. Case 78.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) (NEGATIVE-GUTS C)) 0)) (EQUAL (REMAINDER A (NEGATIVE-GUTS C)) 0)) (NOT (EQUAL B 0))). But this again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and opening up the definitions of NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 77.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (REMAINDER A 0) 0)). This again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and unfolding ZEROP, to: T. Case 76.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (REMAINDER A 0) 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 75.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (REMAINDER A 0) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, using linear arithmetic, applying REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the functions EQUAL, NUMBERP, and ZEROP, to: T. Case 74.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD A 0) 0) 0)) (EQUAL (REMAINDER A 0) 0)). This again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up EQUAL, NUMBERP, and ZEROP, to: T. Case 73.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD A 0) 0) 0))) (NOT (EQUAL (REMAINDER A 0) 0))). This again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the functions EQUAL, NUMBERP, and ZEROP, to: T. Case 72.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) 0) 0)) (EQUAL (REMAINDER A 0) 0)). This again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and expanding ZEROP, to: T. Case 71.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) 0) 0)) (EQUAL (REMAINDER A 0) 0)) (NOT (EQUAL B 0))). This again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the functions NEGATIVEP, NUMBERP, EQUAL, and ZEROP, to: T. Case 70.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0)) (EQUAL (REMAINDER A C) 0)), which again simplifies, rewriting with REMAINDER-GCD-ARG1, to: T. Case 69.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0)) (EQUAL (REMAINDER A C) 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 68.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B)) C) 0)) (EQUAL (REMAINDER A C) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL and NUMBERP, to: T. Case 67.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD A 0) C) 0)) (EQUAL (REMAINDER A C) 0)). But this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL and NUMBERP, to: T. Case 66.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD A 0) C) 0))) (NOT (EQUAL (REMAINDER A C) 0))). However this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL and NUMBERP, to: T. Case 65.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD A B) C) 0)) (EQUAL (REMAINDER A C) 0)), which again simplifies, applying REMAINDER-GCD-ARG1, to: T. Case 64.(IMPLIES (AND (NOT (NEGATIVEP A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD A B) C) 0)) (EQUAL (REMAINDER A C) 0)) (NOT (EQUAL B 0))). However this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions NEGATIVEP, NUMBERP, and EQUAL, to: T. Case 63.(IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 62.(IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) 0) 0))) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 61.(IMPLIES (AND (NOT (NEGATIVEP A)) (NOT (NUMBERP A)) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B)) C) 0))) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 60.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, obviously, to: T. Case 59.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, trivially, to: T. Case 58.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, clearly, to: T. Case 57.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (EQUAL B 0) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, obviously, to: T. Case 56.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (EQUAL B 0) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, clearly, to: T. Case 55.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (EQUAL B 0) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, clearly, to: T. Case 54.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, clearly, to: T. Case 53.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, trivially, to: T. Case 52.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, clearly, to: T. Case 51.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, trivially, to: T. Case 50.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 49.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 48.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NEGATIVEP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (NOT (NUMBERP A))) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 47.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, obviously, to: T. Case 46.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 45.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 44.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (NOT (NUMBERP A))) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 43.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, trivially, to: T. Case 42.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 41.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 40.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (NOT (EQUAL (NEGATIVE-GUTS B) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (NOT (NUMBERP A))) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 39.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP A) (NOT (EQUAL A 0)) (NEGATIVEP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, clearly, to: T. Case 38.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, clearly, to: T. Case 37.(IMPLIES (AND (NEGATIVEP A) (EQUAL (NEGATIVE-GUTS A) 0) (NEGATIVEP B) (EQUAL (NEGATIVE-GUTS B) 0) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (NEGATIVEP C)) (NUMBERP C)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, clearly, to: T. Case 36.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). However this again simplifies, rewriting with the lemma REMAINDER-GCD-ARG1, and opening up the functions INEG and EQUAL, to: T. Case 35.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))), which again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and opening up the definitions of EQUAL, NUMBERP, and INEG, to: T. Case 34.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 33.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, trivially, to: T. Case 32.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 31.(IMPLIES (AND (NEGATIVEP A) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) (NEGATIVE-GUTS C)) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). This again simplifies, trivially, to: T. Case 30.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) (NEGATIVE-GUTS C)) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). However this again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP, and INEG, to: T. Case 29.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0))), which again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP, and INEG, to: T. Case 28.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) (NEGATIVE-GUTS C)) 0))) (NOT (EQUAL A 0))), which again simplifies, obviously, to: T. Case 27.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)). But this again simplifies, applying COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, and opening up the functions INEG and EQUAL, to: T. Case 26.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) (NEGATIVE-GUTS C))) 0)) (NOT (EQUAL B 0))). This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 25.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NEGATIVEP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) (NEGATIVE-GUTS C)) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 24.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). However this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0, and opening up ZEROP, to: T. Case 23.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, using linear arithmetic, applying the lemmas REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and unfolding EQUAL, NUMBERP, ZEROP, and INEG, to: T. Case 22.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (NOT (EQUAL B 0))), which again simplifies, obviously, to: T. Case 21.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL A 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, obviously, to: T. Case 20.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) 0) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Case 19.(IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) 0) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, clearly, to: T. Case 18.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) 0) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). This again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the functions EQUAL, NUMBERP, and ZEROP, to: T. Case 17.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) 0) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0))), which again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and opening up the definitions of EQUAL, NUMBERP, ZEROP, and INEG, to: T. Case 16.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) 0) 0))) (NOT (EQUAL A 0))). This again simplifies, obviously, to: T. Case 15.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)). However this again simplifies, rewriting with COMMUTATIVITY-OF-GCD, REMAINDER-ZERO, and EQUAL-GCD-0, and expanding ZEROP, to: T. Case 14.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0)) 0)) (NOT (EQUAL B 0))). However this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and opening up the functions NEGATIVEP, NUMBERP, EQUAL, ZEROP, and INEG, to: T. Case 13.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NOT (NUMBERP C)) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) 0) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))), which again simplifies, trivially, to: T. Case 12.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and unfolding the definitions of INEG and EQUAL, to: T. Case 11.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). But this again simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP, and INEG, to: T. Case 10.(IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (NOT (EQUAL B 0))). This again simplifies, clearly, to: T. Case 9. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL A 0) (NOT (NUMBERP B))) (NOT (EQUAL (NEGATIVE-GUTS B) 0))). This again simplifies, obviously, to: T. Case 8. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NEGATIVEP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) (NEGATIVE-GUTS B)) C) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, trivially, to: T. Case 7. (IMPLIES (AND (NEGATIVEP A) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) C) 0) (NUMBERP A) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, clearly, to: T. Case 6. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) C) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to: T. Case 5. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) C) 0))) (NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0))). But this again simplifies, using linear arithmetic, appealing to the lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL, NUMBERP, and INEG, to: T. Case 4. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0) C) 0))) (NOT (EQUAL A 0))), which again simplifies, trivially, to: T. Case 3. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0) (NOT (EQUAL A 0))) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)). This again simplifies, applying COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1, and opening up the functions INEG and EQUAL, to: T. Case 2. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0)) (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C)) 0)) (NOT (EQUAL B 0))). However this again simplifies, using linear arithmetic, applying REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions NEGATIVEP, NUMBERP, EQUAL, and INEG, to: T. Case 1. (IMPLIES (AND (NEGATIVEP A) (NOT (EQUAL (NEGATIVE-GUTS A) 0)) (NOT (NEGATIVEP C)) (NUMBERP C) (NOT (NEGATIVEP B)) (NUMBERP B) (NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B) C) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, obviously, to: T. Q.E.D. [ 0.0 4.0 0.1 ] IREM-IGCD-ARG1 (PROVE-LEMMA IREM-X-X (REWRITE) (EQUAL (IREM X X) 0) ((ENABLE-THEORY INTEGER-DEFNS))) This conjecture simplifies, rewriting with IQUO-X-X, and expanding the functions IZEROP, FIX-INT, INTEGERP, and IREM, to the following six new conjectures: Case 6. (IMPLIES (AND (NUMBERP X) (NOT (EQUAL X 0))) (EQUAL (IDIFFERENCE X (ITIMES X 1)) 0)). This again simplifies, applying FIX-INT-REMOVER, ITIMES-1-ARG1, COMMUTATIVITY-OF-ITIMES, and IDIFFERENCE-X-X, and unfolding the functions INTEGERP and EQUAL, to: T. Case 5. (IMPLIES (AND (NEGATIVEP X) (NOT (EQUAL (NEGATIVE-GUTS X) 0)) (NOT (EQUAL X 0))) (EQUAL (IDIFFERENCE X (ITIMES X 1)) 0)). However this again simplifies, applying the lemmas FIX-INT-REMOVER, ITIMES-1-ARG1, COMMUTATIVITY-OF-ITIMES, and IDIFFERENCE-X-X, and unfolding INTEGERP and EQUAL, to: T. Case 4. (IMPLIES (AND (NUMBERP X) (EQUAL X 0)) (EQUAL (IDIFFERENCE X (ITIMES X 0)) 0)), which again simplifies, unfolding NUMBERP, ITIMES, IDIFFERENCE, and EQUAL, to: T. Case 3. (IMPLIES (AND (NEGATIVEP X) (NOT (EQUAL (NEGATIVE-GUTS X) 0)) (EQUAL X 0)) (EQUAL (IDIFFERENCE X (ITIMES X 0)) 0)), which again simplifies, obviously, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (NEGATIVEP X))) (EQUAL (IDIFFERENCE 0 (ITIMES X 0)) 0)). However this again simplifies, applying the lemmas ITIMES-0-LEFT and COMMUTATIVITY-OF-ITIMES, and expanding IDIFFERENCE and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (NEGATIVE-GUTS X) 0)) (EQUAL (IDIFFERENCE 0 (ITIMES X 0)) 0)), which again simplifies, rewriting with ITIMES-0-LEFT and COMMUTATIVITY-OF-ITIMES, and expanding the definitions of IDIFFERENCE and EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] IREM-X-X (PROVE-LEMMA GCD-TIMES-EASY-PROOF-HELPER-HELPER NIL (IMPLIES (AND (NUMBERP A) (NUMBERP B) (NUMBERP C)) (EQUAL (REMAINDER (TIMES C (GCD A B)) (GCD A (TIMES B C))) 0)) ((USE (GCD-FACTORS-GIVES-LINEAR-COMBINATION (X A) (Y B))) (INDUCT (APPEND X Y)) (ENABLE-THEORY NATS-TO-INTS) (DISABLE IREM-0-BACKCHAIN NOT-INTEGERP IREM-NOOP))) This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-ITIMES, GCD-IS-IGCD, NUMBERP-ILESSP, ILESSP-STRICT, ITIMES-0-LEFT, TIMES-TO-ITIMES, IABS-SIMPLIFY, IGCD-0-BETTER, ILESSP-FIX-INT-2, ITIMES-FIX-INT2, IREM-OF-0, REMAINDER-TO-IREM, CORRECTNESS-OF-CANCEL-FACTORS-ILESSP-0, IREM-FIX-INT2, IREM-X-X, EQUAL-IREM-ITIMES-0, FIX-INT-ITIMES, IGCD-NON-NEGATIVE, and ILESSP-0-IGCD, and opening up the functions AND, IMPLIES, GCD, TIMES, REMAINDER, EQUAL, ILESSP, FIX-INT, OR, and IZEROP, to: (IMPLIES (AND (NOT (ILESSP A 0)) (NOT (ILESSP B 0)) (EQUAL (IPLUS (ITIMES A (CAR (GCD-FACTORS A B))) (ITIMES B (CDR (GCD-FACTORS A B)))) (IGCD A B)) (NOT (LISTP X)) (ILESSP 0 A) (ILESSP 0 B) (ILESSP 0 C)) (EQUAL (IREM (ITIMES C (IGCD A B)) (IGCD A (ITIMES B C))) 0)), which again simplifies, applying ILESSP-STRICT, to: (IMPLIES (AND (EQUAL (IPLUS (ITIMES A (CAR (GCD-FACTORS A B))) (ITIMES B (CDR (GCD-FACTORS A B)))) (IGCD A B)) (NOT (LISTP X)) (ILESSP 0 A) (ILESSP 0 B) (ILESSP 0 C)) (EQUAL (IREM (ITIMES C (IGCD A B)) (IGCD A (ITIMES B C))) 0)). We use the above equality hypothesis by substituting: (IPLUS (ITIMES A (CAR (GCD-FACTORS A B))) (ITIMES B (CDR (GCD-FACTORS A B)))) for (IGCD A B) and throwing away the equality. We must thus prove: (IMPLIES (AND (NOT (LISTP X)) (ILESSP 0 A) (ILESSP 0 B) (ILESSP 0 C)) (EQUAL (IREM (ITIMES C (IPLUS (ITIMES A (CAR (GCD-FACTORS A B))) (ITIMES B (CDR (GCD-FACTORS A B))))) (IGCD A (ITIMES B C))) 0)). But this further simplifies, applying COMMUTATIVITY2-OF-ITIMES, ITIMES-DISTRIBUTES-OVER-IPLUS, IREM-ITIMES-IGCD, IREM-ITIMES-BASE, IREM-ITIMES-CANCEL, COMMUTATIVITY-OF-ITIMES, ITIMES-0-LEFT, and IREM-IPLUS-0, and opening up the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.9 0.0 ] GCD-TIMES-EASY-PROOF-HELPER-HELPER (PROVE-LEMMA GCD-TIMES-EASY-PROOF-HELPER NIL (EQUAL (REMAINDER (TIMES C (GCD A B)) (GCD A (TIMES B C))) 0) ((USE (GCD-TIMES-EASY-PROOF-HELPER-HELPER)) (DISABLE REMAINDER-TIMES1))) This conjecture simplifies, rewriting with REMAINDER-OF-NON-NUMBER, GCD-REMAINDER, REMAINDER-TIMES2, COMMUTATIVITY-OF-TIMES, QUOTIENT-OF-NON-NUMBER, REMAINDER-TIMES1-INSTANCE, QUOTIENT-TIMES-INSTANCE, EQUAL-TIMES-0, and TIMES-ZERO, and opening up AND, IMPLIES, REMAINDER, NUMBERP, EQUAL, LESSP, TIMES, QUOTIENT, and ZEROP, to two new formulas: Case 2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (NUMBERP B))) (EQUAL (REMAINDER 0 B) 0)), which again simplifies, appealing to the lemma REMAINDER-ZERO, and unfolding the functions ZEROP, NUMBERP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL C 0)) (NUMBERP C) (NUMBERP B)) (EQUAL (REMAINDER B B) 0)), which again simplifies, appealing to the lemma REMAINDER-X-X, and unfolding the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.6 0.0 ] GCD-TIMES-EASY-PROOF-HELPER (PROVE-LEMMA GCD-TIMES-EASY-PROOF NIL (IMPLIES (EQUAL (GCD A B) 1) (EQUAL (GCD A (TIMES B C)) (GCD A C))) ((ENABLE EQUAL-GCD-GCD-AS-REMAINDER REMAINDER-GCD REMAINDER-GCD-ARG1 REMAINDER-TIMES1) (USE (GCD-TIMES-EASY-PROOF-HELPER)) (DISABLE-THEORY REMAINDERS))) This simplifies, applying the lemmas TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES, TIMES-ZERO, GCD-REMAINDER, REMAINDER-TIMES1, COMMON-DIVISOR-DIVIDES-GCD, REMAINDER-GCD, and EQUAL-GCD-GCD-AS-REMAINDER, and opening up the functions ZEROP, REMAINDER, NUMBERP, EQUAL, and LESSP, to: T. Q.E.D. [ 0.0 0.4 0.0 ] GCD-TIMES-EASY-PROOF (PROVE-LEMMA GCD-TIMES-EASY (REWRITE) (IMPLIES (EQUAL (GCD A B) 1) (AND (EQUAL (GCD A (TIMES B C)) (GCD A C)) (EQUAL (GCD A (TIMES C B)) (GCD A C)))) ((USE (GCD-TIMES-EASY-PROOF)) (ENABLE COMMUTATIVITY-OF-TIMES) (DISABLE-THEORY NATURALS))) WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-TIMES-EASY could! WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-TIMES-EASY could! WARNING: Note that the proposed lemma GCD-TIMES-EASY is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and unfolding EQUAL, IMPLIES, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GCD-TIMES-EASY (PROVE-LEMMA LESSP-GCD3 (REWRITE) (AND (EQUAL (LESSP (GCD A B) A) (AND (NOT (EQUAL (REMAINDER B A) 0)) (NOT (ZEROP A)) (NOT (ZEROP B)))) (EQUAL (LESSP (GCD B A) A) (AND (NOT (EQUAL (REMAINDER B A) 0)) (NOT (ZEROP A)) (NOT (ZEROP B))))) ((USE (EQUAL-X-GCD-X-Y (X A) (Y B)) (LESSP-GCD2 (B A) (A B))) (DISABLE-THEORY NATURALS) (ENABLE GCD-ZERO))) WARNING: Note that the proposed lemma LESSP-GCD3 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture simplifies, rewriting with GCD-ZERO, and expanding AND, IMPLIES, ZEROP, LESSP, NOT, REMAINDER, EQUAL, and NUMBERP, to eight new formulas: Case 8. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (NOT (NUMBERP B))) (EQUAL (LESSP (GCD A B) A) F)), which again simplifies, rewriting with GCD-ZERO, and expanding the definition of ZEROP, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (EQUAL B 0)) (EQUAL (LESSP (GCD A B) A) F)). But this again simplifies, appealing to the lemma GCD-ZERO, and unfolding the definition of ZEROP, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (GCD A B) A) T)), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (LESSP A (GCD B A))) (NOT (LESSP A (GCD A B))) (NOT (EQUAL B 0)) (NUMBERP B)) (LESSP (GCD A B) A)), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (NOT (NUMBERP B))) (EQUAL (LESSP (GCD B A) A) F)), which again simplifies, rewriting with GCD-ZERO, and opening up the function ZEROP, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (EQUAL B 0)) (EQUAL (LESSP (GCD B A) A) F)). This again simplifies, appealing to the lemma GCD-ZERO, and expanding the definition of ZEROP, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B))) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (GCD B A) A) T)), which again simplifies, obviously, to: (IMPLIES (AND (NOT (EQUAL A (GCD A B))) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (LESSP A (GCD B A))) (NOT (LESSP A (GCD A B))) (NOT (EQUAL B 0)) (NUMBERP B)) (LESSP (GCD B A) A)), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NUMBERP A) (EQUAL (EQUAL (REMAINDER B A) 0) T) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B)))) (NOT (LESSP (GCD A B) A))), which again simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NUMBERP A) (EQUAL (EQUAL (REMAINDER B A) 0) T) (NOT (EQUAL A (GCD B A))) (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (EQUAL (LESSP A (GCD B A)) F) (NOT (LESSP A (GCD A B)))) (NOT (LESSP (GCD B A) A))). This again simplifies, obviously, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LESSP-GCD3 (PROVE-LEMMA EQUAL-REMAINDER-GCD-0-PROOF NIL (EQUAL (EQUAL (REMAINDER (GCD A B) A) 0) (EQUAL (REMAINDER B A) 0))) This conjecture simplifies, rewriting with REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1, LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and expanding the definitions of NUMBERP, EQUAL, LESSP, and REMAINDER, to the following five new goals: Case 5. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NUMBERP B)). However this again simplifies, rewriting with the lemma REMAINDER-OF-NON-NUMBER, and unfolding the functions LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 4. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL B 0))), which again simplifies, expanding the functions LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A)) (NOT (EQUAL (GCD A B) 0))), which again simplifies, applying EQUAL-GCD-0, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (NOT (NUMBERP A)) (NUMBERP B)) (EQUAL (EQUAL B 0) T)). This again simplifies, rewriting with REMAINDER-ZERO, and expanding ZEROP, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (EQUAL A 0) (NUMBERP B)) (EQUAL (EQUAL B 0) T)). However this again simplifies, rewriting with the lemma REMAINDER-ZERO, and expanding the definition of ZEROP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EQUAL-REMAINDER-GCD-0-PROOF (PROVE-LEMMA EQUAL-REMAINDER-GCD-0 (REWRITE) (AND (EQUAL (EQUAL (REMAINDER (GCD A B) A) 0) (EQUAL (REMAINDER B A) 0)) (EQUAL (EQUAL (REMAINDER (GCD B A) A) 0) (EQUAL (REMAINDER B A) 0)))) WARNING: the previously added lemma, REMAINDER-GCD-ARG1, could be applied whenever the newly proposed EQUAL-REMAINDER-GCD-0 could! WARNING: the previously added lemma, REMAINDER-GCD-ARG1, could be applied whenever the newly proposed EQUAL-REMAINDER-GCD-0 could! WARNING: Note that the proposed lemma EQUAL-REMAINDER-GCD-0 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviation AND, to the following two new goals: Case 2. (EQUAL (EQUAL (REMAINDER (GCD A B) A) 0) (EQUAL (REMAINDER B A) 0)). This simplifies, rewriting with REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1, LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and expanding the functions NUMBERP, EQUAL, LESSP, and REMAINDER, to five new conjectures: Case 2.5. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NUMBERP B)), which again simplifies, applying REMAINDER-OF-NON-NUMBER, and unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2.4. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL B 0))). However this again simplifies, expanding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2.3. (IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A)) (NOT (EQUAL (GCD A B) 0))), which again simplifies, applying EQUAL-GCD-0, to: T. Case 2.2. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (NOT (NUMBERP A)) (NUMBERP B)) (EQUAL (EQUAL B 0) T)). This again simplifies, applying REMAINDER-ZERO, and opening up the function ZEROP, to: T. Case 2.1. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (EQUAL A 0) (NUMBERP B)) (EQUAL (EQUAL B 0) T)). However this again simplifies, applying REMAINDER-ZERO, and unfolding ZEROP, to: T. Case 1. (EQUAL (EQUAL (REMAINDER (GCD B A) A) 0) (EQUAL (REMAINDER B A) 0)). This simplifies, rewriting with COMMUTATIVITY-OF-GCD, REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1, LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and expanding the definitions of NUMBERP, EQUAL, LESSP, and REMAINDER, to five new goals: Case 1.5. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NUMBERP B)), which again simplifies, rewriting with the lemma REMAINDER-OF-NON-NUMBER, and opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 1.4. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL B 0))), which again simplifies, unfolding the functions LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0)) (NOT (EQUAL A 0)) (NUMBERP A)) (NOT (EQUAL (GCD A B) 0))), which again simplifies, rewriting with EQUAL-GCD-0, to: T. Case 1.2. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (NOT (NUMBERP A)) (NUMBERP B)) (EQUAL (EQUAL B 0) T)). But this again simplifies, rewriting with the lemma REMAINDER-ZERO, and opening up ZEROP, to: T. Case 1.1. (IMPLIES (AND (EQUAL (REMAINDER B A) 0) (EQUAL A 0) (NUMBERP B)) (EQUAL (EQUAL B 0) T)), which again simplifies, applying REMAINDER-ZERO, and opening up ZEROP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] EQUAL-REMAINDER-GCD-0 (PROVE-LEMMA EQUAL-REMAINDER-X-Y-X (REWRITE) (EQUAL (EQUAL (REMAINDER X Y) X) (OR (AND (NUMBERP X) (LESSP X Y)) (EQUAL X 0) (AND (EQUAL (FIX Y) 0) (NUMBERP X))))) This simplifies, expanding AND, FIX, and OR, to ten new formulas: Case 10.(IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X)) (NOT (NUMBERP Y))) (NOT (NUMBERP X))), which again simplifies, applying REMAINDER-ZERO, and unfolding ZEROP, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X)) (EQUAL Y 0)) (NOT (NUMBERP X))). But this again simplifies, rewriting with the lemma REMAINDER-ZERO, and opening up the definition of ZEROP, to: T. Case 8. (IMPLIES (NOT (EQUAL (REMAINDER X Y) X)) (NOT (EQUAL X 0))), which again simplifies, opening up LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X)) (NUMBERP X)) (NOT (LESSP X Y))), which again simplifies, rewriting with the lemma REMAINDER-NOOP, to: T. Case 6. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (NUMBERP X)) (NOT (EQUAL X 0)) (NUMBERP Y)) (EQUAL Y 0)), which again simplifies, clearly, to: T. Case 5. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (LESSP X Y)) (NOT (EQUAL X 0)) (NUMBERP Y)) (EQUAL Y 0)). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by (PLUS Z (TIMES Y V)) to eliminate (REMAINDER X Y) and (QUOTIENT X Y). We use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. This generates two new goals: Case 5.2. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (REMAINDER X Y) X) (NOT (LESSP X Y)) (NOT (EQUAL X 0)) (NUMBERP Y)) (EQUAL Y 0)), which further simplifies, clearly, to: T. Case 5.1. (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z Y) (NOT (ZEROP Y))) (NUMBERP V) (EQUAL Z (PLUS Z (TIMES Y V))) (NOT (LESSP (PLUS Z (TIMES Y V)) Y)) (NOT (EQUAL (PLUS Z (TIMES Y V)) 0)) (NUMBERP Y)) (EQUAL Y 0)). But this further simplifies, rewriting with COMMUTATIVITY-OF-TIMES, CORRECTNESS-OF-CANCEL-EQUAL-PLUS, EQUAL-TIMES-0, and PLUS-ZERO-ARG2, and expanding ZEROP, NOT, FIX, EQUAL, and TIMES, to: T. Case 4. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (NUMBERP X)) (NOT (EQUAL X 0)) (NOT (NUMBERP Y))) (EQUAL (NUMBERP X) T)). This again simplifies, trivially, to: T. Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (NUMBERP X)) (NOT (EQUAL X 0)) (EQUAL Y 0)) (EQUAL (NUMBERP X) T)). This again simplifies, trivially, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (LESSP X Y)) (NOT (EQUAL X 0)) (NOT (NUMBERP Y))) (EQUAL (NUMBERP X) T)). This again simplifies, trivially, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Y) X) (NOT (LESSP X Y)) (NOT (EQUAL X 0)) (EQUAL Y 0)) (EQUAL (NUMBERP X) T)). This again simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-REMAINDER-X-Y-X (PROVE-LEMMA GCD-A-GCD-EXP-A (REWRITE) (EQUAL (GCD A (EXP A B)) (IF (ZEROP B) 1 (FIX A)))) WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-A-GCD-EXP-A could! This conjecture simplifies, expanding the definitions of ZEROP and FIX, to the following four new formulas: Case 4. (IMPLIES (NOT (NUMBERP B)) (EQUAL (GCD A (EXP A B)) 1)). This again simplifies, applying EXP-ZERO, REMAINDER-1-ARG2, and GCD-REMAINDER, and opening up ZEROP, EQUAL, and NUMBERP, to: T. Case 3. (IMPLIES (EQUAL B 0) (EQUAL (GCD A (EXP A B)) 1)). This again simplifies, applying EXP-0-ARG2, REMAINDER-1-ARG2, and GCD-REMAINDER, and opening up the functions EQUAL and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NUMBERP A)) (EQUAL (GCD A (EXP A B)) A)). However this again simplifies, rewriting with REMAINDER-EXP and GCD-REMAINDER, and expanding the function EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (NUMBERP A))) (EQUAL (GCD A (EXP A B)) 0)). This again simplifies, rewriting with REMAINDER-ZERO and GCD-REMAINDER, and expanding the definitions of TIMES, EXP, EQUAL, NUMBERP, and ZEROP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-A-GCD-EXP-A (PROVE-LEMMA EQUAL-GCD-TIMES-1-HELP1 NIL (IMPLIES (AND (EQUAL (GCD A B) 1) (EQUAL (GCD A C) 1)) (EQUAL (GCD A (TIMES B C)) 1))) This conjecture simplifies, applying GCD-TIMES-EASY, and unfolding the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EQUAL-GCD-TIMES-1-HELP1 (PROVE-LEMMA REMAINDER-GCD-GCD-0-HACK (REWRITE) (EQUAL (REMAINDER (GCD A (TIMES B C)) (GCD A C)) 0)) This formula can be simplified, using the abbreviations REMAINDER-GCD and REMAINDER-GCD-ARG1, to the following two new goals: Case 2. (EQUAL 0 0). This simplifies, obviously, to: T. Case 1. (EQUAL (REMAINDER (TIMES B C) (GCD A C)) 0). This simplifies, rewriting with the lemmas REMAINDER-TIMES1-INSTANCE and REMAINDER-GCD-0, and unfolding EQUAL, to: T. Q.E.D. [ 0.0 0.2 0.0 ] REMAINDER-GCD-GCD-0-HACK (PROVE-LEMMA LESSP-GCD-TIMES NIL (IMPLIES (OR (NOT (ZEROP A)) (NOT (ZEROP (TIMES B C)))) (NOT (LESSP (GCD A (TIMES B C)) (GCD A C)))) ((USE (REMAINDER-GCD-GCD-0-HACK)) (DISABLE REMAINDER-GCD-GCD-0-HACK) (DISABLE-THEORY NATURALS) (ENABLE REMAINDER-NOOP EQUAL-TIMES-0 EQUAL-GCD-0))) This simplifies, rewriting with REMAINDER-NOOP, EQUAL-TIMES-0, and EQUAL-GCD-0, and opening up the functions ZEROP, NOT, EQUAL, TIMES, and OR, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-GCD-TIMES (PROVE-LEMMA LESSP-1-HACK (REWRITE) (EQUAL (LESSP 1 X) (AND (NOT (ZEROP X)) (NOT (EQUAL X 1))))) WARNING: the newly proposed lemma, LESSP-1-HACK, could be applied whenever the previously added lemma LESSP-1-TIMES could. This conjecture simplifies, unfolding the definitions of ZEROP, NOT, and AND, to four new conjectures: Case 4. (IMPLIES (EQUAL X 0) (EQUAL (LESSP 1 X) F)), which again simplifies, unfolding the functions LESSP and EQUAL, to: T. Case 3. (IMPLIES (NOT (NUMBERP X)) (EQUAL (LESSP 1 X) F)), which again simplifies, unfolding the functions LESSP and EQUAL, to: T. Case 2. (IMPLIES (EQUAL X 1) (EQUAL (LESSP 1 X) F)), which again simplifies, expanding the functions LESSP and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (EQUAL (LESSP 1 X) T)), which again simplifies, clearly, to the new formula: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP 1 X)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-1-HACK (PROVE-LEMMA EQUAL-GCD-TIMES-1-HELP2 NIL (IMPLIES (EQUAL (GCD A (TIMES B C)) 1) (EQUAL (GCD A C) 1)) ((USE (LESSP-GCD-TIMES)) (DISABLE-THEORY REMAINDERS) (ENABLE-THEORY MULTIPLICATION))) This formula simplifies, applying EQUAL-TIMES-0, EQUAL-GCD-0, LESSP-1-HACK, GCD-REMAINDER, COMMUTATIVITY-OF-TIMES, and TIMES-ZERO, and expanding the definitions of ZEROP, NOT, OR, IMPLIES, EQUAL, TIMES, REMAINDER, NUMBERP, and GCD, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-GCD-TIMES-1-HELP2 (PROVE-LEMMA EQUAL-GCD-TIMES-1 (REWRITE) (EQUAL (EQUAL (GCD A (TIMES B C)) 1) (AND (EQUAL (GCD A B) 1) (EQUAL (GCD A C) 1))) ((USE (EQUAL-GCD-TIMES-1-HELP1) (EQUAL-GCD-TIMES-1-HELP2) (EQUAL-GCD-TIMES-1-HELP2 (B C) (C B))) (DISABLE-THEORY NATURALS))) This conjecture simplifies, applying GCD-TIMES-EASY, and expanding the functions AND, IMPLIES, and EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EQUAL-GCD-TIMES-1 (PROVE-LEMMA GCD-EXP-1 (REWRITE) (AND (EQUAL (EQUAL (GCD A (EXP B C)) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C))) (EQUAL (EQUAL (GCD (EXP B C) A) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C)))) ((INDUCT (EXP B C)))) WARNING: Note that the proposed lemma GCD-EXP-1 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and AND, to the following two new conjectures: Case 2. (IMPLIES (ZEROP C) (AND (EQUAL (EQUAL (GCD A (EXP B C)) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C))) (EQUAL (EQUAL (GCD (EXP B C) A) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C))))). This simplifies, appealing to the lemmas EXP-0-ARG2, REMAINDER-1-ARG2, GCD-REMAINDER, and EXP-ZERO, and unfolding ZEROP, EQUAL, NUMBERP, OR, and AND, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL (EQUAL (GCD A (EXP B (SUB1 C))) 1) (OR (EQUAL (GCD A B) 1) (ZEROP (SUB1 C)))) (EQUAL (EQUAL (GCD (EXP B (SUB1 C)) A) 1) (OR (EQUAL (GCD A B) 1) (ZEROP (SUB1 C))))) (AND (EQUAL (EQUAL (GCD A (EXP B C)) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C))) (EQUAL (EQUAL (GCD (EXP B C) A) 1) (OR (EQUAL (GCD A B) 1) (ZEROP C))))). This simplifies, rewriting with the lemmas EQUAL-SUB1-0, EXP-ZERO, REMAINDER-1-ARG2, GCD-REMAINDER, COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1, COMMUTATIVITY-OF-GCD, EQUAL-GCD-TIMES-1, and GCD-TIMES-EASY, and expanding the definitions of ZEROP, OR, EQUAL, NUMBERP, EXP, and AND, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL (GCD A (EXP B (SUB1 C))) 1) (EQUAL (EQUAL C 1) T) (NOT (EQUAL (GCD A B) 1)) (NOT (NUMBERP B))) (NOT (EQUAL (GCD A 0) 1))). However this again simplifies, applying EQUAL-SUB1-0, EXP-ZERO, REMAINDER-1-ARG2, GCD-REMAINDER, REMAINDER-OF-NON-NUMBER, and REMAINDER-ZERO, and expanding the functions ZEROP, EQUAL, NUMBERP, REMAINDER, and LESSP, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL (GCD A (EXP B (SUB1 C))) 1) (EQUAL (EQUAL C 1) T) (EQUAL (GCD A B) 1) (NUMBERP B)) (EQUAL (EQUAL (GCD A B) 1) T)). But this again simplifies, rewriting with EQUAL-SUB1-0, EXP-ZERO, REMAINDER-1-ARG2, and GCD-REMAINDER, and expanding the definitions of ZEROP, EQUAL, and NUMBERP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL (GCD A (EXP B (SUB1 C))) 1) (EQUAL (EQUAL C 1) T) (EQUAL (GCD A B) 1) (NOT (NUMBERP B))) (EQUAL (EQUAL (GCD A 0) 1) T)). This again simplifies, rewriting with EQUAL-SUB1-0, EXP-ZERO, REMAINDER-1-ARG2, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and opening up the functions ZEROP, EQUAL, NUMBERP, REMAINDER, LESSP, and GCD, to: T. Q.E.D. [ 0.0 2.1 0.0 ] GCD-EXP-1 (PROVE-LEMMA GCD-REMAINDER-TIMES-FACT1-PROOF2 (REWRITE) (IMPLIES (EQUAL (GCD A B) 1) (EQUAL (EQUAL (REMAINDER (TIMES C B) A) 0) (EQUAL (REMAINDER C A) 0)))) This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES and GCD-REMAINDER-TIMES-FACT1-PROOF, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-REMAINDER-TIMES-FACT1-PROOF2 (PROVE-LEMMA TIMES-QUOTIENT-BETTER (REWRITE) (IMPLIES (EQUAL (REMAINDER X Y) 0) (AND (EQUAL (TIMES (QUOTIENT X Y) Y) (IF (ZEROP Y) 0 (FIX X))) (EQUAL (TIMES Y (QUOTIENT X Y)) (IF (ZEROP Y) 0 (FIX X)))))) WARNING: the newly proposed lemma, TIMES-QUOTIENT-BETTER, could be applied whenever the previously added lemma TIMES-QUOTIENT could. WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed TIMES-QUOTIENT-BETTER could! WARNING: the newly proposed lemma, TIMES-QUOTIENT-BETTER, could be applied whenever the previously added lemma TIMES-QUOTIENT could. WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed TIMES-QUOTIENT-BETTER could! WARNING: Note that the proposed lemma TIMES-QUOTIENT-BETTER is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding ZEROP, FIX, and AND, to the following four new conjectures: Case 4. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0) (EQUAL Y 0)) (EQUAL (TIMES Y (QUOTIENT X Y)) 0)). This again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0) (NOT (NUMBERP Y))) (EQUAL (TIMES Y (QUOTIENT X Y)) 0)), which again simplifies, applying REMAINDER-ZERO, QUOTIENT-ZERO, TIMES-ZERO, and COMMUTATIVITY-OF-TIMES, and unfolding the definitions of ZEROP and EQUAL, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0) (NOT (NUMBERP X))) (EQUAL (TIMES Y (QUOTIENT X Y)) 0)). This again simplifies, rewriting with REMAINDER-OF-NON-NUMBER, QUOTIENT-OF-NON-NUMBER, and COMMUTATIVITY-OF-TIMES, and expanding the functions LESSP, EQUAL, NUMBERP, REMAINDER, QUOTIENT, and TIMES, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (EQUAL (TIMES Y (QUOTIENT X Y)) X)). But this again simplifies, applying TIMES-QUOTIENT, to: T. Q.E.D. [ 0.0 0.1 0.0 ] TIMES-QUOTIENT-BETTER (PROVE-LEMMA EQUAL-REMAINDER-EXP-0 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER A C) 0) (NOT (ZEROP B))) (EQUAL (REMAINDER (EXP A B) C) 0))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (REMAINDER (EXP A B) C) 0)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z)) to eliminate (REMAINDER A C) and (QUOTIENT A C). We employ LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We would thus like to prove the following four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (REMAINDER (EXP A B) C) 0)). But this simplifies, rewriting with REMAINDER-OF-NON-NUMBER, and expanding LESSP, EQUAL, NUMBERP, REMAINDER, TIMES, and EXP, to: T. Case 3. (IMPLIES (AND (EQUAL C 0) (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (REMAINDER (EXP A B) C) 0)). This simplifies, appealing to the lemmas REMAINDER-ZERO and EXP-0-ARG1, and opening up ZEROP, REMAINDER, EQUAL, TIMES, and EXP, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP C)) (EQUAL (REMAINDER A C) 0) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (REMAINDER (EXP A B) C) 0)), which simplifies, applying the lemmas REMAINDER-ZERO and EXP-0-ARG1, and expanding the definitions of ZEROP, NUMBERP, EQUAL, TIMES, and EXP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL X 0) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (REMAINDER (EXP (PLUS X (TIMES C Z)) B) C) 0)), which simplifies, applying EXP-TIMES, REMAINDER-EXP, and REMAINDER-TIMES1, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EQUAL-REMAINDER-EXP-0 (PROVE-LEMMA REMAINDER-2-HACK (REWRITE) (EQUAL (REMAINDER 2 X) (IF (OR (EQUAL X 1) (EQUAL X 2)) 0 2))) This simplifies, unfolding the definition of OR, to the following three new formulas: Case 3. (IMPLIES (EQUAL X 2) (EQUAL (REMAINDER 2 X) 0)). This again simplifies, opening up REMAINDER and EQUAL, to: T. Case 2. (IMPLIES (EQUAL X 1) (EQUAL (REMAINDER 2 X) 0)), which again simplifies, unfolding the definitions of REMAINDER and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 1)) (NOT (EQUAL X 2))) (EQUAL (REMAINDER 2 X) 2)), which again simplifies, applying REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1, EQUAL-SUB1-0, and LESSP-1-HACK, and unfolding the functions LESSP, EQUAL, SUB1, NUMBERP, and REMAINDER, to the new formula: (IMPLIES (AND (NOT (EQUAL X 1)) (NOT (EQUAL X 2)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (EQUAL (SUB1 X) 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-2-HACK (PROVE-LEMMA REMAINDER-TIMES-HACK2 (REWRITE) (IMPLIES (NOT (EQUAL (REMAINDER A B) 0)) (AND (NOT (EQUAL (REMAINDER A (TIMES B C)) 0)) (NOT (EQUAL (REMAINDER A (TIMES C B)) 0))))) WARNING: Note that the proposed lemma REMAINDER-TIMES-HACK2 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding the definitions of NOT and AND, to: (IMPLIES (NOT (EQUAL (REMAINDER A B) 0)) (NOT (EQUAL (REMAINDER A (TIMES B C)) 0))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following four new conjectures: Case 4. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL (REMAINDER A B) 0))) (NOT (EQUAL (REMAINDER A (TIMES B C)) 0))). However this further simplifies, applying REMAINDER-OF-NON-NUMBER, and opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 3. (IMPLIES (AND (EQUAL B 0) (NOT (EQUAL (REMAINDER A B) 0))) (NOT (EQUAL (REMAINDER A (TIMES B C)) 0))). However this further simplifies, applying REMAINDER-ZERO, and opening up ZEROP, EQUAL, and TIMES, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER A B) 0))) (NOT (EQUAL (REMAINDER A (TIMES B C)) 0))). But this further simplifies, rewriting with REMAINDER-ZERO, and unfolding the functions ZEROP and TIMES, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (EQUAL X 0))) (NOT (EQUAL (REMAINDER (PLUS X (TIMES B Z)) (TIMES B C)) 0))). However this further simplifies, appealing to the lemmas REMAINDER-TIMES2-INSTANCE, REMAINDER-PLUS-TIMES-TIMES, and EQUAL-PLUS-0, and opening up the definitions of ZEROP and NOT, to: T. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-TIMES-HACK2 (PROVE-LEMMA GCD-A-ADD1-A (REWRITE) (EQUAL (GCD A (ADD1 A)) 1)) WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-A-ADD1-A could! This simplifies, using linear arithmetic, rewriting with GCD-REMAINDER, REMAINDER-NOOP, DIFFERENCE-ADD1-ARG2, DIFFERENCE-SUB1-ARG2, DIFFERENCE-X-X, SUB1-ADD1, and SUB1-TYPE-RESTRICTION, and unfolding NUMBERP, EQUAL, SUB1, ADD1, DIFFERENCE, LESSP, and GCD, to the following three new conjectures: Case 3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (LESSP (SUB1 A) A))) (EQUAL (ADD1 A) 1)). However this again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (LESSP (SUB1 A) A) (LESSP A A)) (EQUAL (GCD A 0) 1)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (LESSP (SUB1 A) A) (NOT (LESSP A A))) (EQUAL (GCD A 1) 1)), which again simplifies, applying REMAINDER-1-ARG2 and GCD-REMAINDER, and opening up the functions EQUAL and NUMBERP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-A-ADD1-A (PROVE-LEMMA REMAINDER-TIMES-TIMES-HACK (REWRITE) (EQUAL (REMAINDER (TIMES B (TIMES A C)) (TIMES A X)) (TIMES A (REMAINDER (TIMES B C) X)))) This simplifies, appealing to the lemmas COMMUTATIVITY2-OF-TIMES and REMAINDER-TIMES2-INSTANCE, to: T. Q.E.D. [ 0.0 1.4 0.0 ] REMAINDER-TIMES-TIMES-HACK (PROVE-LEMMA REMAINDER-PLUS-TIMES-HACK (REWRITE) (EQUAL (REMAINDER (PLUS (TIMES A X) (TIMES B (TIMES C (TIMES A Y)))) (TIMES A Z)) (TIMES A (REMAINDER (PLUS X (TIMES B (TIMES C Y))) Z))) ((USE (REMAINDER-TIMES-TIMES-PROOF (Y (PLUS X (TIMES B (TIMES C Y)))) (X A) (Z Z))) (DISABLE-THEORY NATURALS) (ENABLE TIMES-DISTRIBUTES-OVER-PLUS COMMUTATIVITY2-OF-TIMES))) This formula simplifies, appealing to the lemmas TIMES-DISTRIBUTES-OVER-PLUS and COMMUTATIVITY2-OF-TIMES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-PLUS-TIMES-HACK (DEFN FIB (X) (IF (ZEROP X) 0 (IF (EQUAL X 1) 1 (PLUS (FIB (SUB1 (SUB1 X))) (FIB (SUB1 X)))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIB is accepted under the principle of definition. Note that (NUMBERP (FIB X)) is a theorem. [ 0.0 0.0 0.0 ] FIB (PROVE-LEMMA FIB-PLUS (REWRITE) (EQUAL (FIB (PLUS J K)) (IF (ZEROP J) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB J)) (TIMES (FIB (SUB1 J)) (FIB K)))))) This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and COMMUTATIVITY-OF-TIMES, and expanding the definitions of PLUS and ZEROP, to the following three new formulas: Case 3. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP K))) (EQUAL (FIB 0) (FIB K))). But this again simplifies, unfolding the definitions of FIB and EQUAL, to: T. Case 2. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K))) (EQUAL (FIB 0) (FIB K))), which again simplifies, expanding FIB and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J)) (EQUAL (FIB (ADD1 (PLUS K (SUB1 J)))) (PLUS (TIMES (FIB J) (FIB (ADD1 K))) (TIMES (FIB K) (FIB (SUB1 J)))))). Applying the lemma SUB1-ELIM, replace J by (ADD1 X) to eliminate (SUB1 J). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove the new goal: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0))) (EQUAL (FIB (ADD1 (PLUS K X))) (PLUS (TIMES (FIB (ADD1 X)) (FIB (ADD1 K))) (TIMES (FIB K) (FIB X))))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, to the new goal: (IMPLIES (NUMBERP X) (EQUAL (FIB (ADD1 (PLUS K X))) (PLUS (TIMES (FIB K) (FIB X)) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (FIB (PLUS J K)) (IF (ZEROP J) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB J)) (TIMES (FIB (SUB1 J)) (FIB K))))), named *1. Let us appeal to the induction principle. There are four plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p J K)) (IMPLIES (AND (NOT (ZEROP J)) (EQUAL J 1)) (p J K)) (IMPLIES (AND (NOT (ZEROP J)) (NOT (EQUAL J 1)) (p (SUB1 (SUB1 J)) K) (p (SUB1 J) K)) (p J K))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT J) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new goals: Case 3. (IMPLIES (ZEROP J) (EQUAL (FIB (PLUS J K)) (IF (ZEROP J) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB J)) (TIMES (FIB (SUB1 J)) (FIB K)))))), which simplifies, expanding the functions ZEROP, EQUAL, and PLUS, to two new conjectures: Case 3.2. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K))) (EQUAL (FIB 0) (FIB K))), which again simplifies, unfolding the functions FIB and EQUAL, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP K))) (EQUAL (FIB 0) (FIB K))), which again simplifies, opening up FIB and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP J)) (EQUAL J 1)) (EQUAL (FIB (PLUS J K)) (IF (ZEROP J) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB J)) (TIMES (FIB (SUB1 J)) (FIB K)))))), which simplifies, applying PLUS-ADD1-ARG1, TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES, and PLUS-ZERO-ARG2, and expanding the functions ZEROP, EQUAL, PLUS, FIB, SUB1, and TIMES, to: (IMPLIES (NOT (NUMBERP K)) (EQUAL (FIB 1) (FIB (ADD1 K)))), which again simplifies, rewriting with SUB1-TYPE-RESTRICTION, and opening up the functions FIB and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (NOT (EQUAL J 1)) (EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K)) (IF (ZEROP (SUB1 (SUB1 J))) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (SUB1 (SUB1 (SUB1 J)))) (FIB K))))) (EQUAL (FIB (PLUS (SUB1 J) K)) (IF (ZEROP (SUB1 J)) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB (SUB1 J))) (TIMES (FIB (SUB1 (SUB1 J))) (FIB K)))))) (EQUAL (FIB (PLUS J K)) (IF (ZEROP J) (FIB K) (PLUS (TIMES (FIB (ADD1 K)) (FIB J)) (TIMES (FIB (SUB1 J)) (FIB K)))))). This simplifies, applying EQUAL-SUB1-0, COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, TIMES-DISTRIBUTES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and unfolding ZEROP, PLUS, and FIB, to two new goals: Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL J 1)) (NOT (EQUAL (SUB1 J) 1)) (EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K)) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 (SUB1 J))))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))))) (EQUAL (FIB (PLUS (SUB1 J) K)) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 J)))))) (EQUAL (FIB (ADD1 (PLUS (SUB1 J) K))) (PLUS (TIMES (FIB K) (FIB (SUB1 J))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 J))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J))))))), which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, EQUAL-SUB1-0, TIMES-DISTRIBUTES-OVER-PLUS, and ASSOCIATIVITY-OF-PLUS, and unfolding the function FIB, to: (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL J 1)) (NOT (EQUAL (SUB1 J) 1)) (EQUAL (FIB (PLUS K (SUB1 (SUB1 J)))) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 (SUB1 J))))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))))) (EQUAL (FIB (PLUS K (SUB1 J))) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 (SUB1 J)))))))) (EQUAL (FIB (ADD1 (PLUS K (SUB1 J)))) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB K) (FIB (SUB1 (SUB1 (SUB1 J))))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 (SUB1 J)))))))). Applying the lemma SUB1-ELIM, replace J by (ADD1 X) to eliminate (SUB1 J), X by (ADD1 Z) to eliminate (SUB1 X), and Z by (ADD1 X) to eliminate (SUB1 Z). We rely upon the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces the following three new formulas: Case 1.2.3. (IMPLIES (AND (EQUAL X 0) (NUMBERP X) (NOT (EQUAL (ADD1 X) 0)) (NOT (EQUAL (ADD1 X) 1)) (NOT (EQUAL X 1)) (EQUAL (FIB (PLUS K (SUB1 X))) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 X)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 X))))) (EQUAL (FIB (PLUS K X)) (PLUS (TIMES (FIB K) (FIB (SUB1 X))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 X))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 X))))))) (EQUAL (FIB (ADD1 (PLUS K X))) (PLUS (TIMES (FIB K) (FIB (SUB1 X))) (TIMES (FIB K) (FIB (SUB1 (SUB1 X)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 X))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 X))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 X))))))). This further simplifies, trivially, to: T. Case 1.2.2. (IMPLIES (AND (EQUAL Z 0) (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL (ADD1 (ADD1 Z)) 0)) (NOT (EQUAL (ADD1 (ADD1 Z)) 1)) (NOT (EQUAL (ADD1 Z) 1)) (EQUAL (FIB (PLUS K Z)) (PLUS (TIMES (FIB K) (FIB (SUB1 Z))) (TIMES (FIB (ADD1 K)) (FIB Z)))) (EQUAL (FIB (PLUS K (ADD1 Z))) (PLUS (TIMES (FIB K) (FIB Z)) (TIMES (FIB (ADD1 K)) (FIB Z)) (TIMES (FIB (ADD1 K)) (FIB (SUB1 Z)))))) (EQUAL (FIB (ADD1 (PLUS K (ADD1 Z)))) (PLUS (TIMES (FIB K) (FIB Z)) (TIMES (FIB K) (FIB (SUB1 Z))) (TIMES (FIB (ADD1 K)) (FIB Z)) (TIMES (FIB (ADD1 K)) (FIB Z)) (TIMES (FIB (ADD1 K)) (FIB (SUB1 Z)))))). This further simplifies, trivially, to: T. Case 1.2.1. (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0)) (NOT (EQUAL (ADD1 (ADD1 X)) 0)) (NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 0)) (NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 1)) (NOT (EQUAL (ADD1 (ADD1 X)) 1)) (EQUAL (FIB (PLUS K (ADD1 X))) (PLUS (TIMES (FIB K) (FIB X)) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))))) (EQUAL (FIB (PLUS K (ADD1 (ADD1 X)))) (PLUS (TIMES (FIB K) (FIB (ADD1 X))) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))) (TIMES (FIB (ADD1 K)) (FIB X))))) (EQUAL (FIB (ADD1 (PLUS K (ADD1 (ADD1 X))))) (PLUS (TIMES (FIB K) (FIB (ADD1 X))) (TIMES (FIB K) (FIB X)) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))) (TIMES (FIB (ADD1 K)) (FIB X))))). But this further simplifies, appealing to the lemmas ADD1-EQUAL, PLUS-ADD1-ARG2, SUB1-ADD1, COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and opening up NUMBERP and FIB, to: (IMPLIES (AND (NUMBERP X) (EQUAL (FIB (ADD1 (PLUS K X))) (PLUS (TIMES (FIB K) (FIB X)) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))))) (EQUAL (PLUS (FIB (PLUS K X)) (FIB (ADD1 (PLUS K X)))) (PLUS (TIMES (FIB K) (FIB (ADD1 X))) (TIMES (FIB X) (FIB (ADD1 K))) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))))) (EQUAL (PLUS (FIB (PLUS K X)) (FIB (ADD1 (PLUS K X))) (FIB (ADD1 (PLUS K X)))) (PLUS (TIMES (FIB K) (FIB X)) (TIMES (FIB K) (FIB (ADD1 X))) (TIMES (FIB X) (FIB (ADD1 K))) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X))) (TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL J 1)) (EQUAL (SUB1 J) 1) (EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K)) (FIB K)) (EQUAL (FIB (PLUS (SUB1 J) K)) (PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J)))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 J)))))) (EQUAL (FIB (ADD1 (PLUS (SUB1 J) K))) (PLUS (TIMES (FIB K) (FIB (SUB1 J))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 J))) (TIMES (FIB (ADD1 K)) (FIB (SUB1 (SUB1 J))))))), which again simplifies, applying PLUS-ADD1-ARG1, TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES, SUB1-ADD1, ADD1-EQUAL, and PLUS-ZERO-ARG2, and expanding the definitions of SUB1, EQUAL, PLUS, FIB, TIMES, NUMBERP, and ZEROP, to the following two new conjectures: Case 1.1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL J 1)) (EQUAL (SUB1 J) 1) (EQUAL (FIB 0) (FIB K)) (EQUAL (FIB 1) (FIB (ADD1 K))) (NOT (NUMBERP K))) (EQUAL (PLUS (FIB 0) (FIB 1)) 1)). But this again simplifies, applying SUB1-TYPE-RESTRICTION, and expanding the definitions of FIB, EQUAL, and PLUS, to: T. Case 1.1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL J 1)) (EQUAL (SUB1 J) 1) (EQUAL (FIB 0) (FIB K)) (EQUAL (FIB 1) (FIB (ADD1 K))) (NUMBERP K)) (EQUAL (PLUS (FIB K) (FIB (ADD1 K))) 1)). However this again simplifies, opening up FIB, PLUS, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.8 0.0 ] FIB-PLUS (PROVE-LEMMA GCD-FIB-NEXT-FIB (REWRITE) (EQUAL (GCD (FIB N) (FIB (ADD1 N))) 1)) WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-FIB-NEXT-FIB could! Give the conjecture the name *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1)) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (NOT (EQUAL N 1)) (p (SUB1 N)) (p (SUB1 (SUB1 N)))) (p N))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates three new goals: Case 3. (IMPLIES (ZEROP N) (EQUAL (GCD (FIB N) (FIB (ADD1 N))) 1)), which simplifies, applying SUB1-TYPE-RESTRICTION, and unfolding the functions ZEROP, FIB, ADD1, GCD, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1)) (EQUAL (GCD (FIB N) (FIB (ADD1 N))) 1)). This simplifies, opening up ZEROP, FIB, GCD, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (NOT (EQUAL N 1)) (EQUAL (GCD (FIB (SUB1 N)) (FIB (ADD1 (SUB1 N)))) 1) (EQUAL (GCD (FIB (SUB1 (SUB1 N))) (FIB (ADD1 (SUB1 (SUB1 N))))) 1)) (EQUAL (GCD (FIB N) (FIB (ADD1 N))) 1)). This simplifies, applying ADD1-SUB1, COMMUTATIVITY-OF-PLUS, GCD-PLUS-INSTANCE, EQUAL-SUB1-0, COMMUTATIVITY-OF-GCD, SUB1-ADD1, ADD1-EQUAL, REMAINDER-X-X, and GCD-PLUS, and unfolding the definitions of ZEROP, FIB, EQUAL, and NUMBERP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.3 0.0 ] GCD-FIB-NEXT-FIB (PROVE-LEMMA GCD-FIB (REWRITE) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A B))) ((DISABLE GCD-DIFFERENCE2 REMAINDER-DIFFERENCE1))) WARNING: the newly proposed lemma, GCD-FIB, could be applied whenever the previously added lemma GCD-FIB-NEXT-FIB could. WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied whenever the newly proposed GCD-FIB could! Call the conjecture *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture, all of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP A) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP A B) (p A (DIFFERENCE B A))) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP A B)) (p (DIFFERENCE A B) B)) (p A B))). Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, and ADD1-EQUAL, and the definitions of ORDINALP, FIX, LESSP, ORD-LESSP, and ZEROP can be used to prove that the measure (CONS (ADD1 A) (FIX B)) decreases according to the well-founded relation ORD-LESSP in each induction step of the scheme. The above induction scheme leads to four new goals: Case 4. (IMPLIES (ZEROP A) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A B)))), which simplifies, applying the lemmas GCD-REMAINDER and REMAINDER-OF-NON-NUMBER, and opening up the definitions of ZEROP, FIB, REMAINDER, NUMBERP, EQUAL, and LESSP, to two new formulas: Case 4.2. (IMPLIES (AND (EQUAL A 0) (NOT (NUMBERP B))) (EQUAL (FIB B) (FIB 0))), which again simplifies, opening up the definitions of FIB and EQUAL, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (NUMBERP B))) (EQUAL (FIB B) (FIB 0))), which again simplifies, unfolding the functions FIB and EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A B)))), which simplifies, rewriting with the lemmas GCD-REMAINDER, REMAINDER-NOOP, and REMAINDER-OF-NON-NUMBER, and expanding the functions ZEROP, FIB, REMAINDER, NUMBERP, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP A B) (EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A))) (FIB (GCD A (DIFFERENCE B A))))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A B)))), which simplifies, opening up ZEROP and GCD, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP A B) (EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A))) (FIB (GCD A (DIFFERENCE B A))))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A (DIFFERENCE B A))))). Appealing to the lemma DIFFERENCE-ELIM, we now replace B by (PLUS A X) to eliminate (DIFFERENCE B A). We employ the type restriction lemma noted when DIFFERENCE was introduced to constrain the new variable. The result is two new formulas: Case 2.2. (IMPLIES (AND (LESSP B A) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP A B) (EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A))) (FIB (GCD A (DIFFERENCE B A))))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A (DIFFERENCE B A))))), which further simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (NUMBERP X) (NOT (LESSP (PLUS A X) A)) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL (PLUS A X) 0)) (LESSP A (PLUS A X)) (EQUAL (GCD (FIB A) (FIB X)) (FIB (GCD A X)))) (EQUAL (GCD (FIB A) (FIB (PLUS A X))) (FIB (GCD A X)))), which further simplifies, rewriting with CORRECTNESS-OF-CANCEL-LESSP-PLUS, EQUAL-PLUS-0, COMMUTATIVITY-OF-TIMES, FIB-PLUS, REMAINDER-TIMES1-INSTANCE, and GCD-PLUS, and expanding the definitions of FIX, ZEROP, NOT, and EQUAL, to: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL X 0)) (EQUAL (GCD (FIB A) (FIB X)) (FIB (GCD A X)))) (EQUAL (GCD (FIB A) (TIMES (FIB X) (FIB (SUB1 A)))) (FIB (GCD A X)))). Applying the lemma SUB1-ELIM, replace A by (ADD1 Z) to eliminate (SUB1 A). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new conjecture: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL X 0)) (EQUAL (GCD (FIB (ADD1 Z)) (FIB X)) (FIB (GCD (ADD1 Z) X)))) (EQUAL (GCD (FIB (ADD1 Z)) (TIMES (FIB X) (FIB Z))) (FIB (GCD (ADD1 Z) X)))), which further simplifies, applying COMMUTATIVITY-OF-GCD, GCD-FIB-NEXT-FIB, and GCD-TIMES-EASY, and unfolding EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP A B)) (EQUAL (GCD (FIB (DIFFERENCE A B)) (FIB B)) (FIB (GCD (DIFFERENCE A B) B)))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD A B)))). This simplifies, appealing to the lemma COMMUTATIVITY-OF-GCD, and expanding the definitions of ZEROP and GCD, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP A B)) (EQUAL (GCD (FIB B) (FIB (DIFFERENCE A B))) (FIB (GCD (DIFFERENCE A B) B)))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD (DIFFERENCE A B) B)))), which further simplifies, rewriting with COMMUTATIVITY-OF-GCD, to the new conjecture: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP A B)) (EQUAL (GCD (FIB B) (FIB (DIFFERENCE A B))) (FIB (GCD B (DIFFERENCE A B))))) (EQUAL (GCD (FIB A) (FIB B)) (FIB (GCD B (DIFFERENCE A B))))). Applying the lemma DIFFERENCE-ELIM, replace A by (PLUS B X) to eliminate (DIFFERENCE A B). We use the type restriction lemma noted when DIFFERENCE was introduced to restrict the new variable. We thus obtain: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (PLUS B X) 0)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP (PLUS B X) B)) (EQUAL (GCD (FIB B) (FIB X)) (FIB (GCD B X)))) (EQUAL (GCD (FIB (PLUS B X)) (FIB B)) (FIB (GCD B X)))), which further simplifies, applying EQUAL-PLUS-0, CORRECTNESS-OF-CANCEL-LESSP-PLUS, COMMUTATIVITY-OF-TIMES, FIB-PLUS, REMAINDER-TIMES1-INSTANCE, and GCD-PLUS, and unfolding EQUAL, to: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (GCD (FIB B) (FIB X)) (FIB (GCD B X)))) (EQUAL (GCD (FIB B) (TIMES (FIB X) (FIB (SUB1 B)))) (FIB (GCD B X)))). Applying the lemma SUB1-ELIM, replace B by (ADD1 Z) to eliminate (SUB1 B). We rely upon the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (GCD (FIB (ADD1 Z)) (FIB X)) (FIB (GCD (ADD1 Z) X)))) (EQUAL (GCD (FIB (ADD1 Z)) (TIMES (FIB X) (FIB Z))) (FIB (GCD (ADD1 Z) X)))), which finally simplifies, applying the lemmas COMMUTATIVITY-OF-GCD, GCD-FIB-NEXT-FIB, and GCD-TIMES-EASY, and opening up the function EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 6.2 0.0 ] GCD-FIB (PROVE-LEMMA EQUAL-FIB-CONSTANT (REWRITE) (AND (EQUAL (EQUAL (FIB A) 0) (ZEROP A)) (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2))))) WARNING: Note that the proposed lemma EQUAL-FIB-CONSTANT is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture can be simplified, using the abbreviation AND, to two new goals: Case 2. (EQUAL (EQUAL (FIB A) 0) (ZEROP A)), which simplifies, unfolding ZEROP, to three new goals: Case 2.3. (IMPLIES (NOT (EQUAL (FIB A) 0)) (NUMBERP A)), which again simplifies, unfolding the functions FIB and EQUAL, to: T. Case 2.2. (IMPLIES (NOT (EQUAL (FIB A) 0)) (NOT (EQUAL A 0))), which again simplifies, opening up FIB and EQUAL, to: T. Case 2.1. (IMPLIES (AND (EQUAL (FIB A) 0) (NOT (EQUAL A 0))) (NOT (NUMBERP A))), which we will name *1. Case 1. (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2))). This simplifies, unfolding the function OR, to the following three new conjectures: Case 1.3. (IMPLIES (NOT (EQUAL (FIB A) 1)) (NOT (EQUAL A 1))). However this again simplifies, unfolding FIB and EQUAL, to: T. Case 1.2. (IMPLIES (NOT (EQUAL (FIB A) 1)) (NOT (EQUAL A 2))), which again simplifies, expanding the functions FIB and EQUAL, to: T. Case 1.1. (IMPLIES (AND (EQUAL (FIB A) 1) (NOT (EQUAL A 1))) (EQUAL (EQUAL A 2) T)), which again simplifies, obviously, to the new conjecture: (IMPLIES (AND (EQUAL (FIB A) 1) (NOT (EQUAL A 1))) (EQUAL A 2)), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (AND (EQUAL (EQUAL (FIB A) 0) (ZEROP A)) (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2)))), named *1. Let us appeal to the induction principle. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP A) (p A)) (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1)) (p A)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (p (SUB1 A)) (p (SUB1 (SUB1 A)))) (p A))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to six new formulas: Case 6. (IMPLIES (ZEROP A) (EQUAL (EQUAL (FIB A) 0) (ZEROP A))), which simplifies, expanding the definitions of ZEROP, FIB, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1)) (EQUAL (EQUAL (FIB A) 0) (ZEROP A))), which simplifies, expanding ZEROP, FIB, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (EQUAL (EQUAL (FIB (SUB1 A)) 0) (ZEROP (SUB1 A))) (EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0) (ZEROP (SUB1 (SUB1 A)))) (EQUAL (EQUAL (FIB (SUB1 A)) 1) (OR (EQUAL (SUB1 A) 1) (EQUAL (SUB1 A) 2))) (EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 1) (OR (EQUAL (SUB1 (SUB1 A)) 1) (EQUAL (SUB1 (SUB1 A)) 2)))) (EQUAL (EQUAL (FIB A) 0) (ZEROP A))), which simplifies, applying the lemmas EQUAL-SUB1-0, PLUS-ADD1-ARG1, COMMUTATIVITY-OF-PLUS, EQUAL-PLUS-0, PLUS-ZERO-ARG2, and PLUS-ADD1-ARG2, and opening up the definitions of ZEROP, OR, FIB, EQUAL, PLUS, SUB1, and NUMBERP, to: T. Case 3. (IMPLIES (ZEROP A) (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2)))), which simplifies, expanding the functions ZEROP, FIB, EQUAL, and OR, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1)) (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2)))), which simplifies, expanding the functions ZEROP, FIB, EQUAL, and OR, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (EQUAL (EQUAL (FIB (SUB1 A)) 0) (ZEROP (SUB1 A))) (EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0) (ZEROP (SUB1 (SUB1 A)))) (EQUAL (EQUAL (FIB (SUB1 A)) 1) (OR (EQUAL (SUB1 A) 1) (EQUAL (SUB1 A) 2))) (EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 1) (OR (EQUAL (SUB1 (SUB1 A)) 1) (EQUAL (SUB1 (SUB1 A)) 2)))) (EQUAL (EQUAL (FIB A) 1) (OR (EQUAL A 1) (EQUAL A 2)))), which simplifies, applying EQUAL-SUB1-0, PLUS-ADD1-ARG1, ADD1-EQUAL, COMMUTATIVITY-OF-PLUS, PLUS-ZERO-ARG2, and PLUS-ADD1-ARG2, and expanding the functions ZEROP, OR, FIB, EQUAL, PLUS, NUMBERP, and SUB1, to the following six new conjectures: Case 1.6. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (NOT (EQUAL (SUB1 A) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0)) (NOT (EQUAL (SUB1 A) 2)) (NOT (EQUAL (FIB (SUB1 A)) 1)) (EQUAL (FIB (SUB1 (SUB1 A))) 1) (EQUAL (EQUAL (SUB1 (SUB1 A)) 2) T)) (NOT (EQUAL A 2))). However this again simplifies, using linear arithmetic, to: T. Case 1.5. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (NOT (EQUAL (SUB1 A) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0)) (NOT (EQUAL (SUB1 A) 2)) (NOT (EQUAL (FIB (SUB1 A)) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1)) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (NOT (EQUAL (SUB1 (SUB1 A)) 2)) (NOT (EQUAL A 2))) (NOT (EQUAL (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) 1))), which again simplifies, using linear arithmetic, to: T. Case 1.4. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (NOT (EQUAL (SUB1 A) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0)) (NOT (EQUAL (SUB1 A) 2)) (NOT (EQUAL (FIB (SUB1 A)) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1)) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (NOT (EQUAL (SUB1 (SUB1 A)) 2)) (EQUAL A 2)) (EQUAL (EQUAL (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) 1) T)), which again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (NOT (EQUAL (SUB1 A) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0)) (NOT (EQUAL (SUB1 A) 2)) (NOT (EQUAL (FIB (SUB1 A)) 1)) (EQUAL (FIB (SUB1 (SUB1 A))) 1) (EQUAL (SUB1 (SUB1 A)) 1)) (NOT (EQUAL A 2))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (SUB1 2) 0) (NOT (EQUAL 2 0)) (NUMBERP 2) (NOT (EQUAL 2 1)) (NOT (EQUAL (FIB (SUB1 2)) 0)) (NOT (EQUAL (SUB1 2) 1)) (NOT (EQUAL 1 0)) (NOT (EQUAL (SUB1 2) 2)) (NOT (EQUAL (FIB (SUB1 2)) 1)) (EQUAL (FIB 1) 1)) (NOT (EQUAL (SUB1 (SUB1 2)) 1))). However this again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (NOT (EQUAL (SUB1 A) 1)) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0)) (EQUAL (SUB1 A) 2) (EQUAL (EQUAL (FIB (SUB1 A)) 1) T) (EQUAL (FIB (SUB1 (SUB1 A))) 1)) (NOT (EQUAL A 2))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (EQUAL (FIB (SUB1 A)) 0)) (EQUAL (SUB1 A) 1) (EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0) T) (EQUAL (FIB (SUB1 A)) 1) (NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1))) (EQUAL A 2)), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] EQUAL-FIB-CONSTANT (PROVE-LEMMA FIB-SMALL (REWRITE) (IMPLIES (LESSP A 3) (EQUAL (FIB A) (IF (ZEROP A) 0 1)))) This formula simplifies, opening up ZEROP, to the following three new formulas: Case 3. (IMPLIES (AND (LESSP A 3) (NOT (NUMBERP A))) (EQUAL (FIB A) 0)). This again simplifies, opening up the functions NUMBERP, EQUAL, LESSP, and FIB, to: T. Case 2. (IMPLIES (AND (LESSP A 3) (EQUAL A 0)) (EQUAL (FIB A) 0)), which again simplifies, unfolding the functions LESSP, FIB, and EQUAL, to: T. Case 1. (IMPLIES (AND (LESSP A 3) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (FIB A) 1)), which again simplifies, applying EQUAL-FIB-CONSTANT, to: (IMPLIES (AND (LESSP A 3) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1))) (EQUAL A 2)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FIB-SMALL (DEFN DOUBLE-FIB-INDUCTION (A B) (IF (OR (LESSP A 3) (LESSP B 3)) T (AND (DOUBLE-FIB-INDUCTION (SUB1 A) (SUB1 B)) (DOUBLE-FIB-INDUCTION (SUB1 (SUB1 A)) (SUB1 (SUB1 B)))))) Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of OR establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each recursive call. Hence, DOUBLE-FIB-INDUCTION is accepted under the definitional principle. The definition of DOUBLE-FIB-INDUCTION can be justified in another way. Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of OR inform us that the measure (COUNT B) decreases according to the well-founded relation LESSP in each recursive call. From the definition we can conclude that (TRUEP (DOUBLE-FIB-INDUCTION A B)) is a theorem. [ 0.0 0.0 0.0 ] DOUBLE-FIB-INDUCTION (PROVE-LEMMA LESSP-FIB-FIB (REWRITE) (EQUAL (LESSP (FIB A) (FIB B)) (AND (LESSP A B) (NOT (AND (EQUAL A 1) (EQUAL B 2))))) ((INDUCT (DOUBLE-FIB-INDUCTION A B)))) This formula can be simplified, using the abbreviations NOT, OR, and AND, to the following two new formulas: Case 2. (IMPLIES (OR (LESSP A 3) (LESSP B 3)) (EQUAL (LESSP (FIB A) (FIB B)) (AND (LESSP A B) (NOT (AND (EQUAL A 1) (EQUAL B 2)))))). This simplifies, applying FIB-SMALL, and expanding the definitions of OR, AND, and NOT, to 24 new formulas: Case 2.24. (IMPLIES (AND (LESSP A 3) (EQUAL A 1) (EQUAL B 2) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP 1 (FIB B)) F)), which again simplifies, expanding the definitions of LESSP, EQUAL, NUMBERP, and FIB, to: T. Case 2.23. (IMPLIES (AND (LESSP A 3) (NOT (LESSP A B)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP 1 (FIB B)) F)), which again simplifies, using linear arithmetic and rewriting with FIB-SMALL and LESSP-1-HACK, to: T. Case 2.22. (IMPLIES (AND (LESSP A 3) (NOT (LESSP A B)) (NOT (NUMBERP A))) (EQUAL (LESSP 0 (FIB B)) F)). However this again simplifies, using linear arithmetic, rewriting with FIB-SMALL, and unfolding NUMBERP, EQUAL, LESSP, and FIB, to: T. Case 2.21. (IMPLIES (AND (LESSP A 3) (NOT (LESSP A B)) (EQUAL A 0)) (EQUAL (LESSP 0 (FIB B)) F)). However this again simplifies, using linear arithmetic, rewriting with the lemma FIB-SMALL, and unfolding the definitions of LESSP, EQUAL, and FIB, to: T. Case 2.20. (IMPLIES (AND (LESSP A 3) (EQUAL A 1) (EQUAL B 2) (NOT (NUMBERP A))) (EQUAL (LESSP 0 (FIB B)) F)), which again simplifies, trivially, to: T. Case 2.19. (IMPLIES (AND (LESSP A 3) (EQUAL A 1) (EQUAL B 2) (EQUAL A 0)) (EQUAL (LESSP 0 (FIB B)) F)). However this again simplifies, using linear arithmetic, to: T. Case 2.18. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP 1 (FIB B)) T)), which again simplifies, applying EQUAL-FIB-CONSTANT and LESSP-1-HACK, to the following three new goals: Case 2.18.3. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (EQUAL A 0)) (NUMBERP A)) (NOT (EQUAL B 0))). This again simplifies, using linear arithmetic, to: T. Case 2.18.2. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (EQUAL A 0)) (NUMBERP A)) (NUMBERP B)), which again simplifies, expanding the definition of LESSP, to: T. Case 2.18.1. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (EQUAL A 0)) (NUMBERP A)) (NOT (EQUAL B 1))), which again simplifies, using linear arithmetic, to: T. Case 2.17. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP 1 (FIB B)) T)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP 2 3) (LESSP 2 B) (NOT (EQUAL 2 1)) (NOT (EQUAL 2 0)) (NUMBERP 2)) (EQUAL (LESSP 1 (FIB B)) T)). This again simplifies, applying LESSP-1-HACK, EQUAL-SUB1-0, and EQUAL-FIB-CONSTANT, and unfolding LESSP, SUB1, NUMBERP, and EQUAL, to: (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (EQUAL (SUB1 B) 1))) (NOT (EQUAL B 2))), which again simplifies, using linear arithmetic, to: T. Case 2.16. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (NUMBERP A))) (EQUAL (LESSP 0 (FIB B)) T)), which again simplifies, appealing to the lemma EQUAL-FIB-CONSTANT, and unfolding the functions NUMBERP, EQUAL, and LESSP, to: T. Case 2.15. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL A 1)) (EQUAL A 0)) (EQUAL (LESSP 0 (FIB B)) T)), which again simplifies, applying EQUAL-FIB-CONSTANT, and expanding the definitions of LESSP and EQUAL, to: T. Case 2.14. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (NUMBERP A))) (EQUAL (LESSP 0 (FIB B)) T)). This again simplifies, applying EQUAL-FIB-CONSTANT, and expanding NUMBERP, EQUAL, and LESSP, to: T. Case 2.13. (IMPLIES (AND (LESSP A 3) (LESSP A B) (NOT (EQUAL B 2)) (EQUAL A 0)) (EQUAL (LESSP 0 (FIB B)) T)). But this again simplifies, applying EQUAL-FIB-CONSTANT, and unfolding the functions LESSP and EQUAL, to: T. Case 2.12. (IMPLIES (AND (LESSP B 3) (EQUAL A 1) (EQUAL B 2) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (FIB A) 1) F)). But this again simplifies, expanding LESSP, EQUAL, NUMBERP, and FIB, to: T. Case 2.11. (IMPLIES (AND (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (FIB A) 1) F)), which again simplifies, clearly, to: (IMPLIES (AND (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which we will name *1. Case 2.10. (IMPLIES (AND (LESSP B 3) (NOT (LESSP A B)) (NOT (NUMBERP B))) (EQUAL (LESSP (FIB A) 0) F)). But this again simplifies, expanding NUMBERP, EQUAL, and LESSP, to: T. Case 2.9. (IMPLIES (AND (LESSP B 3) (NOT (LESSP A B)) (EQUAL B 0)) (EQUAL (LESSP (FIB A) 0) F)), which again simplifies, expanding LESSP and EQUAL, to: T. Case 2.8. (IMPLIES (AND (LESSP B 3) (EQUAL A 1) (EQUAL B 2) (NOT (NUMBERP B))) (EQUAL (LESSP (FIB A) 0) F)), which again simplifies, obviously, to: T. Case 2.7. (IMPLIES (AND (LESSP B 3) (EQUAL A 1) (EQUAL B 2) (EQUAL B 0)) (EQUAL (LESSP (FIB A) 0) F)). But this again simplifies, using linear arithmetic, to: T. Case 2.6. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (FIB A) 1) T)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP 1 3) (LESSP A 1) (NOT (EQUAL 1 2)) (NOT (EQUAL 1 0)) (NUMBERP 1)) (EQUAL (LESSP (FIB A) 1) T)). However this again simplifies, using linear arithmetic, rewriting with the lemma FIB-SMALL, and expanding the definitions of LESSP, EQUAL, and NUMBERP, to three new conjectures: Case 2.6.3. (IMPLIES (AND (LESSP A 1) (NOT (EQUAL A 0)) (NUMBERP A)) (LESSP 1 1)), which again simplifies, using linear arithmetic, to: T. Case 2.6.2. (IMPLIES (AND (LESSP A 1) (EQUAL A 0)) (LESSP 0 1)), which again simplifies, trivially, to: T. Case 2.6.1. (IMPLIES (AND (LESSP A 1) (NOT (NUMBERP A))) (LESSP 0 1)). This again simplifies, using linear arithmetic, to: T. Case 2.5. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (FIB A) 1) T)), which again simplifies, using linear arithmetic and rewriting with FIB-SMALL, to the following three new formulas: Case 2.5.3. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (NUMBERP A))) (EQUAL (LESSP (FIB A) 1) T)). But this again simplifies, using linear arithmetic, rewriting with FIB-SMALL, and expanding the definitions of LESSP and EQUAL, to: T. Case 2.5.2. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NUMBERP A) (NOT (EQUAL A 0))) (LESSP 1 1)). This again simplifies, using linear arithmetic, to: T. Case 2.5.1. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NUMBERP A) (EQUAL A 0)) (LESSP 0 1)), which again simplifies, using linear arithmetic, to: T. Case 2.4. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (NOT (NUMBERP B))) (EQUAL (LESSP (FIB A) 0) T)), which again simplifies, unfolding the functions NUMBERP, EQUAL, and LESSP, to: T. Case 2.3. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL A 1)) (EQUAL B 0)) (EQUAL (LESSP (FIB A) 0) T)), which again simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL B 2)) (NOT (NUMBERP B))) (EQUAL (LESSP (FIB A) 0) T)), which again simplifies, unfolding the functions NUMBERP, EQUAL, and LESSP, to: T. Case 2.1. (IMPLIES (AND (LESSP B 3) (LESSP A B) (NOT (EQUAL B 2)) (EQUAL B 0)) (EQUAL (LESSP (FIB A) 0) T)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (LESSP A 3)) (NOT (LESSP B 3)) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) (AND (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (AND (EQUAL (SUB1 (SUB1 A)) 1) (EQUAL (SUB1 (SUB1 B)) 2))))) (EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))) (AND (LESSP (SUB1 A) (SUB1 B)) (NOT (AND (EQUAL (SUB1 A) 1) (EQUAL (SUB1 B) 2)))))) (EQUAL (LESSP (FIB A) (FIB B)) (AND (LESSP A B) (NOT (AND (EQUAL A 1) (EQUAL B 2)))))), which simplifies, applying EQUAL-SUB1-0, FIB-SMALL, LESSP-1-HACK, PLUS-ADD1-ARG1, and COMMUTATIVITY-OF-PLUS, and expanding the definitions of SUB1, NUMBERP, EQUAL, LESSP, AND, NOT, PLUS, FIB, and ADD1, to the following five new formulas: Case 1.5. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (NOT (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B)))) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) F) (NOT (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))) (NOT (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B))))))). This again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (NOT (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B)))) (NOT (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B))))) (NOT (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))) (NOT (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B))))))), which again simplifies, using linear arithmetic, to: T. Case 1.4. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 B)) 2)) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) T) (NOT (EQUAL (SUB1 A) 1)) (EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))) T)) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 B)) 2)) (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) (NOT (EQUAL (SUB1 A) 1)) (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 B)) 2)) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) T) (NOT (EQUAL (SUB1 B) 2)) (EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))) T)) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 B)) 2)) (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) (NOT (EQUAL (SUB1 B) 2)) (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) T) (NOT (EQUAL (SUB1 A) 1)) (EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))) T)) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) (NOT (EQUAL (SUB1 A) 1)) (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (EQUAL (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) T) (NOT (EQUAL (SUB1 B) 2)) (EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B))) T)) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (SUB1 (SUB1 A)) 1)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (NOT (LESSP (SUB1 (SUB1 B)) 1)) (LESSP (SUB1 (SUB1 A)) (SUB1 (SUB1 B))) (NOT (EQUAL (SUB1 (SUB1 A)) 1)) (LESSP (FIB (SUB1 (SUB1 A))) (FIB (SUB1 (SUB1 B)))) (NOT (EQUAL (SUB1 B) 2)) (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))) (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) (PLUS (FIB (SUB1 B)) (FIB (SUB1 (SUB1 B)))))), which again simplifies, using linear arithmetic, to: T. So next consider: (IMPLIES (AND (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which we named *1 above. We will try to prove it by induction. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP A) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (p (SUB1 (SUB1 A)) B) (p (SUB1 A) (SUB1 B))) (p A B))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instances chosen for B. The above induction scheme produces the following ten new conjectures: Case 10.(IMPLIES (AND (ZEROP A) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))). This simplifies, expanding the definitions of ZEROP, EQUAL, and LESSP, to: T. Case 9. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))). This simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (ZEROP 1)) (LESSP 1 3) (NOT (LESSP 1 1)) (NOT (EQUAL 1 0)) (NUMBERP 1)) (NOT (LESSP (FIB 1) 1))), which again simplifies, opening up ZEROP, LESSP, EQUAL, NUMBERP, and FIB, to: T. Case 8. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (NOT (LESSP (SUB1 B) 3)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (NOT (LESSP (SUB1 B) 3)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (LESSP (SUB1 A) (SUB1 B)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (LESSP (SUB1 A) (SUB1 B)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (EQUAL (SUB1 B) 0) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, using linear arithmetic, to two new formulas: Case 4.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (ZEROP A)) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (EQUAL (SUB1 B) 0) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which again simplifies, unfolding the function ZEROP, to: T. Case 4.1. (IMPLIES (AND (NUMBERP A) (NOT (ZEROP 2)) (NOT (EQUAL 2 1)) (LESSP (SUB1 (SUB1 2)) B) (EQUAL (SUB1 B) 0) (LESSP B 3) (NOT (LESSP 2 B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB 2) 1))), which again simplifies, applying EQUAL-SUB1-0, and expanding ZEROP, EQUAL, SUB1, LESSP, NUMBERP, and FIB, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (EQUAL (SUB1 B) 0) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))). This simplifies, appealing to the lemmas EQUAL-SUB1-0 and COMMUTATIVITY-OF-PLUS, and unfolding the definitions of ZEROP, SUB1, NUMBERP, EQUAL, LESSP, and FIB, to the new goal: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (EQUAL B 1) (LESSP B 3)) (NOT (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) 1))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (NOT (LESSP (FIB (SUB1 A)) 1)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding the definitions of ZEROP, LESSP, and FIB, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (LESSP (SUB1 (SUB1 A)) B) (NOT (LESSP (FIB (SUB1 A)) 1)) (LESSP B 3) (NOT (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) 1))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (NOT (LESSP (FIB (SUB1 A)) 1)) (LESSP B 3) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (FIB A) 1))), which simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and unfolding the functions ZEROP, LESSP, and FIB, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1)) (NOT (LESSP (FIB (SUB1 (SUB1 A))) 1)) (NOT (LESSP (FIB (SUB1 A)) 1)) (LESSP B 3) (NOT (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (PLUS (FIB (SUB1 A)) (FIB (SUB1 (SUB1 A)))) 1))). This again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 1.4 0.1 ] LESSP-FIB-FIB (PROVE-LEMMA REMAINDER-FIB-FIB-0 (REWRITE) (EQUAL (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (OR (EQUAL (REMAINDER A B) 0) (EQUAL B 2))) ((USE (EQUAL-REMAINDER-GCD-0-PROOF (A (FIB B)) (B (FIB A)))) (DISABLE EQUAL-REMAINDER-GCD-0 GCD-REMAINDER))) This formula can be simplified, using the abbreviation GCD-FIB, to the new conjecture: (IMPLIES (EQUAL (EQUAL (REMAINDER (FIB (GCD B A)) (FIB B)) 0) (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (EQUAL (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (OR (EQUAL (REMAINDER A B) 0) (EQUAL B 2)))), which simplifies, rewriting with COMMUTATIVITY-OF-GCD, and opening up OR and EQUAL, to the following three new conjectures: Case 3. (IMPLIES (AND (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0))) (NOT (EQUAL (REMAINDER A B) 0))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by (PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. This generates four new formulas: Case 3.4. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0))) (NOT (EQUAL (REMAINDER A B) 0))), which further simplifies, using linear arithmetic, rewriting with the lemmas FIB-SMALL and EQUAL-FIB-CONSTANT, and expanding the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 3.3. (IMPLIES (AND (EQUAL B 0) (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0))) (NOT (EQUAL (REMAINDER A B) 0))), which further simplifies, rewriting with the lemmas REMAINDER-ZERO, EQUAL-FIB-CONSTANT, and GCD-0, and expanding the functions FIB and ZEROP, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0))) (NOT (EQUAL (REMAINDER A B) 0))), which further simplifies, using linear arithmetic, applying FIB-SMALL, REMAINDER-ZERO, and EQUAL-FIB-CONSTANT, and expanding ZEROP and GCD, to: T. Case 3.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (EQUAL (REMAINDER (FIB (PLUS X (TIMES B Z))) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD (PLUS X (TIMES B Z)) B)) (FIB B)) 0))) (NOT (EQUAL X 0))). However this further simplifies, applying GCD-TIMES, COMMUTATIVITY-OF-GCD, and REMAINDER-X-X, and opening up the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0)) (NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0))) (NOT (EQUAL B 2))). But this again simplifies, rewriting with the lemma REMAINDER-1-ARG2, and expanding the definitions of FIB and EQUAL, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (EQUAL (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0) T) (NOT (EQUAL (REMAINDER A B) 0))) (EQUAL B 2)), which again simplifies, obviously, to: (IMPLIES (AND (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0) (NOT (EQUAL (REMAINDER A B) 0))) (EQUAL B 2)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following four new conjectures: Case 1.4. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0) (NOT (EQUAL (REMAINDER A B) 0))) (EQUAL B 2)). But this further simplifies, using linear arithmetic, rewriting with FIB-SMALL, EQUAL-FIB-CONSTANT, REMAINDER-ZERO, and REMAINDER-OF-NON-NUMBER, and unfolding the definitions of LESSP, EQUAL, NUMBERP, REMAINDER, GCD, and ZEROP, to: T. Case 1.3. (IMPLIES (AND (EQUAL B 0) (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0) (NOT (EQUAL (REMAINDER A B) 0))) (EQUAL B 2)). But this further simplifies, rewriting with REMAINDER-ZERO, EQUAL-FIB-CONSTANT, and GCD-0, and opening up FIB, ZEROP, GCD, REMAINDER, and EQUAL, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP B)) (EQUAL (REMAINDER (FIB A) (FIB B)) 0) (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B)) 0) (NOT (EQUAL (REMAINDER A B) 0))) (EQUAL B 2)). This further simplifies, using linear arithmetic, rewriting with FIB-SMALL, REMAINDER-ZERO, EQUAL-FIB-CONSTANT, and GCD-0, and unfolding the definitions of ZEROP, FIB, REMAINDER, EQUAL, NUMBERP, and GCD, to: T. Case 1.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (EQUAL (REMAINDER (FIB (PLUS X (TIMES B Z))) (FIB B)) 0) (EQUAL (REMAINDER (FIB (GCD (PLUS X (TIMES B Z)) B)) (FIB B)) 0) (NOT (EQUAL X 0))) (EQUAL B 2)). This further simplifies, applying COMMUTATIVITY-OF-TIMES, FIB-PLUS, REMAINDER-TIMES1-INSTANCE, GCD-PLUS, LESSP-FIB-FIB, LESSP-GCD3, REMAINDER-NOOP, EQUAL-GCD-0, and EQUAL-FIB-CONSTANT, and expanding ZEROP, NOT, and EQUAL, to: T. Q.E.D. [ 0.0 0.9 0.0 ] REMAINDER-FIB-FIB-0 (PROVE-LEMMA FIB-TIMES-OPEN (REWRITE) (IMPLIES (LESSP 0 K) (EQUAL (FIB (TIMES K N)) (PLUS (TIMES (FIB N) (FIB (ADD1 (TIMES (SUB1 K) N)))) (TIMES (FIB (SUB1 N)) (FIB (TIMES (SUB1 K) N)))))) ((USE (FIB-PLUS (J (TIMES (SUB1 K) N)) (K N))) (DISABLE FIB-PLUS))) This simplifies, using linear arithmetic, applying COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, TIMES-ZERO, FIB-SMALL, SUB1-NNUMBERP, COMMUTATIVITY2-OF-PLUS, PLUS-ZERO-ARG2, ADD1-SUB1, and TIMES-1-ARG1, and unfolding the definitions of TIMES, ZEROP, EQUAL, LESSP, FIB, ADD1, PLUS, and SUB1, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N))) 0)) (EQUAL (FIB (PLUS N (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))) (PLUS (TIMES (FIB N) (FIB (SUB1 (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))))) (TIMES (FIB (ADD1 N)) (FIB (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N))))))) (NOT (EQUAL K 0)) (NUMBERP K)) (EQUAL (FIB (ADD1 (PLUS (SUB1 K) (SUB1 N) (TIMES (SUB1 K) (SUB1 N))))) (PLUS (TIMES (FIB N) (FIB (ADD1 (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))))) (TIMES (FIB (SUB1 N)) (FIB (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))))))), which again simplifies, rewriting with EQUAL-SUB1-0, EQUAL-TIMES-0, EQUAL-PLUS-0, COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, TIMES-DISTRIBUTES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and expanding the functions EQUAL, NUMBERP, and FIB, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL K 1)) (EQUAL (FIB (PLUS N (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))) (PLUS (TIMES (FIB N) (FIB (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N))))) (TIMES (FIB N) (FIB (SUB1 (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))))) (TIMES (FIB (SUB1 N)) (FIB (PLUS (SUB1 K) (TIMES (SUB1 K) (SUB1 N))))))) (NOT (EQUAL K 0)) (NUMBERP K)) (EQUAL (FIB (ADD1 (PLUS (SUB1 K) (SUB1 N) (TIMES (SUB1 K) (SUB1 N))))) (FIB (PLUS N (SUB1 K) (TIMES (SUB1 K) (SUB1 N)))))). Applying the lemma SUB1-ELIM, replace K by (ADD1 X) to eliminate (SUB1 K). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL (ADD1 X) 1)) (EQUAL (FIB (PLUS N X (TIMES X (SUB1 N)))) (PLUS (TIMES (FIB N) (FIB (PLUS X (TIMES X (SUB1 N))))) (TIMES (FIB N) (FIB (SUB1 (PLUS X (TIMES X (SUB1 N)))))) (TIMES (FIB (SUB1 N)) (FIB (PLUS X (TIMES X (SUB1 N))))))) (NOT (EQUAL (ADD1 X) 0))) (EQUAL (FIB (ADD1 (PLUS X (SUB1 N) (TIMES X (SUB1 N))))) (FIB (PLUS N X (TIMES X (SUB1 N)))))), which further simplifies, rewriting with ADD1-EQUAL, and expanding NUMBERP, to: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL X 0)) (EQUAL (FIB (PLUS N X (TIMES X (SUB1 N)))) (PLUS (TIMES (FIB N) (FIB (PLUS X (TIMES X (SUB1 N))))) (TIMES (FIB N) (FIB (SUB1 (PLUS X (TIMES X (SUB1 N)))))) (TIMES (FIB (SUB1 N)) (FIB (PLUS X (TIMES X (SUB1 N)))))))) (EQUAL (FIB (ADD1 (PLUS X (SUB1 N) (TIMES X (SUB1 N))))) (FIB (PLUS N X (TIMES X (SUB1 N)))))). Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL X 0)) (EQUAL (FIB (PLUS (ADD1 Z) X (TIMES X Z))) (PLUS (TIMES (FIB (ADD1 Z)) (FIB (PLUS X (TIMES X Z)))) (TIMES (FIB (ADD1 Z)) (FIB (SUB1 (PLUS X (TIMES X Z))))) (TIMES (FIB Z) (FIB (PLUS X (TIMES X Z))))))) (EQUAL (FIB (ADD1 (PLUS X Z (TIMES X Z)))) (FIB (PLUS (ADD1 Z) X (TIMES X Z))))), which finally simplifies, applying COMMUTATIVITY2-OF-PLUS, PLUS-ADD1-ARG1, and COMMUTATIVITY-OF-PLUS, to: T. Q.E.D. [ 0.0 1.6 0.0 ] FIB-TIMES-OPEN (DISABLE FIB-TIMES-OPEN) [ 0.0 0.0 0.0 ] FIB-TIMES-OPEN-OFF (PROVE-LEMMA FIB-ADD1-TIMES-OPEN (REWRITE) (IMPLIES (LESSP 0 K) (EQUAL (FIB (ADD1 (TIMES K N))) (PLUS (TIMES (FIB (ADD1 (TIMES (SUB1 K) N))) (FIB (ADD1 N))) (TIMES (FIB (TIMES (SUB1 K) N)) (FIB N))))) ((USE (FIB-PLUS (J (ADD1 (TIMES (SUB1 K) N))) (K N))) (DISABLE FIB-PLUS))) This conjecture can be simplified, using the abbreviations IMPLIES and PLUS-ADD1-ARG1, to the conjecture: (IMPLIES (AND (EQUAL (FIB (ADD1 (PLUS (TIMES (SUB1 K) N) N))) (IF (ZEROP (ADD1 (TIMES (SUB1 K) N))) (FIB N) (PLUS (TIMES (FIB (ADD1 N)) (FIB (ADD1 (TIMES (SUB1 K) N)))) (TIMES (FIB (SUB1 (ADD1 (TIMES (SUB1 K) N)))) (FIB N))))) (LESSP 0 K)) (EQUAL (FIB (ADD1 (TIMES K N))) (PLUS (TIMES (FIB (ADD1 (TIMES (SUB1 K) N))) (FIB (ADD1 N))) (TIMES (FIB (TIMES (SUB1 K) N)) (FIB N))))). This simplifies, applying COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, and SUB1-ADD1, and unfolding the functions ZEROP, EQUAL, LESSP, and TIMES, to: T. Q.E.D. [ 0.0 0.2 0.0 ] FIB-ADD1-TIMES-OPEN (DISABLE FIB-ADD1-TIMES-OPEN) [ 0.0 0.0 0.0 ] FIB-ADD1-TIMES-OPEN-OFF (PROVE-LEMMA FIB-TIMES-SPECIAL-STEP (REWRITE) (IMPLIES (LESSP 1 K) (EQUAL (REMAINDER (TIMES K (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB (SUB1 N)) (TIMES (SUB1 K) (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))))) (TIMES (FIB N) (FIB N))))) ((DISABLE-THEORY GCDS) (DISABLE GCD-REMAINDER-TIMES-FACT1-PROOF2 DIFFERENCE-LEQ-ARG1 GCD-REMAINDER-TIMES-FACT1-PROOF EQUAL-REMAINDER-PLUS-0 REMAINDER-NOOP LESSP-1-HACK))) WARNING: the previously added lemma, REMAINDER-TIMES-TIMES-HACK, could be applied whenever the newly proposed FIB-TIMES-SPECIAL-STEP could! This formula can be simplified, using the abbreviations IMPLIES, REMAINDER-PLUS-TIMES-HACK, and REMAINDER-TIMES-TIMES-HACK, to: (IMPLIES (LESSP 1 K) (EQUAL (TIMES (FIB N) (REMAINDER (TIMES K (EXP (FIB (ADD1 N)) (SUB1 K))) (FIB N))) (TIMES (FIB N) (REMAINDER (PLUS (EXP (FIB (ADD1 N)) (SUB1 K)) (TIMES (FIB (SUB1 N)) (SUB1 K) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))) (FIB N))))), which simplifies, rewriting with EQUAL-SUB1-0, CORRECTNESS-OF-CANCEL-EQUAL-TIMES, and EQUAL-FIB-CONSTANT, and unfolding EXP, TIMES, ZEROP, FIX, and OR, to the following four new formulas: Case 4. (IMPLIES (AND (LESSP 1 K) (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL K 1)) (EQUAL (REMAINDER (TIMES K 1) (FIB N)) (REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0)) (FIB N)))). However this again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (LESSP 1 K) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NUMBERP K))) (EQUAL (REMAINDER (TIMES K 1) (FIB N)) (REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0)) (FIB N)))), which again simplifies, unfolding the definition of LESSP, to: T. Case 2. (IMPLIES (AND (LESSP 1 K) (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL K 0)) (EQUAL (REMAINDER (TIMES K 1) (FIB N)) (REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0)) (FIB N)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP 1 K) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL K 1))) (EQUAL (REMAINDER (TIMES K (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))) (FIB N)) (REMAINDER (PLUS (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))) (TIMES (FIB (SUB1 N)) (PLUS (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))) (TIMES (SUB1 (SUB1 K)) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))))) (FIB N)))), which again simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES1, REMAINDER-TIMES1-INSTANCE, REMAINDER-PLUS, and ASSOCIATIVITY-OF-PLUS, and opening up the functions NUMBERP, FIB, and EQUAL, to: (IMPLIES (AND (LESSP 1 K) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL K 1))) (EQUAL (REMAINDER (TIMES K (FIB (SUB1 N)) (EXP (PLUS (FIB N) (FIB (SUB1 N))) (SUB1 (SUB1 K)))) (FIB N)) (REMAINDER (PLUS (TIMES (FIB (SUB1 N)) (EXP (PLUS (FIB N) (FIB (SUB1 N))) (SUB1 (SUB1 K)))) (TIMES (FIB (SUB1 N)) (EXP (PLUS (FIB N) (FIB (SUB1 N))) (SUB1 (SUB1 K)))) (TIMES (FIB (SUB1 N)) (SUB1 (SUB1 K)) (EXP (PLUS (FIB N) (FIB (SUB1 N))) (SUB1 (SUB1 K))))) (FIB N)))). Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 X) to eliminate (SUB1 N). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove: (IMPLIES (AND (NUMBERP X) (LESSP 1 K) (NOT (EQUAL (ADD1 X) 0)) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL K 1))) (EQUAL (REMAINDER (TIMES K (FIB X) (EXP (PLUS (FIB (ADD1 X)) (FIB X)) (SUB1 (SUB1 K)))) (FIB (ADD1 X))) (REMAINDER (PLUS (TIMES (FIB X) (EXP (PLUS (FIB (ADD1 X)) (FIB X)) (SUB1 (SUB1 K)))) (TIMES (FIB X) (EXP (PLUS (FIB (ADD1 X)) (FIB X)) (SUB1 (SUB1 K)))) (TIMES (FIB X) (SUB1 (SUB1 K)) (EXP (PLUS (FIB (ADD1 X)) (FIB X)) (SUB1 (SUB1 K))))) (FIB (ADD1 X))))). However this further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, to: (IMPLIES (AND (NUMBERP X) (LESSP 1 K) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL K 1))) (EQUAL (REMAINDER (TIMES K (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 (SUB1 K)))) (FIB (ADD1 X))) (REMAINDER (PLUS (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 (SUB1 K)))) (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 (SUB1 K)))) (TIMES (FIB X) (SUB1 (SUB1 K)) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 (SUB1 K))))) (FIB (ADD1 X))))). Applying the lemma SUB1-ELIM, replace K by (ADD1 Z) to eliminate (SUB1 K) and Z by (ADD1 V) to eliminate (SUB1 Z). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces the following two new goals: Case 1.2. (IMPLIES (AND (EQUAL Z 0) (NUMBERP Z) (NUMBERP X) (LESSP 1 (ADD1 Z)) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL (ADD1 Z) 1))) (EQUAL (REMAINDER (TIMES (ADD1 Z) (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 Z))) (FIB (ADD1 X))) (REMAINDER (PLUS (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 Z))) (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 Z))) (TIMES (FIB X) (SUB1 Z) (EXP (PLUS (FIB X) (FIB (ADD1 X))) (SUB1 Z)))) (FIB (ADD1 X))))). This finally simplifies, trivially, to: T. Case 1.1. (IMPLIES (AND (NUMBERP V) (NOT (EQUAL (ADD1 V) 0)) (NUMBERP X) (LESSP 1 (ADD1 (ADD1 V))) (NOT (EQUAL (ADD1 (ADD1 V)) 0)) (NOT (EQUAL (ADD1 (ADD1 V)) 1))) (EQUAL (REMAINDER (TIMES (ADD1 (ADD1 V)) (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) V)) (FIB (ADD1 X))) (REMAINDER (PLUS (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) V)) (TIMES (FIB X) (EXP (PLUS (FIB X) (FIB (ADD1 X))) V)) (TIMES (FIB X) V (EXP (PLUS (FIB X) (FIB (ADD1 X))) V))) (FIB (ADD1 X))))). However this finally simplifies, rewriting with SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY2-OF-TIMES, and TIMES-DISTRIBUTES-OVER-PLUS, and expanding SUB1, NUMBERP, EQUAL, LESSP, and TIMES, to: T. Q.E.D. [ 0.0 3.4 0.0 ] FIB-TIMES-SPECIAL-STEP (PROVE-LEMMA FIB-REMAINDER-HACK (REWRITE) (EQUAL (REMAINDER (FIB (TIMES X Y)) (FIB X)) 0)) This formula can be simplified, using the abbreviations REMAINDER-TIMES1-INSTANCE and REMAINDER-FIB-FIB-0, to: (IMPLIES (NOT (EQUAL 0 0)) (EQUAL X 2)), which simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FIB-REMAINDER-HACK (PROVE-LEMMA REMAINDER-BACKCHAIN-PROOF1 NIL (IMPLIES (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER (TIMES A D) C) (REMAINDER (TIMES B D) C)))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z)) to eliminate (REMAINDER A C) and (QUOTIENT A C). We use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following four new formulas: Case 4. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER A C) (REMAINDER B C))) (EQUAL (REMAINDER (TIMES A D) C) (REMAINDER (TIMES B D) C))). This simplifies, applying REMAINDER-OF-NON-NUMBER and REMAINDER-TIMES1, and expanding the functions LESSP, EQUAL, NUMBERP, REMAINDER, and TIMES, to: T. Case 3. (IMPLIES (AND (EQUAL C 0) (EQUAL (REMAINDER A C) (REMAINDER B C))) (EQUAL (REMAINDER (TIMES A D) C) (REMAINDER (TIMES B D) C))). However this simplifies, rewriting with REMAINDER-ZERO, and unfolding ZEROP, TIMES, REMAINDER, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP C)) (EQUAL (REMAINDER A C) (REMAINDER B C))) (EQUAL (REMAINDER (TIMES A D) C) (REMAINDER (TIMES B D) C))). But this simplifies, applying the lemma REMAINDER-ZERO, and opening up ZEROP, TIMES, NUMBERP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL X (REMAINDER B C))) (EQUAL (REMAINDER (TIMES (PLUS X (TIMES C Z)) D) C) (REMAINDER (TIMES B D) C))), which simplifies, rewriting with LESSP-REMAINDER, COMMUTATIVITY-OF-TIMES, ASSOCIATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and opening up the definitions of ZEROP, NOT, and EQUAL, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (TIMES D (REMAINDER B C)) C) (REMAINDER (TIMES B D) C))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by (PLUS X (TIMES C V)) to eliminate (REMAINDER B C) and (QUOTIENT B C). We employ LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following two new formulas: Case 1.2. (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (TIMES D (REMAINDER B C)) C) (REMAINDER (TIMES B D) C))). However this further simplifies, using linear arithmetic, applying REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, and COMMUTATIVITY-OF-TIMES, and opening up the definitions of NUMBERP, EQUAL, and TIMES, to: T. Case 1.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (TIMES D X) C) (REMAINDER (TIMES (PLUS X (TIMES C V)) D) C))). But this further simplifies, applying COMMUTATIVITY-OF-TIMES, ASSOCIATIVITY-OF-TIMES, TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding the functions ZEROP, NOT, and EQUAL, to: T. Q.E.D. [ 0.0 0.4 0.0 ] REMAINDER-BACKCHAIN-PROOF1 (PROVE-LEMMA REMAINDER-BACKCHAIN-PROOF2 NIL (IMPLIES (AND (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS A D) C) (REMAINDER (PLUS B E) C)))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z)) to eliminate (REMAINDER A C) and (QUOTIENT A C). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We would thus like to prove the following four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS A D) C) (REMAINDER (PLUS B E) C))). However this simplifies, applying REMAINDER-OF-NON-NUMBER and REMAINDER-PLUS, and unfolding the functions LESSP, EQUAL, NUMBERP, REMAINDER, and PLUS, to: (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL 0 (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C)) (NOT (NUMBERP D))) (EQUAL (REMAINDER 0 C) (REMAINDER D C))), which again simplifies, applying the lemma REMAINDER-OF-NON-NUMBER, and opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 3. (IMPLIES (AND (EQUAL C 0) (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS A D) C) (REMAINDER (PLUS B E) C))), which simplifies, applying REMAINDER-ZERO and PLUS-ZERO-ARG2, and unfolding ZEROP, PLUS, EQUAL, REMAINDER, and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP C)) (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS A D) C) (REMAINDER (PLUS B E) C))). But this simplifies, appealing to the lemmas REMAINDER-ZERO and PLUS-ZERO-ARG2, and unfolding the functions ZEROP, PLUS, EQUAL, and NUMBERP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL X (REMAINDER B C)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS (PLUS X (TIMES C Z)) D) C) (REMAINDER (PLUS B E) C))), which simplifies, rewriting with the lemmas LESSP-REMAINDER, COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and expanding the functions ZEROP, NOT, and EQUAL, to the goal: (IMPLIES (AND (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS D (REMAINDER B C)) C) (REMAINDER (PLUS B E) C))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace D by (PLUS X (TIMES C V)) to eliminate (REMAINDER D C) and (QUOTIENT D C). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove two new conjectures: Case 1.2. (IMPLIES (AND (NOT (NUMBERP D)) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL (REMAINDER D C) (REMAINDER E C))) (EQUAL (REMAINDER (PLUS D (REMAINDER B C)) C) (REMAINDER (PLUS B E) C))), which further simplifies, using linear arithmetic, applying REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, REMAINDER-X-X, REMAINDER-REMAINDER, and REMAINDER-PLUS, and expanding NUMBERP, PLUS, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL X (REMAINDER E C))) (EQUAL (REMAINDER (PLUS (PLUS X (TIMES C V)) (REMAINDER B C)) C) (REMAINDER (PLUS B E) C))). However this further simplifies, applying LESSP-REMAINDER, COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding ZEROP, NOT, and EQUAL, to: (IMPLIES (AND (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS (REMAINDER B C) (REMAINDER E C)) C) (REMAINDER (PLUS B E) C))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by (PLUS X (TIMES C W)) to eliminate (REMAINDER B C) and (QUOTIENT B C). We use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following two new formulas: Case 1.1.2. (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS (REMAINDER B C) (REMAINDER E C)) C) (REMAINDER (PLUS B E) C))). This further simplifies, using linear arithmetic, rewriting with REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, REMAINDER-X-X, and REMAINDER-REMAINDER, and expanding the functions NUMBERP, EQUAL, and PLUS, to the new conjecture: (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0)) (NOT (NUMBERP E))) (EQUAL (REMAINDER E C) (REMAINDER 0 C))), which finally simplifies, using linear arithmetic, applying REMAINDER-NOOP and REMAINDER-OF-NON-NUMBER, and unfolding NUMBERP and EQUAL, to: T. Case 1.1.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP W) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C) (REMAINDER (PLUS (PLUS X (TIMES C W)) E) C))). This further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and opening up the functions ZEROP, NOT, and EQUAL, to the goal: (IMPLIES (AND (NUMBERP X) (LESSP X C) (NUMBERP W) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C) (REMAINDER (PLUS E X) C))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace E by (PLUS X1 (TIMES C Z1)) to eliminate (REMAINDER E C) and (QUOTIENT E C). We employ LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove two new goals: Case 1.1.1.2. (IMPLIES (AND (NOT (NUMBERP E)) (NUMBERP X) (LESSP X C) (NUMBERP W) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C) (REMAINDER (PLUS E X) C))), which finally simplifies, using linear arithmetic, applying REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, and PLUS-ZERO-ARG2, and expanding the definitions of NUMBERP, ZEROP, and PLUS, to: T. Case 1.1.1.1. (IMPLIES (AND (NUMBERP X1) (EQUAL (LESSP X1 C) (NOT (ZEROP C))) (NUMBERP Z1) (NUMBERP X) (LESSP X C) (NUMBERP W) (NUMBERP V) (NUMBERP Z) (NUMBERP C) (NOT (EQUAL C 0))) (EQUAL (REMAINDER (PLUS X X1) C) (REMAINDER (PLUS (PLUS X1 (TIMES C Z1)) X) C))). But this finally simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding the definitions of ZEROP, NOT, and EQUAL, to: T. Q.E.D. [ 0.0 0.7 0.0 ] REMAINDER-BACKCHAIN-PROOF2 (PROVE-LEMMA REMAINDER-FIB-BACKCHAIN (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER (FIB X) C) (REMAINDER (EXP P Q) C)) (EQUAL (REMAINDER (FIB Y) C) (REMAINDER (TIMES R S) C))) (EQUAL (REMAINDER (PLUS (TIMES A (FIB X)) (TIMES B (FIB Y))) C) (REMAINDER (PLUS (TIMES A (EXP P Q)) (TIMES B (TIMES R S))) C))) ((USE (REMAINDER-BACKCHAIN-PROOF2 (A (TIMES A (FIB X))) (B (TIMES A (EXP P Q))) (D (TIMES B (FIB Y))) (E (TIMES B (TIMES R S))) (C C)) (REMAINDER-BACKCHAIN-PROOF1 (A (FIB Y)) (B (TIMES R S)) (C C) (D B)) (REMAINDER-BACKCHAIN-PROOF1 (A (FIB X)) (B (EXP P Q)) (C C) (D A))) (DISABLE-THEORY NATURALS) (ENABLE COMMUTATIVITY-OF-TIMES))) WARNING: Note that REMAINDER-FIB-BACKCHAIN contains the free variables S, R, Q, and P which will be chosen by instantiating the hypotheses: (EQUAL (REMAINDER (FIB X) C) (REMAINDER (EXP P Q) C)) and (EQUAL (REMAINDER (FIB Y) C) (REMAINDER (TIMES R S) C)). This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and unfolding the functions AND and IMPLIES, to: T. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-FIB-BACKCHAIN (PROVE-LEMMA FIB-TIMES-SPECIAL NIL (IMPLIES (LESSP 1 K) (AND (EQUAL (REMAINDER (FIB (TIMES K N)) (EXP (FIB N) 2)) (REMAINDER (TIMES K (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K)))) (EXP (FIB N) 2))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES K N))) (EXP (FIB N) 2)) (REMAINDER (EXP (FIB (ADD1 N)) K) (EXP (FIB N) 2))))) ((INDUCT (TIMES K N)) (DISABLE TIMES EQUAL-SUB1-0 REMAINDER-TIMES2-INSTANCE DIFFERENCE-LEQ-ARG1 GCD-REMAINDER-TIMES-FACT1-PROOF2 LESSP-FIB-FIB REMAINDER-NOOP LESSP-1-HACK REMAINDER-TIMES-TIMES-HACK EXP REMAINDER-PLUS-TIMES-HACK REMAINDER-TIMES2 COMMUTATIVITY2-OF-TIMES COMMUTATIVITY-OF-PLUS) (ENABLE FIB-ADD1-TIMES-OPEN FIB-TIMES-OPEN REMAINDER-TIMES-TIMES) (DISABLE-THEORY GCDS))) This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to the following two new formulas: Case 2. (IMPLIES (AND (ZEROP K) (LESSP 1 K)) (AND (EQUAL (REMAINDER (FIB (TIMES K N)) (EXP (FIB N) 2)) (REMAINDER (TIMES K (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (EXP (FIB N) 2))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES K N))) (EXP (FIB N) 2)) (REMAINDER (EXP (FIB (ADD1 N)) K) (EXP (FIB N) 2))))). This simplifies, opening up the definitions of ZEROP and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (IMPLIES (LESSP 1 (SUB1 K)) (AND (EQUAL (REMAINDER (FIB (TIMES (SUB1 K) N)) (EXP (FIB N) 2)) (REMAINDER (TIMES (SUB1 K) (FIB N) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))) (EXP (FIB N) 2))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES (SUB1 K) N))) (EXP (FIB N) 2)) (REMAINDER (EXP (FIB (ADD1 N)) (SUB1 K)) (EXP (FIB N) 2))))) (LESSP 1 K)) (AND (EQUAL (REMAINDER (FIB (TIMES K N)) (EXP (FIB N) 2)) (REMAINDER (TIMES K (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (EXP (FIB N) 2))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES K N))) (EXP (FIB N) 2)) (REMAINDER (EXP (FIB (ADD1 N)) K) (EXP (FIB N) 2))))). This simplifies, using linear arithmetic, applying the lemmas COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, TIMES-1-ARG1, EXP-ADD1, FIB-TIMES-OPEN, FIB-TIMES-SPECIAL-STEP, FIB-ADD1-TIMES-OPEN, REMAINDER-TIMES-TIMES, FIB-REMAINDER-HACK, REMAINDER-PLUS, REMAINDER-FIB-BACKCHAIN, REMAINDER-TIMES1, and REMAINDER-TIMES1-INSTANCE, and opening up the functions SUB1, NUMBERP, EQUAL, LESSP, AND, and IMPLIES, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (EQUAL (SUB1 (SUB1 K)) 0) (NOT (EQUAL (SUB1 K) 0))) (EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 (TIMES N (SUB1 K))))) (TIMES (FIB (SUB1 N)) (FIB (TIMES N (SUB1 K))))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB (SUB1 N)) (FIB N) (SUB1 K))) (TIMES (FIB N) (FIB N))))). Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove the formula: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 (ADD1 Z)) 0)) (EQUAL Z 0) (NOT (EQUAL (ADD1 Z) 0))) (EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 (TIMES N (ADD1 Z))))) (TIMES (FIB (SUB1 N)) (FIB (TIMES N (ADD1 Z))))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (ADD1 Z))) (TIMES (FIB (SUB1 N)) (FIB N) (ADD1 Z))) (TIMES (FIB N) (FIB N))))). But this further simplifies, applying TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, and EXP-ADD1, and opening up the definitions of NUMBERP and EQUAL, to the following two new formulas: Case 1.3.2. (IMPLIES (NOT (NUMBERP N)) (EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB 1)) (TIMES (FIB (SUB1 N)) (FIB 0))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N))) (TIMES (FIB N) (FIB (SUB1 N)))) (TIMES (FIB N) (FIB N))))). However this again simplifies, using linear arithmetic, applying the lemmas FIB-SMALL, SUB1-NNUMBERP, and SUB1-TYPE-RESTRICTION, and expanding the functions FIB, TIMES, PLUS, REMAINDER, and EQUAL, to: T. Case 1.3.1. (IMPLIES (NUMBERP N) (EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N))) (TIMES (FIB (SUB1 N)) (FIB N))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N))) (TIMES (FIB N) (FIB (SUB1 N)))) (TIMES (FIB N) (FIB N))))), which again simplifies, applying SUB1-ADD1, ADD1-EQUAL, and COMMUTATIVITY-OF-TIMES, and unfolding NUMBERP and FIB, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (EQUAL (SUB1 (SUB1 K)) 0) (NOT (EQUAL (SUB1 K) 0))) (EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (FIB (ADD1 (TIMES N (SUB1 K))))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) K) (TIMES (FIB N) (FIB N))))). Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 (ADD1 Z)) 0)) (EQUAL Z 0) (NOT (EQUAL (ADD1 Z) 0))) (EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (FIB (ADD1 (TIMES N (ADD1 Z))))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) (ADD1 (ADD1 Z))) (TIMES (FIB N) (FIB N))))). This further simplifies, applying the lemmas TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, and EXP-ADD1, and unfolding NUMBERP and EQUAL, to the conjecture: (IMPLIES (NOT (NUMBERP N)) (EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (FIB 1)) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (FIB (ADD1 N)) (FIB (ADD1 N))) (TIMES (FIB N) (FIB N))))). However this again simplifies, using linear arithmetic, rewriting with SUB1-TYPE-RESTRICTION and FIB-SMALL, and unfolding the functions FIB, TIMES, REMAINDER, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (EQUAL (REMAINDER (FIB (TIMES N (SUB1 K))) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (SUB1 K) (FIB N) (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))) (TIMES (FIB N) (FIB N)))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES N (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) (SUB1 K)) (TIMES (FIB N) (FIB N)))) (NOT (EQUAL (SUB1 K) 0))) (EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) K) (TIMES (FIB N) (FIB N))))). Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We rely upon the type restriction lemma noted when SUB1 was introduced to constrain the new variable. This generates the goal: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 (ADD1 Z)) 0)) (EQUAL (REMAINDER (FIB (TIMES N (ADD1 Z))) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (ADD1 Z) (FIB N) (EXP (FIB (ADD1 N)) Z)) (TIMES (FIB N) (FIB N)))) (EQUAL (REMAINDER (FIB (ADD1 (TIMES N (ADD1 Z)))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) (ADD1 Z)) (TIMES (FIB N) (FIB N)))) (NOT (EQUAL (ADD1 Z) 0))) (EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (ADD1 Z))) (TIMES (FIB N) (FIB N))) (REMAINDER (EXP (FIB (ADD1 N)) (ADD1 (ADD1 Z))) (TIMES (FIB N) (FIB N))))). But this further simplifies, using linear arithmetic, rewriting with TIMES-ADD1, EQUAL-TIMES-0, FIB-SMALL, COMMUTATIVITY-OF-TIMES, FIB-ADD1-TIMES-OPEN, ASSOCIATIVITY-OF-TIMES, TIMES-DISTRIBUTES-OVER-PLUS, FIB-TIMES-OPEN, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, FIB-PLUS, EXP-ADD1, EQUAL-TIMES-X-X, PLUS-ZERO-ARG2, EXP-1-ARG1, and SUB1-TYPE-RESTRICTION, and opening up the functions LESSP, EQUAL, NUMBERP, ZEROP, ADD1, FIB, TIMES, and REMAINDER, to: T. Q.E.D. [ 0.0 2.3 0.1 ] FIB-TIMES-SPECIAL (PROVE-LEMMA FIB-REMAINDER-TIMES-SPECIAL (REWRITE) (EQUAL (REMAINDER (FIB (TIMES N K)) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES K (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N)))) ((USE (FIB-TIMES-SPECIAL)) (DISABLE REMAINDER-TIMES-TIMES-HACK) (DISABLE-THEORY NATURALS) (ENABLE-THEORY EXPONENTIATION MULTIPLICATION))) This conjecture simplifies, rewriting with LESSP-1-HACK, COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, TIMES-1-ARG1, EXP-ADD1, COMMUTATIVITY2-OF-TIMES, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, and SUB1-NNUMBERP, and opening up TIMES, EXP, AND, IMPLIES, FIB, LESSP, EQUAL, NUMBERP, REMAINDER, and SUB1, to the following four new goals: Case 4. (IMPLIES (AND (EQUAL K 1) (NOT (NUMBERP N))) (EQUAL (REMAINDER (FIB 0) (TIMES (FIB N) (FIB N))) (REMAINDER (FIB N) (TIMES (FIB N) (FIB N))))). However this again simplifies, using linear arithmetic, rewriting with the lemma FIB-SMALL, and unfolding the definitions of FIB, TIMES, REMAINDER, and EQUAL, to: T. Case 3. (IMPLIES (AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (SUB1 K) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N)))) (EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K))))) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (FIB N)))) (NOT (EQUAL K 0)) (NUMBERP K)) (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (SUB1 K) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N))))), which again simplifies, clearly, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (SUB1 K) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N)))) (EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K))))) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (FIB N)))) (EQUAL K 0)) (EQUAL (REMAINDER (FIB 0) (TIMES (FIB N) (FIB N))) (REMAINDER 0 (TIMES (FIB N) (FIB N))))). But this again simplifies, using linear arithmetic, applying COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1, FIB-PLUS, EXP-0-ARG2, LESSP-TIMES1, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, TIMES-ZERO, FIB-SMALL, and SUB1-TYPE-RESTRICTION, and opening up the definitions of SUB1, EQUAL, TIMES, FIB, ADD1, NUMBERP, LESSP, REMAINDER, PLUS, EXP, and ZEROP, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K)))) (TIMES (FIB N) (FIB N))) (REMAINDER (PLUS (TIMES (FIB N) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (SUB1 K) (EXP (FIB (ADD1 N)) (SUB1 K)))) (TIMES (FIB N) (FIB N)))) (EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K))))) (TIMES (FIB N) (FIB N))) (REMAINDER (TIMES (FIB (ADD1 N)) (EXP (FIB (ADD1 N)) (SUB1 K))) (TIMES (FIB N) (FIB N)))) (NOT (NUMBERP K))) (EQUAL (REMAINDER (FIB 0) (TIMES (FIB N) (FIB N))) (REMAINDER 0 (TIMES (FIB N) (FIB N))))). But this again simplifies, using linear arithmetic, rewriting with SUB1-NNUMBERP, COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1, FIB-PLUS, EXP-0-ARG2, LESSP-TIMES1, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, TIMES-ZERO, FIB-SMALL, and SUB1-TYPE-RESTRICTION, and unfolding the definitions of EQUAL, TIMES, FIB, ADD1, NUMBERP, LESSP, REMAINDER, PLUS, EXP, and ZEROP, to: T. Q.E.D. [ 0.0 0.6 0.0 ] FIB-REMAINDER-TIMES-SPECIAL (PROVE-LEMMA REMAINDER-TIMES-TIMES-HACK2 (REWRITE) (EQUAL (REMAINDER (TIMES K N) (TIMES N P)) (TIMES N (REMAINDER K P)))) This simplifies, appealing to the lemmas REMAINDER-TIMES1-INSTANCE, QUOTIENT-TIMES-INSTANCE, REMAINDER-TIMES2, and CORRECTNESS-OF-CANCEL-EQUAL-TIMES, and opening up the definitions of EQUAL, ZEROP, FIX, and OR, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NUMBERP K))) (EQUAL (REMAINDER 0 P) (REMAINDER K P))). This again simplifies, appealing to the lemma REMAINDER-OF-NON-NUMBER, and unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-TIMES-TIMES-HACK2 (PROVE-LEMMA MATIJASEVICH-LEMMA-HELPER NIL (IMPLIES (AND (LESSP 2 N) (EQUAL (REMAINDER M N) 0)) (EQUAL (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) ((DISABLE TIMES-ADD1 REMAINDER-TIMES2 LESSP-1-HACK FIB GCD GCD-REMAINDER REMAINDER-TIMES2-INSTANCE) (ENABLE REMAINDER-TIMES-TIMES))) This conjecture simplifies, clearly, to the following two new formulas: Case 2. (IMPLIES (AND (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (NOT (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) (NOT (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by (PLUS X (TIMES N Z)) to eliminate (REMAINDER M N) and (QUOTIENT M N). We employ LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. This generates four new formulas: Case 2.4. (IMPLIES (AND (NOT (NUMBERP M)) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (NOT (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) (NOT (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0))), which further simplifies, using linear arithmetic, applying REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, EQUAL-TIMES-0, and EQUAL-FIB-CONSTANT, and opening up the definitions of NUMBERP, EQUAL, LESSP, and REMAINDER, to: T. Case 2.3. (IMPLIES (AND (EQUAL N 0) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (NOT (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) (NOT (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0))). However this further simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP N)) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (NOT (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) (NOT (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0))), which further simplifies, opening up LESSP, to: T. Case 2.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X N) (NOT (ZEROP N))) (NUMBERP Z) (NUMBERP N) (NOT (EQUAL N 0)) (LESSP 2 N) (EQUAL X 0) (NOT (EQUAL (REMAINDER (PLUS X (TIMES N Z)) (TIMES N (FIB N))) 0))) (NOT (EQUAL (REMAINDER (FIB (PLUS X (TIMES N Z))) (TIMES (FIB N) (FIB N))) 0))), which further simplifies, rewriting with REMAINDER-TIMES-TIMES, EQUAL-TIMES-0, REMAINDER-TIMES-TIMES-HACK, FIB-REMAINDER-TIMES-SPECIAL, EQUAL-FIB-CONSTANT, GCD-EXP-1, GCD-FIB, GCD-A-ADD1-A, and GCD-REMAINDER-TIMES-FACT1-PROOF2, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, PLUS, and FIB, to: T. Case 1. (IMPLIES (AND (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0)) (EQUAL (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0) T)). This again simplifies, clearly, to: (IMPLIES (AND (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0)) (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace M by (PLUS X (TIMES N Z)) to eliminate (REMAINDER M N) and (QUOTIENT M N). We rely upon LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following four new conjectures: Case 1.4. (IMPLIES (AND (NOT (NUMBERP M)) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0)) (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0)). However this further simplifies, using linear arithmetic, applying REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, and FIB-SMALL, and unfolding NUMBERP, EQUAL, LESSP, and REMAINDER, to: T. Case 1.3. (IMPLIES (AND (EQUAL N 0) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0)) (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0)). However this further simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP N)) (LESSP 2 N) (EQUAL (REMAINDER M N) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0)) (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0)), which further simplifies, expanding the function LESSP, to: T. Case 1.1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X N) (NOT (ZEROP N))) (NUMBERP Z) (NUMBERP N) (NOT (EQUAL N 0)) (LESSP 2 N) (EQUAL X 0) (EQUAL (REMAINDER (PLUS X (TIMES N Z)) (TIMES N (FIB N))) 0)) (EQUAL (REMAINDER (FIB (PLUS X (TIMES N Z))) (TIMES (FIB N) (FIB N))) 0)), which further simplifies, rewriting with REMAINDER-TIMES-TIMES, EQUAL-TIMES-0, REMAINDER-TIMES1, COMMUTATIVITY-OF-TIMES, REMAINDER-TIMES-TIMES-HACK, and FIB-REMAINDER-TIMES-SPECIAL, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, PLUS, and TIMES, to: T. Q.E.D. [ 0.0 0.7 0.0 ] MATIJASEVICH-LEMMA-HELPER (PROVE-LEMMA MATIJASEVICH-LEMMA (REWRITE) (IMPLIES (LESSP 2 N) (EQUAL (EQUAL (REMAINDER (FIB M) (TIMES (FIB N) (FIB N))) 0) (EQUAL (REMAINDER M (TIMES N (FIB N))) 0))) ((USE (MATIJASEVICH-LEMMA-HELPER)))) This simplifies, using linear arithmetic, rewriting with LESSP-1-HACK, EQUAL-SUB1-0, REMAINDER-FIB-FIB-0, and REMAINDER-TIMES-HACK2, and expanding the definitions of SUB1, NUMBERP, EQUAL, LESSP, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.5 0.0 ] MATIJASEVICH-LEMMA