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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ prime(43) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 1 < j → (prime(j) ↔ (∀ i. 1 < i ∧ i * i ≤ j → j % i ≠ 0))

• Proof step 4:

  1 < 43, ∃ i. ¬(1 < i ∧ i * i ≤ 43 → 43 % i ≠ 0) ⊦

Rule argument

Additional information

Used terms: 43

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

Lemma prime-def-mod

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  43 % i = 0, 0 < i, 1 < i, i * i ≤ 43 ⊦

Rule argument

Additional information

Used simplifier rules: 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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  43 % i = 0, 1 < i, 0 < i, i * i ≤ 43, ¬ 7 * 7 ≤ i * i ⊦

Rule argument

Additional information

Used simplifier rules: associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult 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 Used formulas: 7 * 7 ≤ i * i

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ i * i ≤ j * j ↔ abs(i) ≤ abs(j)

• Proof step 8:

  43 % i = 0, 0 < i, 1 < i, i * i ≤ 43, ¬ abs(7) ≤ abs(i) ⊦

Rule argument

Additional information

Used terms: i, 7

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  43 % i = 0, 1 < i, 0 < i, i < 7, i * i ≤ 43 ⊦

Rule argument

Additional information

Used simplifier rules: forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 1 < i → abs(i) = i; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ i ≠ j -1 → (i < j ↔ i < j -1)

• Proof step 11:

  43 % i = 0, i ≠ 7 -1, i < 7 -1, 0 < i, 1 < i, i * i ≤ 43 ⊦

Rule argument

Additional information

Used terms: 7, i

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  43 % i = 0, i ≠ 6, 1 < i, 0 < i, i < 6, i * i ≤ 43 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ i ≠ j -1 → (i < j ↔ i < j -1)

• Proof step 14:

  43 % i = 0, i ≠ 6 -1, i ≠ 6, i < 6 -1, 0 < i, 1 < i, i * i ≤ 43 ⊦

Rule argument

Additional information

Used terms: 6, i

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  43 % i = 0, i ≠ 6, i ≠ 5, 1 < i, 0 < i, i < 5, i * i ≤ 43 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ i < j ↔ i +1 = j ∨ i +1 < j

• Proof step 17:

  43 % i = 0, i ≠ 6, i ≠ 5, 0 < i, 1 < i, i * i ≤ 43, i +1 = 5 ∨ i +1 < 5 ⊦

Rule argument

Additional information

Used terms: 5, i

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

A spec-lemma

Proof step 17 from proof prime-43 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  43 % i = 0, 4 ≠ i, i ≠ 5, i ≠ 6, 0 < i, 1 < i, i < 4, i * i ≤ 43 ⊦

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i +1 = i + 1; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s)

Proof step 18 from proof prime-43 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ i ≠ j -1 → (i < j ↔ i < j -1)

• Proof step 20:

  43 % i = 0, 4 ≠ i, i ≠ 4 -1, i ≠ 5, i ≠ 6, i < 4 -1, 1 < i, 0 < i, i * i ≤ 43 ⊦

Rule argument

Additional information

Used terms: 4, i

Proof step 19 from proof prime-43 (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof prime-43 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  43 % i = 0, 4 ≠ i, i ≠ 5, i ≠ 6, i ≠ 3, 0 < i, 1 < i, i < 3, i * i ≤ 43 ⊦

Rule argument

Additional information

Proof step 21 from proof prime-43 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ i ≠ j -1 → (i < j ↔ i < j -1)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j → (j < 2 ↔ j = 1); (s) ⊦ i = 1 → j % i = 0; (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 forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs Used terms: 3, i

Proof step 22 from proof prime-43 (previous step) (back to tree)

A spec-lemma