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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  decode(encode(i)) ≠ i ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ i < 0 → encode(i) = 2 * i→n(i) - 1

• Proof step 4:

  decode(encode(i)) ≠ i, ¬ i < 0 ⊦

• Proof step 7:

  decode(2 * i→n(i) - 1) ≠ i, i < 0 ⊦

Rule argument

Additional information

Used terms: i

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

Lemma enc-int-neg

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  decode(2 * i→n(i)) ≠ i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: enc-int-pos: ⊦ 0 ≤ i → encode(i) = 2 * i→n(i); ⊦ 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)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ n % 2 = 0 → decode(n) = n→i(n / 2)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ (m * n) % n = 0; (s) ⊦ (2 * m) / 2 = m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ 0 ≤ i → n→i(i→n(i)) = i; (s) Used terms: 2 * i→n(i)

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

Lemma dec-int-pos

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  2 * i→n(i) = m + 1, 2 * i→n(i) ≠ 0, decode(m) ≠ i, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ i→n(i) = 0 ↔ i = 0; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: 2 * i→n(i), m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  2 * i→n(i) = m + 1, decode(m) ≠ i, i ≠ 0, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ i→n(i) = 0 ↔ i = 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ n % 2 ≠ 0 → decode(n) = ~ n→i((n + 1) / 2)

• Proof step 11:

  m % 2 = 0, 2 * i→n(i) = m + 1, decode(m) ≠ i, i ≠ 0, i < 0 ⊦

• Proof step 14:

  2 * i→n(i) = m + 1, m % 2 ≠ 0, i ≠ 0, ~ n→i((m + 1) / 2) ≠ i, i < 0 ⊦

Rule argument

Additional information

Used terms: m

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

Lemma dec-int-neg

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  m % 2 = 0, 2 * i→n(i) = m + 1, i ≠ 0, n→i(m / 2) ≠ i, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: dec-int-pos: ⊦ n % 2 = 0 → decode(n) = n→i(n / 2);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ n ≠ 0 → (m % n = 0 ↔ (∃ n0. m = n0 * n))

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: 2, m

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

A spec-lemma

Proof step 14 from proof dec-int (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  2 * i→n(i) = m + 1, m % 2 ≠ 0, n→i((m + 1) / 2) + i ≠ 0, i ≠ 0, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i = j ↔ i + j = 0; (s)

Proof step 15 from proof dec-int (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  2 * i→n(i) = m + 1, m = m0 * 2 + n0, n→i((m + 1) / 2) + i ≠ 0, 2 ≠ 0, i ≠ 0, n0 ≠ 0, i < 0, n0 < 2 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: m, 2, m0, n0

Proof step 16 from proof dec-int (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  m0 + 1 = i→n(i), ~1 ≠ n→i(m0) + i, i ≠ 0, i < 0 ⊦

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 ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m * n + n = m1 * n ↔ m + 1 = m1 ∨ n = 0; (s) ⊦ m ≠ 0 → (m < 2 ↔ m = 1); (s) ⊦ n→i(m + n) = n→i(m) + n→i(n); (s) ⊦ (2 * m + n + 1) / 2 = m + (n + 1) / 2; (s)

Proof step 17 from proof dec-int (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 18:

  m0 + 1 = i→n(i), ~1 ≠ n→i(m0) + i, i ≠ 0, n→i(m0 + 1) ≠ n→i(i→n(i)), i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n→i(n + 1) = n→i(n) + 1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ i < 0 → n→i(i→n(i)) = ~ i; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = 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 formulas: n→i(m0 + 1) = n→i(i→n(i))

Proof step 18 from proof dec-int (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information