Proof step 1 from proof ex-ls-add (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  i < j ⊦ ∃ i0. j = i + i0 ∧ 0 < i0

Rule argument

Additional information

Used simplifier rules: add-less: ⊦ 0 < i → i1 < i1 + i; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i;

Proof step 2 from proof ex-ls-add (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  i0 +1 < j, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1) ⊦ ∃ i1. j = i0 +1 + i1 ∧ 0 < i1

• Proof step 5:

  i0 -1 < j, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1) ⊦ ∃ i1. j = i0 -1 + i1 ∧ 0 < i1

Rule argument

Additional information

Used simplifier rules: add-zero-rev: ⊦ 0 + i = i; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i; int generated by 0, +1, -1;; lf-07: ⊦ ¬ i < i0 ∧ j < i0 → j < i; (forward) from specification int-basic1 lf-04: ⊦ ¬ j < i ∧ j < i0 → i < i0; (forward) from specification int-basic1

Proof step 3 from proof ex-ls-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  i0 + 1 < j, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1) ⊦ ∃ i1. j = (i0 + 1) + i1 ∧ 0 < i1

Rule argument

Additional information

Used simplifier rules: succ-01: ⊦ i +1 = i + 1; add-a: ⊦ i + j + i0 = (i + j) + i0;

Proof step 4 from proof ex-ls-add (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lst-03: ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0; succ-01: ⊦ i +1 = i + 1; ls-01: ⊦ i + j < i + i0 ↔ j < i0; add-less: ⊦ 0 < i → i1 < i1 + i; add-in: ⊦ i + j = i + i0 ↔ j = i0; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i; ⊦ i < j -1 ↔ i +1 < j; (s) ⊦ i = j -1 ↔ i +1 = j; (s) Used terms: j -1

Proof step 5 from proof ex-ls-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  i0 < j + 1, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1) ⊦ ∃ i1. j + 1 = i0 + i1 ∧ 0 < i1

Rule argument

Additional information

Used simplifier rules: add-pred-01: ⊦ i -1 + j = (i + j)-1; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i; succ-01: ⊦ i +1 = i + 1; ⊦ i = j -1 ↔ i +1 = j; (s) ⊦ i -1 < j ↔ i < j +1; (s)

Proof step 6 from proof ex-ls-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1), i0 +1 = j + 1 ∨ i0 +1 < j + 1 ⊦ ∃ i1. j + 1 = i0 + i1 ∧ 0 < i1

Rule argument

Additional information

Used terms: j + 1, i0

Proof step 7 from proof ex-ls-add (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof ex-ls-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1), i0 = j ∨ i0 < j ⊦ ∃ i1. j + 1 = i0 + i1 ∧ 0 < i1

Rule argument

Additional information

Used simplifier rules: add-in: ⊦ i + j = i + i0 ↔ j = i0; succ-01: ⊦ i +1 = i + 1; ls-01: ⊦ i + j < i + i0 ↔ j < i0; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i;

Proof step 9 from proof ex-ls-add (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  i0 ≠ j, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1), i0 = j ∨ i0 < j ⊦ ∃ i1. j + 1 = i0 + i1 ∧ 0 < i1

Rule argument

Additional information

Used simplifier rules: add-in: ⊦ i + j = i + i0 ↔ j = i0; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i; Used formulas: i0 = j

Proof step 10 from proof ex-ls-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  i0 ≠ j, i0 < j, ∀ j. i0 < j → (∃ i1. j = i0 + i1 ∧ 0 < i1) ⊦ ∃ i1. j + 1 = i0 + i1 ∧ 0 < i1

Rule argument

Additional information

Proof step 11 from proof ex-ls-add (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: eq: ⊦ i = i + j ↔ j = 0; add-less: ⊦ 0 < i → i1 < i1 + i; add-in: ⊦ i + j = i + i0 ↔ j = i0; zero-02: ⊦ 0 < i ∧ 0 < j → 0 < i + j; add-a: ⊦ i + j + i0 = (i + j) + i0; add-c: ⊦ i + j = j + i; lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1 Used terms: j