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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  t ≠ leaf, a < t.toList.last, t ≤ a ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  branch(t0, a0, t1) ≠ leaf, a < branch(t0, a0, t1).toList.last, branch(t0, a0, t1) ≤ a, ∀ a. ¬(t1 ≠ leaf ∧ a < t1.toList.last ∧ t1 ≤ a), ∀ a. ¬(t0 ≠ leaf ∧ a < t0.toList.last ∧ t0 ≤ a) ⊦

Rule argument

Additional information

Used simplifier rules: tree freely generated by leaf, branch;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  t1 ≠ leaf, a0 < (a0 ' + t1.toList).last, a < (a0 ' + t1.toList).last, t1 ≤ a, t0 ≤ a, ¬ a < a0, ∀ a1. ¬ a1 < t1.toList.last ∨ ¬ t1 ≤ a1, t0 = leaf ∨ (∀ a1. ¬ a1 < t0.toList.last ∨ ¬ t0 ≤ a1) ⊦

Rule argument

Additional information

Used simplifier rules: tree-le-elem-rec: ⊦ branch(t0, b, t1) ≤ a ↔ t0 ≤ a ∧ ¬ a < b ∧ t1 ≤ a; toList-rec: ⊦ branch(t0, a, t1).toList = t0.toList + (a + t1.toList); tree-le-elem-base: ⊦ leaf ≤ a; toList-base: ⊦ leaf.toList = []; ⊦ ¬ a < a; (s) ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem ⊦ (x + a ' + y).last = (a ' + y).last; (s) ⊦ a + x = a ' + x; (s) ⊦ leaf ≠ branch(t, val, t0); (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 5:

  t1.toList ≠ [], t1 ≠ leaf, a < (a0 ' + t1.toList).last, a0 < (a0 ' + t1.toList).last, t0 ≤ a, t1 ≤ a, ¬ a < a0, ∀ a1. ¬ a1 < t1.toList.last ∨ ¬ t1 ≤ a1, t0 = leaf ∨ (∀ a1. ¬ a1 < t0.toList.last ∨ ¬ t0 ≤ a1) ⊦

Rule argument

Additional information

Used simplifier rules: nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.last = a; (s) ⊦ ¬ a < a; (s) Used formulas: t1.toList = []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  t1.toList ≠ [], t1 ≠ leaf, a < t1.toList.last, a0 < t1.toList.last, t1 ≤ a, t0 ≤ a, ¬ a < a0, ∀ a1. ¬ a1 < t1.toList.last ∨ ¬ t1 ≤ a1, t0 = leaf ∨ (∀ a1. ¬ a1 < t0.toList.last ∨ ¬ t0 ≤ a1) ⊦

Rule argument

Additional information

Used simplifier rules: nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → (a ' + x).last = x.last; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a