Proof step 1 from proof min-a (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  min(i, min(j, j0)) ≠ min(min(i, j), j0) ⊦

Rule argument

Additional information

Proof step 2 from proof min-a (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 3:

  min(i, min(j, j0)) ≠ min(min(i, j), j0), i < min(j, j0) ⊦

• Proof step 5:

  min(i, min(j, j0)) ≠ min(min(i, j), j0), ¬ i < min(j, j0) ⊦

Rule argument

Additional information

Used formulas: i < min(j, j0)

Proof step 3 from proof min-a (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  i ≠ min(min(i, j), j0), i < min(j, j0) ⊦

Rule argument

Additional information

Used simplifier rules: Min-left: ⊦ j < i → min(j, i) = j;

Proof step 4 from proof min-a (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Min-left: ⊦ j < i → min(j, i) = j; Min-right: ⊦ ¬ j < i → min(j, i) = i; Min-left: ⊦ j < i → min(j, i) = j; lf-07: ⊦ ¬ i < i0 ∧ j < i0 → j < i; (forward) from specification int-basic1 lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 Used formulas: j < j0

Proof step 5 from proof min-a (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  min(j, j0) ≠ min(min(i, j), j0), ¬ i < min(j, j0) ⊦

Rule argument

Additional information

Used simplifier rules: Min-right: ⊦ ¬ j < i → min(j, i) = i;

Proof step 6 from proof min-a (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  min(j, j0) ≠ min(min(i, j), j0), ¬ j < j0, ¬ i < min(j, j0) ⊦

Rule argument

Additional information

Used simplifier rules: Min-right: ⊦ ¬ j < i → min(j, i) = i; Min-left: ⊦ j < i → min(j, i) = j; Used formulas: j < j0

Proof step 7 from proof min-a (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  j0 ≠ min(min(i, j), j0), ¬ j < j0, ¬ i < j0 ⊦

Rule argument

Additional information

Used simplifier rules: Min-right: ⊦ ¬ j < i → min(j, i) = i;

Proof step 8 from proof min-a (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

  j0 ≠ min(min(i, j), j0), min(i, j) < j0, ¬ j < j0, ¬ i < j0 ⊦

Rule argument

Additional information

Used simplifier rules: Min-right: ⊦ ¬ j < i → min(j, i) = i; Used formulas: min(i, j) < j0

Proof step 9 from proof min-a (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  j0 ≠ min(i, j), min(i, j) < j0, min(i, j) < j, min(i, j) < i, ¬ j < j0, ¬ i < j0 ⊦

Rule argument

Additional information

Used simplifier rules: Min-left: ⊦ j < i → min(j, i) = j; lf-07: ⊦ ¬ i < i0 ∧ j < i0 → j < i; (forward) from specification int-basic1

Proof step 10 from proof min-a (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Min-left: ⊦ j < i → min(j, i) = j; Min-right: ⊦ ¬ j < i → min(j, i) = i; ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ i < j → ¬ j < i; (s) Used formulas: i < j