Proof step 1 from proof trp-ignore-subtree (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  trp(r, t(p := t0), p, r1) ≠ trp(r, t, p, r1), p ∈ t ⊦

Rule argument

Additional information

Proof step 2 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  trp(r, t(b + p0 := t0), b + p0, r1) ≠ trp(r, t, b + p0, r1), b + p0 ∈ t, ∀ r, t, t0, r1. ¬(trp(r, t(p0 := t0), p0, r1) ≠ trp(r, t, p0, r1) ∧ p0 ∈ t) ⊦

Rule argument

Additional information

Used simplifier rules: trp-base: ⊦ trp(r, t, [], r0) = (⌜r = r0⌝ ∧ emp); List[A] freely generated by [], +; ⊦ t([] := t0) = t0; (s) ⊦ hP0 = hP1 → ((hP ∧ hP0) = (hP ∧ hP1) ↔ true); (ss) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep

Proof step 3 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  trp(r, t(b ' + p0 := t0), b ' + p0, r1) ≠ trp(r, t, b ' + p0, r1), b ' + p0 ∈ t, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

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

Proof step 4 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  t = branch(t3, a, t4), trp(r, t(b ' + p0 := t0), b ' + p0, r1) ≠ trp(r, t, b ' + p0, r1), b ' + p0 ∈ t, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Used simplifier rules: trp-leaf: ⊦ trp(r, leaf, b ' + p, r0) = false; Tree[A] freely generated by leaf, branch; ⊦ p ∈ leaf ↔ p = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 5 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  trp(r, (b ⊃ branch(t3, a, t4(p0 := t0));branch(t3(p0 := t0), a, t4)), b ' + p0, r1) ≠ trp(r, branch(t3, a, t4), b ' + p0, r1), p0 ∈ (b ⊃ t4;t3), ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

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 := t0) = (b ⊃ branch(t1, a, t2(p := t0));branch(t1(p := t0), a, t2)); (s)

Proof step 6 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  b, trp(r, branch(t3, a, t4(p0 := t0)), b ' + p0, r1) ≠ trp(r, branch(t3, a, t4), b ' + p0, r1), p0 ∈ (b ⊃ t4;t3), ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

• Proof step 24:

  ¬ b, trp(r, branch(t3(p0 := t0), a, t4), b ' + p0, r1) ≠ trp(r, branch(t3, a, t4), b ' + p0, r1), p0 ∈ (b ⊃ t4;t3), ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 7 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  trp(r, branch(t3, a, t4(p0 := t0)), true ' + p0, r1) ≠ trp(r, branch(t3, a, t4), true ' + p0, r1), p0 ∈ t4, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 8 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 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 10:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: r, p0, true, r1, t4(p0 := t0), a, t3

Proof step 9 from proof trp-ignore-subtree (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 10 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 11 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ 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 13:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: r, p0, true, r1, t4, a, t3

Proof step 12 from proof trp-ignore-subtree (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 13 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  _∃(λ r2, r3. r => mknode(r2, a, r3) * tr(r2, t3) * trp(r3, t4(p0 := t0), p0, r1)) ≠ _∃(λ r2, r3. r => mknode(r2, a, r3) * tr(r2, t3) * trp(r3, t4, p0, r1)), p0 ∈ t4, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 14 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Proof step 15 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

Proof step 16 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 17:

  ¬((r => mknode(r0, a, c) * tr(r0, t3) * trp(c, t4(p0 := t0), p0, r1))(h) ↔ (r => mknode(r0, a, c) * tr(r0, t3) * trp(c, t4, p0, r1))(h)), p0 ∈ t4, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 17 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

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

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(c, t4, p0, r1), r => mknode(r0, a, c) * tr(r0, t3)

Proof step 18 from proof trp-ignore-subtree (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

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

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(c, t4(p0 := t0), p0, r1), r => mknode(r0, a, c) * tr(r0, t3)

Proof step 20 from proof trp-ignore-subtree (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Proof step 22 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ¬(trp(c, t4(p0 := t0), p0, r1)(h0) ↔ trp(c, t4, p0, r1)(h0)), h0 ⊥ h1, p0 ∈ t4, (r => mknode(r0, a, c) * tr(r0, t3))(h1), ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 23 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c, t4, t0, r1

Proof step 24 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  trp(r, branch(t3(p0 := t0), a, t4), false ' + p0, r1) ≠ trp(r, branch(t3, a, t4), false ' + p0, r1), p0 ∈ t3, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 25 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ 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 27:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: r, p0, false, r1, t4, a, t3(p0 := t0)

Proof step 26 from proof trp-ignore-subtree (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 27 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 28 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ 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 30:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: r, p0, false, r1, t4, a, t3

Proof step 29 from proof trp-ignore-subtree (previous step) (back to tree)

Lemma trp-branch-rec

Proof step 30 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  _∃(λ r2, r3. r => mknode(r2, a, r3) * trp(r2, t3(p0 := t0), p0, r1) * tr(r3, t4)) ≠ _∃(λ r2, r3. r => mknode(r2, a, r3) * trp(r2, t3, p0, r1) * tr(r3, t4)), p0 ∈ t3, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 31 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Proof step 32 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

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

Proof step 33 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 34:

  ¬((r => mknode(r0, a, c) * trp(r0, t3(p0 := t0), p0, r1) * tr(c, t4))(h) ↔ (r => mknode(r0, a, c) * trp(r0, t3, p0, r1) * tr(c, t4))(h)), p0 ∈ t3, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 34 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  p0 ∈ t3, ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ trp(r0, t3(p0 := t0), p0, r1)(h0) ∧ (r => mknode(r0, a, c) * tr(c, t4))(h1)) ↔ (r => mknode(r0, a, c) * trp(r0, t3, p0, r1) * tr(c, t4))(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(r0, t3(p0 := t0), p0, r1), r => mknode(r0, a, c) * tr(c, t4)

Proof step 35 from proof trp-ignore-subtree (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

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

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(r0, t3, p0, r1), r => mknode(r0, a, c) * tr(c, t4)

Proof step 37 from proof trp-ignore-subtree (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

Proof step 39 from proof trp-ignore-subtree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  ¬(trp(r0, t3(p0 := t0), p0, r1)(h0) ↔ trp(r0, t3, p0, r1)(h0)), h0 ⊥ h1, p0 ∈ t3, (r => mknode(r0, a, c) * tr(c, t4))(h1), ∀ r0, t1, t2, r2. trp(r0, t1(p0 := t2), p0, r2) = trp(r0, t1, p0, r2) ∨ ¬ p0 ∈ t1 ⊦

Rule argument

Additional information

Proof step 40 from proof trp-ignore-subtree (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0, t3, t0, r1