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:

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

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

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

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)), a ∈ st0, a0 ∈ 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)), a ∈ st1(a0 := d), a0 ∈ st0, ¬ 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)), a ≠ a0, st0(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

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)), a ≠ a0, st0(a) ≠ st1(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

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

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

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

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

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

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-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