Proof step 1 from proof max_prime_divisor-ge2 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  2 ≤ i, ¬ prime(i), ¬ 2 ≤ i / max_prime_divisor(i) ⊦

Rule argument

Additional information

Proof step 2 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i / max_prime_divisor(i) < 2, 0 < i, i / max_prime_divisor(i) < i, 2 ≤ i, 0 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 3 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) | i

• Proof step 5:

  i / max_prime_divisor(i) < i, 0 < i, i / max_prime_divisor(i) < 2, 0 ≤ i, 2 ≤ i, ¬ prime(i), ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) | i ⊦

Rule argument

Additional information

Used terms: i

Proof step 4 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Lemma max_prime_divisor-divides

Proof step 5 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 7:

  i / max_prime_divisor(i) < 2, 0 < i, i / max_prime_divisor(i) < i, 2 ≤ i, 0 ≤ i, ¬ prime(i), ¬ prime(i) ∧ 2 ≤ i → (∃ i0. max_prime_divisor(i) * i0 = i) ⊦

Rule argument

Additional information

Used terms: i, max_prime_divisor(i)

Proof step 6 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Lemma divides

Proof step 7 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  max_prime_divisor(i) * i0 = i, i / max_prime_divisor(i) < i, 0 < i, i / max_prime_divisor(i) < 2, 0 ≤ i, 2 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Proof step 8 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 9:

  max_prime_divisor(i) * i0 = i, (max_prime_divisor(i) * i0) / max_prime_divisor(i) < 2, 0 < i, (max_prime_divisor(i) * i0) / max_prime_divisor(i) < i, 2 ≤ i, 0 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Proof step 9 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  j ≠ 0 ⊦ (j * i) / j = i

• Proof step 11:

  max_prime_divisor(i) * i0 = i, max_prime_divisor(i) ≠ 0, i0 < i, 0 < i, i0 < 2, 0 ≤ i, 2 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: max_prime_divisor-not-zero: ⊦ ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) ≠ 0; Used terms: i0, max_prime_divisor(i)

Proof step 10 from proof max_prime_divisor-ge2 (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  max_prime_divisor(i) * i0 = i, i0 < 2, 0 < i, i0 < i, 2 ≤ i, 0 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: max_prime_divisor-not-zero: ⊦ ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) ≠ 0; forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs

Proof step 12 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 0 < j → (j < 2 ↔ j = 1)

• Proof step 14:

  max_prime_divisor(i) * i0 = i, i0 < i, 0 < i, i0 < 2, 0 ≤ i, 2 ≤ i, ¬ 0 < i0, ¬ prime(i) ⊦

• Proof step 20:

  max_prime_divisor(i) * i0 = i, i0 = 1, i0 < i, 0 < i, 0 < i0, 0 ≤ i, 2 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used terms: i0

Proof step 13 from proof max_prime_divisor-ge2 (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  max_prime_divisor(i) * i0 = i, i0 < i, 0 < i, i0 ≤ 0, 0 ≤ i, 2 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 15 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ 0 ≤ i ∧ 0 < j ∧ i1 < 0 → i * i1 ≠ j

• Proof step 17:

  max_prime_divisor(i) * i0 = i, 0 < i, i0 < i, 2 ≤ i, 0 ≤ i, i0 ≤ 0, ¬ prime(i) ⊦ 0 ≤ max_prime_divisor(i) ∧ 0 < i ∧ i0 < 0

Rule argument

Additional information

Used terms: i, i0, max_prime_divisor(i)

Proof step 16 from proof max_prime_divisor-ge2 (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  max_prime_divisor(i) * i0 = i, i0 < i, 0 < i, i0 ≤ 0, 0 ≤ i, 2 ≤ i, ¬ prime(i) ⊦ 0 ≤ max_prime_divisor(i) ∧ i0 < 0

Rule argument

Additional information

Proof step 18 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  max_prime_divisor(i) * i0 = i, i0 ≠ 0, 0 < i, i0 < i, 2 ≤ i, 0 ≤ i, i0 ≤ 0, ¬ prime(i) ⊦ 0 ≤ max_prime_divisor(i) ∧ i0 < 0

Rule argument

Additional information

Used simplifier rules: ⊦ i * 0 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: i0 = 0

Proof step 19 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: max_prime_divisor-nls-zero: ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ max_prime_divisor(i) < 0; ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 20 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  max_prime_divisor(i) = i, 1 < i, 0 < i, 2 ≤ i, 0 ≤ i, ¬ prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s)

Proof step 21 from proof max_prime_divisor-ge2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 22:

  ⊦ ¬ prime(i) ∧ 2 ≤ i → prime(max_prime_divisor(i))

Rule argument

Additional information

Used terms: i

Proof step 22 from proof max_prime_divisor-ge2 (previous step) (back to tree)

Lemma max_prime_divisor-prime