Proof step 1 from proof toList-ordered-tree-ordered (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ordered≤(t.toList), ¬ ordered≤(t) ⊦

Rule argument

Additional information

Proof step 2 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ordered≤(branch(t0, a, t1).toList), ¬ ordered≤(branch(t0, a, t1)) ⊦ ordered≤(t0.toList) ∧ ¬ ordered≤(t0), ordered≤(t1.toList) ∧ ¬ ordered≤(t1)

Rule argument

Additional information

Used simplifier rules: toList-base: ⊦ leaf.toList = []; ordered-base: ⊦ ordered≤(leaf); tree freely generated by leaf, branch;; ⊦ ordered≤([]); (s)

Proof step 3 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ordered≤(t0.toList + a ' + t1.toList), ordered≤(t1), ordered≤(t0), ¬ ordered≤(branch(t0, a, t1)) ⊦

Rule argument

Additional information

Used simplifier rules: toList-rec: ⊦ branch(t0, a, t1).toList = t0.toList + (a + t1.toList); ⊦ ordered≤(x + y) → ordered≤(x); (s) ⊦ ordered≤(x + y) → ordered≤(y); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 4 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ordered≤(branch(t0, a, t1)) ↔ ordered≤(t0) ∧ t0 ≤ a ∧ a ≤ t1 ∧ ordered≤(t1)

• Proof step 6:

  ordered≤(t0), ordered≤(t1), ordered≤(t0.toList + a ' + t1.toList), ¬ ordered≤(t0) ∨ ¬ t0 ≤ a ∨ ¬ a ≤ t1 ∨ ¬ ordered≤(t1) ⊦

Rule argument

Additional information

Used terms: t0, a, t1

Proof step 5 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Lemma ordered-rec

Proof step 6 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ordered≤(t0.toList + a ' + t1.toList), ordered≤(t1), ordered≤(t0), ¬ t0 ≤ a ∨ ¬ a ≤ t1 ⊦

Rule argument

Additional information

Proof step 7 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  ordered≤(t0), ordered≤(t1), ordered≤(t0.toList + a ' + t1.toList), ¬ t0 ≤ a ⊦

• Proof step 20:

  ordered≤(t0), ordered≤(t1), ordered≤(t0.toList + a ' + t1.toList), ¬ a ≤ t1 ⊦

Rule argument

Additional information

Proof step 8 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ t ≤ a ↔ (∀ b. b ∈ t → ¬ a < b)

• Proof step 10:

  ordered≤(t0.toList + a ' + t1.toList), ordered≤(t1), ordered≤(t0), ∃ b. ¬(b ∈ t0 → ¬ a < b) ⊦

Rule argument

Additional information

Used terms: t0, a

Proof step 9 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Lemma tree-le-elem-unfold

Proof step 10 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a < b, ordered≤(t0), ordered≤(t1), ordered≤(t0.toList + a ' + t1.toList), b ∈ t0 ⊦

Rule argument

Additional information

Proof step 11 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m])

• Proof step 13:

  a < b, ordered≤(t1), ordered≤(t0), b ∈ t0, ∀ m, n. m ≤ n ∧ n < #(t0.toList + a ' + t1.toList) → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used terms: t0.toList + a ' + t1.toList

Proof step 12 from proof toList-ordered-tree-ordered (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a < b, ordered≤(t0), ordered≤(t1), b ∈ t0, ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 14 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ a ∈ t ↔ a ∈ t.toList

• Proof step 16:

  a < b, ordered≤(t1), ordered≤(t0), b ∈ t0.toList, ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used terms: b, t0

Proof step 15 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Lemma in-tree-in-toList

Proof step 16 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 18:

  a < b, ordered≤(t0), ordered≤(t1), ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m], ∃ n. n < # t0.toList ∧ t0.toList[n] = b ⊦

Rule argument

Additional information

Used terms: b, t0.toList

Proof step 17 from proof toList-ordered-tree-ordered (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  t0.toList ≠ [], a < t0.toList[n], n < # t0.toList, ordered≤(t0), ordered≤(t1), ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 19 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ (x + a ' + y)[# x] = a; (s) ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n, # t0.toList

Proof step 20 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ a ≤ t ↔ (∀ b. b ∈ t → ¬ b < a)

• Proof step 22:

  ordered≤(t0.toList + a ' + t1.toList), ordered≤(t1), ordered≤(t0), ∃ b. ¬(b ∈ t1 → ¬ b < a) ⊦

Rule argument

Additional information

Used terms: a, t1

Proof step 21 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Lemma elem-le-tree-unfold

Proof step 22 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  b < a, ordered≤(t0), ordered≤(t1), ordered≤(t0.toList + a ' + t1.toList), b ∈ t1 ⊦

Rule argument

Additional information

Proof step 23 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m])

• Proof step 25:

  b < a, ordered≤(t1), ordered≤(t0), b ∈ t1, ∀ m, n. m ≤ n ∧ n < #(t0.toList + a ' + t1.toList) → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used terms: t0.toList + a ' + t1.toList

Proof step 24 from proof toList-ordered-tree-ordered (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  b < a, ordered≤(t0), ordered≤(t1), b ∈ t1, ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 26 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ a ∈ t ↔ a ∈ t.toList

• Proof step 28:

  b < a, ordered≤(t1), ordered≤(t0), b ∈ t1.toList, ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used terms: b, t1

Proof step 27 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Lemma in-tree-in-toList

Proof step 28 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 30:

  b < a, ordered≤(t0), ordered≤(t1), ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m], ∃ n. n < # t1.toList ∧ t1.toList[n] = b ⊦

Rule argument

Additional information

Used terms: b, t1.toList

Proof step 29 from proof toList-ordered-tree-ordered (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof toList-ordered-tree-ordered (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  t1.toList ≠ [], t1.toList[n] < a, n < # t1.toList, ordered≤(t0), ordered≤(t1), ∀ m, n. m ≤ n ∧ ¬ # t0.toList + # t1.toList < n → ¬ (t0.toList + a ' + t1.toList)[n] < (t0.toList + a ' + t1.toList)[m] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 31 from proof toList-ordered-tree-ordered (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m + n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ (x + y)[n + # x] = y[n]; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ (x + a ' + y)[# x] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # t0.toList, # t0.toList + n +1