Proof step 1 from proof perm-del-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(perm(y -l a, z) ↔ true), perm(x -l a, z), perm(x, y) ⊦

Rule argument

Additional information

Proof step 2 from proof perm-del-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  perm(x, y), perm(x -l a, z), perm(y, x), perm(z, x -l a), ¬ perm(y -l a, z) ⊦

Rule argument

Additional information

Used simplifier rules: neq: ⊦ perm(x, y) ∧ ¬ perm(x0, y) → x ≠ x0; sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); neq: ⊦ perm(x, y) ∧ ¬ perm(x0, y) → x ≠ x0; sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); trans: ⊦ perm(x, y) ∧ perm(y, z) → perm(x, z); sym-01: ⊦ perm(x, y) → perm(y, x); ref: ⊦ perm(x, x);

Proof step 3 from proof perm-del-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ perm(x, y) ↔ (∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y))

• Proof step 5:

  perm(z, x -l a), perm(y, x), perm(x -l a, z), perm(x, y), ∃ a0. ¬(a0 ∈ y -l a ∨ a0 ∈ z → #oc(a0, y -l a) = #oc(a0, z)) ⊦

Rule argument

Additional information

Used terms: z, y -l a

Proof step 4 from proof perm-del-01 (previous step) (back to tree)

Lemma perm-all

Proof step 5 from proof perm-del-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #oc(a0, y -l a) ≠ #oc(a0, z), perm(x, y), perm(x -l a, z), perm(y, x), perm(z, x -l a), a0 ∈ y -l a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Proof step 6 from proof perm-del-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ a ≠ b → #oc(a, x -l b) = #oc(a, x)

• Proof step 8:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(z, x -l a), perm(y, x), perm(x -l a, z), perm(x, y), a0 ∈ y -l a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ocs-del: ⊦ #oc(a, x -l a) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; perm-del-in: ⊦ a ∈ y → ¬ perm(x -l a, y); Used terms: a, y, a0

Proof step 7 from proof perm-del-01 (previous step) (back to tree)

Lemma ocs-del-length

Proof step 8 from proof perm-del-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x, y), perm(x -l a, z), perm(y, x), perm(z, x -l a), a0 ∈ y -l a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Proof step 9 from proof perm-del-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ perm(x, y) ↔ (∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y))

• Proof step 11:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(z, x -l a), perm(x -l a, z), perm(x, y), ∀ a. a ∈ y ∨ a ∈ x → #oc(a, y) = #oc(a, x), a0 ∈ y -l a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used terms: x, y

Proof step 10 from proof perm-del-01 (previous step) (back to tree)

Lemma perm-all

Proof step 11 from proof perm-del-01 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x, y), perm(x -l a, z), perm(z, x -l a), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), a0 ∈ y -l a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used terms: a0

Proof step 12 from proof perm-del-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ a ∈ x -l b ↔ a ∈ x ∧ a ≠ b

• Proof step 14:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(z, x -l a), perm(x -l a, z), perm(x, y), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), a0 ∈ y ∧ a0 ≠ a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used terms: a, y, a0

Proof step 13 from proof perm-del-01 (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof perm-del-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x, y), perm(x -l a, z), perm(z, x -l a), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), a0 ∈ y ∨ a0 ∈ z ⊦

Rule argument

Additional information

Proof step 15 from proof perm-del-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ perm(x, y) ↔ (∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y))

• Proof step 17:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x -l a, z), perm(x, y), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), ∀ a0. a0 ∈ z ∨ a0 ∈ x -l a → #oc(a0, z) = #oc(a0, x -l a), a0 ∈ y ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used terms: x -l a, z

Proof step 16 from proof perm-del-01 (previous step) (back to tree)

Lemma perm-all

Proof step 17 from proof perm-del-01 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x, y), perm(x -l a, z), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), a0 ∈ z ∨ a0 ∈ x -l a → #oc(a0, z) = #oc(a0, x -l a), a0 ∈ y ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used terms: a0

Proof step 18 from proof perm-del-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  #oc(a0, y) ≠ #oc(a0, z), a0 ≠ a, perm(x -l a, z), perm(x, y), a0 ∈ y ∨ a0 ∈ x → #oc(a0, y) = #oc(a0, x), a0 ∈ z ∨ a0 ∈ x → #oc(a0, z) = #oc(a0, x), a0 ∈ y ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ocs-del-length: ⊦ a ≠ b → #oc(a, x -l b) = #oc(a, x); ⊦ a ∈ x -l b ↔ a ∈ x ∧ a ≠ b; (ws)

Proof step 19 from proof perm-del-01 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0;