Proof step 1 from proof lift-unknown (conclusion) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  (r ==>_ * hR)[rs, f, g] ⊦ ∃ a. (a[r =>_] * hR)[rs, f, g]

• Proof step 41:

  ¬ (r ==>_ * hR)[rs, f, g], ∃ a. (a[r =>_] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 2 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ r ==>_ = _∃(λ o, a. r ==>(o, a))

• Proof step 4:

  (_∃(λ o, a. r ==>(o, a)) * hR)[rs, f, g] ⊦ ∃ a. (a[r =>_] * hR)[rs, f, g]

Rule argument

Additional information

Used terms: r

Proof step 3 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (r ==>(o, a) * hR)[rs, f, g] ⊦ ∃ a. (a[r =>_] * hR)[rs, f, g]

Rule argument

Additional information

Used simplifier rules: 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] ⊦ (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]); (s)

Proof step 5 from proof lift-unknown (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  (r ==>(o, a) * hR)[rs, f, g], ¬ (a[r =>_] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Used terms: a

Proof step 6 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  ¬ (a[r =>_] * hR)[rs, f, g], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ r ==>(o, a)[rs0, f, g] ∧ hR[rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs, hR, g, r ==>(o, a), f

Proof step 7 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  rs0 ∩ rs1 = ∅, r ==>(o, a)[rs0, f, g], hR[rs1, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g] ⊦

Rule argument

Additional information

Proof step 9 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], r ==>(o, a)[rs0, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r =>_][rs0, f, g] ∧ hR[rs1, f, g] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: rs0, hR, g, a[r =>_], f, rs1

Proof step 10 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  rs0 ∩ rs1 = ∅, r ==>(o, a)[rs0, f, g], hR[rs1, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g], ¬ a[r =>_][rs0, f, g] ⊦

Rule argument

Additional information

Proof step 12 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], r ==>(o, a)[rs0, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g], ¬ a[r =>_](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a[r =>_]

Proof step 13 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  rs0 ∩ rs1 = ∅, r ==>(o, a)[rs0, f, g], hR[rs1, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g], ¬ r =>_(mk(rs0, f)) ∨ (∃ r. ¬(r ∈ rs0 → g(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, r =>_, rs0, g, f

Proof step 15 from proof lift-unknown (previous step) (back to tree)

Lemma lift-aux

Proof step 16 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], r ==>(o, a)[rs0, f, g], ¬ (a[r =>_] * hR)[rs0 ∪ rs1, f, g], ¬ r =>_(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Proof step 17 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ r =>_ = _∃(λ o. r => o)

• Proof step 19:

  rs0 ∩ rs1 = ∅, r ==>(o, a)[rs0, f, g], hR[rs1, f, g], ¬ (a[_∃(λ o. r => o)] * hR)[rs0 ∪ rs1, f, g], ¬ (_∃(λ o. r => o))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Used terms: r

Proof step 18 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], r ==>(o, a)[rs0, f, g], ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used simplifier rules: lift-ex-o: ⊦ a[_∃ ohP] = _∃(λ o, a0. a[ohP(o)]); ⊦ (_∃ oP)(h) ↔ (∃ o. oP(o)(h)); (s) 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] ⊦ (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]); (s)

Proof step 20 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  rs0 ∩ rs1 = ∅, r ==>(o, a)(mk(rs0, f, g)), hR[rs1, f, g], ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: g, f, rs0, r ==>(o, a)

Proof step 21 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ r ==>(o, a)(ha) ↔ ha = (∅ ++ r)[r, o, a] ∧ r ≠ null

• Proof step 24:

  mk(rs0, f, g) = (∅ ++ r)[r, o, a], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

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

Proof step 23 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  mk(rs0, f, g) = (∅ ++ r)[r, o, a], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 25 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r0. (r0 ∈ mk(rs0, f, g) ↔ r0 ∈ (∅ ++ r)[r, o, a]) ∧ (r0 ∈ mk(rs0, f, g) → mk(rs0, f, g)[r0]o = (∅ ++ r)[r, o, a][r0]o ∧ mk(rs0, f, g)[r0]a = (∅ ++ r)[r, o, a][r0]a), ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: mk(rs0, f, g), (∅ ++ r)[r, o, a]

Proof step 26 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r1. (r1 ∈ rs0 ↔ r1 ∈ (∅ ++ r)[r, o, a]) ∧ (r1 ∈ rs0 → f(r1) = (∅ ++ r)[r, o, a][r1]o ∧ g(r1) = (∅ ++ r)[r, o, a][r1]a), ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, 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 28 from proof lift-unknown (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  r ∈ rs0 ↔ r ∈ (∅ ++ r)[r, o, a], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r ∈ rs0 → f(r) = (∅ ++ r)[r, o, a][r]o ∧ g(r) = (∅ ++ r)[r, o, a][r]a, ∀ r1. (r1 ∈ rs0 ↔ r1 ∈ (∅ ++ r)[r, o, a]) ∧ (r1 ∈ rs0 → f(r1) = (∅ ++ r)[r, o, a][r1]o ∧ g(r1) = (∅ ++ r)[r, o, a][r1]a), ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦ ∃ o. (a[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: r

Proof step 29 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)), ¬(∃ o. ((r => o))(mk(rs0, f))) ∨ ¬(r0 ∈ rs0 → g(r0) = g(r)) ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[refset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[refset] r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) ⊦ ha[r0, o, a][r]a = (r = r0 ∧ r0 ∈ ha ⊃ a;ha[r]a); (s) ⊦ ha[r0, o, a][r]o = (r = r0 ∧ r0 ∈ ha ⊃ o;ha[r]o); (s) ⊦ r ∈ ha[r0, o, a] ↔ r ∈ ha; (s)

Proof step 30 from proof lift-unknown (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 31:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g], ∃ o. ((r => o))(mk(rs0, f))

• Proof step 39:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, g(r0) ≠ g(r), r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r0 ∈ rs0, r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 31 from proof lift-unknown (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ¬ ((r => f(r)))(mk(rs0, f)), ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. ((r => o))(mk(rs0, f)), ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: f(r)

Proof step 32 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null

• Proof step 34:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)), mk(rs0, f) ≠ (∅ ++ r)[r, f(r)] ∨ r = null ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g], ∃ o. ((r => o))(mk(rs0, f))

Rule argument

Additional information

Used terms: mk(rs0, f), f(r), r

Proof step 33 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, mk(rs0, f) ≠ (∅ ++ r)[r, f(r)], r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. ((r => o))(mk(rs0, f)), ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 35 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 37:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)), ∃ r0. ¬((r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, f(r)]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, f(r)][r0])) ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g], ∃ o. ((r => o))(mk(rs0, f))

Rule argument

Additional information

Used terms: (∅ ++ r)[r, f(r)], mk(rs0, f)

Proof step 36 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 37 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. ((r => o))(mk(rs0, f)), ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g], (r0 ∈ rs0 → r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ f(r);(∅ ++ r)[r0]))

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); (s) ⊦ r ∈ rs → mk(rs, f)[r] = f(r); (s) ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

Proof step 38 from proof lift-unknown (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 39 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, g(r0) ≠ g(r), r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r ∈ rs0, r0 ∈ rs0, ∀ r1. (r1 ∈ rs0 → r1 = r) ∧ (r1 ∈ rs0 → f(r1) = (r1 = r ⊃ f(r);(∅ ++ r)[r1]o) ∧ g(r1) = (r1 = r ⊃ g(r);(∅ ++ r)[r1]a)) ⊦ ∃ o. (g(r)[r => o] * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 40 from proof lift-unknown (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 41 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  (a[r =>_] * hR)[rs, f, g], ¬ (r ==>_ * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 42 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  ¬ (r ==>_ * hR)[rs, f, g], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[r =>_][rs0, f, g] ∧ hR[rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs, hR, g, a[r =>_], f

Proof step 43 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  rs0 ∩ rs1 = ∅, a[r =>_][rs0, f, g], hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g] ⊦

Rule argument

Additional information

Proof step 45 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

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

• Proof step 47:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r =>_][rs0, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g] ⊦ r ==>_[rs0, f, g] ∧ hR[rs1, f, g] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: rs0, hR, g, r ==>_, f, rs1

Proof step 46 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  rs0 ∩ rs1 = ∅, a[r =>_][rs0, f, g], hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g] ⊦

Rule argument

Additional information

Proof step 48 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r =>_](mk(rs0, f, g)), ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g] ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a[r =>_]

Proof step 49 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

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

• Proof step 52:

  rs0 ∩ rs1 = ∅, r =>_(mk(rs0, f)), hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, r =>_, rs0, g, f

Proof step 51 from proof lift-unknown (previous step) (back to tree)

Lemma lift-aux

Proof step 52 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  rs0 ∩ rs1 = ∅, r =>_(mk(rs0, f)), hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 53 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ r =>_ = _∃(λ o. r => o)

• Proof step 55:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], (_∃(λ o. r => o))(mk(rs0, f)), ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: r

Proof step 54 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  rs0 ∩ rs1 = ∅, ((r => o))(mk(rs0, f)), hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ oP)(h) ↔ (∃ o. oP(o)(h)); (s)

Proof step 56 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null

• Proof step 58:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

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

Proof step 57 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 58 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ¬ r ==>_[rs0, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 59 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

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

• Proof step 61:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ r ==>_(mk(rs0, f, g)), ¬ (r ==>_ * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: g, f, rs0, r ==>_

Proof step 60 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ r ==>_ = _∃(λ o, a. r ==>(o, a))

• Proof step 63:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (_∃(λ o, a. r ==>(o, a)) * hR)[rs0 ∪ rs1, f, g], ¬ (_∃(λ o, a. r ==>(o, a)))(mk(rs0, f, g)), ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: r

Proof step 62 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 63 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], ∃ o, a. r ==>(o, a)(mk(rs0, f, g))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ oaR)(ha) ↔ (∃ o, a. oaR(o, a)(ha)); (s) 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] ⊦ (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]); (s)

Proof step 64 from proof lift-unknown (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 65:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ r ==>(o, a)(mk(rs0, f, g)), ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: o, a

Proof step 65 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ r ==>(o, a)(ha) ↔ ha = (∅ ++ r)[r, o, a] ∧ r ≠ null

• Proof step 67:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, mk(rs0, f, g) ≠ (∅ ++ r)[r, o, a] ∨ r = null ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

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

Proof step 66 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, mk(rs0, f, g) ≠ (∅ ++ r)[r, o, a], r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 68 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 70:

  rs0 ∩ rs1 = ∅, mk(rs0, f, g) ≠ (∅ ++ r)[r, o, a], r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, o]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, o][r0]) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: (∅ ++ r)[r, o], mk(rs0, f)

Proof step 69 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  rs0 ∩ rs1 = ∅, mk(rs0, f, g) ≠ (∅ ++ r)[r, o, a], r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); (s) ⊦ r ∈ rs → mk(rs, f)[r] = f(r); (s) ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

Proof step 71 from proof lift-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a, ∃ r0. ¬ ( (r0 ∈ mk(rs0, f, g) ↔ r0 ∈ (∅ ++ r)[r, o, a]) ∧ (r0 ∈ mk(rs0, f, g) → mk(rs0, f, g)[r0]o = (∅ ++ r)[r, o, a][r0]o ∧ mk(rs0, f, g)[r0]a = (∅ ++ r)[r, o, a][r0]a)) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Used terms: mk(rs0, f, g), (∅ ++ r)[r, o, a]

Proof step 72 from proof lift-unknown (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0]o) ∧ g(r0) = (r0 = r ⊃ a;(∅ ++ r)[r0]a))

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) ⊦ ha[r0, o, a][r]a = (r = r0 ∧ r0 ∈ ha ⊃ a;ha[r]a); (s) ⊦ r ∈ rs → mk(rs, f, g)[r]a = g(r); (s) ⊦ ha[r0, o, a][r]o = (r = r0 ∧ r0 ∈ ha ⊃ o;ha[r]o); (s) ⊦ r ∈ rs → mk(rs, f, g)[r]o = f(r); (s) ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s) ⊦ r ∈ ha[r0, o, a] ↔ r ∈ ha; (s)

Proof step 74 from proof lift-unknown (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 75:

  r0 = r, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0]o) ∧ g(r0) = (r0 = r ⊃ a;(∅ ++ r)[r0]a))

• Proof step 79:

  rs0 ∩ rs1 = ∅, r ≠ null, r0 ≠ r, hR[rs1, f, g], ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0]o) ∧ g(r0) = (r0 = r ⊃ a;(∅ ++ r)[r0]a))

Rule argument

Additional information

Used formulas: r0 = r

Proof step 75 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], r ∈ rs0 ∧ f(r) = o ∧ g(r) = a

Rule argument

Additional information

Proof step 76 from proof lift-unknown (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 77:

  r ∈ rs0 ↔ r = r, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r ∈ rs0 → f(r) = (r = r ⊃ o;(∅ ++ r)[r]), ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g], r ∈ rs0 ∧ f(r) = o ∧ g(r) = a

Rule argument

Additional information

Used terms: r

Proof step 77 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], r ∈ rs0, ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 → r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ f(r);(∅ ++ r)[r0])) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 78 from proof lift-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 79 from proof lift-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  rs0 ∩ rs1 = ∅, r ≠ null, r0 ≠ r, hR[rs1, f, g], r0 ∈ rs0, ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])) ⊦ ∃ o, a. (r ==>(o, a) * hR)[rs0 ∪ rs1, f, g]

Rule argument

Additional information

Proof step 80 from proof lift-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0