Proof step 1 from proof eq-shift-put (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(st(a := d) = st0 ↔ st = st0(a := st(a)) ∧ a ∈ st0 ∧ st0(a) = d), a ∈ st ⊦

Rule argument

Additional information

Proof step 2 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(st(a := d) = st0 ↔ st = st0(a := st(a)) ∧ a ∈ st0 ∧ st0(a) = d), a ∈ st ⊦

Rule argument

Additional information

Proof step 3 from proof eq-shift-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  a ∈ st ⊦ (∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0)) ↔ st = st0(a := st(a)) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Used terms: st0, st(a := d)

Proof step 4 from proof eq-shift-put (previous step) (back to tree)

Lemma Extension

Proof step 5 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a ∈ st ⊦ (∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0)) ↔ st = st0(a := st(a)) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Proof step 6 from proof eq-shift-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  a ∈ st ⊦ (∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0)) ↔ (∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0)) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Used terms: st0(a := st(a)), st

Proof step 7 from proof eq-shift-put (previous step) (back to tree)

Lemma Extension

Proof step 8 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a ∈ st ⊦ (∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0)) ↔ (∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0)) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Proof step 9 from proof eq-shift-put (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0)) ∧ a ∈ st0 ∧ st0(a) = d

• Proof step 18:

  st0(a) = d, a ∈ st, a ∈ st0, ∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ⊦ ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0)

Rule argument

Additional information

Proof step 10 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Proof step 11 from proof eq-shift-put (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  a0 = a, a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ∧ a ∈ st0 ∧ st0(a) = d

• Proof step 14:

  a0 ≠ a, a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Used formulas: a0 = a

Proof step 12 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a ∈ st, a ∈ st0(a := st(a)), ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ st0(a) = d ∧ a ∈ st0

Rule argument

Additional information

Used simplifier rules: notmemlookup: ⊦ ¬ a ∈ st → st(a) = ∅(a); At-same: ⊦ st(a := d)(a) = d; In-insert: ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st;

Proof step 13 from proof eq-shift-put (previous step) (back to tree)

User applied rule all left

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; Used terms: a

Proof step 14 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  a0 ≠ a, a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a0) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Used simplifier rules: At-other: ⊦ a ≠ b → st(b := d)(a) = st(a);

Proof step 15 from proof eq-shift-put (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  a ∈ st(a := d) ↔ a ∈ st0, st(a := d)(a) = st0(a), a0 ≠ a, a ∈ st, ∀ a0. (a0 ∈ st(a := d) ↔ a0 ∈ st0) ∧ st(a := d)(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a0) ∧ a ∈ st0 ∧ st0(a) = d

Rule argument

Additional information

Used terms: a

Proof step 16 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  a0 ≠ a, a ∈ st, a ∈ st(a := st0(a)), a ∈ st0, ∀ a0. (a0 ∈ st(a := st0(a)) ↔ a0 ∈ st0) ∧ st(a := st0(a))(a0) = st0(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0) ∧ st(a0) = st0(a0)

Rule argument

Additional information

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

Proof step 17 from proof eq-shift-put (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 18 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  a ∈ st0, a ∈ st, ∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ⊦ (a0 ∈ st(a := st0(a)) ↔ a0 ∈ st0) ∧ st(a := st0(a))(a0) = st0(a0)

Rule argument

Additional information

Proof step 19 from proof eq-shift-put (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  a0 ≠ a, a ∈ st, a ∈ st0, ∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ⊦ (a0 ∈ st(a := st0(a)) ↔ a0 ∈ st0) ∧ st(a := st0(a))(a0) = st0(a0)

Rule argument

Additional information

Used simplifier rules: notmemlookup: ⊦ ¬ a ∈ st → st(a) = ∅(a); At-same: ⊦ st(a := d)(a) = d; In-insert: ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; Used formulas: a0 = a

Proof step 20 from proof eq-shift-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  a0 ≠ a, a ∈ st0, a ∈ st, ∀ a0. (a0 ∈ st ↔ a0 ∈ st0(a := st(a))) ∧ st(a0) = st0(a := st(a))(a0) ⊦ (a0 ∈ st ↔ a0 ∈ st0) ∧ st(a0) = st0(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 21 from proof eq-shift-put (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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