Proof step 1 from proof emptymove-splitfirst (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  s ≠ s2, move(IOAut(start, step, ext))(s, [], s2) ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], s2)

Rule argument

Additional information

Proof step 2 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  s ≠ s2, ∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ s = sl[0] ∧ s2 = sl.last ∧ IOAut(start, step, ext).ext !(al) = [] ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], s2)

Rule argument

Additional information

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

Proof step 3 from proof emptymove-splitfirst (previous step) (back to tree)

Lemma move

Proof step 4 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ext !(al) = [], sl[0] ≠ sl.last, frag*(IOAut(start, step, ext))(sl, al) ⊦ ∃ s1, a. ext(a) = None ∧ step(sl[0], a, s1) ∧ move(IOAut(start, step, ext))(s1, [], sl.last)

Rule argument

Additional information

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

Proof step 5 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  ext !(al) = [], sl = s + sl0, sl[0] ≠ sl.last, frag*(IOAut(start, step, ext))(sl, al) ⊦ ∃ s1, a. ext(a) = None ∧ step(sl[0], a, s1) ∧ move(IOAut(start, step, ext))(s1, [], sl.last)

Rule argument

Additional information

Used simplifier rules: not-finfrag-empty: ⊦ ¬ frag*(IOAut(start, step, ext))([], al); List('a) freely generated by [], +;;

Proof step 6 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ext !(al) = [], s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(s ' + sl0, al) ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], (s ' + sl0).last)

Rule argument

Additional information

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

Proof step 7 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  ext !(al) = [], al = a0 + al0, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(s ' + sl0, al) ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], (s ' + sl0).last)

Rule argument

Additional information

Used simplifier rules: finfrag-onlyone: ⊦ frag*(IOAut(start, step, ext))(sl, []) ↔ sl = sl.head '; List('a) freely generated by [], +;; ⊦ ext !([]) = []; (s) ⊦ (a ' + x).head = a; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.last = a; (s)

Proof step 8 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(s ' + sl0, a0 ' + al0) ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], (s ' + sl0).last)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) ⊦ ext !(al + al0) = ext !(al) + ext !(al0); (s)

Proof step 9 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ frag*(IOAut(start, step, ext))(s ' + sl, a ' + al) ↔ step(s, a, sl.head) ∧ frag*(IOAut(start, step, ext))(sl, al)

• Proof step 11:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, sl0.head) ⊦ ∃ s1, a. ext(a) = None ∧ step(s, a, s1) ∧ move(IOAut(start, step, ext))(s1, [], (s ' + sl0).last)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al0, s, ext, sl0, a0, start, step

Proof step 10 from proof emptymove-splitfirst (previous step) (back to tree)

Lemma finfrag-rec

Proof step 11 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, sl0.head) ⊦ ext(a0) = None ∧ step(s, a0, hd(⌜sl0⌝ )) ∧ move(IOAut(start, step, ext))(hd(⌜sl0⌝ ), [], (s ' + sl0).last)

Rule argument

Additional information

Used terms: hd(⌜sl0⌝ ), a0

Proof step 12 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, sl0.head) ⊦ step(s, a0, hd(⌜sl0⌝ )) ∧ move(IOAut(start, step, ext))(hd(⌜sl0⌝ ), [], (s ' + sl0).last)

Rule argument

Additional information

Proof step 13 from proof emptymove-splitfirst (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, sl0.head) ⊦ step(s, a0, hd(⌜sl0⌝ )) ∧ (∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ hd(⌜sl0⌝ ) = sl[0] ∧ (s ' + sl0).last = sl.last ∧ IOAut(start, step, ext).ext !(al) = [])

Rule argument

Additional information

Used terms: IOAut(start, step, ext), hd(⌜sl0⌝ ), [], (s ' + sl0).last

Proof step 14 from proof emptymove-splitfirst (previous step) (back to tree)

Lemma move

Proof step 15 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ext !(al0) = [], ext(a0) = None, s ≠ (s ' + sl0).last, frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, sl0.head) ⊦ step(s, a0, hd(⌜sl0⌝ )) ∧ (∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ hd(⌜sl0⌝ ) = sl[0] ∧ (s ' + sl0).last = sl.last ∧ ext !(al) = [])

Rule argument

Additional information

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

Proof step 16 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  ext !(al0) = [], ext(a0) = None, sl0 = s0 + sl1, s ≠ (s ' + sl0).last, sl0 ≠ [], frag*(IOAut(start, step, ext))(sl0, al0), step(s, a0, s0) ⊦ step(s, a0, hd(⌜sl0⌝ )) ∧ (∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ hd(⌜sl0⌝ ) = sl[0] ∧ (s ' + sl0).last = sl.last ∧ ext !(al) = [])

Rule argument

Additional information

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

Proof step 17 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ext !(al0) = [], ext(a0) = None, s ≠ (s0 ' + sl1).last, frag*(IOAut(start, step, ext))(s0 ' + sl1, al0), step(s, a0, s0) ⊦ ∃ al, sl. frag*(IOAut(start, step, ext))(sl, al) ∧ s0 = sl[0] ∧ (sl[0] ' + sl1).last = sl.last ∧ ext !(al) = []

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ a + x = a ' + x; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ hd(⌜a '⌝ + ⌜x⌝ ) = a; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 18 from proof emptymove-splitfirst (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

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 ' + sl1