Proof step 1 from proof prime-smallest (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 * m ≤ n → n % m ≠ 0)

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

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

• Proof step 5:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n), 2 ≤ n0, n0 * n0 ≤ n ⊦

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ¬ prime(n), 2 ≤ n ⊦ ∃ m. m | n ∧ prime(m) ∧ m * m ≤ n

• Proof step 8:

  n ≠ 1, n ≠ 0, ¬ prime(n), ∀ m. 2 ≤ m ∧ m * m ≤ n → n % m ≠ 0, ∃ m. m | n ∧ prime(m) ∧ m * m ≤ n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m ≠ 0 → (m < 2 ↔ m = 1); (s) Used terms: n

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

Lemma not-prime

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  n ≠ 1, n ≠ 0, prime(n0), n0 | n, n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n0), n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: divi-zero-01: ⊦ 0 | m ↔ m = 0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ 0 ≤ m; (s) Used terms: n, n0

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

Lemma divi-mod

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n0), n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  n = m0 * n0 + n1, n1 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, n1 < n0, prime(n0), n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ 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 13 from proof prime-smallest (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: mult-02: ⊦ prime(m) → (prime(m * n) ↔ n = 1); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) 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) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m ≠ 0 → (m * n = 0 ↔ n = 0); (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used terms: m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: one: ⊦ ¬ prime(1); ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m < n → m ≤ n; (s) n ≠ 0 ⊦ (m * n) % n = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m ≠ 0 → (m < 2 ↔ m = 1); (s) ⊦ m0 * m = 1 ↔ m0 = 1 ∧ m = 1; (ws) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) Used terms: n0