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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0 ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 2^ m ≤ n ∧ n < 2^ m +1 → log2 n = m

• Proof step 5:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, 2^(log2 n + 1) ≤ 2 * n + 1 ∧ 2 * n + 1 < 2^ (log2 n + 1)+1 → log2(2 * n + 1) = log2 n + 1 ⊦

Rule argument

Additional information

Used terms: log2 n + 1, 2 * n + 1

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

Lemma Log2def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0 ⊦ 2 ^ log2 n ≤ n ∧ 2 * n + 1 < 4 * 2 ^ log2 n

Rule argument

Additional information

Used simplifier rules: lemma-ax2: ⊦ 2^(n + 1) = 2 * 2^ n; pot2-def: ⊦ 2^ m = 2 ^ m; add: ⊦ m ^ (n + n0) = m ^ n * m ^ n0; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ 2 * n ≤ 2 * m + 1 ↔ n ≤ m; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, ¬ 2 ^ log2 n ≤ n ⊦

• Proof step 13:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, ¬ 2 * n + 1 < 4 * 2 ^ log2 n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, n < 2 ^ log2 n ⊦

Rule argument

Additional information

Used simplifier rules: two-pot-zero: ⊦ 2 ^ n ≠ 0; f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  ⊦ n ≠ 0 → ¬ n < 2^ log2 n

• Proof step 10:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, n < 2 ^ log2 n, n ≠ 0 → ¬ n < 2^ log2 n ⊦

Rule argument

Additional information

Used terms: n

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

Lemma lls

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

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, n < 2 ^ log2 n, ¬ n < 2^ log2 n ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ 2^ m = 2 ^ m

Rule argument

Additional information

Used terms: log2 n

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

Lemma pot2-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, ¬ 2 * n + 1 < 4 * 2 ^ log2 n ⊦

Rule argument

Additional information

Proof step 14 from proof lsucc-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ m < n ↔ ¬ n ≤ m

• Proof step 16:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, 4 * 2 ^ log2 n ≤ 2 * n + 1 ⊦

Rule argument

Additional information

Used terms: 2 * n + 1, 4 * 2 ^ log2 n

Proof step 15 from proof lsucc-01 (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof lsucc-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, 4 * 2 ^ log2 n ≤ 2 * n + 1 ⊦

Rule argument

Additional information

Proof step 17 from proof lsucc-01 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

  ⊦ 2 * m + 1 < 2 * n ↔ m < n

• Proof step 19:

  2 * n + 1 < 2 * 2 ^ log2 n * 2 ↔ n < 2 ^ log2 n * 2, log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, 4 * 2 ^ log2 n ≤ 2 * n + 1 ⊦

Rule argument

Additional information

Used terms: n, 2 ^ log2 n * 2

Proof step 18 from proof lsucc-01 (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof lsucc-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  2 * n + 1 < 4 * 2 ^ log2 n ↔ n < 2 ^ log2 n * 2, log2(2 * n + 1) ≠ log2 n + 1, n ≠ 0, 4 * 2 ^ log2 n ≤ 2 * n + 1 ⊦

Rule argument

Additional information

Used simplifier rules: mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 20 from proof lsucc-01 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 21:

  ⊦ n < 2 * 2^ log2 n

Rule argument

Additional information

Used simplifier rules: pot2-def: ⊦ 2^ m = 2 ^ m; two-pot-zero: ⊦ 2 ^ n ≠ 0; fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ ¬ n < n; (s) Used terms: n

Proof step 21 from proof lsucc-01 (previous step) (back to tree)

Lemma ltwo-05