Proof step 1 from proof tr-unfold-path (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  tr(r, t) ≠ _∃(λ r0. trp(r, t, p, r0) * tr(r0, t(p))), p ∈ t ⊦

Rule argument

Additional information

Proof step 2 from proof tr-unfold-path (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  tr(r, t) ≠ _∃(λ r0. trp(r, t, [], r0) * tr(r0, t([]))), [] ∈ t ⊦

• Proof step 5:

  tr(r, t) ≠ _∃(λ r0. trp(r, t, b + p0, r0) * tr(r0, t(b + p0))), b + p0 ∈ t, ∀ r, t. ¬(tr(r, t) ≠ _∃(λ r0. trp(r, t, p0, r0) * tr(r0, t(p0))) ∧ p0 ∈ t) ⊦

Rule argument

Additional information

Used simplifier rules: List[A] freely generated by [], +;

Proof step 3 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  tr(r, t) ≠ _∃(λ r0. ⌜r = r0⌝ ∧ tr(r0, t)) ⊦

Rule argument

Additional information

Used simplifier rules: trp-base: ⊦ trp(r, t, [], r0) = (⌜r = r0⌝ ∧ emp); ⊦ [] ∈ t; (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep ⊦ emp * hP = hP; (s) ⊦ (⌜bv⌝ ∧ hP0) * hP1 = (⌜bv⌝ ∧ hP0 * hP1); (s) ⊦ t([]) = t; (s)

Proof step 4 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜bv⌝ (h) ↔ bv; (s) ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s) ⊦ (hP0 ∧ hP1)(h) ↔ hP0(h) ∧ hP1(h); (s) ⊦ ⌜false⌝ = false; (s) ⊦ ¬ false(h); (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep

Proof step 5 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  tr(r, t) ≠ _∃(λ r0. trp(r, t, b ' + p0, r0) * tr(r0, t(b ' + p0))), b ' + p0 ∈ t, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 6 from proof tr-unfold-path (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  t = branch(t1, a, t2), tr(r, t) ≠ _∃(λ r0. trp(r, t, b ' + p0, r0) * tr(r0, t(b ' + p0))), b ' + p0 ∈ t, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Used simplifier rules: trp-leaf: ⊦ trp(r, leaf, b ' + p, r0) = false; Tree[A] freely generated by leaf, branch; ⊦ tr(r, leaf) = (emp ∧ ⌜r = null⌝ ); (s) ⊦ false * hP = false; (s) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep ⊦ p ∈ leaf ↔ p = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 7 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  tr(r, branch(t1, a, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), b ' + p0, r0) * tr(r0, (b ⊃ t2(p0);t1(p0)))), p0 ∈ (b ⊃ t2;t1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ b ' + p ∈ branch(t1, a, t2) ↔ p ∈ (b ⊃ t2;t1); (s) ⊦ branch(t1, a, t2)(b ' + p) = (b ⊃ t2(p);t1(p)); (s)

Proof step 8 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ tr(r, branch(t0, a, t1)) = _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1))

• Proof step 10:

  _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), b ' + p0, r0) * tr(r0, (b ⊃ t2(p0);t1(p0)))), p0 ∈ (b ⊃ t2;t1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Used terms: r, t1, a, t2

Proof step 9 from proof tr-unfold-path (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof tr-unfold-path (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  b, _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), b ' + p0, r0) * tr(r0, (b ⊃ t2(p0);t1(p0)))), p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

• Proof step 43:

  ¬ b, _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), b ' + p0, r0) * tr(r0, (b ⊃ t2(p0);t1(p0)))), p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Proof step 11 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0))), p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Proof step 12 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 13:

  ¬((_∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)))(h) ↔ (_∃(λ r0. trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0))))(h)), p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Proof step 13 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ (∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)) ↔ (∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s) ⊦ (_∃ bcP)(h) ↔ (∃ b, c. bcP(b, c)(h)); (s)

Proof step 14 from proof tr-unfold-path (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0, ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h)

• Proof step 28:

  p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0, ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Proof step 15 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h)

Rule argument

Additional information

Proof step 16 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 18:

  p0 ∈ t2, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ (r => mknode(r0, a, r1) * tr(r0, t1))(h0) ∧ tr(r1, t2)(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h)

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h, r => mknode(r0, a, r1) * tr(r0, t1), tr(r1, t2)

Proof step 17 from proof tr-unfold-path (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Proof step 19 from proof tr-unfold-path (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), tr(r1, t2) = _∃(λ r. trp(r1, t2, p0, r) * tr(r, t2(p0))) ∨ ¬ p0 ∈ t2 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used terms: r1, t2

Proof step 20 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  tr(r1, t2) = _∃(λ r. trp(r1, t2, p0, r) * tr(r, t2(p0))), h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Proof step 21 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 22:

  tr(r1, t2)(h1) ↔ (_∃(λ r. trp(r1, t2, p0, r) * tr(r, t2(p0))))(h1), h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used terms: h1

Proof step 22 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), (trp(r1, t2, p0, r2) * tr(r2, t2(p0)))(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 23 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), (trp(r1, t2, p0, r2) * tr(r2, t2(p0)))(h1), ¬ (trp(r, branch(t1, a, t2), true ' + p0, r2) * tr(r2, t2(p0)))(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: r2

Proof step 24 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ trp(r, branch(t1, a, t2), b ' + p, r0) = _∃(λ r1, r2. r => mknode(r1, a, r2) * (b ⊃ tr(r1, t1) * trp(r2, t2, p, r0);trp(r1, t1, p, r0) * tr(r2, t2)))

• Proof step 26:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), (trp(r1, t2, p0, r2) * tr(r2, t2(p0)))(h1), ¬ (_∃(λ r1, r3. r => mknode(r1, a, r3) * (true ⊃ tr(r1, t1) * trp(r3, t2, p0, r2);trp(r1, t1, p0, r2) * tr(r3, t2))) * tr(r2, t2(p0)))(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: r, p0, true, r2, t2, a, t1

Proof step 25 from proof tr-unfold-path (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 26 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r0, a, r1) * tr(r0, t1))(h0), tr(r1, t2)(h1), (trp(r1, t2, p0, r2) * tr(r2, t2(p0)))(h1) ⊦ ∃ r0, c. ((r => mknode(r0, a, c) * tr(r0, t1) * trp(c, t2, p0, r2)) * tr(r2, t2(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bcP * hP)(h) ↔ (∃ b, c. (bcP(b, c) * hP)(h)); (s)

Proof step 27 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → (hP0 * hP1)(h0 ∪ h1); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r0, r1

Proof step 28 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  p0 ∈ t2, (trp(r, branch(t1, a, t2), true ' + p0, r0) * tr(r0, t2(p0)))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Proof step 29 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ trp(r, branch(t1, a, t2), b ' + p, r0) = _∃(λ r1, r2. r => mknode(r1, a, r2) * (b ⊃ tr(r1, t1) * trp(r2, t2, p, r0);trp(r1, t1, p, r0) * tr(r2, t2)))

• Proof step 31:

  (_∃(λ r1, r2. r => mknode(r1, a, r2) * (true ⊃ tr(r1, t1) * trp(r2, t2, p0, r0);trp(r1, t1, p0, r0) * tr(r2, t2))) * tr(r0, t2(p0)))(h), p0 ∈ t2, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used terms: r, p0, true, r0, t2, a, t1

Proof step 30 from proof tr-unfold-path (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 31 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  p0 ∈ t2, ((r => mknode(r1, a, r2) * tr(r1, t1) * trp(r2, t2, p0, r0)) * tr(r0, t2(p0)))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bcP * hP)(h) ↔ (∃ b, c. (bcP(b, c) * hP)(h)); (s)

Proof step 32 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 34:

  p0 ∈ t2, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0) ∧ (r => mknode(r1, a, r2) * tr(r1, t1))(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h, trp(r2, t2, p0, r0) * tr(r0, t2(p0)), r => mknode(r1, a, r2) * tr(r1, t1)

Proof step 33 from proof tr-unfold-path (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Proof step 35 from proof tr-unfold-path (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 36:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0), tr(r2, t2) = _∃(λ r1. trp(r2, t2, p0, r1) * tr(r1, t2(p0))) ∨ ¬ p0 ∈ t2 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Used terms: r2, t2

Proof step 36 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  tr(r2, t2) = _∃(λ r1. trp(r2, t2, p0, r1) * tr(r1, t2(p0))), h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Proof step 37 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 38:

  tr(r2, t2)(h0) ↔ (_∃(λ r1. trp(r2, t2, p0, r1) * tr(r1, t2(p0))))(h0), h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Used terms: h0

Proof step 38 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0), tr(r2, t2)(h0) ↔ (∃ r. (trp(r2, t2, p0, r) * tr(r, t2(p0)))(h0)) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 39 from proof tr-unfold-path (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0), ¬ tr(r2, t2)(h0) ⊦ ∃ r. (trp(r2, t2, p0, r) * tr(r, t2(p0)))(h0), ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

• Proof step 41:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), tr(r2, t2)(h0), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0), ∃ r. (trp(r2, t2, p0, r) * tr(r, t2(p0)))(h0) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Proof step 40 from proof tr-unfold-path (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 41 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  h0 ⊥ h1, p0 ∈ t2, (r => mknode(r1, a, r2) * tr(r1, t1))(h1), tr(r2, t2)(h0), (trp(r2, t2, p0, r3) * tr(r3, t2(p0)))(h0), (trp(r2, t2, p0, r0) * tr(r0, t2(p0)))(h0) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Proof step 42 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → (hP0 * hP1)(h0 ∪ h1); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r1, r2

Proof step 43 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  _∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)) ≠ _∃(λ r0. trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0))), p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Proof step 44 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 45:

  ¬ ((_∃(λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2)))(h) ↔ (_∃(λ r0. trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0))))(h)), p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Proof step 45 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ (∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)) ↔ (∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s) ⊦ (_∃ bcP)(h) ↔ (∃ b, c. bcP(b, c)(h)); (s)

Proof step 46 from proof tr-unfold-path (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 47:

  p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0, ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h)

• Proof step 60:

  p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0, ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h) ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Proof step 47 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r0, t1) * tr(r1, t2))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h)

Rule argument

Additional information

Proof step 48 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 50:

  p0 ∈ t1, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ (r => mknode(r0, a, r1) * tr(r1, t2))(h0) ∧ tr(r0, t1)(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h)

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h, r => mknode(r0, a, r1) * tr(r1, t2), tr(r0, t1)

Proof step 49 from proof tr-unfold-path (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Proof step 51 from proof tr-unfold-path (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 52:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), tr(r0, t1) = _∃(λ r1. trp(r0, t1, p0, r1) * tr(r1, t1(p0))) ∨ ¬ p0 ∈ t1 ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used terms: r0, t1

Proof step 52 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  tr(r0, t1) = _∃(λ r1. trp(r0, t1, p0, r1) * tr(r1, t1(p0))), h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Proof step 53 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 54:

  tr(r0, t1)(h1) ↔ (_∃(λ r1. trp(r0, t1, p0, r1) * tr(r1, t1(p0))))(h1), h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used terms: h1

Proof step 54 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), (trp(r0, t1, p0, r2) * tr(r2, t1(p0)))(h1) ⊦ ∃ r0. (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 55 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 56:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), (trp(r0, t1, p0, r2) * tr(r2, t1(p0)))(h1), ¬ (trp(r, branch(t1, a, t2), false ' + p0, r2) * tr(r2, t1(p0)))(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: r2

Proof step 56 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ trp(r, branch(t1, a, t2), b ' + p, r0) = _∃(λ r1, r2. r => mknode(r1, a, r2) * (b ⊃ tr(r1, t1) * trp(r2, t2, p, r0);trp(r1, t1, p, r0) * tr(r2, t2)))

• Proof step 58:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), (trp(r0, t1, p0, r2) * tr(r2, t1(p0)))(h1), ¬ (_∃(λ r1, r3. r => mknode(r1, a, r3) * (false ⊃ tr(r1, t1) * trp(r3, t2, p0, r2);trp(r1, t1, p0, r2) * tr(r3, t2))) * tr(r2, t1(p0)))(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: r, p0, false, r2, t2, a, t1

Proof step 57 from proof tr-unfold-path (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 58 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r0, a, r1) * tr(r1, t2))(h0), tr(r0, t1)(h1), (trp(r0, t1, p0, r2) * tr(r2, t1(p0)))(h1) ⊦ ∃ r0, c. ((r => mknode(r0, a, c) * trp(r0, t1, p0, r2) * tr(c, t2)) * tr(r2, t1(p0)))(h0 ∪ h1)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bcP * hP)(h) ↔ (∃ b, c. (bcP(b, c) * hP)(h)); (s)

Proof step 59 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → (hP0 * hP1)(h0 ∪ h1); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r0, r1

Proof step 60 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  p0 ∈ t1, (trp(r, branch(t1, a, t2), false ' + p0, r0) * tr(r0, t1(p0)))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Proof step 61 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ trp(r, branch(t1, a, t2), b ' + p, r0) = _∃(λ r1, r2. r => mknode(r1, a, r2) * (b ⊃ tr(r1, t1) * trp(r2, t2, p, r0);trp(r1, t1, p, r0) * tr(r2, t2)))

• Proof step 63:

  (_∃(λ r1, r2. r => mknode(r1, a, r2) * (false ⊃ tr(r1, t1) * trp(r2, t2, p0, r0);trp(r1, t1, p0, r0) * tr(r2, t2))) * tr(r0, t1(p0)))(h), p0 ∈ t1, ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used terms: r, p0, false, r0, t2, a, t1

Proof step 62 from proof tr-unfold-path (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 63 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  p0 ∈ t1, ((r => mknode(r1, a, r2) * trp(r1, t1, p0, r0) * tr(r2, t2)) * tr(r0, t1(p0)))(h), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bcP * hP)(h) ↔ (∃ b, c. (bcP(b, c) * hP)(h)); (s)

Proof step 64 from proof tr-unfold-path (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 66:

  p0 ∈ t1, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0) ∧ (r => mknode(r1, a, r2) * tr(r2, t2))(h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h)

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h, trp(r1, t1, p0, r0) * tr(r0, t1(p0)), r => mknode(r1, a, r2) * tr(r2, t2)

Proof step 65 from proof tr-unfold-path (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦ ∃ r0, c. (r => mknode(r0, a, c) * tr(r0, t1) * tr(c, t2))(h0 ∪ h1)

Rule argument

Additional information

Proof step 67 from proof tr-unfold-path (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 68:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ¬ (r => mknode(r1, a, r2) * tr(r1, t1) * tr(r2, t2))(h0 ∪ h1), ∀ r0, t0. tr(r0, t0) = _∃(λ r1. trp(r0, t0, p0, r1) * tr(r1, t0(p0))) ∨ ¬ p0 ∈ t0 ⊦

Rule argument

Additional information

Used terms: r1, r2

Proof step 68 from proof tr-unfold-path (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 69:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ¬ (r => mknode(r1, a, r2) * tr(r1, t1) * tr(r2, t2))(h0 ∪ h1), tr(r1, t1) = _∃(λ r. trp(r1, t1, p0, r) * tr(r, t1(p0))) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Used terms: r1, t1

Proof step 69 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  tr(r1, t1) = _∃(λ r. trp(r1, t1, p0, r) * tr(r, t1(p0))), h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ¬ (r => mknode(r1, a, r2) * tr(r1, t1) * tr(r2, t2))(h0 ∪ h1) ⊦

Rule argument

Additional information

Proof step 70 from proof tr-unfold-path (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 71:

  tr(r1, t1)(h0) ↔ (_∃(λ r. trp(r1, t1, p0, r) * tr(r, t1(p0))))(h0), h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ¬ (r => mknode(r1, a, r2) * tr(r1, t1) * tr(r2, t2))(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: h0

Proof step 71 from proof tr-unfold-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  h0 ⊥ h1, p0 ∈ t1, (r => mknode(r1, a, r2) * tr(r2, t2))(h1), (trp(r1, t1, p0, r0) * tr(r0, t1(p0)))(h0), ¬ (r => mknode(r1, a, r2) * tr(r1, t1) * tr(r2, t2))(h0 ∪ h1), ¬ tr(r1, t1)(h0) ⊦ ∃ r. (trp(r1, t1, p0, r) * tr(r, t1(p0)))(h0)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → (hP0 * hP1)(h0 ∪ h1); (ss) ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 72 from proof tr-unfold-path (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r0