Proof step 1 from proof rely-trans (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  rely(me, hO0, h0, hO1, h1), rely(me, hO1, h1, hO2, h2), ¬ rely(me, hO0, h0, hO2, h2) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-trans (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  rely(me, hO1, h1, hO2, h2), rely(me, hO0, h0, hO1, h1), ¬ rely(me, hO0, h0, hO2, h2) ⊦

Rule argument

Additional information

Proof step 3 from proof rely-trans (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

  rely(me, hO0, h0, hO1, h1), rely(me, hO1, h1, hO2, h2), ∃ r. ¬((hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))) ⊦

Rule argument

Additional information

Used terms: hO2, hO0, me, h0, h2

Proof step 4 from proof rely-trans (previous step) (back to tree)

Lemma rely

Proof step 5 from proof rely-trans (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rely(me, hO1, h1, hO2, h2), rely(me, hO0, h0, hO1, h1) ⊦ (hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))

Rule argument

Additional information

Proof step 6 from proof rely-trans (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

  rely(me, hO0, h0, hO1, h1), ∀ r. (hO1(r) = me ↔ hO2(r) = me) ∧ (hO1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r])) ⊦ (hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))

Rule argument

Additional information

Used terms: hO2, hO1, me, h1, h2

Proof step 7 from proof rely-trans (previous step) (back to tree)

Lemma rely

Proof step 8 from proof rely-trans (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  hO1(r) = me ↔ hO2(r) = me, rely(me, hO0, h0, hO1, h1), hO1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r]) ⊦ (hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))

Rule argument

Additional information

Used terms: r

Proof step 9 from proof rely-trans (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  hO1(r) = me ↔ hO2(r) = me, rely(me, hO0, h0, hO1, h1), hO2(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r]) ⊦ (hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))

Rule argument

Additional information

Proof step 10 from proof rely-trans (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

  hO1(r) = me ↔ hO2(r) = me, hO2(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r]), ∀ r. (hO0(r) = me ↔ hO1(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])) ⊦ (hO0(r) = me ↔ hO2(r) = me) ∧ (hO0(r) = me → (r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h0 → h0[r] = h2[r]))

Rule argument

Additional information

Used terms: hO1, hO0, me, h0, h1

Proof step 11 from proof rely-trans (previous step) (back to tree)

Lemma rely

Proof step 12 from proof rely-trans (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r