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[a0 := d], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := (st0[a0 := d])[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 = a0 ∨ a ∈ st0 ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := (st0[a0 := d])[a]]

Rule argument

Additional information

Used terms: d, a0, 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 = a0, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := (st0[a0 := d])[a]]

• Proof step 13:

  a ∈ st0, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := (st0[a0 := d])[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. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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:

  a0 ∈ st0 → (∃ st1. ¬ a0 ∈ st1 ∧ st0 = st1[a0 := st0[a0]]), ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

Rule argument

Additional information

Used terms: a0

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:

  a0 ∈ st0 → ¬ a0 ∈ st1 ∧ st0 = st1[a0 := st0[a0]], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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:

  a0 ∈ st0, a0 ∈ st0 → ¬ a0 ∈ st1 ∧ st0 = st1[a0 := st0[a0]], ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

Rule argument

Additional information

Used simplifier rules: inj-put: ⊦ ¬ a ∈ st ∧ ¬ a ∈ st0 → (st[a := d] = st0[a := d] ↔ st = st0); Used formulas: a0 ∈ 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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d], ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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[a0 := st0[a0]], st0[a0 := d] ≠ st1[a0 := d], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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[a0 := d] = st1[a := (st0[a0 := d])[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[a0 := d] = st1[a := (st0[a0 := d])[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 = a0, st0 = st1[a := st0[a]], a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := (st0[a0 := d])[a]]

• Proof step 34:

  st0 = st1[a := st0[a]], a ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := st0[a]]

Rule argument

Additional information

Used terms: a, d, a0, 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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d], ¬ a0 ∈ st1 ∧ st0[a0 := d] = st1[a0 := d]

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[a0 := st0[a0]], st0[a0 := d] ≠ st1[a0 := d], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]), ∃ a. ¬((a ∈ st0[a0 := d] ↔ a ∈ st1[a0 := d]) ∧ (st0[a0 := d])[a] = (st1[a0 := d])[a]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

Rule argument

Additional information

Used terms: st1[a0 := d], st0[a0 := d]

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[a0 := st0[a0]], a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d], (a ∈ st0[a0 := d] ↔ a ∈ st1[a0 := d]) ∧ (st0[a0 := d])[a] = (st1[a0 := d])[a]

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[a0 := st0[a0]], ¬(a ∈ st0[a0 := d] ↔ a ∈ st1[a0 := d]), a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

• Proof step 30:

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

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[a0 := st0[a0]], ¬(a = a0 ∨ a ∈ st0 ↔ a ∈ st1[a0 := d]), a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

Rule argument

Additional information

Used terms: d, a0, st0, a

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[a0 := st0[a0]], ¬(a ∈ st0 ↔ a ∈ st1[a0 := d]), a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

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[a0 := st0[a0]], a0 ∈ st0, a ∈ st0, ¬ a ∈ st1[a0 := d], ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

• Proof step 29:

  st0 = st1[a0 := st0[a0]], a0 ∈ st0, a ∈ st1[a0 := d], ¬ a ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

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[a0 := st0[a0]], st0[a] ≠ (st1[a0 := d])[a], a ≠ a0, a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ (st[a := d])[a] = d; Used terms: a, d, a0, 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[a0 := st0[a0]], st0[a] ≠ st1[a], a ≠ a0, a0 ∈ st0, ¬ a0 ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st. ¬ a0 ∈ st ∧ st0[a0 := d] = st[a0 := d]

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 ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = 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 ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := st0[a]], ¬ a ∈ st1[a0 := d] ∧ st0[a0 := d] = (st1[a0 := d])[a := st0[a]]

Rule argument

Additional information

Used terms: st1[a0 := d]

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[a0 := d] ≠ (st1[a0 := d])[a := st0[a]], a ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = 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 ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]), ∃ a1. ¬((a1 ∈ st0[a0 := d] ↔ a1 ∈ (st1[a0 := d])[a := st0[a]]) ∧ (st0[a0 := d])[a1] = ((st1[a0 := d])[a := st0[a]])[a1]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := st0[a]]

Rule argument

Additional information

Used terms: (st1[a0 := d])[a := st0[a]], st0[a0 := d]

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 ≠ a0, a ∈ st0, ¬ a ∈ st1, ∀ a. a ∈ st0 → (∃ st1. ¬ a ∈ st1 ∧ st0 = st1[a := st0[a]]) ⊦ ∃ st1. ¬ a ∈ st1 ∧ st0[a0 := d] = st1[a := st0[a]], (a1 ∈ st0[a0 := d] ↔ a1 ∈ (st1[a0 := d])[a := st0[a]]) ∧ (st0[a0 := d])[a1] = ((st1[a0 := d])[a := st0[a]])[a1]

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 ≠ a0, 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]])[a0 := d] = st[a := (st1[a := st0[a]])[a]], (a1 ∈ (st1[a := st0[a]])[a0 := d] ↔ a1 ∈ (st1[a0 := d])[a := (st1[a := st0[a]])[a]]) ∧ ((st1[a := st0[a]])[a0 := d])[a1] = ((st1[a0 := d])[a := (st1[a := st0[a]])[a]])[a1]

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 ≠ a0, ¬ 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]])[a0 := d] = st[a := st0[a]], (a1 ∈ (st1[a := st0[a]])[a0 := d] ↔ a1 ∈ (st1[a0 := d])[a := st0[a]]) ∧ ((st1[a := st0[a]])[a0 := d])[a1] = ((st1[a0 := d])[a := st0[a]])[a1]

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 ≠ a0, a1 ≠ a0, ¬ 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]])[a0 := d] = st[a := st0[a]], (a1 ∈ (st1[a := st0[a]])[a0 := d] ↔ a1 ∈ (st1[a0 := d])[a := st0[a]]) ∧ ((st1[a := st0[a]])[a0 := d])[a1] = ((st1[a0 := d])[a := st0[a]])[a1]

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: a1 = a0

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 ≠ a0, a1 ≠ a0, ¬ 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]])[a0 := d] = st[a := st0[a]], (a1 ∈ st1[a := st0[a]] ↔ a1 ∈ (st1[a0 := d])[a := st0[a]]) ∧ (st1[a := st0[a]])[a1] = ((st1[a0 := d])[a := st0[a]])[a1]

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: a1 = a