Proof step 1 from proof tree-le-elem-unfold (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ¬ t ≤ a, ∀ b. b ∈ t → ¬ a < b ⊦

Rule argument

Additional information

Used simplifier rules: tree-le-elem-in-tree: ⊦ b ∈ t ∧ t ≤ a → ¬ a < b;

Proof step 2 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬ branch(t0, a0, t1) ≤ a, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, ∀ a. ¬(¬ t1 ≤ a ∧ (∀ b. b ∈ t1 → ¬ a < b)), ∀ a. ¬(¬ t0 ≤ a ∧ (∀ b. b ∈ t0 → ¬ a < b)) ⊦

Rule argument

Additional information

Used simplifier rules: tree-le-elem-base: ⊦ leaf ≤ a; tree freely generated by leaf, branch;;

Proof step 3 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, ∀ a1. t0 ≤ a1 ∨ ¬(∀ b. b ∈ t0 → ¬ a1 < b), ∀ a1. t1 ≤ a1 ∨ ¬(∀ b. b ∈ t1 → ¬ a1 < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used simplifier rules: tree-le-elem-rec: ⊦ branch(t0, b, t1) ≤ a ↔ t0 ≤ a ∧ ¬ a < b ∧ t1 ≤ a;

Proof step 4 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  ∀ a1. t1 ≤ a1 ∨ ¬(∀ b. b ∈ t1 → ¬ a1 < b), ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(∀ b. b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used terms: a

Proof step 5 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, ∀ a1. t1 ≤ a1 ∨ ¬(∀ b. b ∈ t1 → ¬ a1 < b), t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Proof step 6 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b), t1 ≤ a ∨ ¬(∀ b. b ∈ t1 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used terms: a

Proof step 7 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b), t1 ≤ a ∨ ¬(b0 ∈ t1 → ¬ a < b0) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Proof step 8 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  b0 ∈ branch(t0, a0, t1) → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t1 ≤ a ∨ ¬(b0 ∈ t1 → ¬ a < b0), t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used terms: b0

Proof step 9 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ a ∈ branch(t0, b, t1) ↔ a ∈ t0 ∨ a = b ∨ a ∈ t1

• Proof step 11:

  b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b), t1 ≤ a ∨ ¬(b0 ∈ t1 → ¬ a < b0) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used terms: b0, t0, a0, t1

Proof step 10 from proof tree-le-elem-unfold (previous step) (back to tree)

Lemma in-rec

Proof step 11 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  t1 ≤ a, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t1 ≤ a ∨ ¬(b0 ∈ t1 → ¬ a < b0), t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0 ∧ t1 ≤ a

Rule argument

Additional information

Used formulas: t1 ≤ a

Proof step 12 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  t1 ≤ a, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Proof step 13 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  t1 ≤ a, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, b ∈ branch(t0, a0, t1) → ¬ a < b, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Used terms: b

Proof step 14 from proof tree-le-elem-unfold (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ a ∈ branch(t0, b, t1) ↔ a ∈ t0 ∨ a = b ∨ a ∈ t1

• Proof step 16:

  t1 ≤ a, b ∈ t0 ∨ b = a0 ∨ b ∈ t1 → ¬ a < b, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Used terms: b, t0, a0, t1

Proof step 15 from proof tree-le-elem-unfold (previous step) (back to tree)

Lemma in-rec

Proof step 16 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  b ≠ a0, t1 ≤ a, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, b ∈ t0 ∨ b = a0 ∨ b ∈ t1 → ¬ a < b, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Used formulas: b = a0

Proof step 17 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  b ≠ a0, t1 ≤ a, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, b ∈ t0 ∨ b ∈ t1 → ¬ a < b, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Proof step 18 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 19:

  b ≠ a0, b0 ≠ a0, t1 ≤ a, b ∈ t0 ∨ b ∈ t1 → ¬ a < b, b0 ∈ t0 ∨ b0 = a0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Used formulas: b0 = a0

Proof step 19 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  b ≠ a0, b0 ≠ a0, t1 ≤ a, b ∈ t0 ∨ b ∈ t1 → ¬ a < b, b0 ∈ t0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Proof step 20 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  b ≠ a0, b0 ≠ a0, t1 ≤ a, t0 ≤ a, b0 ∈ t0 ∨ b0 ∈ t1 → ¬ a < b0, b ∈ t0 ∨ b ∈ t1 → ¬ a < b, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b, t0 ≤ a ∨ ¬(b ∈ t0 → ¬ a < b) ⊦ t0 ≤ a ∧ ¬ a < a0

Rule argument

Additional information

Used formulas: t0 ≤ a

Proof step 21 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  b ≠ a0, b0 ≠ a0, a < a0, t0 ≤ a, t1 ≤ a, b ∈ t0 ∨ b ∈ t1 → ¬ a < b, b0 ∈ t0 ∨ b0 ∈ t1 → ¬ a < b0, ∀ b. b ∈ branch(t0, a0, t1) → ¬ a < b ⊦

Rule argument

Additional information

Proof step 22 from proof tree-le-elem-unfold (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-rec: ⊦ a ∈ branch(t0, b, t1) ↔ a ∈ t0 ∨ a = b ∨ a ∈ t1; Used terms: a0