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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a ∈ ax ⊦ ∃ ax0, d, ax1. ax = ax0 + (a × d)' + ax1 ∧ ¬ a ∈ ax0

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a ∈ ax ⊦ ∃ ax0, d, ax1. ax = ax0 + (a × d)' + ax1 ∧ ¬ a ∈ ax0

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a ∈ pair + ax0, ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1) ⊦ ∃ ax1, d, ax2. pair + ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used simplifier rules: empty: ⊦ ¬ a ∈ []; assoclist freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1), a ∈ pair ' ∨ a ∈ ax0 ⊦ ∃ ax1, d, ax2. pair ' + ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used simplifier rules: inapp: ⊦ a ∈ ax + ay ↔ a ∈ ax ∨ a ∈ ay; ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[assoclist]

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1), a ∈ (a0 × d)' ∨ a ∈ ax0 ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used simplifier rules: pair freely generated by ×;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1), a = a0 ∨ a ∈ ax0 ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used simplifier rules: inone: ⊦ a ∈ (b × d0)' ↔ a = b;

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

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  a = a0, ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1), a = a0 ∨ a ∈ ax0 ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

• Proof step 10:

  a ≠ a0, ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1), a = a0 ∨ a ∈ ax0 ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used formulas: a = a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1) ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a0 × d0)' + ax2 ∧ ¬ a0 ∈ ax1

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: empty: ⊦ ¬ a ∈ []; ⊦ [] + x = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list[assoclist] Used terms: [], d, ax0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ≠ a0, a ∈ ax0, ∀ a. a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1) ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 12:

  a ≠ a0, a ∈ ax0, a ∈ ax0 → (∃ ax1, d, ax2. ax0 = ax1 + (a × d)' + ax2 ∧ ¬ a ∈ ax1) ⊦ ∃ ax1, d0, ax2. (a0 × d)' + ax0 = ax1 + (a × d0)' + ax2 ∧ ¬ a ∈ ax1

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a ≠ a0, ¬ a ∈ ax1 ⊦ ∃ ax, d1, ax3. (a0 × d)' + ax1 + (a × d0)' + ax2 = ax + (a × d1)' + ax3 ∧ ¬ a ∈ ax

Rule argument

Additional information

Used simplifier rules: inapp: ⊦ a ∈ ax + ay ↔ a ∈ ax ∨ a ∈ ay; inone: ⊦ a ∈ (b × d0)' ↔ a = b; a: ⊦ (x + y) + z = x + y + z; from specification list[assoclist]

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: inkeys-n: ⊦ a ≠ b → (a ∈ (b × d0)' + ax ↔ a ∈ ax); a: ⊦ (x + y) + z = x + y + z; from specification list[assoclist] Used terms: (a0 × d)' + ax1, d0, ax2