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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((a[hP] * true)[rs, f, g] ↔ (a[hP] * true)[rs0, f0, g0]), rely(a, rs, f, g, rs0, f0, g0) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬((a[hP] * true)[rs, f, g] ↔ (a[hP] * true)[rs0, f0, g0]), ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used simplifier rules: rely: ⊦ rely(a, rs0, f0, g0, rs1, f1, g1) ↔ (∀ r. (g0(r) = a ∧ r ∈ rs0 ↔ g1(r) = a ∧ r ∈ rs1) ∧ (g0(r) = a ∧ r ∈ rs0 → f0(r) = f1(r)));

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  (a[hP] * true)[rs, f, g], ¬ (a[hP] * true)[rs0, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

• Proof step 47:

  (a[hP] * true)[rs0, f0, g0], ¬ (a[hP] * true)[rs, f, g], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 6:

  ¬ (a[hP] * true)[rs0, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[hP][rs0, f, g] ∧ true[rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs, true, g, a[hP], f

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ¬ (a[hP] * true)[rs0, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 9:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)), ∀ rs1, rs2. ¬(rs1 ∪ rs2 = rs0 ∧ rs1 ∩ rs2 = ∅ ∧ a[hP][rs1, f0, g0] ∧ true[rs2, f0, g0]) ⊦

Rule argument

Additional information

Used terms: rs0, true, g0, a[hP], f0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)), ∀ rs, rs3. rs ∪ rs3 ≠ rs0 ∨ rs ∩ rs3 ≠ ∅ ∨ ¬ a[hP][rs, f0, g0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)), rs1 ∪ (rs0 \ rs1) ≠ rs0 ∨ rs1 ∩ (rs0 \ rs1) ≠ ∅ ∨ ¬ a[hP][rs1, f0, g0] ⊦

Rule argument

Additional information

Used terms: rs1, rs0 \ rs1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)), rs1 ∪ (rs0 \ rs1) ≠ rs0 ∨ ¬ a[hP][rs1, f0, g0] ⊦

Rule argument

Additional information

Used simplifier rules: int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union[refset] int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union[refset] ⊦ (s \ s0) ∩ s0 = ∅; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs0 \ rs1) ≠ rs0, a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)) ⊦

• Proof step 25:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f, g], ¬ a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)) ⊦

Rule argument

Additional information

Proof step 13 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs0 \ rs1) ≠ rs0, a[hP][rs1, f, g], ¬ rs1 ⊆ rs0, ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ s ⊆ s0 → s ∪ (s0 \ s) = s0; (s) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] Used formulas: rs1 ⊆ rs0

Proof step 14 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 16:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs0 \ rs1) ≠ rs0, a[hP](mk(rs1, f, g)), ¬ rs1 ⊆ rs0, ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used terms: g, f, rs1, a[hP]

Proof step 15 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 18:

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

Rule argument

Additional information

Used terms: a, hP, rs1, g, f

Proof step 17 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

• Proof step 21:

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

Rule argument

Additional information

Used terms: rs0, rs1

Proof step 20 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Proof step 22 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used terms: r

Proof step 23 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  rs1 ∩ rs2 = ∅, g(r) ≠ a, rs1 ∪ (rs0 \ rs1) ≠ rs0, hP(mk(rs1, f)), r ∈ rs1, r ∈ rs1 ∪ rs2, ¬ r ∈ rs0, ∀ r. r ∈ rs1 → g(r) = a ⊦

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 24 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 25 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 27:

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

Rule argument

Additional information

Used terms: g, f, rs1, a[hP]

Proof step 26 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 29:

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

Rule argument

Additional information

Used terms: g0, f0, rs1, a[hP]

Proof step 28 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 31:

  rs1 ∩ rs2 = ∅, a[hP](mk(rs1, f, g)), ∀ r. (g(r) = a ∧ r ∈ rs1 ∪ rs2 ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs1 ∪ rs2 → f(r) = f0(r)), ¬ hP(mk(rs1, f0)) ∨ (∃ r. ¬(r ∈ rs1 → g0(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, hP, rs1, g0, f0

Proof step 30 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Proof step 32 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 34:

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

Rule argument

Additional information

Used terms: a, hP, rs1, g, f

Proof step 33 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 36:

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

• Proof step 43:

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

Rule argument

Additional information

Proof step 36 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

Used formulas: mk(rs1, f0) = mk(rs1, f)

Proof step 37 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 39:

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

Rule argument

Additional information

Used terms: mk(rs1, f), mk(rs1, f0)

Proof step 38 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ rs → mk(rs, f)[r] = f(r); (s) ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s)

Proof step 40 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

Used terms: r

Proof step 41 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

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

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 42 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 43 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

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

Rule argument

Additional information

Proof step 44 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

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

Rule argument

Additional information

Used terms: r

Proof step 45 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 46 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 47 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 49:

  ¬ (a[hP] * true)[rs, f, g], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∃ rs1, rs2. rs1 ∪ rs2 = rs0 ∧ rs1 ∩ rs2 = ∅ ∧ a[hP][rs1, f0, g0] ∧ true[rs2, f0, g0] ⊦

Rule argument

Additional information

Used terms: rs0, true, g0, a[hP], f0

Proof step 48 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ¬ (a[hP] * true)[rs, f, g], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

Proof step 50 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 52:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∀ rs0, rs1. ¬(rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[hP][rs0, f, g] ∧ true[rs1, f, g]) ⊦

Rule argument

Additional information

Used terms: rs, true, g, a[hP], f

Proof step 51 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 52 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∀ rs0, rs3. rs0 ∪ rs3 ≠ rs ∨ rs0 ∩ rs3 ≠ ∅ ∨ ¬ a[hP][rs0, f, g] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ true[rs, f, g]; (s)

Proof step 53 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 54:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), rs1 ∪ (rs \ rs1) ≠ rs ∨ rs1 ∩ (rs \ rs1) ≠ ∅ ∨ ¬ a[hP][rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs1, rs \ rs1

Proof step 54 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), rs1 ∪ (rs \ rs1) ≠ rs ∨ ¬ a[hP][rs1, f, g] ⊦

Rule argument

Additional information

Used simplifier rules: int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union[refset] int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union[refset] ⊦ (s \ s0) ∩ s0 = ∅; (s)

Proof step 55 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 56:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs \ rs1) ≠ rs, a[hP][rs1, f0, g0], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

• Proof step 68:

  rs1 ∩ rs2 = ∅, a[hP][rs1, f0, g0], ¬ a[hP][rs1, f, g], ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

Proof step 56 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 57:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs \ rs1) ≠ rs, a[hP][rs1, f0, g0], ¬ rs1 ⊆ rs, ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ s ⊆ s0 → s ∪ (s0 \ s) = s0; (s) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] Used formulas: rs1 ⊆ rs

Proof step 57 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 59:

  rs1 ∩ rs2 = ∅, rs1 ∪ (rs \ rs1) ≠ rs, a[hP](mk(rs1, f0, g0)), ¬ rs1 ⊆ rs, ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs1 ∪ rs2) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦

Rule argument

Additional information

Used terms: g0, f0, rs1, a[hP]

Proof step 58 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 61:

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

Rule argument

Additional information

Used terms: a, hP, rs1, g0, f0

Proof step 60 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

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

Rule argument

Additional information

Proof step 62 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

• Proof step 64:

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

Rule argument

Additional information

Used terms: rs, rs1

Proof step 63 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

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

Rule argument

Additional information

Proof step 65 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 66:

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

Rule argument

Additional information

Used terms: r

Proof step 66 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  rs1 ∩ rs2 = ∅, g0(r) ≠ a, rs1 ∪ (rs \ rs1) ≠ rs, hP(mk(rs1, f0)), r ∈ rs1, r ∈ rs1 ∪ rs2, ¬ r ∈ rs, ∀ r. r ∈ rs1 → g0(r) = a ⊦

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 67 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 68 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 70:

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

Rule argument

Additional information

Used terms: g, f, rs1, a[hP]

Proof step 69 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 72:

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

Rule argument

Additional information

Used terms: g0, f0, rs1, a[hP]

Proof step 71 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 72 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 74:

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

Rule argument

Additional information

Used terms: a, hP, rs1, g0, f0

Proof step 73 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 74 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

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

Rule argument

Additional information

Proof step 75 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 77:

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

Rule argument

Additional information

Used terms: a, hP, rs1, g, f

Proof step 76 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 79:

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

• Proof step 86:

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

Rule argument

Additional information

Proof step 79 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 80:

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

Rule argument

Additional information

Used formulas: mk(rs1, f0) = mk(rs1, f)

Proof step 80 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 82:

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

Rule argument

Additional information

Used terms: mk(rs1, f), mk(rs1, f0)

Proof step 81 from proof rely-owned-unchgd (previous step) (back to tree)

A spec-lemma

Proof step 82 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ rs → mk(rs, f)[r] = f(r); (s) ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s)

Proof step 83 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 84:

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

Rule argument

Additional information

Used terms: r

Proof step 84 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  rs1 ∩ rs2 = ∅, f0(r) ≠ f(r), hP(mk(rs1, f0)), r ∈ rs1, ¬ hP(mk(rs1, f)), ∀ r0. (g(r0) = g0(r) ∧ r0 ∈ rs ↔ g0(r0) = g0(r) ∧ r0 ∈ rs1 ∪ rs2) ∧ (g(r0) = g0(r) ∧ r0 ∈ rs → f(r0) = f0(r0)), ∀ r0. r0 ∈ rs1 → g0(r0) = g0(r) ⊦

Rule argument

Additional information

Proof step 85 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] Used terms: r

Proof step 86 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

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

Rule argument

Additional information

Proof step 87 from proof rely-owned-unchgd (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 88:

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

Rule argument

Additional information

Used terms: r

Proof step 88 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

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

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 89 from proof rely-owned-unchgd (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r