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)), h0 ⊥ h1, r ∈ 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 ⊥ ∅; ⊦ ¬ r ∈ ∅; (s) 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 ∈ h0 ∨ r ∈ h1, ∃ r. ¬((r ∈ h1 ↔ r ∈ ∅) ∧ (r ∈ h1 → h1(r) = ∅(r))), ∀ 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)

A spec-lemma

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)), h0 ⊥ h1, r0 ∈ 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: ⊦ ¬ r ∈ ∅; (s)

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: ⊦ ¬ null ∈ h; (s) Used terms: h1, r0

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

A spec-lemma

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); disj-write: r ≠ null, ¬ r ∈ h1 ⊦ h0 ⊥ (h1 ++ r)(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ r ∈ h(r0 := o) ↔ r ∈ h; (s) ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 13:

  ((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 formulas: r = r0

Proof step 13 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 14:

  ((h0 ∪ h) ++ r0)(r) ≠ h0(r), r ≠ r0, r0 ≠ null, h0 ⊥ h, r ∈ h0, ¬ 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 ⊦

• Proof step 16:

  ((h0 ∪ h) ++ r0)(r) ≠ (h ++ r0)(r), r ≠ r0, r0 ≠ null, h0 ⊥ h, ¬ r ∈ h0, ¬ 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

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) ≠ h0(r), r ≠ r0, r0 ≠ null, h0 ⊥ h, r ∈ h0, ¬ 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: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ (h ++ r0)(r) = h(r); (s)

Proof step 15 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: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) r ∈ h ⊦ # h(r := o) = # h; (s) ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; (s) ⊦ 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 16 from proof at-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (h0 ∪ h)(r) ≠ h(r), r ≠ r0, r0 ≠ null, h0 ⊥ h, r ∈ h, ¬ r ∈ h0, ¬ 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: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ (h ++ r0)(r) = h(r); (s)

Proof step 17 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: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) r ∈ h ⊦ # h(r := o) = # h; (s) ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; (s) ⊦ 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