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: h2, hO0, h0, me, hO2

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: h2, hO1, h1, me, hO2

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: h1, hO0, h0, me, hO1

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