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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i ^ j < 0, 0 ≤ i, 0 ≤ j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i ^ j < 0, i ^ j < i, i ^ j < j, 0 ≤ i, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~1 < i ↔ 0 ≤ i; (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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1

• Proof step 5:

  i ^ j < j, i ^ j < i, i ^ j < 0, 0 ≤ j, 0 ≤ i, 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1 ⊦

Rule argument

Additional information

Used terms: i, j

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

Lemma notone

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 numlsf-02: ⊦ (* i) < j → i + 1 ≤ j; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  i ^ j < 0, i ^ j < i, i ^ j < j, i ^ j ≤ 1, 0 ≤ i, 0 ≤ j, ¬ 1 < i ⊦

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs

Proof step 7 from proof notneg (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  i ^ j < 0, 0 ≤ i, 0 ≤ j, i ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 8 from proof notneg (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; one-01: ⊦ 1 ^ j = 1; ⊦ i -1 = i - 1; (s) ⊦ 0 ≤ i → (i * j < 0 ↔ j < 0 ∧ i ≠ 0); (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) ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) Used terms: j, i

Proof step 9 from proof notneg (previous step) (back to tree)

Lemma Pot-pos