Proof step 1 from proof at-uni (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), r ∈ h0 ∪ h1, h0 ⊥ h1 ⊦

Rule argument

Additional information

Proof step 2 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1);

Proof step 3 from proof at-uni (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 4:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # h1

Proof step 4 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Proof step 5 from proof at-uni (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), h1 ≠ ∅, h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Used simplifier rules: uni-emp: ⊦ h0 ∪ ∅ = h0; disj-emp-r: ⊦ h ⊥ ∅; in-emp: ⊦ ¬ r ∈ ∅; Used formulas: h1 = ∅

Proof step 6 from proof at-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), h0 ⊥ h1, ∃ r. ¬((r ∈ h1 ↔ r ∈ ∅) ∧ (r ∈ h1 → h1[r] = ∅[r])), r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Used terms: ∅, h1

Proof step 7 from proof at-uni (previous step) (back to tree)

Lemma ext

Proof step 8 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), r0 ∈ h1, h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Used simplifier rules: in-emp: ⊦ ¬ r ∈ ∅;

Proof step 9 from proof at-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ r ≠ null → (r ∈ h ↔ (∃ h0, o. h = (h0 ++ r)[r, o] ∧ ¬ r ∈ h0))

• Proof step 11:

  (h0 ∪ h1)[r] ≠ (r ∈ h0 ⊃ h0[r];h1[r]), r0 ≠ null, h0 ⊥ h1, ∃ h0, o. h1 = (h0 ++ r0)[r0, o] ∧ ¬ r0 ∈ h0, r ∈ h0 ∨ r ∈ h1, ∀ h, h0, r. # h < # h1 → (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h) → false ⊦

Rule argument

Additional information

Used simplifier rules: sanity: ⊦ ¬ null ∈ h; Used terms: h1, r0

Proof step 10 from proof at-uni (previous step) (back to tree)

Lemma exin

Proof step 11 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ((h0 ∪ h) ++ r0)[r] ≠ (r ∈ h0 ⊃ h0[r];(h ++ r0)[r]), r ≠ r0, r0 ≠ null, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h ∨ r ∈ h0, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

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

Proof step 12 from proof at-uni (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]

• Proof step 14:

  (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];(h ++ r0)[r]), r ≠ r0, r0 ≠ null, r ∈ h0 ∪ h, h0 ⊥ h, ¬ r0 ∈ h0 ∪ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h ∨ r ∈ h0, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); Used terms: r, r0, h0 ∪ h

Proof step 13 from proof at-uni (previous step) (back to tree)

Lemma at-alloc

Proof step 14 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];(h ++ r0)[r]), r ≠ r0, r0 ≠ null, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h ∨ r ∈ h0, r ∈ h0 ∨ r ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1);

Proof step 15 from proof at-uni (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];(h ++ r0)[r]), r ≠ r0, r0 ≠ null, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h0 ∨ r ∈ h, r ∈ h ∨ r ∈ h0, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used formulas: r = r0

Proof step 16 from proof at-uni (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 17:

  (h0 ∪ h)[r] ≠ h0[r], r ≠ r0, r0 ≠ null, r ∈ h0, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h ∨ r ∈ h0, r ∈ h0 ∨ r ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

• Proof step 19:

  (h0 ∪ h)[r] ≠ (h ++ r0)[r], r ≠ r0, r0 ≠ null, h0 ⊥ h, ¬ r ∈ h0, ¬ r0 ∈ h0, ¬ r0 ∈ h, r ∈ h ∨ r ∈ h0, r ∈ h0 ∨ r ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Proof step 17 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (h0 ∪ h)[r] ≠ h0[r], r ≠ r0, r0 ≠ null, r ∈ h0, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false);

Proof step 18 from proof at-uni (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; size-write: r ∈ h ⊦ # h[r, o] = # h; size-alloc: ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: h, h0, r

Proof step 19 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (h0 ∪ h)[r] ≠ (h ++ r0)[r], r ≠ r0, r0 ≠ null, r ∈ h, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false);

Proof step 20 from proof at-uni (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 21:

  (h0 ∪ h)[r] ≠ (h ++ r0)[r], r ≠ r0, r0 ≠ null, r ∈ h, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦ (h0 ∪ h)[r] ≠ (r ∈ h0 ⊃ h0[r];h[r]) ∧ h0 ⊥ h ∧ (r ∈ h0 ∨ r ∈ h)

Rule argument

Additional information

Used simplifier rules: in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; size-write: r ∈ h ⊦ # h[r, o] = # h; size-alloc: ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: h, h0, r

Proof step 21 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (h0 ∪ h)[r] = h[r], h[r] ≠ (h ++ r0)[r], r ≠ r0, r0 ≠ null, r ∈ h, h0 ⊥ h, ¬ r0 ∈ h0, ¬ r0 ∈ h, ∀ h0, h2, r. # h0 < # (h ++ r0)[r0, o] → (h2 ∪ h0)[r] ≠ (r ∈ h2 ⊃ h2[r];h0[r]) ∧ h2 ⊥ h0 ∧ (r ∈ h2 ∨ r ∈ h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false);

Proof step 22 from proof at-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used terms: r, r0, h

Proof step 23 from proof at-uni (previous step) (back to tree)

Lemma at-alloc