Proof step 1 from proof zero-13 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof zero-13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nat2int-04: ⊦ n→i(m) < n→i(n) ↔ m < n; ⊦ ¬ n < n; (s) ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ls-forward: ⊦ i * j < i * j0 → i ≠ 0; (forward) from specification int-mult ⊦ ~1 < i ↔ 0 ≤ i; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + j < i + i0 ↔ j < i0; (s) numlef-01: ⊦ (* i) ≤ j → i - 1 < j; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)