Proof step 1 from proof switch-ownership (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  !(me, hO1, hP) ≠ !(me, hO2, hP), rely(me, hO1, h1, hO2, h2) ⊦

Rule argument

Additional information

Proof step 2 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  !(me, hO1, hP) ≠ !(me, hO2, hP), rely(me, hO1, h1, hO2, h2) ⊦

Rule argument

Additional information

Proof step 3 from proof switch-ownership (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 4:

  ¬(!(me, hO1, hP)(h) ↔ !(me, hO2, hP)(h)), rely(me, hO1, h1, hO2, h2) ⊦

Rule argument

Additional information

Proof step 4 from proof switch-ownership (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  !(me, hO1, hP)(h), rely(me, hO1, h1, hO2, h2), ¬ !(me, hO2, hP)(h) ⊦

• Proof step 16:

  !(me, hO2, hP)(h), rely(me, hO1, h1, hO2, h2), ¬ !(me, hO1, hP)(h) ⊦

Rule argument

Additional information

Proof step 5 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 7:

  hP(h), rely(me, hO1, h1, hO2, h2), ¬ !(me, hO2, hP)(h), ∀ r. r ∈ h → hO1(r) = me ⊦

Rule argument

Additional information

Used terms: h, hP, hO1, me

Proof step 6 from proof switch-ownership (previous step) (back to tree)

Lemma owned

Proof step 7 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  hP(h), rely(me, hO1, h1, hO2, h2), ¬ !(me, hO2, hP)(h), ∀ r. r ∈ h → hO1(r) = me ⊦

Rule argument

Additional information

Proof step 8 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 10:

  hP(h), rely(me, hO1, h1, hO2, h2), ∀ r. r ∈ h → hO1(r) = me, ¬ hP(h) ∨ (∃ r. ¬(r ∈ h → hO2(r) = me)) ⊦

Rule argument

Additional information

Used terms: h, hP, hO2, me

Proof step 9 from proof switch-ownership (previous step) (back to tree)

Lemma owned

Proof step 10 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  hO2(r) ≠ me, hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h, ∀ r. r ∈ h → hO1(r) = me ⊦

Rule argument

Additional information

Proof step 11 from proof switch-ownership (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  hO2(r) ≠ me, hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h, r ∈ h → hO1(r) = me ⊦

Rule argument

Additional information

Used terms: r

Proof step 12 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  hO2(r) ≠ hO1(r), hP(h), rely(hO1(r), hO1, h1, hO2, h2), r ∈ h ⊦

Rule argument

Additional information

Proof step 13 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ rely(me, of1, h1, of2, h2) ↔ (∀ r. (of1(r) = me ↔ of2(r) = me) ∧ (of1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r])))

• Proof step 15:

  hO2(r) ≠ hO1(r), hP(h), r ∈ h, ∀ r0. (hO1(r0) = hO1(r) ↔ hO2(r0) = hO1(r)) ∧ (hO1(r0) = hO1(r) → (r0 ∈ h1 ↔ r0 ∈ h2) ∧ (r0 ∈ h1 → h1[r0] = h2[r0])) ⊦

Rule argument

Additional information

Used terms: hO2, hO1, hO1(r), h1, h2

Proof step 14 from proof switch-ownership (previous step) (back to tree)

Lemma rely

Proof step 15 from proof switch-ownership (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 16 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 18:

  !(me, hO2, hP)(h), rely(me, hO1, h1, hO2, h2), ¬ hP(h) ∨ (∃ r. ¬(r ∈ h → hO1(r) = me)) ⊦

Rule argument

Additional information

Used terms: h, hP, hO1, me

Proof step 17 from proof switch-ownership (previous step) (back to tree)

Lemma owned

Proof step 18 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  hO1(r) ≠ me, !(me, hO2, hP)(h), hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: owned-P: ⊦ !(me, hO, hP)(h) ∧ ¬ hP(h) → false;

Proof step 19 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 21:

  hO1(r) ≠ me, hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h, ∀ r. r ∈ h → hO2(r) = me ⊦

Rule argument

Additional information

Used terms: h, hP, hO2, me

Proof step 20 from proof switch-ownership (previous step) (back to tree)

Lemma owned

Proof step 21 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  hO1(r) ≠ me, hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h, ∀ r. r ∈ h → hO2(r) = me ⊦

Rule argument

Additional information

Proof step 22 from proof switch-ownership (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  hO1(r) ≠ me, hP(h), rely(me, hO1, h1, hO2, h2), r ∈ h, r ∈ h → hO2(r) = me ⊦

Rule argument

Additional information

Used terms: r

Proof step 23 from proof switch-ownership (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  hO1(r) ≠ hO2(r), hP(h), rely(hO2(r), hO1, h1, hO2, h2), r ∈ h ⊦

Rule argument

Additional information

Proof step 24 from proof switch-ownership (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ rely(me, of1, h1, of2, h2) ↔ (∀ r. (of1(r) = me ↔ of2(r) = me) ∧ (of1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r])))

• Proof step 26:

  hO1(r) ≠ hO2(r), hP(h), r ∈ h, ∀ r0. (hO1(r0) = hO2(r) ↔ hO2(r0) = hO2(r)) ∧ (hO1(r0) = hO2(r) → (r0 ∈ h1 ↔ r0 ∈ h2) ∧ (r0 ∈ h1 → h1[r0] = h2[r0])) ⊦

Rule argument

Additional information

Used terms: hO2, hO1, hO2(r), h1, h2

Proof step 25 from proof switch-ownership (previous step) (back to tree)

Lemma rely

Proof step 26 from proof switch-ownership (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r