Proof step 1 from proof leqstar-alt-def (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  IOAut?(aioaut) ⊦ (∀ el. trace*(cioaut)(el) → trace*(aioaut)(el)) ↔ (∀ csl, cal. frag*(cioaut)(csl, cal) ∧ cioaut.start(csl[0]) → (∃ asl, aal. frag*(aioaut)(asl, aal) ∧ aioaut.start(asl[0]) ∧ aioaut.ext !(aal) = cioaut.ext !(cal)))

Rule argument

Additional information

Used simplifier rules: leqstar-def: ⊦ C_≤*T_A(cioaut, aioaut) ↔ (∀ el. trace*(cioaut)(el) → trace*(aioaut)(el)); ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 2 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cstart, cstep, cext), IOAut?(aioaut) ⊦ (∀ el. trace*(cioaut)(el) → trace*(aioaut)(el)) ↔ (∀ csl, cal. frag*(cioaut)(csl, cal) ∧ cioaut.start(csl[0]) → (∃ asl, aal. frag*(aioaut)(asl, aal) ∧ aioaut.start(asl[0]) ∧ aioaut.ext !(aal) = cioaut.ext !(cal)))

Rule argument

Additional information

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

Proof step 3 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  IOAut?(aioaut) ⊦ (∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(aioaut)(el)) ↔ (∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(aioaut)(asl, aal) ∧ aioaut.start(asl[0]) ∧ aioaut.ext !(aal) = cext !(cal)))

Rule argument

Additional information

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

Proof step 4 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(astart, astep, aext), IOAut?(aioaut) ⊦ (∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(aioaut)(el)) ↔ (∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(aioaut)(asl, aal) ∧ aioaut.start(asl[0]) ∧ aioaut.ext !(aal) = cext !(cal)))

Rule argument

Additional information

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

Proof step 5 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  IOAut?(IOAut(astart, astep, aext)) ⊦ (∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(IOAut(astart, astep, aext))(el)) ↔ (∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)))

Rule argument

Additional information

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

Proof step 6 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  IOAut?(IOAut(astart, astep, aext)), ∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(IOAut(astart, astep, aext))(el) ⊦ ∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal))

• Proof step 18:

  IOAut?(IOAut(astart, astep, aext)), ∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)) ⊦ ∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(IOAut(astart, astep, aext))(el)

Rule argument

Additional information

Proof step 7 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ el. trace*(IOAut(cstart, cstep, cext))(el) → trace*(IOAut(astart, astep, aext))(el) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Proof step 8 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), trace*(IOAut(cstart, cstep, cext))(cext !(cal)) → trace*(IOAut(astart, astep, aext))(cext !(cal)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Used terms: cext !(cal)

Proof step 9 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ¬ trace*(IOAut(cstart, cstep, cext))(cext !(cal)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

• Proof step 14:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), trace*(IOAut(astart, astep, aext))(cext !(cal)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Proof step 10 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ sl, al. ¬(cext !(cal) = cext !(al) ∧ exec*(IOAut(cstart, cstep, cext))(sl, al)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Used terms: cstart, cstep, cext, cext !(cal)

Proof step 11 from proof leqstar-alt-def (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ sl, al. cext !(cal) ≠ cext !(al) ∨ ¬ frag*(IOAut(cstart, cstep, cext))(sl, al) ∨ ¬ cstart(sl[0]) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

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

Proof step 13 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: csl, cal

Proof step 14 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∃ sl, al. cext !(cal) = aext !(al) ∧ exec*(IOAut(astart, astep, aext))(sl, al) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Used terms: astart, astep, aext, cext !(cal)

Proof step 15 from proof leqstar-alt-def (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  cext !(cal) = aext !(aal), IOAut?(IOAut(astart, astep, aext)), astart(asl[0]), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), frag*(IOAut(astart, astep, aext))(asl, aal) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

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

Proof step 17 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: asl, aal

Proof step 18 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  IOAut?(IOAut(astart, astep, aext)), trace*(IOAut(cstart, cstep, cext))(el), ¬ trace*(IOAut(astart, astep, aext))(el), ∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)) ⊦

Rule argument

Additional information

Proof step 19 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  IOAut?(IOAut(astart, astep, aext)), ¬ trace*(IOAut(astart, astep, aext))(el), ∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)), ∃ sl, al. el = cext !(al) ∧ exec*(IOAut(cstart, cstep, cext))(sl, al) ⊦

Rule argument

Additional information

Used terms: cstart, cstep, cext, el

Proof step 20 from proof leqstar-alt-def (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)), ∀ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)) ⊦

Rule argument

Additional information

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

Proof step 22 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  IOAut?(IOAut(astart, astep, aext)), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)), frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) → (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)) ⊦

Rule argument

Additional information

Used terms: csl, cal

Proof step 23 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  aext !(aal) = cext !(cal), IOAut?(IOAut(astart, astep, aext)), astart(asl[0]), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), frag*(IOAut(astart, astep, aext))(asl, aal), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)) ⊦

Rule argument

Additional information

Proof step 24 from proof leqstar-alt-def (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  aext !(aal) = cext !(cal), IOAut?(IOAut(astart, astep, aext)), astart(asl[0]), cstart(csl[0]), frag*(IOAut(astart, astep, aext))(asl, aal), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ sl, al. ¬(cext !(cal) = aext !(al) ∧ exec*(IOAut(astart, astep, aext))(sl, al)) ⊦

Rule argument

Additional information

Used terms: astart, astep, aext, cext !(cal)

Proof step 25 from proof leqstar-alt-def (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  aext !(aal) = cext !(cal), IOAut?(IOAut(astart, astep, aext)), astart(asl[0]), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), frag*(IOAut(astart, astep, aext))(asl, aal), ∀ sl, al. cext !(cal) ≠ aext !(al) ∨ ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ ¬ astart(sl[0]) ⊦

Rule argument

Additional information

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

Proof step 27 from proof leqstar-alt-def (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: asl, aal