Proof step 1 from proof allge-rec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(all≥(b ' + x, a) ↔ ¬ b < a ∧ all≥(x, a)) ⊦

Rule argument

Additional information

Proof step 2 from proof allge-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ (∀ b0. b0 = b ∨ b0 ∈ x → ¬ b0 < a) ↔ ¬ b < a ∧ (∀ b. b ∈ x → ¬ b < a)

Rule argument

Additional information

Used simplifier rules: allge-def: ⊦ all≥(x, a) ↔ (∀ b. b ∈ x → ¬ b < a); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 3 from proof allge-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  b < a ⊦ (∀ b0. b0 = b ∨ b0 ∈ x → ¬ b0 < a) ↔ ¬ b < a ∧ (∀ b. b ∈ x → ¬ b < a)

Rule argument

Additional information

Used formulas: b < a

Proof step 4 from proof allge-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  b < a, ∀ b0. b0 = b ∨ b0 ∈ x → ¬ b0 < a ⊦

Rule argument

Additional information

Proof step 5 from proof allge-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: b