Proof step 1 from proof abs-wfind (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ p(i), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i) ⊦

Rule argument

Additional information

Proof step 2 from proof abs-wfind (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  ∀ i. (∀ i0. 0 ≤ i0 ∧ i0 < i → p(i0)) → 0 ≤ i → p(i) ⊦ 0 ≤ i → p(i)

• Proof step 4:

  0 ≤ i, ∀ i0. 0 ≤ i0 ∧ i0 < i → (∀ p, i. ¬(i0 = abs(i) ∧ ¬ p(i) ∧ (∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i)))) ⊦ ∀ p, i1. ¬(i = abs(i1) ∧ ¬ p(i1) ∧ (∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i)))

Rule argument

Additional information

Used simplifier rules: abs-03: ⊦ 0 ≤ abs(i); Used terms: abs(i), λ i0. ∀ p, i. ¬(i0 = abs(i) ∧ ¬ p(i) ∧ (∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i)))

Proof step 3 from proof abs-wfind (previous step) (back to tree)

Lemma nat-wfind

Proof step 4 from proof abs-wfind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬ p(i1), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i), ∀ i0. ¬ i0 < 0 ∧ i0 < abs(i1) → (∀ p0, i. i0 ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))) ⊦

Rule argument

Additional information

Used simplifier rules: abs-03: ⊦ 0 ≤ abs(i); le-def: ⊦ i ≤ j ↔ ¬ j < i;

Proof step 5 from proof abs-wfind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  ¬ p(i1), (∀ i0. abs(i0) < abs(i1) → p(i0)) → p(i1), ∀ i0. ¬ i0 < 0 ∧ i0 < abs(i1) → (∀ p0, i. i0 ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i) ⊦

Rule argument

Additional information

Used terms: i1

Proof step 6 from proof abs-wfind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  abs(i0) < abs(i1), ¬ p(i1), ¬ p(i0), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i), ∀ i0. ¬ i0 < 0 ∧ i0 < abs(i1) → (∀ p0, i. i0 ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))) ⊦

Rule argument

Additional information

Proof step 7 from proof abs-wfind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  abs(i0) < abs(i1), ¬ p(i1), ¬ p(i0), ¬ abs(i0) < 0 ∧ abs(i0) < abs(i1) → (∀ p0, i. abs(i0) ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))), ∀ i0. ¬ i0 < 0 ∧ i0 < abs(i1) → (∀ p0, i. i0 ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i) ⊦

Rule argument

Additional information

Used terms: abs(i0)

Proof step 8 from proof abs-wfind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  abs(i0) < abs(i1), ¬ p(i1), ¬ p(i0), ∀ i. (∀ i0. abs(i0) < abs(i) → p(i0)) → p(i), ∀ i0. ¬ i0 < 0 ∧ i0 < abs(i1) → (∀ p0, i. i0 ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i))), ∀ p0, i. abs(i0) ≠ abs(i) ∨ p0(i) ∨ ¬(∀ i. (∀ i0. abs(i0) < abs(i) → p0(i0)) → p0(i)) ⊦

Rule argument

Additional information

Used simplifier rules: absls: ⊦ ¬ abs(i) < 0;

Proof step 9 from proof abs-wfind (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: p, i0