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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  0 < i, 2 ≤ i, 0 ≤ i, ¬ prime(i) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | 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 prime-ex-max (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 1 < i → (prime(i) ↔ (∀ j. prime(j) ∧ j * j ≤ i → ¬ j | i))

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) Used terms: i

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

Lemma prime-def-prime

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ 0 < i → (i * j ≤ i ↔ j ≤ 1); (s) ⊦ 0 < i → (i ≤ 1 ↔ i = 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 ≤ j → (j ≤ i ↔ i = j); (s) Used formulas: j < i

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

User applied rule weakening

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 9:

  j < i, 0 < i, prime(j), j | i, 2 ≤ i, 0 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: i→n(i - j)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  0 < i, j < i, prime(j), j | i, 0 ≤ i, 2 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  j < i, 0 < i, prime(j), j | i, 2 ≤ i, 0 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i), prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

Used terms: j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  0 < i, j < i, j < j0, j0 < i, prime(j), prime(j0), j | i, j0 | i, 0 ≤ i, 2 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  j0 < i, j < j0, 0 < i, j < i, prime(j0), prime(j), j0 | i, j | i, 2 ≤ i, 0 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

Used formulas: j < i

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  j < i, 0 < i, j < j0, j0 < i, prime(j), prime(j0), j | i, j0 | i, 0 ≤ i, 2 ≤ i, ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

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

User applied rule apply induction

And obtained the following new goals

• Proof step 15:

  j0 < i, j < j0, 0 < i, j < i, prime(j0), prime(j), j0 | i, j | i, 2 ≤ i, 0 ≤ i, ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i), ∀ i0, j0. i→n(i0 - j0) < i→n(i - j) → j0 < i0 ∧ 0 < i0 ∧ prime(j0) ∧ j0 | i0 ∧ 2 ≤ i0 ∧ 0 ≤ i0 → (∃ j. prime(j) ∧ j | i0 ∧ j < i0 ∧ (∀ j0. j < j0 ∧ j0 < i0 ∧ prime(j0) → ¬ j0 | i0)) ⊦ ∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s) ⊦ j < i → abs(i - j) = i - j; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i < j - i0 ↔ i + i0 < j; (s) ⊦ i + j < i + i0 ↔ j < i0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: i, j0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: j1