Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <26719-0@swan.cl.cam.ac.uk>; Tue, 21 Apr 1992 22:52:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22256; Tue, 21 Apr 92 14:28:03 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA22251; Tue, 21 Apr 92 14:27:16 -0700 Received: by grolsch.cs.ubc.ca id AA07809 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Tue, 21 Apr 1992 14:27:15 -0700 Date: 21 Apr 92 22:34 +0100 From: Jeffrey Joyce To: info-hol Message-Id: <4602*joyce@cs.ubc.ca> Subject: arithmetic challenge I've heard from several people who have used other theorem-provers to prove the following theorem (or at least a hand-translation of it into the local notation). These other theorem-provers are BMTP (CLI), EVES (ORA) and PVS (SRI). "!A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + (((B DIV (2 EXP i)) MOD 2) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1))))" In general, most of these efforts seemed to have required between 2 and 4 hours of effort. This includes time spent working through a hand-proof of the theorem and identifying useful lemmas. In some cases, these lemmas were also proved as part of the overall effort -- while in other cases the lemmas were simply postulated. The proof scripts for these results appear to vary between 1 and 5 pages. So far, I have not heard of any successful attempt to prove this theorem in HOL. John Rushby (of SRI) kindly gave me his permission to make public his correspondence with me on their use of the PVS theorem-prover to prove this theorem (which I have attached below). I note that John's message includes his own arithmetic challenge -- any takers ? - Jeff Message inbox:4808 - Read From: John Rushby To: Cc: In-Reply-To: <4581*joyce@cs.ubc.ca> Subject: Re: theorem-proving challenge >Mail-System-Version: Jeff, Shankar had a go at your test-piece. We don't have a mod/div/exp library written for PVS, so he compiled a short list of lemmas sufficient for this proof. Note that these lemmas haven't been proved--we're working on other things at the moment--but he believes they're all pretty easy. First time through, he hit a bug fairly early in the proof (PVS is still under active development). The transcript below is his second attempt. As you can see from the statistics at the bottom, it took him a little over 16 minutes from start to finish. The PVS typechecker pointed out (by generating a manifestly unprovable type-correctness proof obligation) that the theorem as you typed it is in error. See the the transcript below for the theorem actually proved. The first part of the listing below is the specification of the problem and assumed lemmas in PVS; the next part is a transcript of the interactive proof. The user inputs to the PVS prover are the parenthesized commands following the "Rule?" prompt. The rest is PVS prover output. The prover uses a sequent representation: the idea is that the conjunction of the stuff above the line should imply the disjunction of that below. The (assert) rule tells the decision procedures to take note of the situation, and possibly simplify things. A rule like (assert (-1)) says invoke assert on just the formula labeled -1; (assert -) means apply it to all the stuff above the line; (assert +) applies to all the stuff below the line; (assert) means apply it to everything. Labels in braces (e.g., {3}) simply direct the user's attention to what has changed since the previous sequent. The final part of the listing is PVS's summary of the proof. This is meant to be something readable you could put in a report. You're welcome to post this to info-hol if you think there'd be interest. John PS. A fairly nasty piece of arithmetic that shows up in the proof of the interactive convergence clock synchronization algorithm is the following: rearrange_delta: LEMMA delta >= 2 * (eps + rho * S) + 2 * m * Delta / (n - m) + n * rho * R / (n - m) + rho * Delta + n * rho * Sigma / (n - m) IMPLIES delta >= ((delta + 2 * Delta) * m + 2 * (eps + rho * S + half(rho) * Delta) * (n - m)) / n + rho * R + rho * Sigma __________________________________________________________________ joyce: THEORY BEGIN a, b,c, i, j,k,l,m,n: VAR nat posnat : TYPE = {i| i > 0} div(a,(b:posnat)): RECURSIVE nat = (IF a>=b THEN 1+div(a-b, b) ELSE 0 ENDIF) BY (LAMBDA a,(b:posnat): a) mod(a,(b:posnat)): RECURSIVE nat = (IF a>=b THEN mod(a-b, b) ELSE a ENDIF) BY (LAMBDA a,(b:posnat): a) pow2(i): RECURSIVE posnat = (IF i>0 THEN 2*pow2(i-1) ELSE 1 ENDIF) BY (LAMBDA i: i) pow2_plus: LEMMA pow2(a+b) = pow2(a)*pow2(b) mod_bnd: LEMMA b>0 IMPLIES mod(a,b) 0 IMPLIES mod(a, b) = a - div(a, b) * b pp: VAR PRED[nat] strong_ind: LEMMA pp(0) AND (FORALL j: (FORALL (i|i<=j) : pp(i)) IMPLIES pp(j+1)) IMPLIES pp(n) div_div: LEMMA b>0 AND c>0 IMPLIES div(div(a, b),c) = div(a, b*c) x, y, z, u, v: VAR number both_sides: LEMMA x/=0 AND x*y = x*z IMPLIES y=z postimes: LEMMA x>0 AND y>0 IMPLIES x*y>0 mod_prod: LEMMA b > 0 AND mod(a, b) = 0 IMPLIES mod(a * c, b) = 0 plus_div: LEMMA c > 0 AND (mod(a, c) = 0 OR mod(b, c) = 0) IMPLIES div(a + b, c) = (div(a, c) + div(b, c)) times_div: LEMMA b > 0 AND mod(a, b) = 0 IMPLIES div(a * c, b) = div(a, b) * c minus_div: LEMMA c>0 AND a>=b AND (mod(a,c)=0 OR mod(b,c)=0) IMPLIES div(a-b,c) = (div(a,c) - div(b,c)) div_pow2: LEMMA a>0 IMPLIES mod(pow2(a), 2) = 0 joyce: LEMMA i 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (assert (1)) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.1.3. That completes the proof of joyce.1.1.1.1.1. joyce.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (lemma "pow2_plus" ("a" "n!4 - (i!5 + 1)" "b" "i!5")) Applying pow2_plus where a gets n!4 - (i!5 + 1) b gets i!5 this yields 2 subgoals: joyce.1.1.1.1.2.1 : {-1} pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.2.1 : [-1] pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) Rule? (replace -1) Replacing using formula -1, this simplifies to: joyce.1.1.1.1.2.1 : [-1] pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.2.1. joyce.1.1.1.1.2.2 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [3] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (3)) this simplifies to: joyce.1.1.1.1.2.2 : [-1] i!5 < n!4 |------- [1] (n!4 - (i!5 + 1)) >= 0 [2] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.2.2. That completes the proof of joyce.1.1.1.1.2. joyce.1.1.1.1.3 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.3 : [-1] i!5 < n!4 |------- [1] (n!4 - (i!5 + 1)) >= 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.3. joyce.1.1.1.1.4 : [-1] i!5 < n!4 |------- {1} (n!4 - 1) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.4 : [-1] i!5 < n!4 |------- [1] (n!4 - 1) >= 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.4. That completes the proof of joyce.1.1.1.1. joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1), 2) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- [1] mod(2, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.2. That completes the proof of joyce.1.1.1. joyce.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3, 2) * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.2 : [-1] i!5 < n!4 |------- [1] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.2.1. joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.2.2. That completes the proof of joyce.1.1.2. That completes the proof of joyce.1.1. joyce.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.2 : [-1] i!5 < n!4 |------- [1] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.1. joyce.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.2.1. joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.2.2. That completes the proof of joyce.1.2.2. That completes the proof of joyce.1.2. That completes the proof of joyce.1. joyce.2 : [-1] i!5 < n!4 |------- {1} (mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 OR mod(div(c!1, pow2(i!5)), 2) = 0) [2] div((pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5))), 2) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.2 : [-1] i!5 < n!4 |------- [1] (mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 OR mod(div(c!1, pow2(i!5)), 2) = 0) Rule? (dsimp) Apply disjunctive simplification, this simplifies to: joyce.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 {2} mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.1. joyce.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3, 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "div_pow2") No matching instance for div_pow2 found. No change. joyce.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3, 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.2.1. joyce.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5), 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3, 2) = 0 [3] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [4] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "div_pow2") Rewriting using div_pow2, this simplifies to: joyce.2.2.2 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(pow2(n!4 - i!5) * a!3, 2) = 0 [3] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [4] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.2.2. That completes the proof of joyce.2.2. That completes the proof of joyce.2. Q.E.D. --------------------------------------------------------------------------- Would you like me to print a brief version of the proof? (Yes or No) yes joyce : |------- {1} (FORALL (c: nat), (b: nat), (a: nat), (n: nat), (i: nat): i < n IMPLIES div((pow2(n - i) * a * mod(b, pow2(i)) + div(c, pow2(i))), 2) + pow2(n - 1) * a * mod(div(b, pow2(i)), 2) = pow2(n - (i + 1)) * a * mod(b, pow2(i + 1)) + div(c, pow2(i + 1))) Rewriting using plus_div, which yields 2 subgoals: joyce.1 : [-1] i!5 < n!4 |------- {1} (div(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) + div(div(c!1, pow2(i!5)), 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using div_div, Invoking decision procedures, Rewriting using pow2, Rewriting using times_div, which yields 2 subgoals: joyce.1.1 : [-1] i!5 < n!4 |------- {1} (div(2 * pow2((n!4 - i!5) - 1) * a!3, 2) * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using times_div, which yields 2 subgoals: joyce.1.1.1 : [-1] i!5 < n!4 |------- {1} (div(2 * pow2((n!4 - i!5) - 1), 2) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using times_div, which yields 2 subgoals: joyce.1.1.1.1 : [-1] i!5 < n!4 |------- {1} (div(2, 2) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using div, Rewriting using div, Case splitting on pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1))*pow2(i!5) which yields 4 subgoals: joyce.1.1.1.1.1 : {-1} pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Case splitting on mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) which yields 3 subgoals: joyce.1.1.1.1.1.1 : {-1} mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) [-2] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using pow2, Invoking decision procedures, which completes the proof of joyce.1.1.1.1.1.1. joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using div_mod, Rewriting using div_mod, Rewriting using div_mod, Rewriting using div_div, Rewriting using pow2, Invoking decision procedures, which completes the proof of joyce.1.1.1.1.1.2. joyce.1.1.1.1.1.3 : [-1] i!5 < n!4 |------- {1} 2 > 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Invoking decision procedures, which completes the proof of joyce.1.1.1.1.1.3. joyce.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Applying pow2_plus where a gets n!4 - (i!5 + 1) b gets i!5 which yields 2 subgoals: joyce.1.1.1.1.2.1 : {-1} pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Invoking decision procedures, which completes the proof of joyce.1.1.1.1.2.1. joyce.1.1.1.1.2.2 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [3] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Invoking decision procedures, which completes the proof of joyce.1.1.1.1.2.2. joyce.1.1.1.1.3 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Invoking decision procedures, which completes the proof of joyce.1.1.1.1.3. joyce.1.1.1.1.4 : [-1] i!5 < n!4 |------- {1} (n!4 - 1) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Invoking decision procedures, which completes the proof of joyce.1.1.1.1.4. joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1), 2) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using mod, Rewriting using mod, Invoking decision procedures, which completes the proof of joyce.1.1.1.2. joyce.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3, 2) * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using mod_prod, which yields 2 subgoals: joyce.1.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Invoking decision procedures, which completes the proof of joyce.1.1.2.1. joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rewriting using mod, Rewriting using mod, Invoking decision procedures, which completes the proof of joyce.1.1.2.2. joyce.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using mod_prod, which yields 2 subgoals: joyce.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Invoking decision procedures, which completes the proof of joyce.1.2.1. joyce.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rewriting using mod_prod, which yields 2 subgoals: joyce.1.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Invoking decision procedures, which completes the proof of joyce.1.2.2.1. joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rewriting using mod, Rewriting using mod, Invoking decision procedures, which completes the proof of joyce.1.2.2.2. joyce.2 : [-1] i!5 < n!4 |------- {1} (mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 OR mod(div(c!1, pow2(i!5)), 2) = 0) [2] div((pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5))), 2) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rewriting using mod_prod, which yields 2 subgoals: joyce.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(div(c!1, pow2(i!5)), 2) = 0 Invoking decision procedures, which completes the proof of joyce.2.1. joyce.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3, 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rewriting using mod_prod, which yields 2 subgoals: joyce.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Invoking decision procedures, which completes the proof of joyce.2.2.1. joyce.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5), 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3, 2) = 0 [3] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [4] mod(div(c!1, pow2(i!5)), 2) = 0 Rewriting using div_pow2, Invoking decision procedures, which completes the proof of joyce.2.2.2. Q.E.D. Elapsed Real Time = 1000.78 seconds (16 minutes, 40.78 seconds) Total Run Time = 253.07 seconds (4 minutes, 13.07 seconds) User Run Time = 250.26 seconds (4 minutes, 10.26 seconds) System Run Time = 2.81 seconds Process Page Faults = 10,846 Dynamic Bytes Consed = 0 Ephemeral Bytes Consed = 39,827,712 There were 76 ephemeral GCs joyce : |------- {1} (FORALL (c: nat), (b: nat), (a: nat), (n: nat), (i: nat): i < n IMPLIES div((pow2(n - i) * a * mod(b, pow2(i)) + div(c, pow2(i))), 2) + pow2(n - 1) * a * mod(div(b, pow2(i)), 2) = pow2(n - (i + 1)) * a * mod(b, pow2(i + 1)) + div(c, pow2(i + 1))) -------