Proof step 1 from proof sort-possible (conclusion) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 2:

  asc ⊦ ∃ a0. perm(a, a0) ∧ ordered≤((asc ⊃ a0;rev(a0))) ∧ # a = # a0

• Proof step 7:

  ¬ asc ⊦ ∃ a0. perm(a, a0) ∧ ordered≤((asc ⊃ a0;rev(a0))) ∧ # a = # a0

Rule argument

Additional information

Used formulas: asc

Proof step 2 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(a0) ∧ # a = # a0

Rule argument

Additional information

Proof step 3 from proof sort-possible (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ∃ y. perm(x, y) ∧ ordered≤(y) ∧ # x = # y

• Proof step 5:

  ∃ y. perm(a, y) ∧ ordered≤(y) ∧ # a = # y ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(a0) ∧ # a = # a0

Rule argument

Additional information

Used terms: a

Proof step 4 from proof sort-possible (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # a = # a0, ordered≤(a0), perm(a, a0) ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(a0) ∧ # a = # a0

Rule argument

Additional information

Proof step 6 from proof sort-possible (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

Proof step 7 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(rev(a0)) ∧ # a = # a0

Rule argument

Additional information

Proof step 8 from proof sort-possible (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  ⊦ ∃ y. perm(x, y) ∧ ordered≤(y) ∧ # x = # y

• Proof step 10:

  ∃ y. perm(rev(a), y) ∧ ordered≤(y) ∧ # rev(a) = # y ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(rev(a0)) ∧ # a = # a0

Rule argument

Additional information

Used terms: rev(a)

Proof step 9 from proof sort-possible (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # a = # a0, ordered≤(a0), perm(rev(a), a0) ⊦ ∃ a0. perm(a, a0) ∧ ordered≤(rev(a0)) ∧ # a = # a0

Rule argument

Additional information

Used simplifier rules: ⊦ # rev(x) = # x; (s)

Proof step 11 from proof sort-possible (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  # a = # a0, ordered≤(a0), perm(rev(a), a0) ⊦ perm(a, rev(a0)) ∧ ordered≤(rev(rev(a0))) ∧ # a = # rev(a0)

Rule argument

Additional information

Used terms: rev(a0)

Proof step 12 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # a = # a0, ordered≤(a0), perm(rev(a), a0), ¬ perm(a, a0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # rev(x) = # x; (s) ⊦ rev(rev(x)) = x; (s) ⊦ perm(x, rev(y)) ↔ perm(x, y); (s)

Proof step 13 from proof sort-possible (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ perm(x, y) ↔ perm(y, x)

• Proof step 15:

  # a = # a0, ordered≤(a0), perm(a0, rev(a)), ¬ perm(a, a0) ⊦

Rule argument

Additional information

Used terms: rev(a), a0

Proof step 14 from proof sort-possible (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof sort-possible (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # a = # a0, ordered≤(a0), perm(a0, a), ¬ perm(a, a0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ perm(x, rev(y)) ↔ perm(x, y); (s)

Proof step 16 from proof sort-possible (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ perm(x, y) ↔ perm(y, x)

Rule argument

Additional information

Used terms: a, a0

Proof step 17 from proof sort-possible (previous step) (back to tree)

A spec-lemma