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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (i ^ j) ^ j0 ≠ i ^ (j * j0), 0 ≤ j0, 0 ≤ j, 0 ≤ i ⊦

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 3:

  (i ^ j) ^ j0 ≠ i ^ (j * j0), 0 ≤ j0, 0 ≤ j, 0 ≤ i, ∀ j, i, j1. i→n(j) < i→n(j0) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  (i ^ j) ^ j0 ≠ i ^ (j * j0), 0 ≤ i, 0 ≤ j, 0 ≤ j0, ∀ j, i, j1. i→n(j) < i→n(j0) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 6:

  (i ^ j) ^ j0 -1 * i ^ j ≠ i ^ (j * j0), 0 < j0, 0 ≤ j0, 0 ≤ j, 0 ≤ i, ∀ j, i, j1. i→n(j) < i→n(j0) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ 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 terms: j0, i ^ j

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

Lemma Pot-pos

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  j0 = i0 +1, (i ^ j) ^ i0 * i ^ j ≠ i ^ (j * j0), 0 < j0, 0 ≤ i, 0 ≤ j, 0 ≤ j0, ∀ j, i, j1. i→n(j) < i→n(j0) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i = j -1 ↔ j = i +1; (elim) Used terms: j0, i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (i ^ j) ^ i0 * i ^ j ≠ i ^ (j * (i0 + 1)), ~1 ≤ i0, 0 ≤ j, 0 ≤ i, 0 ≤ i0, ∀ j, i, j1. i→n(j) < i→n(i0 +1) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

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 ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i +1 = i + 1; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s)

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

User applied rule apply induction

And obtained the following new goals

• Proof step 9:

  (i ^ j) ^ i0 * i ^ j ≠ i ^ (j * (i0 + 1)), 0 ≤ i0, 0 ≤ i, 0 ≤ j, ~1 ≤ i0, ∀ j, i, j1. i→n(j) < i→n(i0 +1) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦ (i ^ j) ^ i0 ≠ i ^ (j * i0) ∧ 0 ≤ i0 ∧ 0 ≤ j ∧ 0 ≤ i

Rule argument

Additional information

Used simplifier rules: ⊦ i +1 = i + 1; (s) ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ ¬ i < i; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: i0, i, j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (i ^ j) ^ i0 = i ^ (j * i0), i ^ (j * i0) * i ^ j ≠ i ^ (j * (i0 + 1)), ~1 ≤ i0, 0 ≤ j, 0 ≤ i, 0 ≤ i0, ∀ j, i, j1. i→n(j) < i→n(i0 +1) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ (* i0) * i + i = (i0 + 1) * i

• Proof step 12:

  (i ^ j) ^ i0 = i ^ (j * i0), i ^ (j * i0) * i ^ j ≠ i ^ (i0 * j + j), 0 ≤ i0, 0 ≤ i, 0 ≤ j, ~1 ≤ i0, ∀ j, i, j1. i→n(j) < i→n(i0 +1) → (i ^ j1) ^ j ≠ i ^ (j1 * j) ∧ 0 ≤ j ∧ 0 ≤ j1 ∧ 0 ≤ i → false ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, i0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 0 ≤ j ∧ 0 ≤ j0 → i ^ (j + j0) = i ^ j * i ^ j0

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i * j + i = i * (j + 1); (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult Used terms: j, i0 * j, i

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

Lemma pot-dist-pos