Proof step 35 from proof rely-owned-unchgd (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 36:

  rs2 ∩ rs1 = ∅, P(mk(rs2, f)), ∀ r. (g(r) = a ∧ r ∈ rs2 ∪ rs1 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs2 ∪ rs1 → f(r) = f0(r)), ∀ r. r ∈ rs2 → g(r) = a ⊦ P(mk(rs2, f0))

• Proof step 43:

  rs2 ∩ rs1 = ∅, P(mk(rs2, f)), r ∈ rs2, ∀ r. (g(r) = a ∧ r ∈ rs2 ∪ rs1 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs2 ∪ rs1 → f(r) = f0(r)), ∀ r. r ∈ rs2 → g(r) = a ⊦ g0(r) = a

Rule argument

Additional information