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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(2 ^ i ≤ 1 ↔ i < 1) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(2 ^ i ≤ 1 ↔ i < 1) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  2 ^ i ≤ 1, ¬ i < 1 ⊦

• Proof step 9:

  i < 1, ¬ 2 ^ i ≤ 1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1

• Proof step 6:

  2 ^ i ≤ 1, ¬ i < 1 ⊦ 1 < 2 ∧ 0 < i

Rule argument

Additional information

Used terms: i, 2

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

Lemma notone

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  2 ^ i ≤ 1, 1 ≤ i, i ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ i ≤ j ↔ ¬ j < i

Rule argument

Additional information

Used simplifier rules: notone: ⊦ 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1; ⊦ 1 ≤ i ↔ 0 < i; (s) Used terms: 0, i

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  i < 1, 1 < 2 ^ i, 2 ≤ 2 ^ i ⊦

Rule argument

Additional information

Used simplifier rules: numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (forward) from specification int-abs numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ i < 0 → 2 ^ i = 0

• Proof step 12:

  1 < 2 ^ i, i < 1, 2 ≤ 2 ^ i, ¬ i < 0 ⊦

Rule argument

Additional information

Used terms: i

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

Lemma two-minus

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  i < 1, 1 < 2 ^ i, 2 ≤ 2 ^ i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ i ≤ j ↔ ¬ j < i

Rule argument

Additional information

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

Proof step 14 from proof two-leone (previous step) (back to tree)

A spec-lemma