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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  perm(x, x0), perm(y, y0), ¬ perm(x \ y, x0 \ y0) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬ perm(x \ y, x0 \ y0), ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: perm: ⊦ perm(x, y) ↔ x ⊆m y ∧ y ⊆m x; msubset: ⊦ x ⊆m y ↔ (∀ a. #oc(a, x) ≤ #oc(a, y)); sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ perm(x, y) ↔ x ⊆m y ∧ y ⊆m x

• Proof step 5:

  ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x), ¬ x \ y ⊆m x0 \ y0 ∨ ¬ x0 \ y0 ⊆m x \ y ⊦

Rule argument

Additional information

Used terms: x0 \ y0, x \ y

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

Lemma perm

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0), ¬ #oc(a, x \ y) ≤ #oc(a, x0 \ y0) ∨ ¬ #oc(a0, x0 \ y0) ≤ #oc(a0, x \ y) ⊦

Rule argument

Additional information

Used simplifier rules: msubset: ⊦ x ⊆m y ↔ (∀ a. #oc(a, x) ≤ #oc(a, y));

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ¬ #oc(a, x \ y) ≤ #oc(a, x0 \ y0), ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

• Proof step 14:

  ¬ #oc(a0, x0 \ y0) ≤ #oc(a0, x \ y), ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ¬ a ∈ y, ¬ #oc(a, x \ y) ≤ #oc(a, x0 \ y0), ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff: ⊦ a ∈ y → #oc(a, x \ y) = 0; ⊦ 0 ≤ m; (s) Used formulas: a ∈ y

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #oc(a, x0 \ y0) < #oc(a, x), a ∈ x, ¬ a ∈ y, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff-01: ⊦ ¬ a ∈ y → #oc(a, x \ y) = #oc(a, x); oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  #oc(a, x0 \ y0) < #oc(a, x), a ∈ x, a ∈ y0, ¬ a ∈ y, ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

• Proof step 12:

  #oc(a, x0 \ y0) < #oc(a, x), a ∈ x, ¬ a ∈ y0, ¬ a ∈ y, ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

Rule argument

Additional information

Used formulas: a ∈ y0

Proof step 10 from proof diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ∈ y0, a ∈ x, ¬ a ∈ y, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff: ⊦ a ∈ y → #oc(a, x \ y) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 11 from proof diff (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; ⊦ m ≤ 0 ↔ m = 0; (s) Used terms: a

Proof step 12 from proof diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  #oc(a, x0) < #oc(a, x), a ∈ x, ¬ a ∈ y0, ¬ a ∈ y, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff-01: ⊦ ¬ a ∈ y → #oc(a, x \ y) = #oc(a, x);

Proof step 13 from proof diff (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: a

Proof step 14 from proof diff (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 15:

  ¬ a0 ∈ y0, ¬ #oc(a0, x0 \ y0) ≤ #oc(a0, x \ y), ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff: ⊦ a ∈ y → #oc(a, x \ y) = 0; ⊦ 0 ≤ m; (s) Used formulas: a0 ∈ y0

Proof step 15 from proof diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #oc(a0, x \ y) < #oc(a0, x0), a0 ∈ x0, ¬ a0 ∈ y0, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff-01: ⊦ ¬ a ∈ y → #oc(a, x \ y) = #oc(a, x); oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 16 from proof diff (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  #oc(a0, x \ y) < #oc(a0, x0), a0 ∈ x0, a0 ∈ y, ¬ a0 ∈ y0, ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

• Proof step 19:

  #oc(a0, x \ y) < #oc(a0, x0), a0 ∈ x0, ¬ a0 ∈ y, ¬ a0 ∈ y0, ∀ a. #oc(a, y) ≤ #oc(a, y0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, x0) ≤ #oc(a, x) ⊦

Rule argument

Additional information

Used formulas: a0 ∈ y

Proof step 17 from proof diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  a0 ∈ y, a0 ∈ x0, ¬ a0 ∈ y0, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff: ⊦ a ∈ y → #oc(a, x \ y) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 18 from proof diff (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; ⊦ m ≤ 0 ↔ m = 0; (s) Used terms: a0

Proof step 19 from proof diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #oc(a0, x) < #oc(a0, x0), a0 ∈ x0, ¬ a0 ∈ y, ¬ a0 ∈ y0, ∀ a. #oc(a, x0) ≤ #oc(a, x), ∀ a. #oc(a, x) ≤ #oc(a, x0), ∀ a. #oc(a, y0) ≤ #oc(a, y), ∀ a. #oc(a, y) ≤ #oc(a, y0) ⊦

Rule argument

Additional information

Used simplifier rules: oc-diff-01: ⊦ ¬ a ∈ y → #oc(a, x \ y) = #oc(a, x);

Proof step 20 from proof diff (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: a0