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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ≤bF(cioaut, aioaut), ¬ ≤nF(cioaut, aioaut) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cstart, cstep, cext), ≤bF(cioaut, aioaut), ¬ ≤nF(cioaut, aioaut) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ≤bF(IOAut(cstart, cstep, cext), aioaut), ¬ ≤nF(IOAut(cstart, cstep, cext), aioaut) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(astart, astep, aext), ≤bF(IOAut(cstart, cstep, cext), aioaut), ¬ ≤nF(IOAut(cstart, cstep, cext), aioaut) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ≤bF(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)), ¬ ≤nF(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ≤bF(cioaut, aioaut) ↔ (∃ r. bfwsim(cioaut, aioaut, r))

• Proof step 8:

  ¬ ≤nF(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)), ∃ r. bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ ≤nF(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦ 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')))

• Proof step 11:

  bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ ≤nF(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)), 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 10 from proof branchingfw-normedfw (previous step) (back to tree)

Lemma branchingfw-normedfw-aux

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ≤nF(cioaut, aioaut) ↔ (∃ r, size01f. nfwsim(cioaut, aioaut, r, size01f))

• Proof step 13:

  bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ∀ r, size01f. ¬ nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f), 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: IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)

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

A spec-lemma

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ frag(ioa)(⌜sl⌝ , ⌜al⌝ ) ↔ frag*(ioa)(sl, al); (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) Used terms: 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'))