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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  b < a, b ∈ t, a ≤ t ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  b < a, a ≤ t1, a ≤ t0, ¬ a0 < a, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t1 ∨ ¬ a1 ≤ t1, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t0 ∨ ¬ a1 ≤ t0, b ∈ t0 ∨ b = a0 ∨ b ∈ t1 ⊦

Rule argument

Additional information

Used terms: b, t0, a0, t1

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

Lemma in-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  b < a, a ≤ t0, a ≤ t1, ¬ a0 < a, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t0 ∨ ¬ a1 ≤ t0, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t1 ∨ ¬ a1 ≤ t1, b ∈ t0 ∨ b ∈ t1 ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  b < a, a ≤ t1, a ≤ t0, ¬ a0 < a, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t1 ∨ ¬ a1 ≤ t1, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t0 ∨ ¬ a1 ≤ t0, b ∈ t0 ∨ b ∈ t1, ¬ b < a ∨ ¬ b ∈ t1 ∨ ¬ a ≤ t1 ⊦

Rule argument

Additional information

Used terms: b, a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  b < a, b ∈ t0, a ≤ t0, a ≤ t1, ¬ a0 < a, ¬ b ∈ t1, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t0 ∨ ¬ a1 ≤ t0, ∀ b0, a1. ¬ b0 < a1 ∨ ¬ b0 ∈ t1 ∨ ¬ a1 ≤ t1 ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: b, a