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

User applied rule structural induction

And obtained the following new goals

• Proof step 2:

  a ∈ st0[elem, data], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ; In-empty: ⊦ ¬ a ∈ ∅;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st

• Proof step 4:

  ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]), a = elem ∨ a ∈ st0 ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

Rule argument

Additional information

Used terms: data, elem, st0, a

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

Lemma In-insert

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  a = elem, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

• Proof step 13:

  a ∈ st0, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st[a, d][a] = d;

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

User applied rule all left

And obtained the following new goals

• Proof step 7:

  elem ∈ st0 → (∃ st1. ¬ elem ∈ st1 ∧ st0 = st1[elem, st0[elem]]), ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

Used terms: elem

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  elem ∈ st0 → ¬ elem ∈ st1 ∧ st0 = st1[elem, st0[elem]], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  elem ∈ st0, elem ∈ st0 → ¬ elem ∈ st1 ∧ st0 = st1[elem, st0[elem]], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

Used simplifier rules: inj-put: ⊦ ¬ a ∈ st ∧ ¬ a ∈ st0 → (st[a, d] = st0[a, d] ↔ st = st0); Used formulas: elem ∈ st0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data], ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

Used terms: st1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  st0 = st1[elem, st0[elem]], st0[elem, data] ≠ st1[elem, data], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: insins: ⊦ st[a, d0][a, d] = st[a, d]; inj-put: ⊦ ¬ a ∈ st ∧ ¬ a ∈ st0 → (st[a, d] = st0[a, d] ↔ st = st0);

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  a ∈ st0, a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]), ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  st0 = st1[a, st0[a]], a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ a ≠ b → st[b, d][a] = st[a]

• Proof step 17:

  a = elem, st0 = st1[a, st0[a]], a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[elem, data][a]]

• Proof step 34:

  st0 = st1[a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]]

Rule argument

Additional information

Used terms: a, data, elem, st0

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

Lemma At-other

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st[a, d][a] = d;

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

User applied rule exists right

And obtained the following new goals

• Proof step 19:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data], ¬ elem ∈ st1 ∧ st0[elem, data] = st1[elem, data]

Rule argument

Additional information

Used terms: st1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  st0 = st1[elem, st0[elem]], st0[elem, data] ≠ st1[elem, data], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 22:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]), ∃ a. ¬((a ∈ st0[elem, data] ↔ a ∈ st1[elem, data]) ∧ st0[elem, data][a] = st1[elem, data][a]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Used terms: st1[elem, data], st0[elem, data]

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

Lemma Extension

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  st0 = st1[elem, st0[elem]], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data], (elem0 ∈ st0[elem, data] ↔ elem0 ∈ st1[elem, data]) ∧ st0[elem, data][elem0] = st1[elem, data][elem0]

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

  st0 = st1[elem, st0[elem]], ¬(elem0 ∈ st0[elem, data] ↔ elem0 ∈ st1[elem, data]), elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

• Proof step 30:

  st0 = st1[elem, st0[elem]], st0[elem, data][elem0] ≠ st1[elem, data][elem0], elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st

• Proof step 26:

  st0 = st1[elem, st0[elem]], ¬(elem0 = elem ∨ elem0 ∈ st0 ↔ elem0 ∈ st1[elem, data]), elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Used terms: data, elem, st0, elem0

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

Lemma In-insert

Proof step 26 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  st0 = st1[elem, st0[elem]], ¬(elem0 ∈ st0 ↔ elem0 ∈ st1[elem, data]), elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Proof step 27 from proof del-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  st0 = st1[elem, st0[elem]], elem ∈ st0, elem0 ∈ st0, ¬ elem0 ∈ st1[elem, data], ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

• Proof step 29:

  st0 = st1[elem, st0[elem]], elem ∈ st0, elem0 ∈ st1[elem, data], ¬ elem0 ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Proof step 28 from proof del-exists (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st;

Proof step 29 from proof del-exists (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st;

Proof step 30 from proof del-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ a ≠ b → st[b, d][a] = st[a]

• Proof step 32:

  st0 = st1[elem, st0[elem]], st0[elem0] ≠ st1[elem, data][elem0], elem0 ≠ elem, elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st[a, d][a] = d; Used terms: elem0, data, elem, st0

Proof step 31 from proof del-exists (previous step) (back to tree)

Lemma At-other

Proof step 32 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  st0 = st1[elem, st0[elem]], st0[elem0] ≠ st1[elem0], elem0 ≠ elem, elem ∈ st0, ¬ elem ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st. ¬ elem ∈ st ∧ st0[elem, data] = st[elem, data]

Rule argument

Additional information

Used simplifier rules: At-other: ⊦ a ≠ b → st[b, d][a] = st[a];

Proof step 33 from proof del-exists (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: At-other: ⊦ a ≠ b → st[b, d][a] = st[a];

Proof step 34 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  st0 = st1[a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]]

Rule argument

Additional information

Proof step 35 from proof del-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 36:

  st0 = st1[a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]], ¬ a ∈ st1[elem, data] ∧ st0[elem, data] = st1[elem, data][a, st0[a]]

Rule argument

Additional information

Used terms: st1[elem, data]

Proof step 36 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  st0 = st1[a, st0[a]], st0[elem, data] ≠ st1[elem, data][a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]]

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st;

Proof step 37 from proof del-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 39:

  st0 = st1[a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]), ∃ a0. ¬((a0 ∈ st0[elem, data] ↔ a0 ∈ st1[elem, data][a, st0[a]]) ∧ st0[elem, data][a0] = st1[elem, data][a, st0[a]][a0]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]]

Rule argument

Additional information

Used terms: st1[elem, data][a, st0[a]], st0[elem, data]

Proof step 38 from proof del-exists (previous step) (back to tree)

Lemma Extension

Proof step 39 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  st0 = st1[a, st0[a]], a ≠ elem, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a, st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[elem, data] = st1[a, st0[a]], (a0 ∈ st0[elem, data] ↔ a0 ∈ st1[elem, data][a, st0[a]]) ∧ st0[elem, data][a0] = st1[elem, data][a, st0[a]][a0]

Rule argument

Additional information

Proof step 40 from proof del-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 41:

  a ≠ elem, a ∈ st1[a, st0[a]], ¬ a ∈ st1, ∀ a0. a0 ∈ st1[a, st0[a]] → (∃ st. ¬ a0 ∈ st ∧ st1[a, st0[a]] = st[a0, st1[a, st0[a]][a0]]) ⊦ ∃ st. ¬ a ∈ st ∧ st1[a, st0[a]][elem, data] = st[a, st1[a, st0[a]][a]], (a0 ∈ st1[a, st0[a]][elem, data] ↔ a0 ∈ st1[elem, data][a, st1[a, st0[a]][a]]) ∧ st1[a, st0[a]][elem, data][a0] = st1[elem, data][a, st1[a, st0[a]][a]][a0]

Rule argument

Additional information

Proof step 41 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  a ≠ elem, ¬ a ∈ st1, ∀ a0. a0 ∈ st1[a, st0[a]] → (∃ st. ¬ a0 ∈ st ∧ st1[a, st0[a]] = st[a0, st1[a, st0[a]][a0]]) ⊦ ∃ st. ¬ a ∈ st ∧ st1[a, st0[a]][elem, data] = st[a, st0[a]], (a0 ∈ st1[a, st0[a]][elem, data] ↔ a0 ∈ st1[elem, data][a, st0[a]]) ∧ st1[a, st0[a]][elem, data][a0] = st1[elem, data][a, st0[a]][a0]

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; At-same: ⊦ st[a, d][a] = d;

Proof step 42 from proof del-exists (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 43:

  a ≠ elem, a0 ≠ elem, ¬ a ∈ st1, ∀ a0. a0 ∈ st1[a, st0[a]] → (∃ st. ¬ a0 ∈ st ∧ st1[a, st0[a]] = st[a0, st1[a, st0[a]][a0]]) ⊦ ∃ st. ¬ a ∈ st ∧ st1[a, st0[a]][elem, data] = st[a, st0[a]], (a0 ∈ st1[a, st0[a]][elem, data] ↔ a0 ∈ st1[elem, data][a, st0[a]]) ∧ st1[a, st0[a]][elem, data][a0] = st1[elem, data][a, st0[a]][a0]

Rule argument

Additional information

Used simplifier rules: in-neq: ⊦ a ≠ b → (a ∈ st[b, d] ↔ a ∈ st); At-other: ⊦ a ≠ b → st[b, d][a] = st[a]; At-same: ⊦ st[a, d][a] = d; In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; Used formulas: a0 = elem

Proof step 43 from proof del-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  a ≠ elem, a0 ≠ elem, ¬ a ∈ st1, ∀ a0. a0 ∈ st1[a, st0[a]] → (∃ st. ¬ a0 ∈ st ∧ st1[a, st0[a]] = st[a0, st1[a, st0[a]][a0]]) ⊦ ∃ st. ¬ a ∈ st ∧ st1[a, st0[a]][elem, data] = st[a, st0[a]], (a0 ∈ st1[a, st0[a]] ↔ a0 ∈ st1[elem, data][a, st0[a]]) ∧ st1[a, st0[a]][a0] = st1[elem, data][a, st0[a]][a0]

Rule argument

Additional information

Used simplifier rules: in-neq: ⊦ a ≠ b → (a ∈ st[b, d] ↔ a ∈ st); At-other: ⊦ a ≠ b → st[b, d][a] = st[a];

Proof step 44 from proof del-exists (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st[a, d][a] = d; In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; in-neq: ⊦ a ≠ b → (a ∈ st[b, d] ↔ a ∈ st); At-other: ⊦ a ≠ b → st[b, d][a] = st[a]; Used formulas: a0 = a