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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(st[a, d] = st0[a, d] ↔ st = st0), ¬ a ∈ st0, ¬ a ∈ st ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  st[a, d] = st0[a, d], st ≠ st0, ¬ a ∈ st0, ¬ a ∈ st ⊦

Rule argument

Additional information

Proof step 3 from proof inj-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:

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

Rule argument

Additional information

Used terms: st0[a, d], st[a, d]

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

Lemma Extension

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Proof step 6 from proof inj-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 ∈ st0, ¬ a ∈ st, ∀ a0. (a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d]) ∧ st[a, d][a0] = st0[a, d][a0], ∃ a. ¬((a ∈ st ↔ a ∈ st0) ∧ st[a] = st0[a]) ⊦

Rule argument

Additional information

Used terms: st0, st

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

Lemma Extension

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ¬ a ∈ st0, ¬ a ∈ st, ∀ a0. (a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d]) ∧ st[a, d][a0] = st0[a, d][a0] ⊦ (a0 ∈ st ↔ a0 ∈ st0) ∧ st[a0] = st0[a0]

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

  a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d], st[a, d][a0] = st0[a, d][a0], ¬ a ∈ st0, ¬ a ∈ st, ∀ a0. (a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d]) ∧ st[a, d][a0] = st0[a, d][a0] ⊦ (a0 ∈ st ↔ a0 ∈ st0) ∧ st[a0] = st0[a0]

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d], st[a, d][a0] = st0[a, d][a0], ¬ a ∈ st0, ¬ a ∈ st, ∀ a0. (a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d]) ∧ st[a, d][a0] = st0[a, d][a0] ⊦ (a0 ∈ st ↔ a0 ∈ st0) ∧ st[a0] = st0[a0]

Rule argument

Additional information

Proof step 11 from proof inj-put (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; notmemlookup: ⊦ ¬ a ∈ st → st[a] = ∅[a]; At-other: ⊦ a ≠ b → st[b, d][a] = st[a]; In-insert: ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; Used formulas: a0 = a