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

User applied rule case distinction

And obtained the following new goals

• Proof step 79:

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

• Proof step 86:

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

Rule argument

Additional information