Proof step 1 from proof modprime (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Proof step 2 from proof modprime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ prime(n) ↔ 1 < n ∧ (∀ m. m | n → m = 1 ∨ m = n)

• Proof step 4:

  ⊦ 1 < n ∧ (∀ m. m | n → m = 1 ∨ m = n) ↔ n ≠ 0 ∧ n ≠ 1 ∧ (∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0)

Rule argument

Additional information

Used terms: n

Proof step 3 from proof modprime (previous step) (back to tree)

Lemma Prime

Proof step 4 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  n ≠ 1, n ≠ 0 ⊦ (∀ m. m | n → m = 1 ∨ m = n) ↔ (∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0)

Rule argument

Additional information

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

Proof step 5 from proof modprime (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  n ≠ 1, n ≠ 0, ∀ m. m | n → m = 1 ∨ m = n ⊦ ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0

• Proof step 10:

  n ≠ 1, n ≠ 0, ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0 ⊦ ∀ m. m | n → m = 1 ∨ m = n

Rule argument

Additional information

Proof step 6 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  n % n0 = 0, n ≠ 1, n0 ≠ 0, 2 < n, n0 < n, 2 ≤ n0, ∀ m. m | n → m = 1 ∨ m = n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 7 from proof modprime (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  n = m0 * n0 + n1, n1 = 0, n ≠ 1, n0 ≠ 0, n0 < n, 2 < n, n1 < n0, 2 ≤ n0, ∀ m. m | n → m = 1 ∨ m = n ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n, n0, m0, n1

Proof step 8 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  m0 * n0 ≠ 1, m0 ≠ 0, m0 ≠ 1, n0 ≠ 0, 2 < m0 * n0, 2 ≤ n0, ∀ m. m | m0 * n0 → m = 1 ∨ m = m0 * n0 ⊦

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 ≠ 0 → (m * n = 0 ↔ n = 0); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m0 ≠ 0 → (m0 < m0 * m ↔ 1 < m); (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m < n → n ≠ 0; (s)

Proof step 9 from proof modprime (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: divi-mult: ⊦ m | m * n0; ⊦ m * n = m ↔ m = 0 ∨ n = 1; (s) ⊦ m0 * m = 1 ↔ m0 = 1 ∧ m = 1; (ws) ⊦ m0 * 1 = m0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ m < n → n ≠ 0; (s) Used terms: m0

Proof step 10 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  n ≠ 1, n ≠ 0, n0 ≠ 1, n0 ≠ n, n0 | n, ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 11 from proof modprime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  m ≠ 0 ⊦ m | n ↔ n % m = 0

• Proof step 13:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, n0 ≠ 1, n0 ≠ n, ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: divi-zero-01: ⊦ 0 | m ↔ m = 0; Used terms: n, n0

Proof step 12 from proof modprime (previous step) (back to tree)

Lemma divi-mod

Proof step 13 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, n0 ≠ 1, n0 ≠ n, ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 14 from proof modprime (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  n = m0 * n0 + n1, n1 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, n0 ≠ 1, n0 ≠ n, n1 < n0, ∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n, n0, m0, n1

Proof step 15 from proof modprime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  m0 * n0 ≠ 1, m0 ≠ 0, m0 ≠ 1, n0 ≠ 1, n0 ≠ 0, ∀ m. 2 ≤ m ∧ m < m0 * n0 → (m0 * n0) % m ≠ 0 ⊦

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 ⊦ n + 0 = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m < n → n ≠ 0; (s) ⊦ m * n = m ↔ m = 0 ∨ n = 1; (s) ⊦ m ≠ 0 → (m * n = 0 ↔ n = 0); (s)

Proof step 16 from proof modprime (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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