Proof step 28 from proof mod-other-both (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  r = r0, rs1 ∩ rs0 = ∅, P(mk(rs1, f)), R[rs0, f, g], r0 ∈ rs1, ∀ r. r ∈ rs1 → g(r) = a ⊦ # rs1 = 0, a0 = a, g(r) = a, rs1 = ∅, (a[P] * true)[rs1 ∪ rs0, f(r; o), g(r; a0)]

• Proof step 31:

  rs1 ∩ rs0 = ∅, P(mk(rs1, f)), R[rs0, f, g], r0 ∈ rs1, ∀ r. r ∈ rs1 → g(r) = a ⊦ # rs1 = 0, g(r) = a, g(r0) = a, r = r0, rs1 = ∅, (a[P] * true)[rs1 ∪ rs0, f(r; o), g(r; a0)]

Rule argument

Additional information