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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h ++ r0)[r0, o0][r1, o1] ≠ (h[r1, o1] ++ r0)[r0, o0], r0 ≠ r1, r0 ≠ null, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (h ++ r0)[r0, o0][r1, o1] ≠ (h[r1, o1] ++ r0)[r0, o0], r0 ≠ r1, r0 ≠ null, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Proof step 3 from proof sw-alloc-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 5:

  r0 ≠ r1, r0 ≠ null, r1 ∈ h, ¬ r0 ∈ h, ∃ r. ¬ ( (r ∈ (h ++ r0)[r0, o0][r1, o1] ↔ r ∈ (h[r1, o1] ++ r0)[r0, o0]) ∧ (r ∈ (h ++ r0)[r0, o0][r1, o1] → (h ++ r0)[r0, o0][r1, o1][r] = (h[r1, o1] ++ r0)[r0, o0][r])) ⊦

Rule argument

Additional information

Used terms: (h[r1, o1] ++ r0)[r0, o0], (h ++ r0)[r0, o0][r1, o1]

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

Lemma ext

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (r = r1 ⊃ o1;(h ++ r0)[r]) ≠ (h[r1, o1] ++ r0)[r], r ≠ r0, r0 ≠ null, r0 ≠ r1, r1 ∈ h, r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: at-write: ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;

Proof step 6 from proof sw-alloc-put (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  (r = r1 ⊃ o1;(h ++ r0)[r]) ≠ (h[r1, o1] ++ r0)[r], r ≠ r0, r0 ≠ null, r0 ≠ r1, r ∈ h, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used formulas: r = r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (r = r1 ⊃ o1;(h ++ r0)[r]) ≠ (h[r1, o1] ++ r0)[r], r ≠ r0, r0 ≠ null, r0 ≠ r1, r1 ∈ h, r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  r = r1, o1 ≠ (h[r1, o1] ++ r0)[r], r ≠ r0, r0 ≠ null, r0 ≠ r1, r ∈ h, r1 ∈ h, ¬ r0 ∈ h ⊦

• Proof step 14:

  (h ++ r0)[r] ≠ (h[r1, o1] ++ r0)[r], r ≠ r1, r ≠ r0, r0 ≠ null, r0 ≠ r1, r ∈ h, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  o1 ≠ (h[r1, o1] ++ r0)[r1], r0 ≠ null, r0 ≠ r1, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  o1 ≠ (h[r1, o1] ++ r0)[r1], r0 ≠ null, r0 ≠ r1, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used formulas: r1 = r0

Proof step 11 from proof sw-alloc-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  o1 ≠ (h[r1, o1] ++ r0)[r1], r0 ≠ null, r0 ≠ r1, r1 ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Proof step 12 from proof sw-alloc-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; at-write: ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); Used terms: r1, r0, h[r1, o1]

Proof step 13 from proof sw-alloc-put (previous step) (back to tree)

Lemma at-alloc

Proof step 14 from proof sw-alloc-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (h ++ r0)[r] ≠ (h[r1, o1] ++ r0)[r], r ≠ r1, r ≠ r0, r0 ≠ null, r0 ≠ r1, r1 ∈ h, r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Proof step 15 from proof sw-alloc-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

• Proof step 17:

  (h ++ r0)[r] ≠ h[r1, o1][r], r ≠ r1, r ≠ r0, r0 ≠ null, r0 ≠ r1, r ∈ h, r1 ∈ h, r ∈ h[r1, o1], ¬ r0 ∈ h[r1, o1], ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; Used terms: r, r0, h[r1, o1]

Proof step 16 from proof sw-alloc-put (previous step) (back to tree)

Lemma at-alloc

Proof step 17 from proof sw-alloc-put (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (h ++ r0)[r] ≠ h[r], r ≠ r1, r ≠ r0, r0 ≠ null, r0 ≠ r1, r1 ∈ h, r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: at-write: ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h;

Proof step 18 from proof sw-alloc-put (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

Rule argument

Additional information

Used terms: r, r0, h

Proof step 19 from proof sw-alloc-put (previous step) (back to tree)

Lemma at-alloc