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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); 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 del-04 (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(y, x), perm(x, y), ∃ a0. ¬(a0 ∈ x -1l a ∨ a0 ∈ y -1l a → #oc(a0, x -1l a) = #oc(a0, y -1l a)) ⊦

Rule argument

Additional information

Used terms: y -1l a, x -1l a

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

Lemma perm-all

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: y, x

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

Lemma perm-all

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

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

• Proof step 24:

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

Rule argument

Additional information

Used terms: a, x, a0

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

Lemma del1-01

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1

• Proof step 13:

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

• Proof step 15:

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

Rule argument

Additional information

Used terms: x, a

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

Lemma del1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  perm(y, x), a ∈ y -1l a, a ∈ y, ¬ a ∈ x, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y) ⊦

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; in-01-01: ⊦ a ∈ x -1l b → a ∈ x; (forward) from specification list-del ⊦ ¬ a ∈ x → x -1l a = x; (s)

Proof step 14 from proof del-04 (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; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  #oc(a, x) = m + 1, #oc(a, x) ≠ 0, m ≠ #oc(a, y -1l a), perm(y, x), a ∈ x, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

Used simplifier rules: in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: #oc(a, x), m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  #oc(a, x) = m + 1, m ≠ #oc(a, y -1l a), perm(y, x), a ∈ x, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1

• Proof step 20:

  #oc(a, x) = m + 1, m ≠ #oc(a, y) -1, perm(y, x), a ∈ x, a ∈ y, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; in: ⊦ a ∈ y ∧ ¬ a ∈ x → ¬ perm(x, y); ⊦ ¬ a ∈ x → x -1l a = x; (s) Used terms: y, a

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

Lemma del1

Proof step 20 from proof del-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #oc(a, x) = m + 1, m ≠ #oc(a, y) - 1, perm(y, x), a ∈ y, a ∈ x, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s)

Proof step 21 from proof del-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  #oc(a, x) = m + 1, #oc(a, y) = m0 + 1, #oc(a, y) ≠ 0, m ≠ m0, perm(y, x), a ∈ x, a ∈ y, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

Used simplifier rules: in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: #oc(a, y), m0

Proof step 22 from proof del-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #oc(a, y) = m0 + 1, #oc(a, x) = m + 1, m ≠ m0, perm(y, x), a ∈ y, a ∈ x, ∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y), a ∈ x -1l a ∨ a ∈ y -1l a ⊦

Rule argument

Additional information

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

Proof step 23 from proof del-04 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a

Proof step 24 from proof del-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

Used simplifier rules: del1-01: ⊦ a ≠ b → #oc(a, x -1l b) = #oc(a, x); notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; in: ⊦ a ∈ y ∧ ¬ a ∈ x → ¬ perm(x, y); ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)

Proof step 25 from proof del-04 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0