Proof step 1 from proof wf-equiv-noethind (conclusion) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  wf(wf≪) ⊦ ∀ p. (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ a. p(a))

• Proof step 77:

  ¬ wf(wf≪), ∀ p. (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ a. p(a)) ⊦

Rule argument

Additional information

Proof step 2 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 3 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a. ¬ p(a) → (∃ a0. wf≪(a0, a) ∧ ¬ p(a0)) ⊦

• Proof step 73:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∀ a. ¬ p(a) → (∃ a0. wf≪(a0, a) ∧ ¬ p(a0))

Rule argument

Additional information

Used formulas: ∀ a. ¬ p(a) → (∃ a0. wf≪(a0, a) ∧ ¬ p(a0))

Proof step 4 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 5:

  wf(wf≪), ¬ p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 5 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n. ∃ chn. chn(0) = a ∧ (∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1))) ⊦

• Proof step 51:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ ∀ n. ∃ chn. chn(0) = a ∧ (∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))

Rule argument

Additional information

Used formulas: ∀ n. ∃ chn. chn(0) = a ∧ (∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))

Proof step 6 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 7:

  wf(wf≪), ¬ p(a), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 7 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ∀ n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

• Proof step 28:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))) ⊦ ∀ m. ∀ n. m ≤ n → chngen(n)(m) = chngen(m)(m)

Rule argument

Additional information

Used formulas: ∀ m. ∀ n. m ≤ n → chngen(n)(m) = chngen(m)(m)

Proof step 8 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  wf(wf≪), ¬ p(a), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Proof step 9 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ wf(wf≪) ↔ ¬(∃ chn. ∀ n. wf≪(chn(n + 1), chn(n)))

• Proof step 11:

  ¬ p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ chn. ¬(∀ n. wf≪(chn(n + 1), chn(n))) ⊦

Rule argument

Additional information

Used terms: wf≪

Proof step 10 from proof wf-equiv-noethind (previous step) (back to tree)

Lemma wf-def

Proof step 11 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  ¬ p(a), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦ ∀ n. wf≪(chngen(n + 1)(n + 1), chngen(n)(n))

Rule argument

Additional information

Used terms: λ n. chngen(n)(n)

Proof step 12 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ¬ p(a), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))) ⊦

Rule argument

Additional information

Proof step 13 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  chngen(n + 1)(0) = a, ¬ p(a), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ m. m < n + 1 → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)) ⊦

Rule argument

Additional information

Used terms: n + 1

Proof step 14 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ¬ p(chngen(n + 1)(0)), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)) ⊦

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)

Proof step 15 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  ¬ p(chngen(n + 1)(0)), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), n ≤ n + 1 → chngen(n + 1)(n) = chngen(n)(n), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Used terms: n, n + 1

Proof step 16 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  chngen(n + 1)(n) = chngen(n)(n), ¬ p(chngen(n + 1)(0)), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)) ⊦

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 ≤ m + n; (s)

Proof step 17 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  chngen(n + 1)(n) = chngen(n)(n), ¬ p(chngen(n + 1)(0)), ¬ wf≪(chngen(n + 1)(n + 1), chngen(n)(n)), ¬ n < n → chngen(n + 1)(n + 1) = af(chngen(n + 1)(n)) ∧ ¬ p(chngen(n + 1)(n + 1)), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Used terms: n

Proof step 18 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n + 1)(n) = chngen(n)(n), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

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

Proof step 19 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  chngen(n + 1)(n) = chngen(n)(n), chngen(n + 1)(n + 1) = af(chngen(n)(n)), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), (∀ a0. wf≪(a0, af(chngen(n)(n))) → p(a0)) → p(af(chngen(n)(n))), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)) ⊦

Rule argument

Additional information

Used terms: af(chngen(n)(n))

Proof step 20 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n + 1)(n) = chngen(n)(n), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Proof step 21 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  chngen(n + 1)(n) = chngen(n)(n), chngen(n + 1)(n + 1) = af(chngen(n)(n)), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ¬ p(chngen(n)(n)) → wf≪(af(chngen(n)(n)), chngen(n)(n)) ∧ ¬ p(af(chngen(n)(n))), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)) ⊦

Rule argument

Additional information

Used terms: chngen(n)(n)

Proof step 22 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n + 1)(n) = chngen(n)(n), p(chngen(n)(n)), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Proof step 23 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  chngen(n + 1)(n) = chngen(n)(n), chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n)(0) = chngen(n + 1)(0), p(chngen(n)(n)), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n + 1)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ m. m < n → chngen(n)(m + 1) = af(chngen(n)(m)) ∧ ¬ p(chngen(n)(m + 1)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 24 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  chngen(n)(0) = chngen(n + 1)(0), chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n + 1)(n) = chngen(n)(n), p(chngen(n)(n)), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m. m < n → chngen(n)(m + 1) = af(chngen(n)(m)) ∧ ¬ p(chngen(n)(m + 1)), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m) ⊦

Rule argument

Additional information

Proof step 25 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 26:

  chngen(n + 1)(n) = chngen(n)(n), chngen(n + 1)(n + 1) = af(chngen(n)(n)), chngen(n)(0) = chngen(n + 1)(0), n = n1 +1, p(chngen(n)(n)), wf≪(a0, af(chngen(n)(n))), ¬ p(af(chngen(n)(n))), ¬ p(chngen(n)(0)), ¬ p(a0), ¬ wf≪(af(chngen(n)(n)), chngen(n)(n)), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(n)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. ¬ n < m → chngen(n + 1)(m + 1) = af(chngen(n + 1)(m)) ∧ ¬ p(chngen(n + 1)(m + 1)), ∀ m. m < n → chngen(n)(m + 1) = af(chngen(n)(m)) ∧ ¬ p(chngen(n)(m + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 26 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  chngen(n1 + 1)(0) = chngen(2 + n1)(0), chngen(2 + n1)(2 + n1) = af(chngen(n1 + 1)(n1 + 1)), chngen(2 + n1)(n1 + 1) = chngen(n1 + 1)(n1 + 1), p(chngen(n1 + 1)(n1 + 1)), wf≪(a0, chngen(2 + n1)(2 + n1)), ¬ p(chngen(2 + n1)(2 + n1)), ¬ p(chngen(2 + n1)(0)), ¬ p(a0), ¬ wf≪(chngen(2 + n1)(2 + n1), chngen(n1 + 1)(n1 + 1)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m, n. m ≤ n → chngen(n)(m) = chngen(m)(m), ∀ m. ¬ n1 < m → chngen(n1 + 1)(m + 1) = af(chngen(n1 + 1)(m)) ∧ ¬ p(chngen(n1 + 1)(m + 1)), ∀ m. ¬ n1 + 1 < m → chngen(2 + n1)(m + 1) = af(chngen(2 + n1)(m)) ∧ ¬ p(chngen(2 + n1)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(2 + n1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))) ⊦

Rule argument

Additional information

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

Proof step 27 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 28 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all right

And obtained the following new goals

• Proof step 29:

  wf(wf≪), ¬ p(a), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∀ n. m ≤ n → chngen(n)(m) = chngen(m)(m)

Rule argument

Additional information

Proof step 29 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 30:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))) ⊦ ∀ n. 0 ≤ n → chngen(n)(0) = chngen(0)(0)

• Proof step 34:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ wf≪, p, a, chngen, af. wf(wf≪) ∧ ¬ p(a) ∧ (∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1)))) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0)) ⊦ ∀ n. m0 +1 ≤ n → chngen(n)(m0 +1) = chngen(m0 +1)(m0 +1)

Rule argument

Additional information

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

Proof step 30 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  chngen(n)(0) ≠ chngen(0)(0), wf(wf≪), ¬ p(a), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s)

Proof step 31 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 32:

  chngen(n)(0) = a, chngen(n)(0) ≠ chngen(0)(0), wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ m. m < n → chngen(n)(m + 1) = af(chngen(n)(m)) ∧ ¬ p(chngen(n)(m + 1)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 32 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  chngen(n)(0) ≠ chngen(0)(0), wf(wf≪), ¬ p(chngen(n)(0)), ∀ m. m < n → chngen(n)(m + 1) = af(chngen(n)(m)) ∧ ¬ p(chngen(n)(m + 1)), ∀ n0. chngen(n0)(0) = chngen(n)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 33 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: 0

Proof step 34 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ wf≪, p, a, chngen, af. wf(wf≪) ∧ ¬ p(a) ∧ (∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1)))) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0)) ⊦

Rule argument

Additional information

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

Proof step 35 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 36:

  chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(a), wf(wf≪) ∧ ¬ p(a) ∧ (∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1)))) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Used terms: wf≪, p, a, chngen, af

Proof step 36 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0) ⊦

Rule argument

Additional information

Proof step 37 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 38:

  chngen(m0 + 1)(0) = a, chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(a), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ n0. chngen(n0)(0) = a ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < m0 + 1 → chngen(m0 + 1)(m + 1) = af(chngen(m0 + 1)(m)) ∧ ¬ p(chngen(m0 + 1)(m + 1)) ⊦

Rule argument

Additional information

Used terms: m0 + 1

Proof step 38 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(chngen(m0 + 1)(0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(m0 + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ m1. ¬ m0 < m1 → chngen(m0 + 1)(m1 + 1) = af(chngen(m0 + 1)(m1)) ∧ ¬ p(chngen(m0 + 1)(m1 + 1)) ⊦

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)

Proof step 39 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 40:

  chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(chngen(m0 + 1)(0)), ¬ m0 < m0 → chngen(m0 + 1)(m0 + 1) = af(chngen(m0 + 1)(m0)) ∧ ¬ p(chngen(m0 + 1)(m0 + 1)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ n0. chngen(n0)(0) = chngen(m0 + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 40 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  chngen(m0 + 1)(m0 + 1) = af(chngen(m0 + 1)(m0)), chngen(m)(m0 + 1) ≠ chngen(m0 + 1)(m0 + 1), m0 < m, wf(wf≪), ¬ p(chngen(m0 + 1)(0)), ¬ p(chngen(m0 + 1)(m0 + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(m0 + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0) ⊦

Rule argument

Additional information

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

Proof step 41 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 42:

  chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m0 + 1)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ n0. chngen(n0)(0) = chngen(m0 + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 42 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 43:

  chngen(m)(0) = chngen(m0 + 1)(0), chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m0 + 1)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n0. chngen(n0)(0) = chngen(m0 + 1)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ m0. m0 < m → chngen(m)(m0 + 1) = af(chngen(m)(m0)) ∧ ¬ p(chngen(m)(m0 + 1)) ⊦

Rule argument

Additional information

Used terms: m

Proof step 43 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  chngen(m)(0) = chngen(m0 + 1)(0), chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ∀ m0. m0 < m → chngen(m)(m0 + 1) = af(chngen(m)(m0)) ∧ ¬ p(chngen(m)(m0 + 1)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ n0. chngen(n0)(0) = chngen(m)(0) ∧ (∀ m. m < n0 → chngen(n0)(m + 1) = af(chngen(n0)(m)) ∧ ¬ p(chngen(n0)(m + 1))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 44 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  chngen(m)(0) = chngen(m0 + 1)(0), chngen(m0)(0) = chngen(m)(0), chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ m0. m0 < m → chngen(m)(m0 + 1) = af(chngen(m)(m0)) ∧ ¬ p(chngen(m)(m0 + 1)), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 45 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 46:

  chngen(m0)(0) = chngen(m)(0), chngen(m)(0) = chngen(m0 + 1)(0), chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), m0 < m → chngen(m)(m0 + 1) = af(chngen(m)(m0)) ∧ ¬ p(chngen(m)(m0 + 1)), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 46 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  chngen(m)(0) = chngen(m0 + 1)(0), chngen(m0)(0) = chngen(m)(0), chngen(m)(m0 + 1) = af(chngen(m)(m0)), chngen(m)(m0 + 1) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ¬ p(chngen(m)(m0 + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)) ⊦

Rule argument

Additional information

Proof step 47 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 48:

  chngen(m0)(0) = chngen(m)(0), chngen(m)(0) = chngen(m0 + 1)(0), af(chngen(m)(m0)) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ¬ p(af(chngen(m)(m0))), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Proof step 48 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 49:

  chngen(m)(0) = chngen(m0 + 1)(0), chngen(m0)(0) = chngen(m)(0), af(chngen(m)(m0)) ≠ af(chngen(m0 + 1)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0 + 1)(m0))), ¬ p(af(chngen(m)(m0))), m0 ≤ m0 +1 → chngen(m0 +1)(m0) = chngen(m0)(m0), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)) ⊦

Rule argument

Additional information

Used terms: m0 +1

Proof step 49 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  chngen(m0)(0) = chngen(m)(0), chngen(m)(0) = chngen(m0 + 1)(0), chngen(m0 + 1)(m0) = chngen(m0)(m0), af(chngen(m)(m0)) ≠ af(chngen(m0)(m0)), m0 < m, wf(wf≪), ¬ p(chngen(m)(0)), ¬ p(af(chngen(m0)(m0))), ¬ p(af(chngen(m)(m0))), ∀ m. m < m0 → chngen(m0)(m + 1) = af(chngen(m0)(m)) ∧ ¬ p(chngen(m0)(m + 1)), ∀ n. m0 ≤ n → chngen(n)(m0) = chngen(m0)(m0), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

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

Proof step 50 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) Used terms: m

Proof step 51 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  wf(wf≪), ¬ p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∃ chn. chn(0) = a ∧ (∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))

Rule argument

Additional information

Proof step 52 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 53:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ ∃ chn. chn(0) = a ∧ (∀ m. m < 0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))

• Proof step 55:

  wf(wf≪), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ wf≪, p, a, af. wf(wf≪) ∧ ¬ p(a) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∃ chn. chn(0) = a ∧ (∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))) ⊦ ∃ chn. chn(0) = a ∧ (∀ m. m < n0 +1 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))

Rule argument

Additional information

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

Proof step 53 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  wf(wf≪), ¬ p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∃ chn. chn(0) = a

Rule argument

Additional information

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

Proof step 54 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: λ n. a

Proof step 55 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  wf(wf≪), ¬ p(a), ∀ wf≪, p, a, af. wf(wf≪) ∧ ¬ p(a) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∃ chn. chn(0) = a ∧ (∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∃ chn. chn(0) = a ∧ (∀ n. ¬ n0 < n → chn(n + 1) = af(chn(n)) ∧ ¬ p(chn(n + 1)))

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 56 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 57:

  wf(wf≪), ¬ p(a), wf(wf≪) ∧ ¬ p(a) ∧ (∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0))) ∧ (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∃ chn. chn(0) = a ∧ (∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)))), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ ∃ chn. chn(0) = a ∧ (∀ n. ¬ n0 < n → chn(n + 1) = af(chn(n)) ∧ ¬ p(chn(n + 1)))

Rule argument

Additional information

Used terms: wf≪, p, a, af

Proof step 57 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  wf(wf≪), ¬ p(chn(0)), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ ∃ chn0. chn0(0) = chn(0) ∧ (∀ n. ¬ n0 < n → chn0(n + 1) = af(chn0(n)) ∧ ¬ p(chn0(n + 1)))

Rule argument

Additional information

Proof step 58 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 59:

  wf(wf≪), ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦ chn(n0 + 1 := af(chn(n0)))(0) = chn(0) ∧ (∀ n. ¬ n0 < n → chn(n0 + 1 := af(chn(n0)))(n + 1) = af(chn(n0 + 1 := af(chn(n0)))(n)) ∧ ¬ p(chn(n0 + 1 := af(chn(n0)))(n + 1)))

Rule argument

Additional information

Used terms: chn(n0 + 1 := af(chn(n0)))

Proof step 59 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  wf(wf≪), n ≤ n0, ¬ p(chn(0)), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ (n0 = n ⊃ af(chn(n));chn(n + 1)) = af((n0 + 1 = n ⊃ af(chn(n0));chn(n))) ∧ ¬ p((n0 = n ⊃ af(chn(n));chn(n + 1)))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) 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 60 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 61:

  n0 = n, wf(wf≪), n ≤ n0, ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦ (n0 = n ⊃ af(chn(n));chn(n + 1)) = af((n0 + 1 = n ⊃ af(chn(n0));chn(n))) ∧ ¬ p((n0 = n ⊃ af(chn(n));chn(n + 1)))

• Proof step 69:

  n0 ≠ n, wf(wf≪), n ≤ n0, ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦ (n0 = n ⊃ af(chn(n));chn(n + 1)) = af((n0 + 1 = n ⊃ af(chn(n0));chn(n))) ∧ ¬ p((n0 = n ⊃ af(chn(n));chn(n + 1)))

Rule argument

Additional information

Used formulas: n0 = n

Proof step 61 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  p(af(chn(n))), wf(wf≪), ¬ p(chn(0)), ∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦

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 = m + n ↔ n = 0; (s) ⊦ m ≤ m; (s)

Proof step 62 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 63:

  n = 0, p(af(chn(n))), wf(wf≪), ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦

• Proof step 65:

  n = n0 +1, p(af(chn(n))), wf(wf≪), ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦

Rule argument

Additional information

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

Proof step 63 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  p(af(chn(0))), wf(wf≪), ¬ p(chn(0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦

Rule argument

Additional information

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

Proof step 64 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: chn(0)

Proof step 65 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  p(af(chn(n0 + 1))), wf(wf≪), ¬ p(chn(0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ m. ¬ n0 < m → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦

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 66 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 67:

  p(af(chn(n0 + 1))), wf(wf≪), ¬ p(chn(0)), ¬ n0 < n0 → chn(n0 + 1) = af(chn(n0)) ∧ ¬ p(chn(n0 + 1)), ∀ m. ¬ n0 < m → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 67 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  chn(n0 + 1) = af(chn(n0)), p(af(af(chn(n0)))), wf(wf≪), ¬ p(chn(0)), ¬ p(af(chn(n0))), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ m. ¬ n0 < m → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦

Rule argument

Additional information

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

Proof step 68 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: af(chn(n0))

Proof step 69 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  n0 ≠ n, n < n0, wf(wf≪), ¬ p(chn(0)), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦ chn(n + 1) = af((n0 + 1 = n ⊃ af(chn(n0));chn(n))) ∧ ¬ p(chn(n + 1))

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 ↔ m < n); (s)

Proof step 70 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 71:

  n0 ≠ n, n < n0, wf(wf≪), ¬ p(chn(0)), n < n0 → chn(n + 1) = af(chn(n)) ∧ ¬ p(chn(n + 1)), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)) ⊦ chn(n + 1) = af((n0 + 1 = n ⊃ af(chn(n0));chn(n))) ∧ ¬ p(chn(n + 1))

Rule argument

Additional information

Used terms: n

Proof step 71 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  chn(n + 1) = af(chn(n)), af(chn(n)) ≠ af((n0 + 1 = n ⊃ af(chn(n0));chn(n))), n0 ≠ n, n < n0, wf(wf≪), ¬ p(chn(0)), ¬ p(af(chn(n))), ∀ a0. ¬ p(a0) → wf≪(af(a0), a0) ∧ ¬ p(af(a0)), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a), ∀ m. m < n0 → chn(m + 1) = af(chn(m)) ∧ ¬ p(chn(m + 1)) ⊦

Rule argument

Additional information

Proof step 72 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

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 73 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  wf(wf≪), ¬ p(a0), ¬ p(a), ∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a) ⊦ ∃ a1. wf≪(a1, a0) ∧ ¬ p(a1)

Rule argument

Additional information

Proof step 74 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 75:

  wf(wf≪), ¬ p(a0), ¬ p(a), (∀ a1. wf≪(a1, a0) → p(a1)) → p(a0) ⊦ ∃ a1. wf≪(a1, a0) ∧ ¬ p(a1)

Rule argument

Additional information

Used terms: a0

Proof step 75 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  wf(wf≪), wf≪(a1, a0), ¬ p(a0), ¬ p(a), ¬ p(a1) ⊦ ∃ a1. wf≪(a1, a0) ∧ ¬ p(a1)

Rule argument

Additional information

Proof step 76 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a1

Proof step 77 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ wf(wf≪) ↔ ¬(∃ chn. ∀ n. wf≪(chn(n + 1), chn(n)))

• Proof step 79:

  ∀ p. (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ a. p(a)), ∃ chn. ∀ n. wf≪(chn(n + 1), chn(n)) ⊦

Rule argument

Additional information

Used terms: wf≪

Proof step 78 from proof wf-equiv-noethind (previous step) (back to tree)

Lemma wf-def

Proof step 79 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  ∀ n. wf≪(chn(n + 1), chn(n)), ∀ p. (∀ a. (∀ a0. wf≪(a0, a) → p(a0)) → p(a)) → (∀ a. p(a)) ⊦

Rule argument

Additional information

Proof step 80 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 81:

  (∀ a. (∀ a0. wf≪(a0, a) → (∀ n. a0 ≠ chn(n))) → (∀ n. a ≠ chn(n))) → (∀ a. ∀ n. a ≠ chn(n)), ∀ n. wf≪(chn(n + 1), chn(n)) ⊦

Rule argument

Additional information

Used terms: λ a. ∀ n. a ≠ chn(n)

Proof step 81 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  ∀ a0. wf≪(a0, chn(n)) → (∀ n. a0 ≠ chn(n)), ∀ n. wf≪(chn(n + 1), chn(n)) ⊦

Rule argument

Additional information

Proof step 82 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 83:

  wf≪(chn(n + 1), chn(n)), ∀ n. wf≪(chn(n + 1), chn(n)), ∀ a0. wf≪(a0, chn(n)) → (∀ n. a0 ≠ chn(n)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 83 from proof wf-equiv-noethind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 84:

  wf≪(chn(n + 1), chn(n)), wf≪(chn(n + 1), chn(n)) → (∀ n0. chn(n + 1) ≠ chn(n0)), ∀ n. wf≪(chn(n + 1), chn(n)) ⊦

Rule argument

Additional information

Used terms: chn(n + 1)

Proof step 84 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  wf≪(chn(n + 1), chn(n)), ∀ n. wf≪(chn(n + 1), chn(n)), ∀ n0. chn(n + 1) ≠ chn(n0) ⊦

Rule argument

Additional information

Proof step 85 from proof wf-equiv-noethind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n + 1