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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i ^ j < i ^ j0 ↔ j < j0), 1 < i, 0 ≤ j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i ^ j < i ^ j0 ↔ j < j0), 0 < i, 1 < i, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 11:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 1 < i ∧ 0 ≤ j → (i ^ j ≤ i ^ j0 ↔ j ≤ j0)

• Proof step 7:

  1 < i, 0 < i, i ^ j < i ^ j0, j0 ≤ j, 0 ≤ j, 1 < i ∧ 0 ≤ j → (i ^ j ≤ i ^ j0 ↔ j ≤ j0) ⊦

Rule argument

Additional information

Used terms: i, j, j0

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

Lemma le-pos

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

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: le-pos: ⊦ 1 < i ∧ 0 ≤ j → (i ^ j ≤ i ^ j0 ↔ j ≤ j0); ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ ¬ i < i; (s)

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

User applied rule weakening

And obtained the following new goals

• Proof step 10:

  i ^ j < i ^ j0, ¬ j ≤ j0, ¬ i ^ j ≤ i ^ j0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → ¬ j < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

Proof step 12 from proof ls-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 1 < i ∧ 0 ≤ j → (i ^ j ≤ i ^ j0 ↔ j ≤ j0)

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ j → ¬ j < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: j, j0, i

Proof step 13 from proof ls-pos (previous step) (back to tree)

Lemma le-pos