Proof step 1 from proof one (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i / 1 ≠ i ⊦

Rule argument

Additional information

Proof step 2 from proof one (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j)

• Proof step 4:

  i / 1 ≠ i ⊦ 0 < 1 ∧ 0 ≤ i

Rule argument

Additional information

Used simplifier rules: ⊦ i = i + j ↔ j = 0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 1 * i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) i + 1 = i0 ⊦ j < (* i0) → ¬ (* i) < j; (s) Used terms: i, 1, i0, j0

Proof step 3 from proof one (previous step) (back to tree)

Lemma div-elim-pos

Proof step 4 from proof one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i / 1 ≠ i, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 5 from proof one (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j)

Rule argument

Additional information

Used simplifier rules: ⊦ 1 * i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i = i + j ↔ j = 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) Used terms: i, 1, i0, j0

Proof step 6 from proof one (previous step) (back to tree)

Lemma div-elim2