Proof step 1 from proof normedfw-branchingfw-aux (conclusion) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (cext(ca) = None ⊃ r(as, cs0) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ r(as1, cs0) ))

• Proof step 3:

  nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f) ⊦ (∀ cs. cstart(cs) → (∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ cstep(cs, ca, cs0) → (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs0)) ))

Rule argument

Additional information

Used terms: cstep, cext, aext, λ as, cs. ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs), astart, cstart, astep

Proof step 2 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 3 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f) ⊦ (cstart(cs) → (∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as))) ∧ ( move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0) ∧ cstep(cs0, ca, cs1) → (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) ))

Rule argument

Additional information

Proof step 4 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ⊦ nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)))

• Proof step 6:

  nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as))) ⊦ (cstart(cs) → (∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as))) ∧ ( move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0) ∧ cstep(cs0, ca, cs1) → (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) ))

Rule argument

Additional information

Used terms: cstep, cext, aext, r, astart, cstart, astep, size01f

Proof step 5 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ (cstart(cs) → (∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as))) ∧ ( move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0) ∧ cstep(cs0, ca, cs1) → (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) ))

Rule argument

Additional information

Proof step 7 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  cstart(cs), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as)

• Proof step 13:

  cstep(cs0, ca, cs1), move(IOAut(astart, astep, aext))(as, [], as0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as0, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

Proof step 8 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  cstart(cs), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as)

Rule argument

Additional information

Used terms: cs

Proof step 9 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  astart(as), cstart(cs), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as, cs), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as. (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as)

Rule argument

Additional information

Proof step 10 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  astart(as), cstart(cs), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as, cs), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)) ∧ astart(as)

Rule argument

Additional information

Used terms: as

Proof step 11 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  astart(as), cstart(cs), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as, cs), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs)

Rule argument

Additional information

Proof step 12 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ move(IOAut(start, step, ext))(s, [], s); (s) Used terms: as

Proof step 13 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

  nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), cstep(cs, ca, cs'), r(as, cs) ⊦ ∃ asl, aal. asl.head = as ∧ aext !(⌜aal⌝ ) = [] ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ ((∃ as', aa. astep(asl.last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs')) ∨ cext(ca) = None ∧ r(asl.last, cs'))

• Proof step 15:

  cstep(cs0, ca, cs1), move(IOAut(astart, astep, aext))(as, [], as0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∃ asl, aal. asl.head = as0 ∧ aext !(⌜aal⌝ ) = [] ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ (∀ as. as ∈ asl → r(as, cs0)) ∧ ((∃ as', aa. astep(asl.last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1)) ∨ cext(ca) = None ∧ r(asl.last, cs1)) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

Used terms: cstep, cext, cs1, as0, aext, r, ca, astart, cstart, astep, size01f, cs0

Proof step 14 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Lemma triang-fin

Proof step 15 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  aext !(aal) = [], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal), move(IOAut(astart, astep, aext))(as, [], asl.head), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.head, cs0), ∀ as. as ∈ asl → r(as, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), astep(asl.last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r(asl.last, cs1) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

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

Proof step 16 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  aext !(aal) = [], asl = as'0 + asl0, asl ≠ [], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal), move(IOAut(astart, astep, aext))(as, [], as'0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as'0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ as. as ∈ asl → r(as, cs0), astep(asl.last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r(asl.last, cs1) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: asl, as'0, asl0

Proof step 17 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  aext !(aal) = [], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(as'0 ' + asl0, aal), move(IOAut(astart, astep, aext))(as, [], as'0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as'0, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), astep((as'0 ' + asl0).last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r((as'0 ' + asl0).last, cs1) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

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

Proof step 18 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  aext !(aal) = [], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(as'0 ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as'0, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∃ al, sl. frag*(IOAut(astart, astep, aext))(sl, al) ∧ as = sl[0] ∧ as'0 = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = [], astep((as'0 ' + asl0).last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r((as'0 ' + asl0).last, cs1) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), as, [], as'0

Proof step 19 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  aext !(aal) = [], aext !(aal0) = [], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), astep((asl.last ' + asl0).last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r((asl.last ' + asl0).last, cs1) ⊦ (cext(ca) = None ⊃ ∃ as0. move(IOAut(astart, astep, aext))(asl[0], [], as0) ∧ r(as0, cs1) ;∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = asl[0] ∧ (∀ as. as ∈ asl0 → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl0.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1)) )

Rule argument

Additional information

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

Proof step 21 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), astep((asl.last ' + asl0).last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r((asl.last ' + asl0).last, cs1) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(asl[0], [], as0) ∧ r(as0, cs1)

• Proof step 79:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) ≠ None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), astep((asl.last ' + asl0).last, aa, as') ∧ aext(aa) = cext(ca) ∧ r(as', cs1) ∨ cext(ca) = None ∧ r((asl.last ' + asl0).last, cs1) ⊦ ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = asl[0] ∧ (∀ as. as ∈ asl0 → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl0.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1))

Rule argument

Additional information

Proof step 22 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), astep((asl.last ' + asl0).last, aa, as') ∧ aext(aa) = None ∧ r(as', cs1) ∨ r((asl.last ' + asl0).last, cs1) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(asl[0], [], as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 23 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(asl[0], [], as0) ∧ r(as0, cs1)

• Proof step 57:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(asl[0], [], as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 24 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 25:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ move(IOAut(astart, astep, aext))(asl[0], [], as') ∧ r(as', cs1)

Rule argument

Additional information

Used terms: as'

Proof step 25 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ move(IOAut(astart, astep, aext))(asl[0], [], as'), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

Proof step 26 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ al, sl. ¬(frag*(IOAut(astart, astep, aext))(sl, al) ∧ asl[0] = sl[0] ∧ as' = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = []) ⊦

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), asl[0], [], as'

Proof step 27 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ asl[0] ≠ sl[0] ∨ as' ≠ sl.last ∨ aext !(al) ≠ [] ⊦

Rule argument

Additional information

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

Proof step 29 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 30:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + (asl0 + as'), aal0 + (aal + aa)) ∨ asl[0] ≠ (asl + (asl0 + as'))[0] ∨ as' ≠ (asl + (asl0 + as')).last ∨ aext !(aal0 + (aal + aa)) ≠ [] ⊦

Rule argument

Additional information

Used terms: aal0 + (aal + aa), asl + (asl0 + as')

Proof step 30 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0 + as' ', aal0 + aal + aa ') ∨ asl[0] ≠ (asl + asl0 + as' ')[0] ⊦

Rule argument

Additional information

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

Proof step 31 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 33:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, 0 < #(asl + asl0), astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0 + as' ', aal0 + aal + aa ') ∨ asl[0] ≠ (asl + asl0)[0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ #(x + y) = # x + # y; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.last = a; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: 0, asl + asl0, as' '

Proof step 32 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0 + as' ', aal0 + aal + aa ') ∨ asl[0] ≠ (asl + asl0)[0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s)

Proof step 34 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 36:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, 0 < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0 + as' ', aal0 + aal + aa ') ∨ asl[0] ≠ asl[0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # [] = 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ x ≠ [] → (a ' + x).last = x.last; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: 0, asl, asl0

Proof step 35 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0 + as' ', aal0 + aal + aa '), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 37 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ astep((asl + asl0).last, aa, as') ∨ ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: aal0 + aal, as', aext, asl + asl0, aa, astart, astep

Proof step 38 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ astep((asl + asl0).last, aa, as'), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

• Proof step 44:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

Proof step 40 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ¬ astep((asl + asl0).last, aa, as'), r(asl.last, cs0) ∧ cstep(cs0, ca, cs1) → r(asl.last, cs1) ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(asl.last, aa, as') ∧ r(as', cs1)) ∨ (∃ as', aa. astep(asl.last, aa, as') ∧ aext(aa) = None ∧ r(as', cs0) ∧ size01f(cs0, ca, cs1, as') < size01f(cs0, ca, cs1, asl.last)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

Rule argument

Additional information

Used terms: cs0, ca, cs1, asl.last

Proof step 41 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ astep((asl + asl0).last, aa, as'), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), r(asl.last, cs1) ∨ aext(aa0) = None ∧ astep(asl.last, aa0, as'0) ∧ r(as'0, cs1) ∨ astep(asl.last, aa1, as'1) ∧ aext(aa1) = None ∧ r(as'1, cs0) ∧ size01f(cs0, ca, cs1, as'1) < size01f(cs0, ca, cs1, asl.last) ⊦

Rule argument

Additional information

Proof step 42 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ y ≠ [] → (x + y).last = y.last; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # [] = 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ frag*(IOAut(start, step, ext))(s ', al) ↔ al = []; (s) ⊦ a '.last = a; (s) ⊦ x + [] = x; (s) Used terms: asl.last ', asl0

Proof step 43 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

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

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, # asl + # asl0 ≠ 0, asl ≠ [], # aal0 < #(asl + asl0), astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ¬ #(aal0 + aal) < # aal0, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), (aal0 + aal).take(# aal0)) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), (aal0 + aal).drop(# aal0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m + n < m; (s) ⊦ #(x + y) = # x + # y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl + n ≤ # al ↔ false); (as) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: aal0 + aal, aext, asl + asl0, astart, # aal0, astep

Proof step 45 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 46 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

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

Proof step 47 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

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

• Proof step 49:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ # asl < # aal0 + 1, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# al < # sl ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # aal0 + 1, asl, asl0

Proof step 48 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # 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 + 1 ↔ ¬ n < m; (s)

Proof step 50 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

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

• Proof step 52:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, # aal0 < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), # aal0 + 1 ≤ # asl, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# al < # sl ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # aal0 + 1, asl, asl0

Proof step 51 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 52 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, # aal0 < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

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 + 1 ≤ n ↔ m < n; (s)

Proof step 53 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ # x = n → x.take(n) = x

• Proof step 55:

  aext !(aal) = [], aext !(aal0) = [], # asl = # aal0 + 1, aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl, aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: asl, # aal0 + 1

Proof step 54 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  aext !(aal) = [], aext !(aal0) = [], # asl = # aal0 + 1, aext(aa) = None, cext(ca) = None, asl ≠ [], # aal0 < # asl, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

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 ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ m + n; (s) ⊦ m ≤ m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 56 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ # x = n → (x + x0).drop(n) = x0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: asl, as'0, asl1

Proof step 57 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 58:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ move(IOAut(astart, astep, aext))(asl[0], [], (asl.last ' + asl0).last) ∧ r((asl.last ' + asl0).last, cs1)

Rule argument

Additional information

Used terms: (asl.last ' + asl0).last

Proof step 58 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ¬ move(IOAut(astart, astep, aext))(asl[0], [], (asl.last ' + asl0).last), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

Proof step 59 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

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

• Proof step 61:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ al, sl. ¬(frag*(IOAut(astart, astep, aext))(sl, al) ∧ asl[0] = sl[0] ∧ (asl.last ' + asl0).last = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = []) ⊦

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), asl[0], [], (asl.last ' + asl0).last

Proof step 60 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ asl[0] ≠ sl[0] ∨ (asl.last ' + asl0).last ≠ sl.last ∨ aext !(al) ≠ [] ⊦

Rule argument

Additional information

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

Proof step 62 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 63:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal) ∨ asl[0] ≠ (asl + asl0)[0] ∨ (asl.last ' + asl0).last ≠ (asl + asl0).last ∨ aext !(aal0 + aal) ≠ [] ⊦

Rule argument

Additional information

Used terms: aal0 + aal, asl + asl0

Proof step 63 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal) ∨ asl[0] ≠ (asl + asl0)[0] ∨ (asl.last ' + asl0).last ≠ (asl + asl0).last ⊦

Rule argument

Additional information

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

Proof step 64 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 65:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

• Proof step 75:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, asl[0] ≠ (asl + asl0)[0], cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

• Proof step 77:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, (asl.last ' + asl0).last ≠ (asl + asl0).last, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

Rule argument

Additional information

Proof step 65 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

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

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, # aal0 < #(asl + asl0), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ¬ #(aal0 + aal) < # aal0, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), (aal0 + aal).take(# aal0)) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), (aal0 + aal).drop(# aal0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m + n < m; (s) ⊦ #(x + y) = # x + # y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl + n ≤ # al ↔ false); (as) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: aal0 + aal, aext, asl + asl0, astart, # aal0, astep

Proof step 66 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  aext !(aal0) = [], aext !(aal) = [], cext(ca) = None, # aal0 < # asl + # asl0, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

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

Proof step 68 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

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

• Proof step 70:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, # aal0 < # asl + # asl0, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), # aal0 + 1 ≤ # asl, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# al < # sl ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # aal0 + 1, asl, asl0

Proof step 69 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  aext !(aal) = [], aext !(aal0) = [], cext(ca) = None, asl ≠ [], # aal0 < # asl, # aal0 < # asl + # asl0, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r((asl.last ' + asl0).last, cs1), r(asl.last, cs0), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # 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 + 1 ≤ n ↔ m < n; (s)

Proof step 71 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ # x = n → x.take(n) = x

• Proof step 73:

  aext !(aal0) = [], aext !(aal) = [], # asl = # aal0 + 1, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, # aal0 < # asl, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl, aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: asl, # aal0 + 1

Proof step 72 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  aext !(aal0) = [], aext !(aal) = [], # asl = # aal0 + 1, cext(ca) = None, asl ≠ [], # aal0 < # asl + # asl0, # aal0 < # asl, cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r((asl.last ' + asl0).last, cs1), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

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 ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ m; (s) ⊦ m ≤ m + n; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 74 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ 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 ⊦ # x = n → (x + x0).drop(n) = x0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: asl, as1, asl1

Proof step 75 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ n < # x → (x + y)[n] = x[n]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ # [] = 0; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: 0, asl, asl0

Proof step 76 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ y ≠ [] → (x + y).last = y.last; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.last = a; (s) ⊦ x + [] = x; (s) Used terms: asl.last ', asl0

Proof step 78 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 79 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = asl[0] ∧ (∀ as. as ∈ asl0 → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep(asl0.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as1, [], as0) ∧ r(as0, cs1))

Rule argument

Additional information

Proof step 80 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 81:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal) ∧ aext !(aal0 + aal) = [] ∧ (asl + asl0).head = asl[0] ∧ (∀ as. as ∈ asl + asl0 → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep((asl + asl0).last, aa, as') ∧ cext(ca) = aext(aa) ∧ (∃ as0. move(IOAut(astart, astep, aext))(as', [], as0) ∧ r(as0, cs1))

Rule argument

Additional information

Used terms: asl + asl0, aal0 + aal, aa, as'

Proof step 81 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal) ∧ (asl + asl0).head = asl[0] ∧ (as ∈ asl ∨ as ∈ asl0 → (∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0))) ∧ astep((asl + asl0).last, aa, as') ∧ (∃ as0. move(IOAut(astart, astep, aext))(as', [], as0) ∧ r(as0, cs1))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ ext !(al + al0) = ext !(al) + ext !(al0); (s)

Proof step 82 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 83:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl + asl0, aal0 + aal), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

• Proof step 93:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), (asl + asl0).head ≠ asl[0], cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

• Proof step 95:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), as ∈ asl ∨ as ∈ asl0 ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0)

• Proof step 114:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ¬ astep((asl + asl0).last, aa, as'), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

• Proof step 116:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as', [], as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 83 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

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

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, # aal0 < #(asl + asl0), astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ #(aal0 + aal) < # aal0, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), (aal0 + aal).take(# aal0)) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), (aal0 + aal).drop(# aal0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m + n < m; (s) ⊦ #(x + y) = # x + # y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl + n ≤ # al ↔ false); (as) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: aal0 + aal, aext, asl + asl0, astart, # aal0, astep

Proof step 84 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 85 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

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

Proof step 86 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

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

• Proof step 88:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), # aal0 + 1 ≤ # asl, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# al < # sl ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: # aal0 + 1, asl, asl0

Proof step 87 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, # aal0 < # asl, # aal0 < # asl + # asl0, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl.take(# aal0 + 1), aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # 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 + 1 ≤ n ↔ m < n; (s)

Proof step 89 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

  ⊦ # x = n → x.take(n) = x

• Proof step 91:

  aext !(aal) = [], aext !(aal0) = [], # asl = # aal0 + 1, aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, # aal0 < # asl + # asl0, # aal0 < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl, aal0) ∨ ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: asl, # aal0 + 1

Proof step 90 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 91 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  aext !(aal) = [], aext !(aal0) = [], # asl = # aal0 + 1, aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, # aal0 < # asl + # asl0, # aal0 < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ frag*(IOAut(astart, astep, aext))((asl + asl0).drop(# aal0), aal), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

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 ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ m; (s) ⊦ m ≤ m + n; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 92 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ 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 ⊦ # x = n → (x + x0).drop(n) = x0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: asl, as'0, asl1

Proof step 93 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

  ⊦ x ≠ [] → (x + y).head = x.head

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: asl, asl0

Proof step 94 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 95 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 96:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), as ∈ asl, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0)

• Proof step 110:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), as ∈ asl0, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0)

Rule argument

Additional information

Proof step 96 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 97:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), as ∈ asl, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ move(IOAut(astart, astep, aext))(as, [], asl.last) ∧ r(asl.last, cs0)

Rule argument

Additional information

Used terms: asl.last

Proof step 97 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), as ∈ asl, ¬ move(IOAut(astart, astep, aext))(as, [], asl.last), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦

Rule argument

Additional information

Proof step 98 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 99:

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

• Proof step 100:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), as ∈ asl, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ al, sl. ¬(frag*(IOAut(astart, astep, aext))(sl, al) ∧ as = sl[0] ∧ asl.last = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = []) ⊦

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), as, [], asl.last

Proof step 99 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 100 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), as ∈ asl, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ as ≠ sl[0] ∨ asl.last ≠ sl.last ∨ aext !(al) ≠ [] ⊦

Rule argument

Additional information

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

Proof step 101 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

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

• Proof step 103:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ as ≠ sl[0] ∨ asl.last ≠ sl.last ∨ aext !(al) ≠ [], ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∃ n. n < # asl ∧ asl[n] = as ⊦

Rule argument

Additional information

Used terms: as, asl

Proof step 102 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 103 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, n < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ asl[n] ≠ sl[0] ∨ asl.last ≠ sl.last ∨ aext !(al) ≠ [], ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

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

Proof step 104 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 105:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, n < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl.drop(n), aal0.drop(n)) ∨ asl[n] ≠ asl.drop(n)[0] ∨ asl.last ≠ (asl.drop(n)).last ∨ aext !(aal0.drop(n)) ≠ [] ⊦

Rule argument

Additional information

Used terms: aal0.drop(n), asl.drop(n)

Proof step 105 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, n < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ¬ frag*(IOAut(astart, astep, aext))(asl.drop(n), aal0.drop(n)) ∨ aext !(aal0.drop(n)) ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x.drop(n)).last = x.last; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 106 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

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

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), asl ≠ [], cext(ca) ≠ None, n < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.take(n + 1), aal0.take(n)), frag*(IOAut(astart, astep, aext))(asl.drop(n), aal0.drop(n)), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), ¬ # aal0 < n, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ¬ frag*(IOAut(astart, astep, aext))(asl.drop(n), aal0.drop(n)) ∨ aext !(aal0.drop(n)) ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# al + 1 < # sl ↔ false); (as) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: aal0, aext, asl, astart, n, astep

Proof step 107 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 108 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), aext !(aal0.drop(n)) ≠ [], asl ≠ [], cext(ca) ≠ None, n < # asl, astep((asl.last ' + asl0).last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl.drop(n), aal0.drop(n)), frag*(IOAut(astart, astep, aext))(asl.take(n + 1), aal0.take(n)), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), n ≤ # aal0, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

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

Proof step 109 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n); (elim) Used terms: aal0, n, aal1, aal2

Proof step 110 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep(asl0.last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), as ∈ asl0, ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs0)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x → (b ' + x).last = x.last; (s)

Proof step 111 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 112:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep(asl0.last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl, aal0), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(asl.last, cs0), r(as', cs1), as ∈ asl0, ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as0. as0 ∈ asl0 → r(as0, cs0) ⊦ move(IOAut(astart, astep, aext))(as, [], as) ∧ r(as, cs0)

Rule argument

Additional information

Used terms: as

Proof step 112 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = cext(ca), cext(ca) ≠ None, astep(asl0.last, aa, as'), cstep(cs0, ca, cs1), frag*(IOAut(astart, astep, aext))(asl.last ' + asl0, aal), frag*(IOAut(astart, astep, aext))(asl, aal0), nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), r(as', cs1), r(asl.last, cs0), as ∈ asl0, ¬ r(as, cs0), ∀ as0. as0 ∈ asl0 → r(as0, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ move(IOAut(start, step, ext))(s, [], s); (s)

Proof step 113 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: as

Proof step 114 from proof normedfw-branchingfw-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 115:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (a ' + x).last = x.last; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ frag*(IOAut(start, step, ext))(s ', al) ↔ al = []; (s) ⊦ a '.last = a; (s) ⊦ x + [] = x; (s) Used terms: asl, asl0

Proof step 115 from proof normedfw-branchingfw-aux (previous step) (back to tree)

A spec-lemma

Proof step 116 from proof normedfw-branchingfw-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ move(IOAut(start, step, ext))(s, [], s); (s) Used terms: as'