Barzilay & Lee, 2002 | Holland-Minkley et al, 1999 | |

1 (zero_ann_a) |
Assume that a and b are integers and (a = 0 or b = 0) , we need to show a * b = 0. (a = 0 or b = 0) can be split into two cases a = 0 or not. if a = 0 then a * b = 0. if b = 0 we are done. | For an integer a and b, if a = 0 or b = 0 then a * b = 0. Consider that a and b are integers and a = 0 or b = 0. There are 2 possible cases. Now, the goal can be transformed to a * b = 0. Now, the goal can be transformed to a * b = 0. |

2 (add_cancel_in_eq) |
Let a, b and n be integers , a+n = b+n , we need to show a = b. We prove this holds for a+n-n=b+n-n. This case is trivial. | For an integer a, b and n, if a+n = b+n then a=b. Consider that a, b and n are integers and a+n = b+n. Equivalently, the original expression can be rewritten as a=b. Equivalently, the goal can be rewritten as (a+n)-n = (b+n)-n. |

3 (add_mono_wrt_lt) |
Assume a, b and n are integers. Show that a < b if and only if a+n < b+n. Using lemma add_cancel_in_lt , we know that the statement is proved. suppose a+n<b+n then by lemma Add_cancel_in_lt we know that we are done. | For an integer a, b and n, a < b if and only if a+n < b+n. Consider that a, b and n are integers and a < b. Consider that a, b and n are integers and a < b. Applying the add_cancel_in_lt lemma, the goal becomes a+n < b+n. Assume that a, b and n are integers and a+n < b+n. By applying the add_cancel_in_lt lemma, the goal becomes a<b. |

4 (add_mono_wrt_le) |
Assume a, b and n are integers and a <= b. Show that a <= b if and only if a+n <= b+n. If a<=b, using lemma add_cancel_in_le , we get we are done. suppose a+n<=b+n then by lemma add_cancel_in_le , the statement is proved. | For an integer a, b and n, a <= b if and only if a+n <= b+n. Consider that a, b and n are integers and a <= b. Consider that a, b and n are integers and a <= b. From the add_cancel_in_le lemma, we know a+n <= b+n. Consider that a, b and n are integers and a+n <= b+n. Using the add_cancel_in_le lemma, we conclude a <= b. |

5 (mul_bounds_1a) |
Let a and b be natural numbers, show 0<=a*b. We prove this theorem holds for a*0<=a*b. Show that 0<=A*B . a*0<=a*b follows from mul_preserves_le. If a*0<=a*b then we are done. | For a natural number a and b, 0 <= a*b. Assume a and b are natural numbers. There are 2 possible cases. By applying the mul_preserves_le lemma, we conclude a*0 <= a*b. Consider a*0 <= a*b. Equivalently, the goal can be transformed to 0 <= a*b. |

6 (div_base_case) |
Assume that a is a natural number, n is positive natural number and a<n , we need to show a/n = 0. Using lemma div_unique , we get a new goal DIV (A;N;A µ N). div (a;n;a/n) follows from div_fun_sat_div_nrel. By the definition of div_nrel and simple arithmetic we show that Div(a;n;0). | For a natural number a and the positive natural number n, if a < n then a/n = 0. Assume that a is a natural number, n is the positive natural number and a < n. There are 2 possible cases. From the div_fun_sat_div_nrel lemma, the goal becomes Div(a;n;a/n). Now, the goal can be rewritten as Div(a;n;0). |

7 (rem_rec_case) |
Assume that a is a natural number, n is the positive natural number and a >= n, we need to show (a rem n) = ((a-n) rem n). By lemma rem_to_div we show: a-(a/n)*n = a-n-((a-n)/n)*n. By lemma div_rec_case we get : a-(((a-n)/n) 1)*n = a-n-((a-n)/ n)*n. By 0, a + -n + -(n*((a + -n)/n)) = a + -n + -(n*((a + -n)/n)). This case it trivial. | For a natural number a and the positive natural number n, if a >= n then a rem n = (a - n) rem n. Assume that a is a natural number, n is the positive natural number and a >= n. By applying the rem_to_div lemma, we know a rem n = (a - n) rem n. From the div_rec_case lemma, we conclude a - (a/n)*n = a - n - ((a - n)/n)*n. Now, the goal can be transformed to a - ((a - n)/n + 1)*n = a - n - ((a - n)/n)*n. Equivalently, the goal can be transformed to a + -n + -(n*((a + -n)/n)) = a + -n + -(n*((a + -n)/n)). |

8 (rem_rem_to_rem) |
Assume that a is a natural number and n is the positive natural number, we need to show ((a rem n) rem n) = (a rem n). By lemma rem_base_case we get the new goal (a rem n) < n and (a rem n) = (a rem n). From the rem_bounds_1 , goal (a rem n) < n follows. Case of (a rem n) = (a rem n) is trivial. | For a natural number a and the positive natural number n, (a rem n) rem n = a rem n. Assume that a is a natural number and n is the positive natural number. There are 2 possible cases. By the rem_bounds_1 lemma, we conclude a rem n < n. Equivalently, the goal can be transformed to a rem n = a rem n. |

9 (mul_bounds_1b) |
Let a and b are the positive natural numbers, we need to show 0<A*B . We prove this holds for a*0 < a*b. From the mul_preserves_lt , goal a*0 < a*b follows. If a*0 < a*b then we are done. | For the positive natural number a and b, 0 < a*b. Consider a and b are the positive natural numbers. There are 2 possible cases. Using the mul_preserves_lt lemma, the goal becomes a*0 < a*b. Assume a*0 < a*b. Now, the original expression can be rewritten as 0 < a*b. |

10 (absval_sym) |
Assume that i is an integer , we need to show |i| = |-i|. From absval_eq lemma, |i| = |-i| reduces to i = +/-i. By the definition of pm_equal, i = +/-i is proved. | Assume i is an integer. By the absval_eq lemma, the goal becomes |i| = |-i|. Now, the original expression can be rewritten as i +/- = -i. |

11 (absval_ubound) |
Let i be an integer and n be a natural number, show |i| <= n if and only if -n <= i and i <= n. By the definition of absval, |i| <= n if and only if -n <= i and i <= n. is proved. Now split on the two cases. If 0<=I, the resulting formula can be automatically proven by the system. If I<0, and the proof is now trivially finished using arithmetic rules. | For an integer i and a natural number n, |i| <= n if and only if -n <= i and i <= n. Assume that i is an integer and n is a natural number. Equivalently, the original expression can be transformed to |i| <= n if and only if -n <= i and i <= n. There are 2 possible cases. Assume 0 <= i. Now, the goal can be rewritten as i <= n if and only if -n <= i and i <= n. Consider i < 0. Equivalently, the goal can be rewritten as -i <= n if and only if -n <= i and i <= n. |

12 (div_fun_sat_div_nrel) |
Let a be a natural number and n be a positive natural number, show n*(a/n)<=a<n*((a/n+1). From rem_bounds_1 we know that 0<=(a rem n) & (a rem n)<n). 0<=(a rem n) & (a rem n)<n can be split into two cases 0<=(a rem n), (a rem n)<n. We can use lemma add_com to rewrite the goal n*(a/n)<=a<n*(a/n+1). We can use lemma div_rem_sum to rewrite the goal n*(a/n)<=a<n*(a/n+1). From lemma add_com we know (a/n)*n+(a rem n)<n+(a/n)*n. From lemma div_rem_SUM we know n*a/n<=a<n*(a/n+1). n*a/n<=a<n*(a/n + 1) follows directly. | For a natural number a and the positive natural number n, Div(a;n;a/n). Consider that a is a natural number and n is the positive natural number. By applying the rem_bounds_1 lemma, we conclude n * a/n <= a < n * (a/n + 1). Equivalently, the original expression can be rewritten as n * a/n <= a < n * (a/n + 1). By the add_mono_wrt_le_rw lemma, we know n * a/n <= a < n * (a/n + 1). E, we apply the lemma. By the add_com lemma, the goal becomes n * a/n <= a < n * (a/n + 1). Using the div_rem_sum lemma, we conclude n * a/n <= a < n * (a/n + 1). From the add_com lemma, the goal becomes n * a/n <= a < n * (a/n + 1). From the div_rem_sum lemma, the goal becomes n * a/n <= a < n * (a/n + 1). Now, the goal can be transformed to n * a/n <= a < n * (a/n + 1). |

13 (imax_com) |
Assume a and b are integers, show imax(a;b) = imax(b;a). By the definition of imax we need to show that if a<=b then b else a fi = if b<=a then a else b fi. Split on the cases of if a<=b then b else a fi = if b<=a then a else b fi. | For an integer a and b, imax(a;b) = imax(b;a). Consider a and b are integers. Now, the original expression can be transformed to imax(a;b) = imax(b;a). Equivalently, the goal can be transformed to if a<=b then b else a fi = if b<=a then a else b fi. |

14 (imax_lb) |
Let a, b and c be integers, we need to show imax(a;b) <= c if and only if a <= c & b <= c. by subsituting imax to guard, we get if a<=b then b else a fi <= c if and only if a <= c and b <= c. Split on the cases of if a<=b then b else a fi <= c if and only if a <= c and b <= c. | For an integer a, b and c, imax(a;b) <= c if and only if a <= c & b <= c. Assume a, b and c are integers. Equivalently, the goal can be transformed to imax(a;b) <= c if and only if a <= c * b <= c. Equivalently, the original expression can be rewritten as if a<=b then b else a fi <= c if and only if a <= c and b <= c. |

15 (ndiff_add_eq_imax) |
Assume that a and b are integers, we need to show (a -- b) + b = imax(a;b). By the definition of ndiff and simple arithmetic we need to show that imax(a-b;0) + b = imax (a;b). By lemma imax_add_r we show : imax(a-b;0) + b = imax (a;b). | For an integer a and b, (a -- b) + b = imax(a;b). Assume a and b are integers. Now, the original expression can be transformed to (a -- b) + b = imax(a;b). By applying the imax_add_r lemma, we conclude imax(a-b;0) + b = imax(a;b). |

16 (ndiff_id_r) |
Let a be a natural number, we need to show a -- 0 = a. By the definition of ndiff, we need to show that imax (a-0;0) = a. By the definition of imax, we need to show that if (a-0)<=0 then 0 else a-0 fi = a. Split on the cases of if (a-0)<=0 then 0 else a-0 fi = a. | For a natural number a, a -- 0 = a. Assume a is a natural number. Equivalently, the goal can be transformed to a -- 0 = a. Now, the goal can be transformed to imax(a-0;0) = a. Now, the original expression can be transformed to if (a-0)<=0 then 0 else a-0 fi = a. |

17 (ndiff_inv) |
Let a be a natural number and b be an integer, show (a+b) -- b=a. By the definition of ndiff we need to show that imax (a+b-b;0)=a. By the definition of imax, we can show that if ((a+b) - b)<=0 then 0 else (a+b) - b fi = a. Now split on the two cases. | For a natural number a and an integer b, (a+b) -- b = a. Assume that a is a natural number and b is an integer. Now, the original expression can be transformed to (a+b) -- b = a. Now, the goal can be transformed to imax((a+b) - b;0) = a. Equivalently, the original expression can be rewritten as if ((a+b) - b)<=0 then 0 else (a+b) - b fi = a. |

18 (imin_lb) |
Let a, b and c are integers, we need to show imin(a;b) <= c if and only if a <= c or b <= c. by subsituting IMIN, we get a<=b then a else b fi <= c if and only if a <= c or b <= c. Split on the cases of a<=b then a else b fi <= c if and only if a <= c or b <= c. | For an integer a, b and c, imin(a;b) <= c if and only if a <= c or b <= c. Consider a, b and c are integers. Now, the original expression can be rewritten as imin(a;b) <= c if and only if a <= c or b <= c. Now, the original expression can be transformed to if a<=b then a else b fi <= c if and only if a <= c or b <= c. |

19 (imin_add_r) |
Assume that a, b and c are integers., we need to show imin (a;b)+c = imin (a+c;b+c). This case we can rewrite imin (a;b) +c = imin (a+c;b+c) to - (imin (a;b) +c) = -imin (a+c;b+c) using lemma minus_mono_wrt_eq -c+-imin (a;b) = -imin (a+c;b+c). by lemma minus_imin : -c+imax (-a;-b) = imax (- (a+c) ;- (b+c)). by lemma add_com we get : imax (-a;-b) +-c = imax (- (a+c) ;- (b+c)) by lemma imax_add_r we can show : imax (-a;-b) +-c = imax (- (a+c) ;- (b+c)) | For an integer a, b and c, imin(a;b) + c = imin(a+c;b+c). Consider a, b and c are integers. From the minus_mono_wrt_eq lemma, the goal becomes imin(a;b) + c = imin(a+c;b+c). Now, the goal can be rewritten as -(imin(a;b) + c) = -imin(a+c;b+c). By applying the minus_imin lemma, the goal becomes -c + -imin(a;b) = -imin(a+c;b+c). Applying the add_com lemma, the goal becomes -c + imax(-a;-b) = imax(-(a+c);-(b+c)). Applying the imax_add_r lemma, the goal becomes imax(-a;-b) + -c = imax(-(a+c);-(b+c)). |

20 (int-entire) |
Let a and b are integers and a*b = 0, we need to show a = 0 or b = 0. There are two cases depending on whether b=0 or not. If b = 0, then the goal is tranformed into a = 0 or b = 0. If ~(b = 0) , then the goal is tranformed into a = 0. Using lemma mul_cancel_in_eq , we know that the statement is proved. | For an integer a and b, if a*b = 0 then a = 0 or b = 0. Assume that a and b are integers and a*b = 0. There are 2 possible cases. Assume b = 0. Now, the goal can be transformed to a = 0 or b = 0. Consider ~(b = 0). Equivalently, the original expression can be rewritten as a = 0 or b = 0. Using the mul_cancel_in_eq lemma, the goal becomes a = 0. Now, the goal can be rewritten as b*a = b*0. |