Proof step 1 from proof forward-pos (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i < j, 0 < i ⊦ 0 < j ∧ 1 < j

Rule argument

Additional information

Proof step 2 from proof forward-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  0 < j, i < j, 0 < i ⊦ 1 ≠ j ∧ ¬ j < 1

Rule argument

Additional information

Used simplifier rules: trans: ⊦ i < j ∧ j < j0 → i < j0; l: ⊦ i < j ↔ ¬(i = j ∨ j < i);

Proof step 3 from proof forward-pos (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  1 = j, 0 < i, i < j, 0 < j ⊦

• Proof step 9:

  j < 1, 0 < i, i < j, 0 < j ⊦

Rule argument

Additional information

Proof step 4 from proof forward-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i < 1, 0 < i ⊦

Rule argument

Additional information

Used simplifier rules: trans: ⊦ i < j ∧ j < j0 → i < j0;

Proof step 5 from proof forward-pos (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  1 = 0 +1, 0 < i, i < 1 ⊦

Rule argument

Additional information

Used formulas: 1 = 0 +1

Proof step 6 from proof forward-pos (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 7:

  i < 0 +1, 0 < i ⊦

Rule argument

Additional information

Proof step 7 from proof forward-pos (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: ls-01: ⊦ i < j → ¬ j < i; Used terms: i, 0

Proof step 8 from proof forward-pos (previous step) (back to tree)

Lemma lsrec

Proof step 9 from proof forward-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  0 < j, i < j, 0 < i, j < 1, i < 1 ⊦

Rule argument

Additional information

Used simplifier rules: trans: ⊦ i < j ∧ j < j0 → i < j0;

Proof step 10 from proof forward-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ i < j ↔ ¬(i = j ∨ j < i)

Rule argument

Additional information

Used simplifier rules: l: ⊦ i < j ↔ ¬(i = j ∨ j < i); ls-02: ⊦ i < 1 ∧ i ≠ 0 → i < 0; ls-01: ⊦ i < j → ¬ j < i; Used terms: j, 0

Proof step 11 from proof forward-pos (previous step) (back to tree)

Lemma l