Proof step 1 from proof move-split (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  move(IOAut(start, step, ext))(s, el, s2), ¬ # el < n ⊦ ∃ s1. move(IOAut(start, step, ext))(s, el.take(n), s1) ∧ move(IOAut(start, step, ext))(s1, el.drop(n), s2)

Rule argument

Additional information

Proof step 2 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  move(IOAut(start, step, ext))(s, el, s2), n ≤ # el ⊦ ∃ s1. move(IOAut(start, step, ext))(s, el.take(n), s1) ∧ move(IOAut(start, step, ext))(s1, el.drop(n), s2)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 3 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ move(ioa)(s1, el, s2) ↔ (∃ al, sl. frag*(ioa)(sl, al) ∧ s1 = sl[0] ∧ s2 = sl.last ∧ ioa.ext !(al) = el)

• Proof step 5:

  n ≤ # el, ∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ s = sl[0] ∧ s2 = sl.last ∧ IOAut(start, step, ext).ext !(al) = el ⊦ ∃ s1. move(IOAut(start, step, ext))(s, el.take(n), s1) ∧ move(IOAut(start, step, ext))(s1, el.drop(n), s2)

Rule argument

Additional information

Used terms: IOAut(start, step, ext), s, el, s2

Proof step 4 from proof move-split (previous step) (back to tree)

Lemma move

Proof step 5 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  frag*(IOAut(start, step, ext))(sl, al), n ≤ # ext !(al) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al).take(n), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al).drop(n), sl.last)

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).ext = ext; (s)

Proof step 6 from proof move-split (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  ext !(al) = el + el0, # el = n, frag*(IOAut(start, step, ext))(sl, al), n ≤ # ext !(al) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], el, s1) ∧ move(IOAut(start, step, ext))(s1, el0, sl.last)

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: ext !(al), n, el, el0

Proof step 7 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ext !(al) = el + el0, frag*(IOAut(start, step, ext))(sl, al) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], el, s1) ∧ move(IOAut(start, step, ext))(s1, el0, sl.last)

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 ≤ m + n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s)

Proof step 8 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ ext !(al) = el + el0 ↔ (∃ al1, al0. al = al1 + al0 ∧ ext !(al1) = el ∧ ext !(al0) = el0)

• Proof step 10:

  frag*(IOAut(start, step, ext))(sl, al), ∃ al1, al0. al = al1 + al0 ∧ ext !(al1) = el ∧ ext !(al0) = el0 ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], el, s1) ∧ move(IOAut(start, step, ext))(s1, el0, sl.last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: ext, al, el, el0

Proof step 9 from proof move-split (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  frag*(IOAut(start, step, ext))(sl, al1 + al0) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Proof step 11 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ¬ # al < n ∧ n < # sl → ( frag*(IOAut(start, step, ext))(sl, al) ↔ frag*(IOAut(start, step, ext))(sl.take(n + 1), al.take(n)) ∧ frag*(IOAut(start, step, ext))(sl.drop(n), al.drop(n)))

• Proof step 13:

  frag*(IOAut(start, step, ext))(sl, al1 + al0) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last), ¬ #(al1 + al0) < # al1 ∧ # al1 < # sl

• Proof step 18:

  # al1 < # sl, frag*(IOAut(start, step, ext))(sl.take(# al1 + 1), (al1 + al0).take(# al1)), frag*(IOAut(start, step, ext))(sl.drop(# al1), (al1 + al0).drop(# al1)), ¬ #(al1 + al0) < # al1 ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Used terms: ext, # al1, al1 + al0, step, start, sl

Proof step 12 from proof move-split (previous step) (back to tree)

Lemma finfrag-split

Proof step 13 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  frag*(IOAut(start, step, ext))(sl, al1 + al0), # sl ≤ # al1 ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

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

Proof step 14 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ frag*(ioa)(sl, al) ↔ # sl = # al + 1 ∧ (∀ n. n < # al → ioa.step(sl[n], al[n], sl[n +1]))

• Proof step 16:

  # sl = #(al1 + al0) + 1, # sl ≤ # al1, ∀ n. n < #(al1 + al0) → IOAut(start, step, ext).step(sl[n], (al1 + al0)[n], sl[n +1]) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Used terms: IOAut(start, step, ext), sl, al1 + al0

Proof step 15 from proof move-split (previous step) (back to tree)

Lemma fragstar

Proof step 16 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # sl = (# al1 + # al0) + 1, # sl ≤ # al1, ∀ n. n < # al1 + # al0 → step(sl[n], (al1 + al0)[n], sl[n + 1]) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl[0], ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).step = step; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 17 from proof move-split (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ 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

Proof step 18 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  sl ≠ [], # al1 < # sl, frag*(IOAut(start, step, ext))(sl.take(# al1 + 1), al1), frag*(IOAut(start, step, ext))(sl.drop(# al1), al0) ⊦ ∃ s1. move(IOAut(start, step, ext))(sl.head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) ⊦ (x + y).take(# x) = x; (s) ⊦ (x + y).drop(# x) = y; (s)

Proof step 19 from proof move-split (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  # sl0 = # al1, sl = sl0 + sl1, sl ≠ [], # al1 < # sl, frag*(IOAut(start, step, ext))(sl1, al0), frag*(IOAut(start, step, ext))(sl.take(# al1 + 1), al1), # al1 ≤ # sl ⊦ ∃ s1. move(IOAut(start, step, ext))(sl.head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: sl, # al1, sl0, sl1

Proof step 20 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # sl0 = # al1, sl1 ≠ [], frag*(IOAut(start, step, ext))((sl0 + sl1).take(# al1 + 1), al1), frag*(IOAut(start, step, ext))(sl1, al0) ⊦ ∃ s1. move(IOAut(start, step, ext))((sl0 + sl1).head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl1.last)

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 ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ y ≠ [] → (x + y).last = y.last; (s) ⊦ m < n → n ≠ 0; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 21 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ # x < n → (x + y).take(n) = x + y.take(n - # x)

• Proof step 23:

  # sl0 = # al1, sl1 ≠ [], # sl0 < # al1 + 1, frag*(IOAut(start, step, ext))(sl1, al0), frag*(IOAut(start, step, ext))(sl0 + sl1.take(# al1 + 1 - # sl0), al1) ⊦ ∃ s1. move(IOAut(start, step, ext))((sl0 + sl1).head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # al1 + 1, sl0, sl1

Proof step 22 from proof move-split (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # sl0 = # al1, sl1 ≠ [], frag*(IOAut(start, step, ext))(sl1, al0), frag*(IOAut(start, step, ext))(sl0 + sl1.head ', al1) ⊦ ∃ s1. move(IOAut(start, step, ext))((sl0 + sl1).head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) ⊦ x ≠ [] → x.take(1) = x.head '; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m - m = 0; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s)

Proof step 24 from proof move-split (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 25:

  # sl0 = # al1, sl1 = s + sl, sl1 ≠ [], frag*(IOAut(start, step, ext))(sl0 + s ', al1), frag*(IOAut(start, step, ext))(sl1, al0) ⊦ ∃ s1. move(IOAut(start, step, ext))((sl0 + sl1).head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), sl1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: sl1, s, sl

Proof step 25 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  # sl0 = # al1, frag*(IOAut(start, step, ext))(sl0 + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0) ⊦ ∃ s1. move(IOAut(start, step, ext))((sl0 + s ').head, ext !(al1), s1) ∧ move(IOAut(start, step, ext))(s1, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (x + a ' + y).head = (x + a ').head; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 26 from proof move-split (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 27:

  # sl0 = # al1, frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))(sl0 + s ', al1) ⊦ move(IOAut(start, step, ext))((sl0 + s ').head, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used terms: s

Proof step 27 from proof move-split (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  # sl0 = # al1, sl0 + s ' = s0 + sl1, sl0 + s ' ≠ [], frag*(IOAut(start, step, ext))(sl0 + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0) ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl0 + s ', s0, sl1

Proof step 28 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # sl0 = # al1, sl0 + s ' = s0 ' + sl1, frag*(IOAut(start, step, ext))(s0 ' + sl1, al1), frag*(IOAut(start, step, ext))(s ' + sl, al0), s = s0 ∨ s ∈ sl1, s0 ∈ sl0 ∨ s0 = s ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

Proof step 29 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  y ≠ [] ⊦ y + z = a ' + x ↔ a = y.head ∧ x = y.tail + z

• Proof step 31:

  # sl0 = # al1, sl0 + s ' = s0 ' + sl1, sl0 = [], frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))(s0 ' + sl1, al1), s0 ∈ sl0 ∨ s0 = s, s = s0 ∨ s ∈ sl1 ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

• Proof step 36:

  # sl0 = # al1, s0 = sl0.head, sl1 = sl0.tail + s ', sl0 ≠ [], frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))(s0 ' + sl1, al1), s0 ∈ sl0 ∨ s0 = s, s = s0 ∨ s ∈ sl1 ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: sl0, s ', s0, sl1

Proof step 30 from proof move-split (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  frag*(IOAut(start, step, ext))(s0 ' + sl, al0), ¬ move(IOAut(start, step, ext))(s0, ext !(al0), (s0 ' + sl).last) ⊦

Rule argument

Additional information

Used simplifier rules: finfrag-one: ⊦ frag*(IOAut(start, step, ext))(s ', []); move-empty: ⊦ move(IOAut(start, step, ext))(s, [], s); ⊦ ext !([]) = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ ¬ a ∈ []; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ # [] = 0; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ [] + x = x; (s)

Proof step 32 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ move(ioa)(s1, el, s2) ↔ (∃ al, sl. frag*(ioa)(sl, al) ∧ s1 = sl[0] ∧ s2 = sl.last ∧ ioa.ext !(al) = el)

• Proof step 34:

  frag*(IOAut(start, step, ext))(s0 ' + sl, al0), ∀ al, sl0. ¬(frag*(IOAut(start, step, ext))(sl0, al) ∧ s0 = sl0[0] ∧ (s0 ' + sl).last = sl0.last ∧ IOAut(start, step, ext).ext !(al) = ext !(al0)) ⊦

Rule argument

Additional information

Used terms: IOAut(start, step, ext), s0, ext !(al0), (s0 ' + sl).last

Proof step 33 from proof move-split (previous step) (back to tree)

Lemma move

Proof step 34 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  frag*(IOAut(start, step, ext))(s0 ' + sl, al0), ∀ al, sl0. ¬ frag*(IOAut(start, step, ext))(sl0, al) ∨ s0 ≠ sl0[0] ∨ (sl0[0] ' + sl).last ≠ sl0.last ∨ ext !(al) ≠ ext !(al0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).ext = ext; (s)

Proof step 35 from proof move-split (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al0, s0 ' + sl

Proof step 36 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # sl0 = # al1, sl0 ≠ [], frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))(sl0 + s ', al1) ⊦ move(IOAut(start, step, ext))(sl0.head, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: ⊦ x.head ∈ x ↔ x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x ≠ [] → x.head ' + x.tail = x; (s)

Proof step 37 from proof move-split (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 38:

  # sl0 = # al1, sl0 = s0 + sl1, sl0 ≠ [], frag*(IOAut(start, step, ext))(sl0 + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0) ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: sl0, s0, sl1

Proof step 38 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1) ⊦ move(IOAut(start, step, ext))(s0, ext !(al1), s) ∧ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 39 from proof move-split (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0), ¬ move(IOAut(start, step, ext))(s0, ext !(al1), s) ⊦

• Proof step 44:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0), ¬ move(IOAut(start, step, ext))(s, ext !(al0), (s ' + sl).last) ⊦

Rule argument

Additional information

Proof step 40 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ move(ioa)(s1, el, s2) ↔ (∃ al, sl. frag*(ioa)(sl, al) ∧ s1 = sl[0] ∧ s2 = sl.last ∧ ioa.ext !(al) = el)

• Proof step 42:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), ∀ al, sl. ¬(frag*(IOAut(start, step, ext))(sl, al) ∧ s0 = sl[0] ∧ s = sl.last ∧ IOAut(start, step, ext).ext !(al) = ext !(al1)) ⊦

Rule argument

Additional information

Used terms: IOAut(start, step, ext), s0, ext !(al1), s

Proof step 41 from proof move-split (previous step) (back to tree)

Lemma move

Proof step 42 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0), ∀ al, sl0. ¬ frag*(IOAut(start, step, ext))(sl0, al) ∨ s0 ≠ sl0[0] ∨ s ≠ sl0.last ∨ ext !(al) ≠ ext !(al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).ext = ext; (s)

Proof step 43 from proof move-split (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x)[0] = a; (s) ⊦ (a ' + x + b ').last = b; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al1, (s0 ' + sl1) + s '

Proof step 44 from proof move-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ move(ioa)(s1, el, s2) ↔ (∃ al, sl. frag*(ioa)(sl, al) ∧ s1 = sl[0] ∧ s2 = sl.last ∧ ioa.ext !(al) = el)

• Proof step 46:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))(s ' + sl, al0), frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), ∀ al, sl0. ¬(frag*(IOAut(start, step, ext))(sl0, al) ∧ s = sl0[0] ∧ (s ' + sl).last = sl0.last ∧ IOAut(start, step, ext).ext !(al) = ext !(al0)) ⊦

Rule argument

Additional information

Used terms: IOAut(start, step, ext), s, ext !(al0), (s ' + sl).last

Proof step 45 from proof move-split (previous step) (back to tree)

Lemma move

Proof step 46 from proof move-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  # sl1 + 1 = # al1, frag*(IOAut(start, step, ext))((s0 ' + sl1) + s ', al1), frag*(IOAut(start, step, ext))(s ' + sl, al0), ∀ al, sl0. ¬ frag*(IOAut(start, step, ext))(sl0, al) ∨ s ≠ sl0[0] ∨ (sl0[0] ' + sl).last ≠ sl0.last ∨ ext !(al) ≠ ext !(al0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).ext = ext; (s)

Proof step 47 from proof move-split (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al0, s ' + sl