Proof step 1 from proof pfxclosed-trace (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-trace (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ pfxclosed(αp) ↔ (∀ α1, α2. αp(α2) ∧ α1 ⊑ α2 → αp(α1))

• Proof step 4:

  ∃ β, β0. ¬(trace(ioa)(β0) ∧ β ⊑ β0 → trace(ioa)(β)) ⊦

Rule argument

Additional information

Used terms: trace(ioa)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  trace(ioa)(β0), β ⊑ β0, ¬ trace(ioa)(β) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  β = ⌜el⌝ , trace(ioa)(β0), β ⊑ β0, ¬ trace(ioa)(β) ⊦

• Proof step 30:

  β = ⌜ef⌝ , trace(ioa)(β0), β ⊑ β0, ¬ trace(ioa)(β) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  trace(ioa)(β0), ⌜el⌝ ⊑ β0, ¬ trace*(ioa)(el) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ trace(ioa)(⌜el⌝ ) ↔ trace*(ioa)(el); (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  ioa = IOAut(start, step, ext), trace(ioa)(β0), ⌜el⌝ ⊑ β0, ¬ trace*(ioa)(el) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  trace(IOAut(start, step, ext))(β0), ⌜el⌝ ⊑ β0, ¬ trace*(IOAut(start, step, ext))(el) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ trace(IOAut(start, step, ext))(β) ↔ (∃ σ, α. β = ext !(α) ∧ exec(IOAut(start, step, ext))(σ, α))

• Proof step 11:

  ⌜el⌝ ⊑ β0, ¬ trace*(IOAut(start, step, ext))(el), ∃ σ, α. β0 = ext !(α) ∧ exec(IOAut(start, step, ext))(σ, α) ⊦

Rule argument

Additional information

Used terms: start, step, ext, β0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  frag(IOAut(start, step, ext))(σ, α), start(σ[0]), ⌜el⌝ ⊑ ext !(α), ¬ trace*(IOAut(start, step, ext))(el) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  frag(IOAut(start, step, ext))(σ, α), start(σ[0]), ⌜el⌝ ⊑ ext !(α), ∀ sl, al. ¬(el = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al)) ⊦

Rule argument

Additional information

Used terms: start, step, ext, el

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  frag(IOAut(start, step, ext))(σ, α), start(σ[0]), ⌜el⌝ ⊑ ext !(α), ∀ 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 15 from proof pfxclosed-trace (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 17:

  frag(IOAut(start, step, ext))(σ, α), start(σ[0]), ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∃ β. ⌜el⌝ + β = ext !(α) ⊦

Rule argument

Additional information

Used terms: ⌜el⌝ , ext !(α)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ ext !(α) = ⌜el⌝ + β ↔ (∃ al, α0. α = ⌜al⌝ + α0 ∧ ext !(⌜al⌝ ) = ⌜el⌝ ∧ ext !(α0) = β)

• Proof step 20:

  frag(IOAut(start, step, ext))(σ, α), start(σ[0]), ∀ sl, al. el ≠ ext !(al) ∨ ¬ frag*(IOAut(start, step, ext))(sl, al) ∨ ¬ start(sl[0]), ∃ al, α0. α = ⌜al⌝ + α0 ∧ ext !(⌜al⌝ ) = ⌜el⌝ ∧ ext !(α0) = β ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ext, α, el, β

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ ¬ # α < ⌜n⌝ ∧ ⌜n⌝ < # σ → ( frag(IOAut(start, step, ext))(σ, α) ↔ frag*(IOAut(start, step, ext))(σ.take(n + 1), α.take(n)) ∧ frag(IOAut(start, step, ext))(σ.drop(n), α.drop(n)))

• Proof step 23:

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

• Proof step 28:

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

Rule argument

Additional information

Used terms: ext, ⌜al⌝ + α0, start, σ, # al, step

Proof step 22 from proof pfxclosed-trace (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ¬ n∞ + n∞1 < n∞1; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 26:

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

Rule argument

Additional information

Used terms: ext, ⌜al⌝ + α0, start, σ, step

Proof step 25 from proof pfxclosed-trace (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof pfxclosed-trace (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf

Proof step 27 from proof pfxclosed-trace (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ ¬ n∞ + n∞1 < n∞1; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ¬ n∞ + n∞1 < n∞1; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ (⌜x⌝ + σ).drop(# x) = σ; (s) ⊦ (⌜x⌝ + σ).take(# x) = x; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ # σ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf m < n, ¬ # σ < ⌜n⌝ ⊦ σ.take(n)[m] = σ[m]; (s) Used terms: σ.take(# al + 1), al

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  trace(ioa)(β0), ⌜ef⌝ ⊑ β0, ¬ traceω(ioa)(ef) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ trace(ioa)(⌜ef⌝ ) ↔ traceω(ioa)(ef); (s)

Proof step 31 from proof pfxclosed-trace (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ⌜nf⌝ ⊑ ⌜nf0⌝ ↔ nf = nf0; (s) ⊦ trace(ioa)(⌜ef⌝ ) ↔ traceω(ioa)(ef); (s) ⊦ ¬ ⌜nf⌝ ⊑ ⌜x⌝ ; (s)