Proof step 1 from proof gcdnex-prime (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ gcd(m, m0) = 1 ↔ m + m0 = 1 ∨ ¬(∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0)

Rule argument

Additional information

Used simplifier rules: ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

Proof step 2 from proof gcdnex-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ gcd(m, m0) = 1 ↔ m + m0 = 1 ∨ ¬(∃ n. 1 < n ∧ n | m ∧ n | m0)

• Proof step 4:

  ⊦ m + m0 = 1 ∨ ¬(∃ n. 1 < n ∧ n | m ∧ n | m0) ↔ m + m0 = 1 ∨ ¬(∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0)

Rule argument

Additional information

Used terms: m0, m

Proof step 3 from proof gcdnex-prime (previous step) (back to tree)

Lemma gcdnex

Proof step 4 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  m + m0 ≠ 1 ⊦ ¬(∃ m1. m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0) ↔ ¬(∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0)

Rule argument

Additional information

Used simplifier rules: ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

Proof step 5 from proof gcdnex-prime (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  m + m0 ≠ 1, ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0 ⊦ ∃ m1. m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

• Proof step 8:

  m + m0 ≠ 1, ∃ m1. m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0 ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Proof step 6 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, prime(m1), m1 | m, m1 | m0 ⊦ ∃ m1. m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Proof step 7 from proof gcdnex-prime (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: m1

Proof step 8 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m1 | m, m1 | m0 ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Proof step 9 from proof gcdnex-prime (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m1 | m0, m1 | m ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0, prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Used terms: m1

Proof step 10 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m1 | m, m1 | m0, ¬ prime(m1) ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Proof step 11 from proof gcdnex-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ prime(n) ↔ 1 < n ∧ (∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0)

• Proof step 13:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m1 | m0, m1 | m, ¬ 1 < m1 ∨ (∃ m. ¬(2 ≤ m ∧ prime(m) ∧ m * m ≤ m1 → m1 % m ≠ 0)) ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Used terms: m1

Proof step 12 from proof gcdnex-prime (previous step) (back to tree)

Lemma prime-prime

Proof step 13 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  m1 % m2 = 0, m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m2 ≠ 0, prime(m2), m1 | m, m1 | m0, 2 ≤ m2, m2 * m2 ≤ m1 ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Used simplifier rules: not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

Proof step 14 from proof gcdnex-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ n ≠ 0 → (m % n = 0 ↔ (∃ n0. m = n0 * n))

• Proof step 16:

  m + m0 ≠ 1, m1 ≠ 1, m1 ≠ 0, m2 ≠ 0, prime(m2), m1 | m0, m1 | m, m2 * m2 ≤ m1, 2 ≤ m2, ∃ n0. m1 = n0 * m2 ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Used terms: m2, m1

Proof step 15 from proof gcdnex-prime (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  m3 * m2 ≠ 1, m + m0 ≠ 1, m2 ≠ 0, m3 ≠ 0, prime(m2), m3 * m2 | m0, m3 * m2 | m, 2 ≤ m3, m2 ≤ m3, 2 ≤ m2 ⊦ ∃ m1. prime(m1) ∧ m1 ≠ 0 ∧ m1 ≠ 1 ∧ m1 | m ∧ m1 | m0

Rule argument

Additional information

Used simplifier rules: not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat 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) ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws)

Proof step 17 from proof gcdnex-prime (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 18:

  m3 * m2 ≠ 1, m + m0 ≠ 1, m2 ≠ 0, m3 ≠ 0, prime(m2), m3 * m2 | m, m3 * m2 | m0, 2 ≤ m2, m2 ≤ m3, 2 ≤ m3 ⊦ prime(m2) ∧ m2 ≠ 0 ∧ m2 ≠ 1 ∧ m2 | m ∧ m2 | m0

Rule argument

Additional information

Used terms: m2

Proof step 18 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  m3 * m2 ≠ 1, m + m0 ≠ 1, m2 ≠ 0, m2 ≠ 1, m3 ≠ 0, prime(m2), m3 * m2 | m, m3 * m2 | m0, 2 ≤ m2, m2 ≤ m3, 2 ≤ m3 ⊦ m2 | m0 ∧ m2 | m

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 * 1 = m0; (s)

Proof step 19 from proof gcdnex-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

• Proof step 21:

  m3 * m2 ≠ 1, m + m0 ≠ 1, m2 ≠ 0, m2 ≠ 1, m3 ≠ 0, prime(m2), m3 * m2 | m, 2 ≤ m3, m2 ≤ m3, 2 ≤ m2, ∃ n0. (m3 * m2) * n0 = m0 ⊦ m2 | m0 ∧ m2 | m

Rule argument

Additional information

Used terms: m0, m3 * m2

Proof step 20 from proof gcdnex-prime (previous step) (back to tree)

Lemma Divides

Proof step 21 from proof gcdnex-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  m3 * m2 ≠ 1, m + (m3 * m2) * m1 ≠ 1, m2 ≠ 0, m2 ≠ 1, m3 ≠ 0, prime(m2), m3 * m2 | m, 2 ≤ m2, m2 ≤ m3, 2 ≤ m3, ¬ m2 | m ⊦

Rule argument

Additional information

Used simplifier rules: divi-mult: ⊦ m | m * n0; mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult

Proof step 22 from proof gcdnex-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

Rule argument

Additional information

Used simplifier rules: divi-mult: ⊦ m | m * n0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: m, m3 * m2

Proof step 23 from proof gcdnex-prime (previous step) (back to tree)

Lemma Divides