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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  wf(wf1≪), wf(wf2≪), ¬ q(b, c), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  wf(wf1≪), wf(wf2≪) ⊦ wf(λ bc0, bc. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2))

• Proof step 4:

  wf(wf2≪), wf(wf1≪), wf(λ bc0, bc. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2)), ¬ q(b, c), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

Used terms: wf1≪, wf2≪

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

Lemma wf-lexical

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  wf(wf1≪), wf(wf2≪), ¬ q(b, c), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c), ∀ _p. (∀ bc. (∀ bc0. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2) → _p(bc0)) → _p(bc)) → (∀ bc. _p(bc)) ⊦

Rule argument

Additional information

Used terms: λ bc0, bc. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2)

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

Lemma wf-equiv-noethind

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

User applied rule all left

And obtained the following new goals

• Proof step 7:

  wf(wf2≪), wf(wf1≪), ¬ q(b, c), (∀ bc. (∀ bc0. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2) → q(bc0._1, bc0._2)) → q(bc._1, bc._2)) → (∀ bc. q(bc._1, bc._2)), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

Used terms: λ bc. q(bc._1, bc._2)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  wf(wf1≪), wf(wf2≪), ¬ q(b, c), ((∀ bc0. wf1≪(bc0._1, bc._1) ∨ bc0._1 = bc._1 ∧ wf2≪(bc0._2, bc._2) → q(bc0._1, bc0._2)) → q(bc._1, bc._2)) → (∀ bc. q(bc._1, bc._2)), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  bc = (b0, c0), wf(wf2≪), wf(wf1≪), ¬ q(b, c), ((∀ bc0. wf1≪(bc0._1, b0) ∨ bc0._1 = b0 ∧ wf2≪(bc0._2, c0) → q(bc0._1, bc0._2)) → q(b0, c0)) → (∀ bc. q(bc._1, bc._2)), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

Used terms: b0, c0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  wf(wf1≪), wf(wf2≪), ¬ q(b, c), ((∀ bc0. wf1≪(bc0._1, b0) ∨ bc0._1 = b0 ∧ wf2≪(bc0._2, c0) → q(bc0._1, bc0._2)) → q(b0, c0)) → (∀ bc. q(bc._1, bc._2)), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  wf(wf2≪), wf(wf1≪), ¬ q(b0, c0), ¬ q(b, c), ∀ bc0. wf1≪(bc0._1, b0) ∨ bc0._1 = b0 ∧ wf2≪(bc0._2, c0) → q(bc0._1, bc0._2), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c) ⊦

• Proof step 14:

  wf(wf2≪), wf(wf1≪), ¬ q(b, c), ∀ b, c. (∀ b0, c0. wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c0, c) → q(b0, c0)) → q(b, c), ∀ bc. q(bc._1, bc._2) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 12:

  wf(wf1≪), wf(wf2≪), ¬ q(b0, c0), ¬ q(b, c), (∀ b1, c1. wf1≪(b1, b0) ∨ b1 = b0 ∧ wf2≪(c1, c0) → q(b1, c1)) → q(b0, c0), ∀ bc0. wf1≪(bc0._1, b0) ∨ bc0._1 = b0 ∧ wf2≪(bc0._2, c0) → q(bc0._1, bc0._2) ⊦

Rule argument

Additional information

Used terms: b0, c0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  wf(wf2≪), wf(wf1≪), ¬ q(b0, c0), ¬ q(b, c), ¬ q(b1, c1), ∀ bc0. wf1≪(bc0._1, b0) ∨ bc0._1 = b0 ∧ wf2≪(bc0._2, c0) → q(bc0._1, bc0._2), wf1≪(b1, b0) ∨ b1 = b0 ∧ wf2≪(c1, c0) ⊦

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: (b1, c1)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: (b, c)