Proof step 1 from proof gcd-mult (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gcd(n0 * m, n0 * n) ≠ n0 * gcd(m, n) ⊦

Rule argument

Additional information

Proof step 2 from proof gcd-mult (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  gcd(n0 * m, n0 * n) ≠ n0 * gcd(m, n), ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: n0 * m + n0 * n

Proof step 3 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  gcd(n0 * m, n0 * n) ≠ n0 * gcd(m, n), ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Proof step 4 from proof gcd-mult (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ n ≤ m → gcd(m, n) = gcd(m - n, n)

• Proof step 6:

  gcd(n0 * m, n0 * n) ≠ n0 * gcd(m, n), ¬ n0 * n ≤ n0 * m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

• Proof step 18:

  gcd(n0 * m - n0 * n, n0 * n) ≠ n0 * gcd(m, n), n0 * n ≤ n0 * m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used terms: n0 * n, n0 * m

Proof step 5 from proof gcd-mult (previous step) (back to tree)

Lemma gcd-rec1

Proof step 6 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gcd(n0 * m, n0 * n) ≠ n0 * gcd(m, n), n0 ≠ 0, m < n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 7 from proof gcd-mult (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ m ≤ n → gcd(m, n) = gcd(m, n - m)

• Proof step 9:

  gcd(n0 * m, n0 * n - n0 * m) ≠ n0 * gcd(m, n), n0 ≠ 0, m < n, n0 * m ≤ n0 * n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: n0 * n, n0 * m

Proof step 8 from proof gcd-mult (previous step) (back to tree)

Lemma gcd-rec2

Proof step 9 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  gcd(n0 * m, n0 * n - n0 * m) ≠ n0 * gcd(m, n), n0 ≠ 0, m < n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m < n → m ≤ n; (s) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s)

Proof step 10 from proof gcd-mult (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  n0 * n = n1 + n0 * m, gcd(n0 * m, n1) ≠ n0 * gcd(m, n), n0 ≠ 0, m < n, n0 * m ≤ n0 * n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → n * m - n0 * m = (n - n0) * m; (s) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0 * n, n0 * m, n1

Proof step 11 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  n0 * n = n1 + n0 * m, gcd(n0 * m, n1) ≠ n0 * gcd(m, n), n0 ≠ 0, m < n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m < n → m ≤ n; (s) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s)

Proof step 12 from proof gcd-mult (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ m ≤ n → gcd(m, n) = gcd(m, n - m)

• Proof step 14:

  n0 * n = n1 + n0 * m, gcd(n0 * m, n1) ≠ n0 * gcd(m, n - m), n0 ≠ 0, m < n, m ≤ n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) Used terms: m, n

Proof step 13 from proof gcd-mult (previous step) (back to tree)

Lemma gcd-rec2

Proof step 14 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  n0 * n = n1 + n0 * m, gcd(n0 * m, n1) ≠ n0 * gcd(m, n - m), n0 ≠ 0, m < n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 15 from proof gcd-mult (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  n0 * n = n1 + n0 * m, n = n4 + m, gcd(n0 * m, n1) ≠ n0 * gcd(m, n4), n0 ≠ 0, m < n, m ≤ n, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, m, n4

Proof step 16 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  gcd(n0 * m, n0 * n4) ≠ n0 * gcd(m, n4), n0 ≠ 0, n4 ≠ 0, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * (n4 + m) → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m0 * (m + n) = m0 * m + m0 * n; (s)

Proof step 17 from proof gcd-mult (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, n) = n; gcd-a: ⊦ gcd(m, gcd(n, n0)) = gcd(gcd(m, n), n0); ⊦ m0 * (m + n) = m0 * m + m0 * n; (s) ⊦ m + m = 2 * m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 2 * n ≤ n ↔ n = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m * 0 = 0; (s) ⊦ m0 ≠ 0 → (m * m0 = n * m0 ↔ m = n); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: n0, m, n4

Proof step 18 from proof gcd-mult (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  gcd(n0 * m - n0 * n, n0 * n) ≠ n0 * gcd(m, n), n0 ≠ 0, n0 * n ≤ n0 * m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, n) = n; gcd-a: ⊦ gcd(m, gcd(n, n0)) = gcd(gcd(m, n), n0); ⊦ m * 0 = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used formulas: n0 = 0

Proof step 19 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  gcd(n0 * m - n0 * n, n0 * n) ≠ n0 * gcd(m, n), n0 ≠ 0, n ≤ m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s)

Proof step 20 from proof gcd-mult (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  n0 * m = n1 + n0 * n, gcd(n1, n0 * n) ≠ n0 * gcd(m, n), n0 ≠ 0, n ≤ m, n0 * n ≤ n0 * m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 ≤ n → n * m - n0 * m = (n - n0) * m; (s) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m ≤ n → (n < m ↔ false); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0 * m, n0 * n, n1

Proof step 21 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  n0 * m = n1 + n0 * n, gcd(n1, n0 * n) ≠ n0 * gcd(m, n), n0 ≠ 0, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → m0 ≤ n1; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s)

Proof step 22 from proof gcd-mult (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ n ≤ m → gcd(m, n) = gcd(m - n, n)

• Proof step 24:

  n0 * m = n1 + n0 * n, gcd(n1, n0 * n) ≠ n0 * gcd(m - n, n), n0 ≠ 0, n ≤ m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → ¬ n1 < m0; (s) Used terms: n, m

Proof step 23 from proof gcd-mult (previous step) (back to tree)

Lemma gcd-rec1

Proof step 24 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  n0 * m = n1 + n0 * n, gcd(n1, n0 * n) ≠ n0 * gcd(m - n, n), n0 ≠ 0, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → m0 ≤ n1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult

Proof step 25 from proof gcd-mult (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 26:

  n0 * m = n1 + n0 * n, m = n4 + n, gcd(n1, n0 * n) ≠ n0 * gcd(n4, n), n0 ≠ 0, n ≤ m, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * m + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → ¬ n1 < m0; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m, n, n4

Proof step 26 from proof gcd-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  gcd(n0 * n4, n0 * n) ≠ n0 * gcd(n4, n), n0 ≠ 0, ∀ n2, m0, n3. n2 * m0 + n2 * n3 < n0 * (n4 + n) + n0 * n → gcd(n2 * m0, n2 * n3) ≠ n2 * gcd(m0, n3) → false ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m0 * (m + n) = m0 * m + m0 * n; (s)

Proof step 27 from proof gcd-mult (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: gcd-zero-02: ⊦ gcd(n, 0) = n; gcd-a: ⊦ gcd(m, gcd(n, n0)) = gcd(gcd(m, n), n0); ⊦ m0 * (m + n) = m0 * m + m0 * n; (s) ⊦ m + m = 2 * m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 2 * n ≤ n ↔ n = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m * 0 = 0; (s) ⊦ m0 ≠ 0 → (m * m0 = n * m0 ↔ m = n); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: n0, n4, n