Proof step 1 from proof Decl-allocjsiz (conclusion) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r0), ¬ null ∈ h, ¬ null ∈ h0 ⊦ ⟨r := choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null⟩ (h = h0 ∧ r = r0)

• Proof step 18:

  ⟨r := choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null⟩ (h = h0 ∧ r = r0), ¬ null ∈ h, ¬ null ∈ h0 ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r0)

Rule argument

Additional information

Proof step 2 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 3:

  ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1), ¬ null ∈ h, ¬ null ∈ h0 ⊦ (∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null)) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r0. (¬ r0 ∈ h ∧ r0 ≠ null) ∧ ⟨r := {h := h +h r0; r0}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 3 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1), ¬ null ∈ h, ¬ null ∈ h0 ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 4 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 5:

  ⟨r := choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null⟩ (h = h0 ∧ r = r1), ¬ null ∈ h, ¬ null ∈ h0 ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used simplifier rules: decl: alloc#(; h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null};

Proof step 5 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 6:

  ⟨r := {h := h +h r0; r0}⟩ (h = h0 ∧ r = r1), r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

• Proof step 13:

  ⟨r := null⟩ (h = h0 ∧ r = r1), ¬ null ∈ h, ¬ null ∈ h0, ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null) ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 6 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 7:

  ⟨r := r0⟩ (h +h r0 = h0 ∧ r = r1), r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 7 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 8:

  h +h r0 = h0, r0 = r1, r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 8 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ r0 ∈ h +h r ↔ r0 ∈ h ∨ r0 = r; (s)

Proof step 9 from proof Decl-allocjsiz (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ¬ r1 ∈ h ∧ r1 ≠ null ∧ ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r1), (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used terms: r1

Proof step 10 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 11 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 12:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ⟨r := r1⟩ (h +h r1 = h0 ∧ r = r1), (r3 ∈ h ∨ r3 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 12 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Proof step 13 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 14:

  h = h0, null = r1, ¬ null ∈ h, ¬ null ∈ h0, ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null) ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 14 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h = h0, null = r1, ¬ null ∈ h0, ∀ r2. r2 ∈ h0 ∨ r2 = null ⊦ ∃ r2. ¬ r2 ∈ h0 ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1), (r0 ∈ h0 ∨ r0 = null) ∧ ⟨r := null⟩ (r = r1)

Rule argument

Additional information

Proof step 15 from proof Decl-allocjsiz (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  h = h0, null = r1, r0 ≠ null, ¬ null ∈ h0, ¬ r0 ∈ h0, ∀ r2. r2 ∈ h0 ∨ r2 = null ⊦ ∃ r2. ¬ r2 ∈ h0 ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

• Proof step 17:

  h = h0, null = r1, ¬ null ∈ h0, ∀ r2. r2 ∈ h0 ∨ r2 = null ⊦ ⟨r := null⟩ (r = r1), ∃ r2. ¬ r2 ∈ h0 ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 16 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 17 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Proof step 18 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 19:

  ⟨r := {h := h +h r0; r0}⟩ (h = h0 ∧ r = r1), r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1)

• Proof step 29:

  ⟨r := null⟩ (h = h0 ∧ r = r0), ¬ null ∈ h, ¬ null ∈ h0, ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null) ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r0)

Rule argument

Additional information

Proof step 19 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 20:

  ⟨r := r0⟩ (h +h r0 = h0 ∧ r = r1), r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 20 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 21:

  h +h r0 = h0, r0 = r1, r0 ≠ null, ¬ null ∈ h, ¬ null ∈ h0, ¬ r0 ∈ h ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 21 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ r0 ∈ h +h r ↔ r0 ∈ h ∨ r0 = r; (s)

Proof step 22 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 23:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ⟨r := choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used simplifier rules: decl: alloc#(; h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null};

Proof step 23 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 24:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ (∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null)) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r0. (¬ r0 ∈ h ∧ r0 ≠ null) ∧ ⟨r := {h := h +h r0; r0}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 24 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ∃ r2. ¬ r2 ∈ h ∧ r2 ≠ null ∧ ⟨r := {h := h +h r2; r2}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 25 from proof Decl-allocjsiz (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 26:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ¬ r1 ∈ h ∧ r1 ≠ null ∧ ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r1), (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Used terms: r1

Proof step 26 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1), ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 27 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 28:

  h +h r1 = h0, r1 ≠ null, ¬ null ∈ h, ¬ r1 ∈ h ⊦ ⟨r := r1⟩ (h +h r1 = h0 ∧ r = r1), (r0 ∈ h ∨ r0 = null) ∧ ⟨r := null⟩ (h = h0 ∧ r = r1)

Rule argument

Additional information

Proof step 28 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Proof step 29 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 30:

  h = h0, null = r0, ¬ null ∈ h, ¬ null ∈ h0, ∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null) ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r0)

Rule argument

Additional information

Proof step 30 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  h = h0, null = r0, ¬ null ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ ⟨r := alloc#(; h)⟩ (h = h0 ∧ r = r0)

Rule argument

Additional information

Proof step 31 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 32:

  h = h0, null = r0, ¬ null ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ ⟨r := choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null⟩ (h = h0 ∧ r = r0)

Rule argument

Additional information

Used simplifier rules: decl: alloc#(; h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null};

Proof step 32 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 33:

  h = h0, null = r2, ¬ null ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ (∀ r0. ¬(¬ r0 ∈ h ∧ r0 ≠ null)) ∧ ⟨r := null⟩ (h = h0 ∧ r = r2), ∃ r0. (¬ r0 ∈ h ∧ r0 ≠ null) ∧ ⟨r := {h := h +h r0; r0}⟩ (h = h0 ∧ r = r2)

Rule argument

Additional information

Proof step 33 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  h = h0, null = r2, ¬ null ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ (r0 ∈ h0 ∨ r0 = null) ∧ ⟨r := null⟩ (r = r2), ∃ r1. ¬ r1 ∈ h0 ∧ r1 ≠ null ∧ ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r2)

Rule argument

Additional information

Proof step 34 from proof Decl-allocjsiz (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 35:

  h = h0, null = r2, r0 ≠ null, ¬ null ∈ h0, ¬ r0 ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ ∃ r1. ¬ r1 ∈ h0 ∧ r1 ≠ null ∧ ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r2)

• Proof step 36:

  h = h0, null = r2, ¬ null ∈ h0, ∀ r1. r1 ∈ h0 ∨ r1 = null ⊦ ⟨r := null⟩ (r = r2), ∃ r1. ¬ r1 ∈ h0 ∧ r1 ≠ null ∧ ⟨r := {h := h +h r1; r1}⟩ (h = h0 ∧ r = r2)

Rule argument

Additional information

Proof step 35 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 36 from proof Decl-allocjsiz (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information