Proof step 1 from proof choice-aux (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(n)) ∧ (∀ m. m < n → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

Rule argument

Additional information

Proof step 2 from proof choice-aux (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(0)) ∧ (∀ m. m < 0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

• Proof step 5:

  ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ a, elemf. ok(a) ∧ (∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b))) → (∃ nf. nf(0) = a ∧ ok(nf(n0)) ∧ (∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(n0 +1)) ∧ (∀ m. m < n0 +1 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

Proof step 3 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s)

Proof step 4 from proof choice-aux (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: λ n. a

Proof step 5 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ok(a), ∀ a, elemf. ok(a) ∧ (∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b))) → (∃ nf. nf(0) = a ∧ ok(nf(n0)) ∧ (∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(n0 + 1)) ∧ (∀ m. ¬ n0 < m → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s)

Proof step 6 from proof choice-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  ok(a), ok(a) ∧ (∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b))) → (∃ nf. nf(0) = a ∧ ok(nf(n0)) ∧ (∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(n0 + 1)) ∧ (∀ m. ¬ n0 < m → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

Rule argument

Additional information

Used terms: a, elemf

Proof step 7 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ok(nf(n0)), ok(nf(0)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf0. nf0(0) = nf(0) ∧ ok(nf0(n0 + 1)) ∧ (∀ m. ¬ n0 < m → ok(nf0(m)) ∧ nf0(m + 1) = elemf(nf0(m)))

Rule argument

Additional information

Proof step 8 from proof choice-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  ok(nf(0)), ok(nf(n0)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦ nf(n0 + 1; elemf(nf(n0)))(0) = nf(0) ∧ ok(nf(n0 + 1; elemf(nf(n0)))(n0 + 1)) ∧ (∀ m. ¬ n0 < m → ok(nf(n0 + 1; elemf(nf(n0)))(m)) ∧ nf(n0 + 1; elemf(nf(n0)))(m + 1) = elemf(nf(n0 + 1; elemf(nf(n0)))(m)))

Rule argument

Additional information

Used terms: nf(n0 + 1; elemf(nf(n0)))

Proof step 9 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ok(nf(n0)), ok(nf(0)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ok(elemf(nf(n0))) ∧ (¬ n0 < m → ok((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))) ∧ (n0 = m ⊃ elemf(nf(m));nf(m + 1)) = elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 10 from proof choice-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  ok(nf(0)), ok(nf(n0)), ok(nf(n0)) → rel(nf(n0), elemf(nf(n0))) ∧ ok(elemf(nf(n0))), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦ ok(elemf(nf(n0))) ∧ (¬ n0 < m → ok((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))) ∧ (n0 = m ⊃ elemf(nf(m));nf(m + 1)) = elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))))

Rule argument

Additional information

Used terms: nf(n0)

Proof step 11 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ok(nf(n0)), ok(nf(0)), ok(elemf(nf(n0))), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ok((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))) ∧ (n0 = m ⊃ elemf(nf(m));nf(m + 1)) = elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m)))

Rule argument

Additional information

Proof step 12 from proof choice-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  ok(elemf(nf(n0))), ok(nf(0)), ok(nf(n0)), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ¬ ok((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦

• Proof step 16:

  (n0 = m ⊃ elemf(nf(m));nf(m + 1)) ≠ elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))), ok(elemf(nf(n0))), ok(nf(0)), ok(nf(n0)), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦

Rule argument

Additional information

Proof step 13 from proof choice-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  n0 + 1 ≠ m, ok(nf(n0)), ok(nf(0)), ok(elemf(nf(n0))), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ¬ ok(nf(m)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦

Rule argument

Additional information

Proof step 14 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  n0 + 1 ≠ m, ok(elemf(nf(n0))), ok(nf(0)), ok(nf(n0)), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ¬ ok(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦

Rule argument

Additional information

Proof step 15 from proof choice-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m < n → (n < m ↔ n ≠ m); (ss) Used terms: m

Proof step 16 from proof choice-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

  n0 ≠ m, nf(m + 1) ≠ elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))), ok(nf(n0)), ok(nf(0)), ok(elemf(nf(n0))), rel(nf(n0), elemf(nf(n0))), ¬ n0 < m, ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 17 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  n0 ≠ m, nf(m + 1) ≠ elemf((n0 + 1 = m ⊃ elemf(nf(n0));nf(m))), m < n0, ok(nf(n0)), ok(nf(0)), ok(elemf(nf(n0))), rel(nf(n0), elemf(nf(n0))), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss)

Proof step 18 from proof choice-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  n0 + 1 ≠ m, n0 ≠ m, nf(m + 1) ≠ elemf(nf(m)), m < n0, ok(elemf(nf(n0))), ok(nf(0)), ok(nf(n0)), rel(nf(n0), elemf(nf(n0))), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 19 from proof choice-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  n0 + 1 ≠ m, n0 ≠ m, nf(m + 1) ≠ elemf(nf(m)), m < n0, ok(nf(n0)), ok(nf(0)), ok(elemf(nf(n0))), rel(nf(n0), elemf(nf(n0))), ∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦

Rule argument

Additional information

Proof step 20 from proof choice-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m