Proof step 1 from proof branchingfw-normedfw-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:

  ∀ 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) ) ⊦ nfwsim (IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, λ cs, ca, cs', as. min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')))

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 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 5:

  ∀ 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) ), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ (∀ 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) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))))

Rule argument

Additional information

Used terms: cstep, cext, aext, r, astart, cstart, astep, λ cs, ca, cs', as. min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  cstep(cs, ca, cs'), r(as, cs), ∀ 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) ) ⊦ ∃ 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) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), r(as, cs') ∧ cext(ca) = None

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 7:

  cstep(cs, ca, cs'), r(as, cs), r(as, cs) ∧ cstep(cs, ca, cs') → (cext(ca) = None ⊃ r(as, cs') ;∃ 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, cs') ), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs'), r(as, cs') ∧ cext(ca) = None

Rule argument

Additional information

Used terms: cs, ca, cs', as

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  cstep(cs, ca, cs'), r(as, cs), (cext(ca) = None ⊃ r(as, cs') ; 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, cs') ), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ 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) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), r(as, cs') ∧ cext(ca) = None

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  aext !(aal) = [], asl.head = as, cext(ca) = aext(aa), cext(ca) ≠ None, astep(asl.last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(asl, aal), r(as, cs), r(as1, cs'), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl → r(as, cs) ⊦ ∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs'), r(as, cs') ∧ cext(ca) = None

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep(asl.last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(asl, aal), r(as1, cs'), r(asl.head, cs), ∀ as. as ∈ asl → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as', aa. aext(aa) = cext(ca) ∧ astep(asl.head, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(asl.head, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = asl.head ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  aext !(aal) = [], asl = as0 + asl1, cext(ca) = aext(aa), aext(aa) ≠ None, asl ≠ [], astep(asl.last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(asl, aal), r(as0, cs), r(as1, cs'), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl → r(as, cs) ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs')

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, as0, asl1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs) ⊦ ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs'))

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 12 from proof branchingfw-normedfw-aux (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (∃ n. pnat(n)) → pnat(min(pnat))

• Proof step 14:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), (∃ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')) → (∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')) = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used terms: λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as1, cs'), r(as0, cs), (∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')) → frag*(IOAut(astart, astep, aext))(asl0, aal0) ∧ aext !(aal0) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ aext(aa) = aext(aa0) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = asl0.head ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ∧ astep(asl0.last, aa0, as) ∧ r(as, cs'), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs) ⊦ ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')

• Proof step 19:

  aext !(aal) = [], aext !(aal0) = [], asl0.head = as0, aext(aa) = aext(aa0), cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep(asl0.last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(asl0, aal0), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl0 → r(as, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = asl0.head ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 17:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs) ⊦ ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal) ∧ aext !(aal) = [] ∧ (as0 ' + asl1).head = as0 ∧ (∀ as. as ∈ as0 ' + asl1 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ astep((as0 ' + asl1).last, aa, as1) ∧ r(as1, cs')

Rule argument

Additional information

Used terms: as0 ' + asl1, aal, aa, as1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  aext !(aal) = [], cext(ca) = aext(aa), aext(aa) ≠ None, astep(asl1.last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), as ∈ asl1, ¬ r(as, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl0, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = [] ∧ asl0.head = as0 ∧ (∀ as. as ∈ asl0 → r(as, cs)) ∧ cext(ca) = aext(aa) ∧ n = # aal ∧ astep(asl0.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = cext(ca) ∧ astep(as0, aa, as') ∧ r(as', cs')

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) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ (a ' + x).head = a; (s)

Proof step 18 from proof branchingfw-normedfw-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 19 from proof branchingfw-normedfw-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(asl0.last, aa0, as), astep((asl0.head ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(asl0, aal0), frag*(IOAut(astart, astep, aext))(asl0.head ' + asl1, aal), r(as, cs'), r(as1, cs'), r(asl0.head, cs), ∀ as. as ∈ asl0 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = asl0.head ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(asl0.head, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(asl0.head, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = asl0.head ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = aext(aa0), asl0 = as0 + asl2, cext(ca) = aext(aa0), aext(aa0) ≠ None, asl0 ≠ [], astep((as0 ' + asl1).last, aa, as1), astep(asl0.last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(asl0, aal0), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl0 → r(as, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

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: asl0, as0, asl2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  aext !(aal0) = [], aext !(aal) = [], aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as0 ' + asl2).last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl2, aal0), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as, cs'), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl2 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

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 22 from proof branchingfw-normedfw-aux (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 23:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = aext(aa0), asl2 = [], cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl2).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as0 ' + asl2, aal0), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 ∈ asl2 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

• Proof step 25:

  aext !(aal) = [], aext !(aal0) = [], aext(aa) = aext(aa0), asl2 = as3 + asl0, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl2).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as0 ' + asl2, aal0), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 ∈ asl2 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  aext !(aal) = [], aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = 0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ ext !([]) = []; (s) ⊦ ¬ a ∈ []; (s) ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ frag*(IOAut(start, step, ext))(s ', al) ↔ al = []; (s)

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: as, aa0

Proof step 25 from proof branchingfw-normedfw-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) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + as3 ' + asl0, aal0), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as, cs'), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

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) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 27:

  aext !(aal) = [], aext !(aal0) = [], aal0 = aa1 + aal1, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as0 ' + as3 ' + asl0, aal0), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal0 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as0 ' + as3 ' + asl0, aa1 ' + aal1), r(as, cs'), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, (as3 ' + asl0).head), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: aal1, as0, aext, as3 ' + asl0, aa1, astart, astep

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ as', aa. astep(as0, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as' ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), astep(as0, aa1, as3) ∧ aext(aa1) = None ∧ r(as3, cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

Used terms: as3, aa1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 = as3 ∨ as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), r(as3, cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 34:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as0, cs), r(as1, cs'), r(as, cs'), as3 = as3 ∨ as3 ∈ asl0 → r(as3, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), r(as3, cs) ∧ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'))

Rule argument

Additional information

Used terms: as3

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), r(as3, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 36:

  ⊦ pnat(n) → min(pnat) ≤ n

• Proof step 37:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as3, cs), r(as0, cs), r(as1, cs'), r(as, cs'), (∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ # aal1 = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) → min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ # aal1, ∀ as2. as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used terms: λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs'), # aal1

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

A spec-lemma

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

User applied rule case distinction

And obtained the following new goals

• Proof step 38:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), r(as3, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ # aal1 = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')

• Proof step 41:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), r(as3, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ # aal1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 39:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as3, cs), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs'), frag*(IOAut(astart, astep, aext))(as3 + asl0, aal1) ∧ aext !(aal1) = [] ∧ (as3 + asl0).head = as3 ∧ (∀ as. as ∈ as3 + asl0 → r(as, cs)) ∧ aext(aa0) = aext(aa0) ∧ # aal1 = # aal1 ∧ astep((as3 + asl0).last, aa0, as) ∧ r(as, cs')

Rule argument

Additional information

Used terms: as3 + asl0, aal1, aa0, as

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as0 ' + asl1).last, aa, as1), astep(asl0.last, aa0, as), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), r(as3, cs), as2 ∈ asl0, ¬ r(as2, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) = # aal1 + 1, min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as0 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

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) ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ (a ' + x).head = a; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: as2

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

User applied rule subst equation

And obtained the following new goals

• Proof step 42:

  aext !(aal1) = [], aext !(aal) = [], aext(aa1) = None, aext(aa) = aext(aa0), cext(ca) = aext(aa0), aext(aa0) ≠ None, astep(as0, aa1, as3), astep((as3 ' + asl0).last, aa0, as), astep((as0 ' + asl1).last, aa, as1), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), r(as3, cs), r(as0, cs), r(as1, cs'), r(as, cs'), ∀ as2. as2 ∈ asl0 → r(as2, cs), ∀ as. as ∈ asl1 → r(as, cs), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ # aal1, # aal1 + 1 ≤ min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ m + 1 ≤ n ↔ m < n

• Proof step 44:

  aext !(aal) = [], aext !(aal1) = [], aext(aa) = aext(aa0), aext(aa1) = None, cext(ca) = aext(aa0), aext(aa0) ≠ None, astep((as0 ' + asl1).last, aa, as1), astep((as3 ' + asl0).last, aa0, as), astep(as0, aa1, as3), cstep(cs, ca, cs'), frag*(IOAut(astart, astep, aext))(as0 ' + asl1, aal), frag*(IOAut(astart, astep, aext))(as3 ' + asl0, aal1), r(as, cs'), r(as1, cs'), r(as0, cs), r(as3, cs), # aal1 < min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ as. as ∈ asl1 → r(as, cs), ∀ as2. as2 ∈ asl0 → r(as2, cs), min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')) ≤ # aal1 ⊦ ∃ as', aa. aext(aa) = aext(aa0) ∧ astep(as0, aa, as') ∧ r(as', cs')

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), # aal1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ m ≤ n ↔ ¬ n < m

Rule argument

Additional information

Used terms: min (λ n. ∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as3 ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ aext(aa0) = aext(aa) ∧ n = # aal ∧ astep(asl.last, aa, as1) ∧ r(as1, cs')), # aal1

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

A spec-lemma