Proof step 1 from proof rely-owns-none (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(owns-none(a, rs, g) ↔ owns-none(a, rs0, g0)), rely(a, rs, f, g, rs0, f0, g0) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-owns-none (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)) ⊦ (∀ r. r ∈ rs → g(r) ≠ a) ↔ (∀ r. r ∈ rs0 → g0(r) ≠ a)

Rule argument

Additional information

Used simplifier rules: owns-none: ⊦ owns-none(a, rs, g) ↔ (∀ r. r ∈ rs → g(r) ≠ a); 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-owns-none (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∀ r. r ∈ rs → g(r) ≠ a ⊦ ∀ r. r ∈ rs0 → g0(r) ≠ a

• Proof step 8:

  ∀ r. (g(r) = a ∧ r ∈ rs ↔ g0(r) = a ∧ r ∈ rs0) ∧ (g(r) = a ∧ r ∈ rs → f(r) = f0(r)), ∀ r. r ∈ rs0 → g0(r) ≠ a ⊦ ∀ r. r ∈ rs → g(r) ≠ a

Rule argument

Additional information

Proof step 4 from proof rely-owns-none (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r ∈ rs0, ∀ r0. r0 ∈ rs → g(r0) ≠ g0(r), ∀ r0. (g(r0) = g0(r) ∧ r0 ∈ rs ↔ g0(r0) = g0(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g0(r) ∧ r0 ∈ rs → f(r0) = f0(r0)) ⊦

Rule argument

Additional information

Proof step 5 from proof rely-owns-none (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 6:

  g(r) = g0(r) ∧ r ∈ rs ↔ g0(r) = g0(r) ∧ r ∈ rs0, r ∈ rs0, g(r) = g0(r) ∧ r ∈ rs → f(r) = f0(r), ∀ r0. (g(r0) = g0(r) ∧ r0 ∈ rs ↔ g0(r0) = g0(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g0(r) ∧ r0 ∈ rs → f(r0) = f0(r0)), ∀ r0. r0 ∈ rs → g(r0) ≠ g0(r) ⊦

Rule argument

Additional information

Used terms: r

Proof step 6 from proof rely-owns-none (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  f(r) = f0(r), g(r) = g0(r), r ∈ rs0, r ∈ rs, ∀ r0. r0 ∈ rs → g(r0) ≠ g0(r), ∀ r0. (g(r0) = g0(r) ∧ r0 ∈ rs ↔ g0(r0) = g0(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g0(r) ∧ r0 ∈ rs → f(r0) = f0(r0)) ⊦

Rule argument

Additional information

Proof step 7 from proof rely-owns-none (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 8 from proof rely-owns-none (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  r ∈ rs, ∀ r0. r0 ∈ rs0 → g0(r0) ≠ g(r), ∀ r0. (g(r0) = g(r) ∧ r0 ∈ rs ↔ g0(r0) = g(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g(r) ∧ r0 ∈ rs → f(r0) = f0(r0)) ⊦

Rule argument

Additional information

Proof step 9 from proof rely-owns-none (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 10:

  g(r) = g(r) ∧ r ∈ rs ↔ g0(r) = g(r) ∧ r ∈ rs0, r ∈ rs, g(r) = g(r) ∧ r ∈ rs → f(r) = f0(r), ∀ r0. (g(r0) = g(r) ∧ r0 ∈ rs ↔ g0(r0) = g(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g(r) ∧ r0 ∈ rs → f(r0) = f0(r0)), ∀ r0. r0 ∈ rs0 → g0(r0) ≠ g(r) ⊦

Rule argument

Additional information

Used terms: r

Proof step 10 from proof rely-owns-none (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  f(r) = f0(r), g0(r) = g(r), r ∈ rs, r ∈ rs0, ∀ r0. r0 ∈ rs0 → g0(r0) ≠ g(r), ∀ r0. (g(r0) = g(r) ∧ r0 ∈ rs ↔ g0(r0) = g(r) ∧ r0 ∈ rs0) ∧ (g(r0) = g(r) ∧ r0 ∈ rs → f(r0) = f0(r0)) ⊦

Rule argument

Additional information

Proof step 11 from proof rely-owns-none (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r