Proof step 1 from proof write-other-true (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((a[hP] * true)[rs, f(r; o), g] ↔ (a[hP] * true)[rs, f, g]), g(r) ≠ a ⊦

Rule argument

Additional information

Proof step 2 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  g(r) ≠ a, (a[hP] * true)[rs, f(r; o), g], ¬ (a[hP] * true)[rs, f, g] ⊦

Rule argument

Additional information

Used simplifier rules: mod-other-hp: ⊦ g(r) ≠ a ∧ (a[hP] * hR)[rs, f, g] → (a[hP] * true)[rs, f(r; o), g]; sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst]

Proof step 3 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 5:

  g(r) ≠ a, ¬ (a[hP] * true)[rs, f, g], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[hP][rs0, f(r; o), g] ∧ true[rs1, f(r; o), g] ⊦

Rule argument

Additional information

Used terms: rs, true, g, a[hP], f(r; o)

Proof step 4 from proof write-other-true (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP][rs0, f(r; o), g], ¬ (a[hP] * true)[rs0 ∪ rs1, f, g] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

Proof step 6 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g]

• Proof step 8:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP][rs0, f(r; o), g], ¬ (a[hP] * true)[rs0 ∪ rs1, f, g] ⊦ a[hP][rs0, f, g] ∧ true[rs1, f, g] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: rs0, true, g, a[hP], f, rs1

Proof step 7 from proof write-other-true (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP][rs0, f(r; o), g], ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP][rs0, f, g] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

Proof step 9 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 11:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP](mk(rs0, f(r; o), g)), ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP][rs0, f, g] ⊦

Rule argument

Additional information

Used terms: g, f(r; o), rs0, a[hP]

Proof step 10 from proof write-other-true (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 13:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP](mk(rs0, f(r; o), g)), ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a[hP]

Proof step 12 from proof write-other-true (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof write-other-true (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, mk(rs0, f(r; o), g) ≠ mk(rs0, f, g), a[hP](mk(rs0, f(r; o), g)), ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used formulas: mk(rs0, f(r; o), g) = mk(rs0, f, g)

Proof step 14 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ ha0 = ha1 ↔ (∀ r. (r ∈ ha0 ↔ r ∈ ha1) ∧ (r ∈ ha0 → ha0[r]o = ha1[r]o ∧ ha0[r]a = ha1[r]a))

• Proof step 16:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP](mk(rs0, f(r; o), g)), ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)), ∃ r0. ¬ ( (r0 ∈ mk(rs0, f(r; o), g) ↔ r0 ∈ mk(rs0, f, g)) ∧ (r0 ∈ mk(rs0, f(r; o), g) → mk(rs0, f(r; o), g)[r0]o = mk(rs0, f, g)[r0]o ∧ mk(rs0, f(r; o), g)[r0]a = mk(rs0, f, g)[r0]a)) ⊦

Rule argument

Additional information

Used terms: mk(rs0, f(r; o), g), mk(rs0, f, g)

Proof step 15 from proof write-other-true (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, (r = r0 ⊃ o;f(r0)) ≠ f(r0), g(r) ≠ a, a[hP](mk(rs0, f(r; o), g)), r0 ∈ rs0, ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ rs → mk(rs, f, g)[r]a = g(r); (s) ⊦ r ∈ rs → mk(rs, f, g)[r]o = f(r); (s) ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s)

Proof step 17 from proof write-other-true (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  r = r0, rs0 ∩ rs1 = ∅, g(r) ≠ a, o ≠ f(r0), a[hP](mk(rs0, f(r; o), g)), r0 ∈ rs0, ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Proof step 18 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rs0 ∩ rs1 = ∅, g(r0) ≠ a, o ≠ f(r0), a[hP](mk(rs0, f(r0; o), g)), r0 ∈ rs0, ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Proof step 19 from proof write-other-true (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 21:

  rs0 ∩ rs1 = ∅, g(r0) ≠ a, o ≠ f(r0), hP(mk(rs0, f(r0; o))), r0 ∈ rs0, ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)), ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, hP, rs0, g, f(r0; o)

Proof step 20 from proof write-other-true (previous step) (back to tree)

Lemma lift-aux

Proof step 21 from proof write-other-true (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  rs0 ∩ rs1 = ∅, g(r0) ≠ a, o ≠ f(r0), hP(mk(rs0, f(r0; o))), r0 ∈ rs0, ¬ (a[hP] * true)[rs0 ∪ rs1, f, g], ¬ a[hP](mk(rs0, f, g)), ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 22 from proof write-other-true (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0