Proof step 1 from proof pfxclosed-tracestar (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ pfxclosed(trace*(ioa)) ⊦

Rule argument

Additional information

Proof step 2 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ pfxclosed(alp) ↔ (∀ al1, al2. alp(al2) ∧ al1 ⊑ al2 → alp(al1))

• Proof step 4:

  ∃ el, el0. ¬(trace*(ioa)(el0) ∧ el ⊑ el0 → trace*(ioa)(el)) ⊦

Rule argument

Additional information

Used terms: trace*(ioa)

Proof step 3 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  trace*(ioa)(el0), el ⊑ el0, ¬ trace*(ioa)(el) ⊦

Rule argument

Additional information

Proof step 5 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ x ⊑ y ↔ (∃ z. x + z = y)

• Proof step 7:

  trace*(ioa)(el0), ¬ trace*(ioa)(el), ∃ z. el + z = el0 ⊦

Rule argument

Additional information

Used terms: el, el0

Proof step 6 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  trace*(ioa)(el + el1), ¬ trace*(ioa)(el) ⊦

Rule argument

Additional information

Proof step 8 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  ioa = IOAut(start, step, ext), trace*(ioa)(el + el1), ¬ trace*(ioa)(el) ⊦

Rule argument

Additional information

Used simplifier rules: IOAutomaton('s, 'a, 'e) freely generated by IOAut;;

Proof step 9 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  trace*(IOAut(start, step, ext))(el + el1), ¬ trace*(IOAut(start, step, ext))(el) ⊦

Rule argument

Additional information

Proof step 10 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ trace*(IOAut(start, step, ext))(el) ↔ (∃ sl, al. el = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al))

• Proof step 12:

  trace*(IOAut(start, step, ext))(el + el1), ∀ sl, al. ¬(el = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al)) ⊦

Rule argument

Additional information

Used terms: start, step, ext, el

Proof step 11 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  trace*(IOAut(start, step, ext))(el + el1), ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 13 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ trace*(IOAut(start, step, ext))(el) ↔ (∃ sl, al. el = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al))

• Proof step 15:

  ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∃ sl, al. el + el1 = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al) ⊦

Rule argument

Additional information

Used terms: start, step, ext, el + el1

Proof step 14 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  el + el1 = ext !(al), frag*(IOAut(start, step, ext))(sl, al), start(sl[0]), ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 16 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  frag*(IOAut(start, step, ext))(sl, al), start(sl[0]), ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∃ al1, al0. al = al1 + al0 ∧ ext !(al1) = el ∧ ext !(al0) = el1 ⊦

Rule argument

Additional information

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

Proof step 17 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ¬ # 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 21:

  frag*(IOAut(start, step, ext))(sl, al1 + al0), start(sl[0]), ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦ ¬ #(al1 + al0) < # al1 ∧ # al1 < # sl

• Proof step 26:

  # 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)), start(sl[0]), ¬ #(al1 + al0) < # al1, ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

Rule argument

Additional information

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

Proof step 20 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  frag*(IOAut(start, step, ext))(sl, al1 + al0), start(sl[0]), # sl ≤ # al1, ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

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 22 from proof pfxclosed-tracestar (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  # sl = #(al1 + al0) + 1, start(sl[0]), # sl ≤ # al1, ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∀ n. n < #(al1 + al0) → IOAut(start, step, ext).step(sl[n], (al1 + al0)[n], sl[n +1]) ⊦

Rule argument

Additional information

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

Proof step 23 from proof pfxclosed-tracestar (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  # sl = (# al1 + # al0) + 1, start(sl[0]), # sl ≤ # al1, ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∀ n. n < # al1 + # al0 → step(sl[n], (al1 + al0)[n], sl[n + 1]) ⊦

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 25 from proof pfxclosed-tracestar (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 26 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  sl ≠ [], # al1 < # sl, frag*(IOAut(start, step, ext))(sl.take(# al1 + 1), al1), frag*(IOAut(start, step, ext))(sl.drop(# al1), al0), start(sl.head), ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

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 27 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  frag*(IOAut(start, step, ext))(s ' + sl0.take(# al1), al1), frag*(IOAut(start, step, ext))((s ' + sl0).drop(# al1), al0), start(s), # al1 ≤ # sl0, ∀ sl, al. ext !(al1) ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]) ⊦

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 + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 29 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 30:

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

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: sl0, # al1, sl1, sl2

Proof step 30 from proof pfxclosed-tracestar (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

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 31 from proof pfxclosed-tracestar (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: s ' + sl1, al1