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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  4 ^ i ≤ i * i, 0 ≤ i ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  4 ^ i ≤ i * i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs

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

User applied rule induction

And obtained the following new goals

• Proof step 4:

  4 ^ i ≤ i * i, 0 ≤ i, ∀ i0. i→n(i0) < i→n(i) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  0 ≤ i, 4 ^ i ≤ i * i, ∀ i0. i→n(i0) < i→n(i) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

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

User applied rule apply induction

And obtained the following new goals

• Proof step 6:

  4 ^ i ≤ i * i, 0 ≤ i, ∀ i0. i→n(i0) < i→n(i) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦ 4 ^ (i - 1) ≤ (i - 1) * (i - 1) ∧ 0 ≤ i - 1

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 ↔ i = j); (s) Used terms: i - 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  0 ≤ i, 4 ^ i ≤ i * i, ∀ i0. i→n(i0) < i→n(i) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦ 4 ^ (i - 1) ≤ (i - 1) * (i - 1) ∧ 0 < i

Rule argument

Additional information

Used simplifier rules: ⊦ 1 ≤ i ↔ 0 < i; (s) 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 7 from proof pot-square-est-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  i = i1 + 1, 4 ^ i ≤ i * i, 0 ≤ i, ∀ i0. i→n(i0) < i→n(i) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦ 4 ^ i1 ≤ i1 * i1 ∧ 0 < i

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: Pot-neg: ⊦ i < 0 → j ^ i = 1 / j ^ abs(i); ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (s) ⊦ i < 0 → abs(i) = ~ i; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i1, 4

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

Lemma succ

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 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 formulas: i1 * i1 * 4 < 4 ^ i1 * 4

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

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

Proof step 14 from proof pot-square-est-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  (i1 + 1) * (i1 + 1) = i1 * i1 + 2 * i1 + 1, i1 * i1 * 4 < (i1 + 1) * (i1 + 1), i1 * i1 < 4 ^ i1, i1 * i1 * 4 < 4 ^ i1 * 4, 0 ≤ i1, 4 ^ i1 * 4 ≤ (i1 + 1) * (i1 + 1), ∀ i0. i→n(i0) < i→n(i1 + 1) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

• Proof step 18:

  (i1 + 1) * (i1 + 1) ≠ i1 * i1 + 2 * i1 + 1, i1 * i1 * 4 < (i1 + 1) * (i1 + 1), i1 * i1 < 4 ^ i1, i1 * i1 * 4 < 4 ^ i1 * 4, 0 ≤ i1, 4 ^ i1 * 4 ≤ (i1 + 1) * (i1 + 1), ∀ i0. i→n(i0) < i→n(i1 + 1) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

Used formulas: (i1 + 1) * (i1 + 1) = i1 * i1 + 2 * i1 + 1

Proof step 15 from proof pot-square-est-01 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 16:

  i1 * i1 * 4 < 4 ^ i1 * 4, i1 * i1 < 4 ^ i1, i1 * i1 * 4 < i1 * i1 + 2 * i1 + 1, 4 ^ i1 * 4 ≤ i1 * i1 + 2 * i1 + 1, 0 ≤ i1, ∀ i0. i→n(i0) < i→n(i1 + 1) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

Proof step 16 from proof pot-square-est-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 17:

  i1 * i1 * 4 < i1 * i1 + 2 * i1 + 1, i1 * i1 < 4 ^ i1, i1 * i1 * 4 < 4 ^ i1 * 4, i1 * i1 * 3 < 2 * i1 + 1, 0 ≤ i1, 4 ^ i1 * 4 ≤ i1 * i1 + 2 * i1 + 1, ∀ i0. i→n(i0) < i→n(i1 + 1) → 4 ^ i0 ≤ i0 * i0 ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ls-forward: ⊦ i * j < i * j0 → i ≠ 0; (forward) from specification int-mult ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0); (s) ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ (* i2) * i ≤ i + j0 ↔ (i2 - 1) * i ≤ j0; (s) ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 ≤ (* j) ↔ i0 ≤ j / i); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: i1 * i1 * 3 < 2 * i1 + 1

Proof step 17 from proof pot-square-est-01 (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 ≤ (* j) ↔ i0 ≤ j / i); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: i1 = 0

Proof step 18 from proof pot-square-est-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 1 * i = i; (s) ⊦ i * j + i = i * (j + 1); (s) ⊦ i * j + i * j0 = i * (j + j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + j = i + i0 ↔ j = i0; (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: i1 + 1, 1, i1

Proof step 19 from proof pot-square-est-01 (previous step) (back to tree)

A spec-lemma