Proof step 1 from proof exinpot (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  1 < i, 0 < j ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j ∧ j < i ^ (i0 + 1)

Rule argument

Additional information

Proof step 2 from proof exinpot (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  1 < i, 0 < j, ∀ j0, i. i→n(j0) < i→n(j) → 1 < i ∧ 0 < j0 → (∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j0 ∧ j0 < i ^ (i0 + 1)) ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j ∧ j < i ^ (i0 + 1)

Rule argument

Additional information

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

Proof step 3 from proof exinpot (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: succ: ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j; 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 add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2

Proof step 4 from proof exinpot (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 5:

  1 < i, 0 < i, 0 < j, ∀ j0, i. i→n(j0) < i→n(j) → 1 < i ∧ 0 < j0 → (∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j0 ∧ j0 < i ^ (i0 + 1)) ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j ∧ j < i ^ i0 * i, 1 < i ∧ 0 < j - 1

• Proof step 7:

  1 < i, 0 < i, 0 < j, ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j - 1 ∧ j - 1 < i ^ (i0 + 1), ∀ j0, i. i→n(j0) < i→n(j) → 1 < i ∧ 0 < j0 → (∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j0 ∧ j0 < i ^ (i0 + 1)) ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j ∧ j < i ^ i0 * i

Rule argument

Additional information

Used simplifier rules: ⊦ i→n(i - 1) < i→n(i) ↔ 0 < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: j - 1, i

Proof step 5 from proof exinpot (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  1 < i, 0 < i, ∀ j0, i. i→n(j0) < i→n(1) → 1 < i ∧ 0 < j0 → (∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j0 ∧ j0 < i ^ (i0 + 1)) ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ 1 ∧ 1 < i ^ i0 * i

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < j - i0 ↔ i + i0 < j; (s)

Proof step 6 from proof exinpot (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; ⊦ 1 * i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 0

Proof step 7 from proof exinpot (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: succ: ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j; commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs i0 ≠ 0, i0 ≤ i ⊦ (* i) < j → (* i0) < j; (s) ⊦ 0 < i → (i < i * j ↔ 1 < 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 add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + 1 ≤ j ↔ i < j; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s)

Proof step 8 from proof exinpot (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used terms: i0

Proof step 9 from proof exinpot (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  1 < i ^ i0 * i, 0 < i ^ i0, 0 < i, 1 < i, 0 ≤ i0, ∀ j0, i1. i→n(j0) < i→n(i ^ i0 * i) → 1 < i1 ∧ 0 < j0 → (∃ i0. 0 ≤ i0 ∧ i1 ^ i0 ≤ j0 ∧ j0 < i1 ^ (i0 + 1)) ⊦ ∃ i1. 0 ≤ i1 ∧ i ^ i1 ≤ i ^ i0 * i ∧ i0 < i1

Rule argument

Additional information

Used simplifier rules: ls-pos: ⊦ 1 < i ∧ 0 ≤ j → (i ^ j < i ^ j0 ↔ j < j0); commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) < j → (* i0) < j; (s) ⊦ 0 < i → (i < i * j ↔ 1 < j); (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ i ≤ i; (s) ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ 0 < i → (i ≤ i * j ↔ 1 ≤ j); (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → ¬ j < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)

Proof step 10 from proof exinpot (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

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