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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  max_prime_divisor(i) < max_prime_divisor(i / max_prime_divisor(i)), 0 < i, 2 ≤ i, 0 ≤ i, ¬ prime(i), ¬ prime(i / max_prime_divisor(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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ¬ prime(i) ∧ 2 ≤ i → (∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i))

• Proof step 5:

  0 < i, max_prime_divisor(i) < max_prime_divisor(i / max_prime_divisor(i)), 0 ≤ i, 2 ≤ i, ¬ prime(i), ¬ prime(i / max_prime_divisor(i)), ¬ prime(i) ∧ 2 ≤ i → (∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)) ⊦

Rule argument

Additional information

Used terms: i

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

Lemma prime-ex-max

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ j | i ∧ prime(j) ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i) → max_prime_divisor(i) = j

• Proof step 8:

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

Rule argument

Additional information

Used terms: j, i

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

Lemma max_prime_divisor-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ¬ prime(i) ∧ 2 ≤ i → (∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i))

• Proof step 11:

  0 < i, j < max_prime_divisor(i / j), j < i, prime(j), j | i, 0 ≤ i, 2 ≤ i, ¬ prime(i), ¬ prime(i / j), ¬ prime(i / j) ∧ 2 ≤ i / j → (∃ j0. prime(j0) ∧ j0 | i / j ∧ j0 < i / j ∧ (∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j)), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦

Rule argument

Additional information

Used terms: i / j

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

Lemma prime-ex-max

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  j < i, j < max_prime_divisor(i / j), 0 < i, prime(j), j | i, 2 ≤ i, 0 ≤ i, ¬ prime(i), ¬ prime(i / j), 2 ≤ i / j → prime(j0) ∧ j0 | i / j ∧ j0 < i / j ∧ (∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  0 < i, j < max_prime_divisor(i / j), j < i, prime(j), j | i, 0 ≤ i, 2 ≤ i, 2 ≤ i / j, ¬ prime(i), ¬ prime(i / j), 2 ≤ i / j → prime(j0) ∧ j0 | i / j ∧ j0 < i / j ∧ (∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦

• Proof step 24:

  0 < i, j < max_prime_divisor(i / j), j < i, prime(j), j | i, 0 ≤ i, 2 ≤ i, ¬ prime(i), ¬ prime(i / j), ¬ 2 ≤ i / j, 2 ≤ i / j → prime(j0) ∧ j0 | i / j ∧ j0 < i / j ∧ (∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦

Rule argument

Additional information

Used formulas: 2 ≤ i / j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  j < i, j < max_prime_divisor(i / j), 0 < i, j0 < i / j, 0 < i / j, prime(j), prime(j0), j | i, j0 | i / j, 2 ≤ i / j, 2 ≤ i, 0 ≤ i, 0 ≤ i / j, ¬ prime(i), ¬ prime(i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i, ∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j ⊦

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 i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ j | i ∧ prime(j) ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i) → max_prime_divisor(i) = j

• Proof step 16:

  0 < i / j, 0 < i, j < j0, j < i, j0 < i / j, prime(j), prime(j0), j | i, j0 | i / j, 0 ≤ i / j, 0 ≤ i, 2 ≤ i, 2 ≤ i / j, ¬ prime(i), ¬ prime(i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i, ∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j ⊦

Rule argument

Additional information

Used terms: j0, i / j

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

Lemma max_prime_divisor-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  j0 < i / j, j < i, j < j0, 0 < i, 0 < i / j, prime(j0), prime(j), j0 | i / j, j | i, 2 ≤ i / j, 2 ≤ i, 0 ≤ i, 0 ≤ i / j, ¬ prime(i), ¬ prime(i / j), ∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j, ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  0 < i / j, 0 < i, j < j0, j < i, j0 < i / j, prime(j), prime(j0), j0 | i / j, 0 ≤ i / j, 0 ≤ i, 2 ≤ i, 2 ≤ i / j, ¬ prime(i), ¬ prime(i / j), ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i, ∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j, ∃ i0. j * i0 = i ⊦

Rule argument

Additional information

Used terms: i, j

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

Lemma divides

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  0 < i0, j < j0, j0 < i0, 0 < j0, 1 < j0, 0 < j, prime(j0), prime(j), j0 | i0, 0 ≤ j, 0 ≤ i0, 2 ≤ i0, 2 ≤ j * i0, ¬ prime(j * i0), ¬ prime(i0), ∀ j0. j < j0 ∧ j0 < j * i0 ∧ prime(j0) → ¬ j0 | j * i0, ∀ j1. j0 < j1 ∧ j1 < i0 ∧ prime(j1) → ¬ j1 | i0 ⊦

Rule argument

Additional information

Used simplifier rules: prime-not-neg-01: ⊦ j ≤ 0 → ¬ prime(j); i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 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 j ≠ 0 ⊦ (i * j) / j = i; (s) ⊦ i * 0 = 0; (s) ⊦ 0 < i → (i < i * j ↔ 1 < j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  0 < j, 1 < j0, 0 < j0, j0 < i0, j < j0, 0 < i0, prime(j), prime(j0), 2 ≤ j * i0, 2 ≤ i0, 0 ≤ i0, 0 ≤ j, ¬ prime(j * i0), ¬ prime(i0), ∀ j1. j0 < j1 ∧ j1 < i0 ∧ prime(j1) → ¬ j1 | i0, ∀ j0. j < j0 ∧ j0 < j * i0 ∧ prime(j0) → ¬ j0 | j * i0, ∃ i1. j0 * i1 = i0 ⊦

Rule argument

Additional information

Used terms: i0, j0

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

Lemma divides

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  j < j0, 0 < j, 1 < j0, 0 < j0, 1 < i1, 0 < i1, prime(j), prime(j0), 0 ≤ i1, 2 ≤ j * j0 * i1, 2 ≤ j0 * i1, 0 ≤ j, ¬ prime(j0 * i1), ¬ prime(j * j0 * i1), ∀ j1. j0 < j1 ∧ j1 < j0 * i1 ∧ prime(j1) → ¬ j1 | j0 * i1, ∀ j1. j < j1 ∧ j1 < j * j0 * i1 ∧ prime(j1) → ¬ j1 | j * j0 * i1 ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) 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-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ 0 < i → (i < i * j ↔ 1 < j); (s)

Proof step 23 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: div-mult: ⊦ i | i * j; ⊦ 0 < i → (i < i * j ↔ 1 < j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 1 < j → (i * j ≤ 1 ↔ i ≤ 0); (s) ⊦ i < j → (j ≤ i ↔ false); (as) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0

Proof step 24 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

Used simplifier rules: prime-small: ⊦ j < 2 → ¬ prime(j); j0 ≠ 0, j ≤ j0 ⊦ i < (* j) → i < (* j0); (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs

Proof step 25 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

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

Rule argument

Additional information

Used terms: i, j

Proof step 26 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

Lemma divides

Proof step 27 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  j < j * i0, i0 < 2, j < max_prime_divisor(i0), 0 < j * i0, i0 < j * i0, prime(j), 2 ≤ j * i0, 0 ≤ j * i0, ¬ prime(j * i0), ∀ j0. j < j0 ∧ j0 < j * i0 ∧ prime(j0) → ¬ j0 | j * i0 ⊦

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 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult j ≠ 0 ⊦ (i * j) / j = i; (s) ⊦ i * 0 = 0; (s)

Proof step 28 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ 0 < i → (i < i * j ↔ 1 < j)

Rule argument

Additional information

Used simplifier rules: prime-not-neg: ⊦ j < 0 → ¬ prime(j); ⊦ 0 < j → (j < 2 ↔ j = 1); (s) ⊦ i = 1 → i * j = j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ¬ i < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) ⊦ i ≤ 0 → (0 < i * j ↔ j < 0 ∧ i ≠ 0); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < 0 → (0 ≤ i * j ↔ j ≤ 0); (s) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: j, i0

Proof step 29 from proof max_prime_divisor-nls-02 (previous step) (back to tree)

A spec-lemma