Proof step 1 from proof weakbwsim-implies-bwsiminv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ≤wB(cioaut, aioaut), ¬ ≤BI(cioaut, aioaut) ⊦

Rule argument

Additional information

Proof step 2 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cINV, cstep, cext), ≤wB(cioaut, aioaut), ¬ ≤BI(cioaut, aioaut) ⊦

Rule argument

Additional information

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

Proof step 3 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ≤wB(IOAut(cINV, cstep, cext), aioaut), ¬ ≤BI(IOAut(cINV, cstep, cext), aioaut) ⊦

Rule argument

Additional information

Proof step 4 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(aINV, astep, aext), ≤wB(IOAut(cINV, cstep, cext), aioaut), ¬ ≤BI(IOAut(cINV, cstep, cext), aioaut) ⊦

Rule argument

Additional information

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

Proof step 5 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ≤wB(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)), ¬ ≤BI(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)) ⊦

Rule argument

Additional information

Proof step 6 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ≤wB(cioaut, aioaut) ↔ (∃ t, aINV. weakbwsim(cioaut, aioaut, t, aINV))

• Proof step 8:

  ¬ ≤BI(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)), ∃ t, aINV0. weakbwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, aINV0) ⊦

Rule argument

Additional information

Used terms: IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)

Proof step 7 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Lemma weakbackwardsim-def

Proof step 8 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  weakbwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, aINV0), ¬ ≤BI(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)) ⊦

Rule argument

Additional information

Proof step 9 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ≤BI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. bwsim(cioaut, aioaut, t, cINV, aINV))

• Proof step 11:

  weakbwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, aINV0), ∀ t, aINV0, cINV0. ¬ bwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, cINV0, aINV0) ⊦

Rule argument

Additional information

Used terms: IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext)

Proof step 10 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Lemma backwardsiminv-def

Proof step 11 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ⊦ bwsim (IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, λ cs. ∃ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ csl.last = cs, λ as. aINV(as) ∧ (∃ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) ∧ asl.last = as))

• Proof step 13:

  weakbwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, aINV0), ∀ t, aINV0, cINV0. ¬ bwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, cINV0, aINV0), bwsim (IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, λ cs. ∃ csl, cal. exec*(IOAut(cINV, cstep, cext))(csl, cal) ∧ csl.last = cs, λ as. aINV0(as) ∧ (∃ asl, aal. exec*(IOAut(aINV, astep, aext))(asl, aal) ∧ asl.last = as)) ⊦

Rule argument

Additional information

Used terms: astep, aINV, t, aext, cINV, cstep, aINV0, cext

Proof step 12 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Lemma weakbwsim-implies-bwsiminv-aux

Proof step 13 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  weakbwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, aINV0), ∀ t, aINV0, cINV0. ¬ bwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, cINV0, aINV0), bwsim (IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, λ cs. ∃ csl, cal. frag*(IOAut(cINV, cstep, cext))(csl, cal) ∧ cINV(csl[0]) ∧ csl.last = cs, λ as. aINV0(as) ∧ (∃ asl, aal. frag*(IOAut(aINV, astep, aext))(asl, aal) ∧ aINV(asl[0]) ∧ asl.last = as)) ⊦

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 14 from proof weakbwsim-implies-bwsiminv (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, λ as. aINV0(as) ∧ (∃ asl, aal. frag*(IOAut(aINV, astep, aext))(asl, aal) ∧ aINV(asl[0]) ∧ asl.last = as), λ cs. ∃ csl, cal. frag*(IOAut(cINV, cstep, cext))(csl, cal) ∧ cINV(csl[0]) ∧ csl.last = cs