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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  wf(wf1≪), wf(wf2≪), ∃ _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 3 from proof wf-lexical (previous step) (back to tree)

Lemma wf-equiv-noethind

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

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

Rule argument

Additional information

Used terms: wf2≪

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

Lemma wf-equiv-noethind

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

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

Rule argument

Additional information

Used terms: wf1≪

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

Lemma wf-equiv-noethind

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used terms: λ b. ∀ c. _p((b, c))

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

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

• Proof step 35:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used terms: (b, c)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used terms: b0, c0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

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

• Proof step 20:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used terms: b0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Used terms: λ c. _p((b, c))

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

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

• Proof step 34:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

Used terms: (b, c1)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

  bc0 = (b0, c2), wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p(bc0), ∀ b0. wf1≪(b0, b) → (∀ c. _p((b0, c))), ∀ c0. wf2≪(c0, c1) → _p((b, c0)), wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c2, c1) ⊦

Rule argument

Additional information

Used terms: b0, c2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b0, c2)), ∀ c0. wf2≪(c0, c1) → _p((b, c0)), ∀ b0. wf1≪(b0, b) → (∀ c. _p((b0, c))), wf1≪(b0, b) ∨ b0 = b ∧ wf2≪(c2, c1) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  wf1≪(b0, b), wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b0, c2)), ∀ b0. wf1≪(b0, b) → (∀ c. _p((b0, c))), ∀ c0. wf2≪(c0, c1) → _p((b, c0)) ⊦

• Proof step 32:

  b0 = b, wf2≪(c0, c), wf2≪(c2, c1), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b0, c2)), ∀ b0. wf1≪(b0, b) → (∀ c. _p((b0, c))), ∀ c0. wf2≪(c0, c1) → _p((b, c0)) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 30:

  wf1≪(b0, b), wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b0, c2)), wf1≪(b0, b) → (∀ c. _p((b0, c))), ∀ c0. wf2≪(c0, c1) → _p((b, c0)) ⊦

Rule argument

Additional information

Used terms: b0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  wf1≪(b0, b), wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b0, c2)), ∀ c0. wf2≪(c0, c1) → _p((b, c0)), ∀ c. _p((b0, c)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  wf2≪(c2, c1), wf2≪(c0, c), ¬ _p((b, c1)), ¬ _p((b, c)), ¬ _p(bc), ¬ _p((b, c0)), ¬ _p((b, c2)), ∀ c0. wf2≪(c0, c1) → _p((b, c0)), ∀ b0. wf1≪(b0, b) → (∀ c. _p((b0, c))) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c2

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c0

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

User applied rule all left

And obtained the following new goals

• Proof step 36:

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

Rule argument

Additional information

Used terms: bc._1, bc._2

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used terms: b, c