Proof step 1 from proof perm-put-del1 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n < # y, ¬ perm(y[n := a] -1l a, y -1l y[n]) ⊦

Rule argument

Additional information

Proof step 2 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  y ≠ [], n < # y, ¬ perm(y[n := a] -1l a, y -1l y[n]) ⊦

Rule argument

Additional information

Used simplifier rules: sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); sym-02: ⊦ ¬ perm(x, y) → ¬ perm(y, x); ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof perm-put-del1 (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:

  y ≠ [], n < # y, ∃ a0. ¬(a0 ∈ y[n := a] -1l a ∨ a0 ∈ y -1l y[n] → #oc(a0, y[n := a] -1l a) = #oc(a0, y -1l y[n])) ⊦

Rule argument

Additional information

Used terms: y -1l y[n], y[n := a] -1l a

Proof step 4 from proof perm-put-del1 (previous step) (back to tree)

Lemma perm-all

Proof step 5 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #oc(a0, y[n := a] -1l a) ≠ #oc(a0, y -1l y[n]), y ≠ [], n < # y, a0 ∈ y[n := a] -1l a ∨ a0 ∈ y -1l y[n] ⊦

Rule argument

Additional information

Proof step 6 from proof perm-put-del1 (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 -1l b) = #oc(a, x)

• Proof step 8:

  a0 = y[n], #oc(a0, y[n := a] -1l a) ≠ #oc(a0, y -1l y[n]), y ≠ [], n < # y, a0 ∈ y[n := a] -1l a ∨ a0 ∈ y -1l y[n] ⊦

• Proof step 19:

  #oc(a0, y[n := a] -1l a) ≠ #oc(a0, y), a0 ≠ y[n], y ≠ [], n < # y, a0 ∈ y[n := a] -1l a ∨ a0 ∈ y -1l y[n] ⊦

Rule argument

Additional information

Used terms: y[n], y, a0

Proof step 7 from proof perm-put-del1 (previous step) (back to tree)

Lemma del1-01

Proof step 8 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #oc(y[n], y[n := a] -1l a) ≠ #oc(y[n], y -1l y[n]), y ≠ [], n < # y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

Proof step 9 from proof perm-put-del1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  #oc(y[n], y[n := a] -1l a) ≠ #oc(y[n], y) -1, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; ⊦ ¬ a ∈ x → x -1l a = x; (s) ⊦ m < # x → (x[m] ∈ x ↔ true); (ss) Used terms: y, y[n]

Proof step 10 from proof perm-put-del1 (previous step) (back to tree)

Lemma del1

Proof step 11 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #oc(y[n], y[n := a] -1l a) ≠ #oc(y[n], y) - 1, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

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

Proof step 12 from proof perm-put-del1 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  #oc(y[n], y) = m + 1, #oc(y[n], y) ≠ 0, #oc(y[n], y[n := a] -1l a) ≠ m, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

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(y[n], y), m

Proof step 13 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #oc(y[n], y) = m + 1, #oc(y[n], y[n := a] -1l a) ≠ m, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

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

Proof step 14 from proof perm-put-del1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  #oc(y[n], y) = m + 1, #oc(y[n], y[n := a]) ≠ m, y[n] ≠ a, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] -1l a ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

Used simplifier rules: del1: ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1; ⊦ n -1 = n - 1; (s) ⊦ n < # x → x[n := x[n]] = x; (s) in-01-01: ⊦ a ∈ x -1l b → a ∈ x; (forward) from specification polylist-del ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a, y[n := a], y[n]

Proof step 15 from proof perm-put-del1 (previous step) (back to tree)

Lemma del1-01

Proof step 16 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #oc(y[n], y) = m + 1, #oc(y[n], y[n := a]) ≠ m, y[n] ≠ a, y ≠ [], n < # y, y[n] ∈ y, y[n] ∈ y[n := a] ∨ y[n] ∈ y -1l y[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)

Proof step 17 from proof perm-put-del1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ x[m] = a ∧ a ≠ b ∧ m < # x → #oc(a, x[m := b]) = #oc(a, x) -1

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a, n, y, y[n]

Proof step 18 from proof perm-put-del1 (previous step) (back to tree)

Lemma ocs-put-02

Proof step 19 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #oc(a0, y[n := a] -1l a) ≠ #oc(a0, y), a0 ≠ y[n], y ≠ [], n < # y, a0 ∈ y[n := a] -1l a ∨ a0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)

Proof step 20 from proof perm-put-del1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  a0 = a, #oc(a0, y[n := a] -1l a) ≠ #oc(a0, y), a0 ≠ y[n], y ≠ [], n < # y, a0 ∈ y[n := a] -1l a ∨ a0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ocs-put-01: ⊦ x[m] ≠ a ∧ a ≠ b ∧ m < # x → #oc(a, x[m := b]) = #oc(a, x); Used terms: a, y[n := a], a0

Proof step 21 from proof perm-put-del1 (previous step) (back to tree)

Lemma del1-01

Proof step 22 from proof perm-put-del1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #oc(a, y[n := a] -1l a) ≠ #oc(a, y), a ≠ y[n], y ≠ [], n < # y, a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x[m] ≠ a ∧ m < # x → (a ∈ x[m := a] -1l a ↔ a ∈ x); (s)

Proof step 23 from proof perm-put-del1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used simplifier rules: notin: ⊦ ¬ a ∈ x → #oc(a, x) = 0; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; ocs-put: ⊦ x[m] ≠ a ∧ m < # x → #oc(a, x[m := a]) = #oc(a, x) + 1; ⊦ (m + 1)-1 = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ a ∈ x → x -1l a = x; (s) ⊦ a ≠ x[m] ∧ m < # x → (a ∈ x[m := b] ↔ a = b ∨ a ∈ x); (ws) Used terms: y[n := a], a

Proof step 24 from proof perm-put-del1 (previous step) (back to tree)

Lemma del1