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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n→i(m) + n→i(n) < j, i→n(j) ≤ m + n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  n→i(m) + n→i(n) < j, 0 < j, i→n(j) ≤ m + n ⊦

Rule argument

Additional information

Used simplifier rules: pos-add: ⊦ n→i(m) + n→i(n) < j → 0 < j; ⊦ 1 ≤ i ↔ 0 < i; (s) numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ n→i(m + n) = n→i(m) + n→i(n)

• Proof step 5:

  0 < j, n→i(m + n) < j, i→n(j) ≤ m + n ⊦

Rule argument

Additional information

Used terms: n, m

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

Lemma n2i-add

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ i→n(i) ≤ n → ¬ n→i(n) < i

Rule argument

Additional information

Used terms: j, m + n

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

Lemma inni-le