Proof step 1 from proof lastoc (conclusion) (back to tree)

a ∈ x, a ∈ x0 ⊦ ∃ b, y, y0. b ∈ x ∧ x0 = y + b ' + y0 ∧ disj(x, y0)

System applied rule normalize

And obtained the following new goals

Proof step 2:
a ∈ x0, a ∈ x ⊦ ∃ b, y, y0. b ∈ x ∧ x0 = y + b ' + y0 ∧ disj(x, y0)

Rule argument

Additional information

Proof step 2 from proof lastoc (previous step) (back to tree)

a ∈ x0, a ∈ x ⊦ ∃ b, y, y0. b ∈ x ∧ x0 = y + b ' + y0 ∧ disj(x, y0)

User applied rule structural induction

And obtained the following new goals

Proof step 3:
a ∈ a0 + x1, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. b ∈ a0 + x1 ∧ x0 = y + b ' + y0 ∧ disj(a0 + x1, y0)

Rule argument

indvar: x

Additional information

Used simplifier rules: list('a) freely generated by [], +;; ⊦ ¬ a ∈ []; (s)

Proof step 3 from proof lastoc (previous step) (back to tree)

a ∈ a0 + x1, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. b ∈ a0 + x1 ∧ x0 = y + b ' + y0 ∧ disj(a0 + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 4:
a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a = a0 ∨ a ∈ x1 ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 4 from proof lastoc (previous step) (back to tree)

a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a = a0 ∨ a ∈ x1 ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

User applied rule case distinction

And obtained the following new goals

Proof step 5:
a = a0, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)
Proof step 17:
a ∈ x0, a ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

pos: left 3

Additional information

Proof step 5 from proof lastoc (previous step) (back to tree)

a = a0, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 6:
a0 ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

Additional information

Proof step 6 from proof lastoc (previous step) (back to tree)

a0 ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 7:
⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z)
Proof step 8:
∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ y, z. x0 = y + a0 ' + z ∧ ¬ a0 ∈ z ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

spec: list, name:lastoc-rew, seq: ⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z), subst:[x, a] → [x0, a0], <all paths>

Additional information

Used terms: x0, a0

Proof step 7 from proof lastoc (previous step) (back to tree)

⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z)

A spec-lemma

Proof step 8 from proof lastoc (previous step) (back to tree)

∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ y, z. x0 = y + a0 ' + z ∧ ¬ a0 ∈ z ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 9:
¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Rule argument

Additional information

Proof step 9 from proof lastoc (previous step) (back to tree)

¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

User applied rule exists right

And obtained the following new goals

Proof step 10:
¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1), (a0 = a0 ∨ a0 ∈ x1) ∧ y + a0 ' + z = y + a0 ' + z ∧ disj(a0 ' + x1, z)

Rule argument

pos: right 1 terms: a0, y, z abort: F discard: F computed: T

Additional information

Used terms: a0, y, z

Proof step 10 from proof lastoc (previous step) (back to tree)

¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1), (a0 = a0 ∨ a0 ∈ x1) ∧ y + a0 ' + z = y + a0 ' + z ∧ disj(a0 ' + x1, z)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
¬ disj(x1, z), ¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Rule argument

Additional information

Used simplifier rules: first-01: ⊦ ¬ a ∈ x → (disj(a ' + y, x) ↔ disj(y, x)); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 11 from proof lastoc (previous step) (back to tree)

¬ disj(x1, z), ¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 12:
⊦ disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y))
Proof step 13:
¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ a. ¬ ¬(a ∈ x1 ∧ a ∈ z) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Rule argument

spec: <toplevel>, name:disjoint, seq: ⊦ disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y)), subst:[y, x] → [z, x1], <all paths>

Additional information

Used terms: z, x1

Proof step 12 from proof lastoc (previous step) (back to tree)

⊦ disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y))

Lemma disjoint

Proof step 13 from proof lastoc (previous step) (back to tree)

¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ a. ¬ ¬(a ∈ x1 ∧ a ∈ z) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 14:
a ∈ x1, a ∈ z, ¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Rule argument

Additional information

Proof step 14 from proof lastoc (previous step) (back to tree)

a ∈ x1, a ∈ z, ¬ a0 ∈ z, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

User applied rule all left

And obtained the following new goals

Proof step 15:
a ∈ z, a ∈ x1, ¬ a0 ∈ z, a ∈ z ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ z = y + b ' + y0 ∧ disj(x1, y0)), ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Rule argument

pos: left 4 terms: a, z abort: F discard: F computed: T

Additional information

Used terms: a, z

Proof step 15 from proof lastoc (previous step) (back to tree)

a ∈ z, a ∈ x1, ¬ a0 ∈ z, a ∈ z ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ z = y + b ' + y0 ∧ disj(x1, y0)), ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y0, y1. (b = a0 ∨ b ∈ x1) ∧ y + a0 ' + z = y0 + b ' + y1 ∧ disj(a0 ' + x1, y1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 16:
a0 ≠ b, disj(y1, x1), disj(x1, y1), b ∈ x1, a ∈ x1, ¬ a ∈ y1, ¬ b ∈ y1, ¬ a0 ∈ y0, ¬ a0 ∈ y1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y0 ∨ a = b ⊦ ∃ b0, y2, y3. (b0 = a0 ∨ b0 ∈ x1) ∧ y + a0 ' + y0 + b ' + y1 = y2 + b0 ' + y3 ∧ disj(a0 ' + x1, y3)

Rule argument

Additional information

Used simplifier rules: in: ⊦ disj(x, y) ∧ a ∈ x → ¬ a ∈ y; sym: ⊦ disj(x, y) → disj(y, x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ ¬ a ∈ x → (a ∈ a0 ' + x ↔ a = a0); (s)

Proof step 16 from proof lastoc (previous step) (back to tree)

a0 ≠ b, disj(y1, x1), disj(x1, y1), b ∈ x1, a ∈ x1, ¬ a ∈ y1, ¬ b ∈ y1, ¬ a0 ∈ y0, ¬ a0 ∈ y1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y0 ∨ a = b ⊦ ∃ b0, y2, y3. (b0 = a0 ∨ b0 ∈ x1) ∧ y + a0 ' + y0 + b ' + y1 = y2 + b0 ' + y3 ∧ disj(a0 ' + x1, y3)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

pos: right 1 terms: b, y + a0 ' + y0, y1

Additional information

Used simplifier rules: cons-01: ⊦ disj(x, y) → (disj(a ' + x, y) ↔ ¬ a ∈ y); a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: b, y + a0 ' + y0, y1

Proof step 17 from proof lastoc (previous step) (back to tree)

a ∈ x0, a ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 18:
a ∈ x1, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

Additional information

Proof step 18 from proof lastoc (previous step) (back to tree)

a ∈ x1, a ∈ x0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

User applied rule all left

And obtained the following new goals

Proof step 19:
a ∈ x0, a ∈ x1, a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

pos: left 3 terms: a, x0 abort: F discard: F computed: T

Additional information

Used terms: a, x0

Proof step 19 from proof lastoc (previous step) (back to tree)

a ∈ x0, a ∈ x1, a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)) ⊦ ∃ b, y, y0. (b = a0 ∨ b ∈ x1) ∧ x0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 20:
disj(y0, x1), disj(x1, y0), b ∈ x1, a ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

Rule argument

Additional information

Used simplifier rules: in: ⊦ disj(x, y) ∧ a ∈ x → ¬ a ∈ y; sym: ⊦ disj(x, y) → disj(y, x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ x → (a ∈ a0 ' + x ↔ a = a0); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 20 from proof lastoc (previous step) (back to tree)

disj(y0, x1), disj(x1, y0), b ∈ x1, a ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

User applied rule exists right

And obtained the following new goals

Proof step 21:
disj(x1, y0), disj(y0, x1), a ∈ x1, b ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2), (b = a0 ∨ b ∈ x1) ∧ y + b ' + y0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Rule argument

pos: right 1 terms: b, y, y0 abort: F discard: F computed: T

Additional information

Used terms: b, y, y0

Proof step 21 from proof lastoc (previous step) (back to tree)

disj(x1, y0), disj(y0, x1), a ∈ x1, b ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2), (b = a0 ∨ b ∈ x1) ∧ y + b ' + y0 = y + b ' + y0 ∧ disj(a0 ' + x1, y0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 22:
disj(y0, x1), disj(x1, y0), b ∈ x1, a ∈ x1, a0 ∈ y0, ¬ a ∈ y0, ¬ b ∈ y0, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

Rule argument

Additional information

Used simplifier rules: cons-01: ⊦ disj(x, y) → (disj(a ' + x, y) ↔ ¬ a ∈ y); in: ⊦ disj(x, y) ∧ a ∈ x → ¬ a ∈ y; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 22 from proof lastoc (previous step) (back to tree)

disj(y0, x1), disj(x1, y0), b ∈ x1, a ∈ x1, a0 ∈ y0, ¬ a ∈ y0, ¬ b ∈ y0, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 23:
⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z)
Proof step 24:
disj(x1, y0), disj(y0, x1), a ∈ x1, b ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ y, z. y0 = y + a0 ' + z ∧ ¬ a0 ∈ z, a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

Rule argument

spec: list, name:lastoc-rew, seq: ⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z), subst:[x, a] → [y0, a0], <all paths>

Additional information

Used terms: y0, a0

Proof step 23 from proof lastoc (previous step) (back to tree)

⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z)

A spec-lemma

Proof step 24 from proof lastoc (previous step) (back to tree)

disj(x1, y0), disj(y0, x1), a ∈ x1, b ∈ x1, ¬ a ∈ y0, ¬ b ∈ y0, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), ∃ y, z. y0 = y + a0 ' + z ∧ ¬ a0 ∈ z, a ∈ y ∨ a = b ⊦ ∃ b0, y1, y2. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y0 = y1 + b0 ' + y2 ∧ disj(a0 ' + x1, y2)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
disj(z, x1), disj(y1, x1), disj(x1, z), disj(x1, y1), a ∈ x1, b ∈ x1, ¬ b ∈ y1, ¬ a ∈ y1, ¬ b ∈ z, ¬ a ∈ z, ¬ a0 ∈ z, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y2, y3. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y1 + a0 ' + z = y2 + b0 ' + y3 ∧ disj(a0 ' + x1, y3)

Rule argument

Additional information

Used simplifier rules: app-03: ⊦ disj(y + z, x) ↔ disj(x, y) ∧ disj(x, z); first: ⊦ ¬ a ∈ x → (disj(x, a ' + y) ↔ disj(x, y)); app-02: ⊦ disj(x, y + z) ↔ disj(x, y) ∧ disj(x, z); cons: ⊦ disj(x, y) → (disj(x, a ' + y) ↔ ¬ a ∈ x); in: ⊦ disj(x, y) ∧ a ∈ x → ¬ a ∈ y; sym: ⊦ disj(x, y) → disj(y, x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 25 from proof lastoc (previous step) (back to tree)

disj(z, x1), disj(y1, x1), disj(x1, z), disj(x1, y1), a ∈ x1, b ∈ x1, ¬ b ∈ y1, ¬ a ∈ y1, ¬ b ∈ z, ¬ a ∈ z, ¬ a0 ∈ z, ¬ a0 ∈ x1, ∀ a, x0. a ∈ x0 ∧ a ∈ x1 → (∃ b, y, y0. b ∈ x1 ∧ x0 = y + b ' + y0 ∧ disj(x1, y0)), a ∈ y ∨ a = b ⊦ ∃ b0, y2, y3. (b0 = a0 ∨ b0 ∈ x1) ∧ y + b ' + y1 + a0 ' + z = y2 + b0 ' + y3 ∧ disj(a0 ' + x1, y3)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

pos: right 1 terms: a0, y + b ' + y1, z

Additional information

Used simplifier rules: cons-01: ⊦ disj(x, y) → (disj(a ' + x, y) ↔ ¬ a ∈ y); a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0, y + b ' + y1, z