Proof step 1 from proof lst-02 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(j < i ↔ i ≠ j), ¬ i < j ⊦

Rule argument

Additional information

Proof step 2 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i ≠ j, ¬ i < j, ¬ j < i ⊦

Rule argument

Additional information

Proof step 3 from proof lst-02 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  0 ≠ j, ¬ 0 < j, ¬ j < 0 ⊦

• Proof step 23:

  i0 +1 ≠ j, ¬ i0 +1 < j, ¬ j < i0 +1, ∀ j. ¬(i0 ≠ j ∧ ¬ i0 < j ∧ ¬ j < i0) ⊦

• Proof step 34:

  i0 -1 ≠ j, ¬ i0 -1 < j, ¬ j < i0 -1, ∀ j. ¬(i0 ≠ j ∧ ¬ i0 < j ∧ ¬ j < i0) ⊦

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ;

Proof step 4 from proof lst-02 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  0 ≠ j0 +1, ¬ 0 < j0 +1, ¬ j0 +1 < 0 ⊦ 0 ≠ j0 ∧ ¬ 0 < j0 ∧ ¬ j0 < 0

• Proof step 11:

  0 ≠ j0 -1, ¬ 0 < j0 -1, ¬ j0 -1 < 0 ⊦ 0 ≠ j0 ∧ ¬ 0 < j0 ∧ ¬ j0 < 0

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ;

Proof step 5 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  0 ≠ j0, j0 ≠ ~1, ¬ j0 +1 < 0, ¬ 0 < j0 +1 ⊦ ¬ j0 < 0 ∧ ¬ 0 < j0

Rule argument

Additional information

Used simplifier rules: numeral: ⊦ i +1 = (* j) ↔ i = j -1;

Proof step 6 from proof lst-02 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  0 ≠ j0, j0 ≠ ~1, j0 < 0, ¬ j0 +1 < 0, ¬ 0 < j0 +1 ⊦

• Proof step 9:

  0 ≠ j0, j0 ≠ ~1, 0 < j0, ¬ j0 +1 < 0, ¬ 0 < j0 +1 ⊦

Rule argument

Additional information

Proof step 7 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ i < j ↔ i +1 = j ∨ i +1 < j

Rule argument

Additional information

Used simplifier rules: numeral: ⊦ i +1 = (* j) ↔ i = j -1; Used terms: 0, j0

Proof step 8 from proof lst-02 (previous step) (back to tree)

Lemma lsrec

Proof step 9 from proof lst-02 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ i < j ∧ j < j0 → i < j0

Rule argument

Additional information

Used simplifier rules: ls-succ-01: ⊦ i < i +1; Used terms: 0, j0, j0 +1

Proof step 10 from proof lst-02 (previous step) (back to tree)

Lemma trans

Proof step 11 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  1 ≠ j0, 0 ≠ j0, ¬ j0 -1 < 0, ¬ 0 < j0 -1 ⊦ ¬ j0 < 0 ∧ ¬ 0 < j0

Rule argument

Additional information

Used simplifier rules: pred: ⊦ i = j -1 ↔ i +1 = j;

Proof step 12 from proof lst-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  ⊦ i = j -1 ↔ j = i +1

• Proof step 14:

  j0 = i +1, 1 ≠ j0, 0 ≠ j0, ¬ i < 0, ¬ 0 < i ⊦ ¬ j0 < 0 ∧ ¬ 0 < j0

Rule argument

Additional information

Used terms: j0, i

Proof step 13 from proof lst-02 (previous step) (back to tree)

Lemma elim-pred

Proof step 14 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  i ≠ 0, i ≠ ~1, ¬ i < 0, ¬ 0 < i ⊦ ¬ i +1 < 0 ∧ ¬ 0 < i +1

Rule argument

Additional information

Used simplifier rules: numeral: ⊦ i +1 = (* j) ↔ i = j -1;

Proof step 15 from proof lst-02 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  i ≠ 0, i ≠ ~1, i +1 < 0, ¬ i < 0, ¬ 0 < i ⊦

• Proof step 18:

  i ≠ 0, i ≠ ~1, 0 < i +1, ¬ i < 0, ¬ 0 < i ⊦

Rule argument

Additional information

Proof step 16 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ i < j ↔ i +1 = j ∨ i +1 < j

Rule argument

Additional information

Used terms: 0, i

Proof step 17 from proof lst-02 (previous step) (back to tree)

Lemma lsrec

Proof step 18 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ i < j ↔ i +1 = j ∨ i +1 < j

• Proof step 20:

  i ≠ 0, i ≠ ~1, ¬ i < 0, ¬ 0 < i, 0 +1 = i +1 ∨ 0 +1 < i +1 ⊦

Rule argument

Additional information

Used terms: i +1, 0

Proof step 19 from proof lst-02 (previous step) (back to tree)

Lemma lsrec

Proof step 20 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  i ≠ 0, i ≠ ~1, 1 < i +1, ¬ i < 0, ¬ 0 < i ⊦

Rule argument

Additional information

Used simplifier rules: numeral: ⊦ i +1 = (* j) ↔ i = j -1;

Proof step 21 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ 1 < i ↔ 0 < i -1

Rule argument

Additional information

Used simplifier rules: succpred: ⊦ i +1 -1 = i; Used terms: i +1

Proof step 22 from proof lst-02 (previous step) (back to tree)

Lemma one-less

Proof step 23 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  i0 +1 ≠ j, ¬ i0 +1 < j, ¬ j < i0 +1, ∀ j0. i0 = j0 ∨ i0 < j0 ∨ j0 < i0 ⊦

Rule argument

Additional information

Proof step 24 from proof lst-02 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 25:

  i0 +1 ≠ j, ¬ i0 +1 < j, ¬ j < i0 +1, i0 = j -1 ∨ i0 < j -1 ∨ j -1 < i0 ⊦

Rule argument

Additional information

Used terms: j -1

Proof step 25 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  i0 +1 ≠ j, ¬ i0 +1 < j, ¬ j < i0 +1, i0 < j -1 ∨ j -1 < i0 ⊦

Rule argument

Additional information

Used simplifier rules: pred: ⊦ i = j -1 ↔ i +1 = j;

Proof step 26 from proof lst-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

  ⊦ i = j -1 ↔ j = i +1

• Proof step 28:

  j = i +1, i0 +1 ≠ j, ¬ i0 +1 < j, ¬ j < i0 +1, i0 < i ∨ i < i0 ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 27 from proof lst-02 (previous step) (back to tree)

Lemma elim-pred

Proof step 28 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  i0 ≠ i, ¬ i0 +1 < i +1, ¬ i +1 < i0 +1, i0 < i ∨ i < i0 ⊦

Rule argument

Additional information

Used simplifier rules: succ-in: ⊦ i +1 = j +1 ↔ i = j;

Proof step 29 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ i +1 < j ↔ i < j -1

• Proof step 31:

  i0 ≠ i, ¬ i0 +1 < i +1, ¬ i < i0 +1 -1, i0 < i ∨ i < i0 ⊦

Rule argument

Additional information

Used terms: i0 +1, i

Proof step 30 from proof lst-02 (previous step) (back to tree)

Lemma lssucc

Proof step 31 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  i0 ≠ i, i0 < i, ¬ i0 +1 < i +1 ⊦

Rule argument

Additional information

Used simplifier rules: succpred: ⊦ i +1 -1 = i; ls-01: ⊦ i < j → ¬ j < i;

Proof step 32 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ i +1 < j ↔ i < j -1

Rule argument

Additional information

Used simplifier rules: succpred: ⊦ i +1 -1 = i; Used terms: i +1, i0

Proof step 33 from proof lst-02 (previous step) (back to tree)

Lemma lssucc

Proof step 34 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  j +1 ≠ i0, ¬ i0 -1 < j, ¬ j < i0 -1, ∀ j0. i0 = j0 ∨ i0 < j0 ∨ j0 < i0 ⊦

Rule argument

Additional information

Used simplifier rules: pred: ⊦ i = j -1 ↔ i +1 = j;

Proof step 35 from proof lst-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  ⊦ i = j -1 ↔ j = i +1

• Proof step 37:

  i0 = i +1, j +1 ≠ i0, ¬ i < j, ¬ j < i, ∀ j0. i0 = j0 ∨ i0 < j0 ∨ j0 < i0 ⊦

Rule argument

Additional information

Used terms: i0, i

Proof step 36 from proof lst-02 (previous step) (back to tree)

Lemma elim-pred

Proof step 37 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  j ≠ i, ¬ i < j, ¬ j < i, ∀ j0. i +1 = j0 ∨ i +1 < j0 ∨ j0 < i +1 ⊦

Rule argument

Additional information

Used simplifier rules: succ-in: ⊦ i +1 = j +1 ↔ i = j;

Proof step 38 from proof lst-02 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 39:

  j ≠ i, ¬ i < j, ¬ j < i, i +1 = j +1 ∨ i +1 < j +1 ∨ j +1 < i +1 ⊦

Rule argument

Additional information

Used terms: j +1

Proof step 39 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  j ≠ i, ¬ i < j, ¬ j < i, i +1 < j +1 ∨ j +1 < i +1 ⊦

Rule argument

Additional information

Used simplifier rules: succ-in: ⊦ i +1 = j +1 ↔ i = j;

Proof step 40 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ i +1 < j ↔ i < j -1

• Proof step 42:

  j ≠ i, ¬ i < j, ¬ j < i, i < j +1 -1 ∨ j +1 < i +1 ⊦

Rule argument

Additional information

Used terms: j +1, i

Proof step 41 from proof lst-02 (previous step) (back to tree)

Lemma lssucc

Proof step 42 from proof lst-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  j ≠ i, j +1 < i +1, ¬ i < j, ¬ j < i ⊦

Rule argument

Additional information

Used simplifier rules: succpred: ⊦ i +1 -1 = i;

Proof step 43 from proof lst-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ i +1 < j ↔ i < j -1

Rule argument

Additional information

Used simplifier rules: succpred: ⊦ i +1 -1 = i; Used terms: i +1, j

Proof step 44 from proof lst-02 (previous step) (back to tree)

Lemma lssucc