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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ⊦ bwsim (IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, λ cs. ∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs, λ as. aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(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 2 from proof weakbwsim-implies-bwsiminv-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV) ↔ (∀ cs. cstart(cs) → cINV(cs)) ∧ (∀ as. astart(as) → aINV(as)) ∧ (∀ cs, ca, cs0. cINV(cs) ∧ cstep(cs, ca, cs0) → cINV(cs0)) ∧ (∀ as, aa, as0. aINV(as) ∧ astep(as, aa, as0) → aINV(as0)) ∧ (∀ cs. cINV(cs) → (∃ as. t(cs, as) ∧ aINV(as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ cs, ca, cs0, as0. cINV(cs) ∧ cstep(cs, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)))

• Proof step 4:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ⊦ (∀ cs. cstart(cs) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs)) ∧ (∀ as. astart(as) → aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ (∀ cs, ca, cs0. (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs) ∧ cstep(cs, ca, cs0) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs0)) ∧ (∀ as, aa, as0. (aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ astep(as, aa, as0) → aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0)) ∧ (∀ cs. (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs) → (∃ as. t(cs, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as) → astart(as)) ∧ (∀ cs, ca, cs0, as0. (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs) ∧ cstep(cs, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0) → (∃ as. (aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)))

Rule argument

Additional information

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

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

Lemma proofobls-backwardsiminv

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ⊦ (cstart(cs) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs)) ∧ (astart(as) → aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs0 ∧ cstep(csl.last, ca, cs1) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs1)) ∧ ( aINV(asl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0 ∧ astep(asl.last, aa, as1) → aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl0, cal0) ∧ cstart(csl0[0]) ∧ csl0.last = cs2 → (∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as))) ∧ ( cstart(cs3) ∧ t(cs3, asl0.last) ∧ aINV(asl0.last) ∧ frag*(IOAut(astart, astep, aext))(asl0, aal0) ∧ astart(asl0[0]) ∧ asl0.last = as2 → astart(asl0.last)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl1, cal1) ∧ cstart(csl1[0]) ∧ csl1.last = cs4 ∧ cstep(csl1.last, ca0, cs5) ∧ t(cs5, asl1.last) ∧ aINV(asl1.last) ∧ frag*(IOAut(astart, astep, aext))(asl1, aal1) ∧ astart(asl1[0]) ∧ asl1.last = as3 → (∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)))

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ↔ (∀ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) → (∃ as. t(csl.last, as) ∧ aINV(as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) → aINV(asl.last)) ∧ (∀ csl, cal, ca, cs0, as0. exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstep(csl.last, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(csl.last, as)))

• Proof step 7:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ↔ (∀ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) → (∃ as. t(csl.last, as) ∧ aINV(as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) → aINV(asl.last)) ∧ (∀ csl, cal, ca, cs0, as0. exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstep(csl.last, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(csl.last, as))) ⊦ (cstart(cs) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs)) ∧ (astart(as) → aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs0 ∧ cstep(csl.last, ca, cs1) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs1)) ∧ ( aINV(asl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0 ∧ astep(asl.last, aa, as1) → aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl0, cal0) ∧ cstart(csl0[0]) ∧ csl0.last = cs2 → (∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as))) ∧ ( cstart(cs3) ∧ t(cs3, asl0.last) ∧ aINV(asl0.last) ∧ frag*(IOAut(astart, astep, aext))(asl0, aal0) ∧ astart(asl0[0]) ∧ asl0.last = as2 → astart(asl0.last)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl1, cal1) ∧ cstart(csl1[0]) ∧ csl1.last = cs4 ∧ cstep(csl1.last, ca0, cs5) ∧ t(cs5, asl1.last) ∧ aINV(asl1.last) ∧ frag*(IOAut(astart, astep, aext))(asl1, aal1) ∧ astart(asl1[0]) ∧ asl1.last = as3 → (∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)))

Rule argument

Additional information

Used terms: cstep, t, astart, cext, cstart, astep, aINV, aext

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

Lemma proofobls-weakbackwardsim

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ (cstart(cs) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs)) ∧ (astart(as) → aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs0 ∧ cstep(csl.last, ca, cs1) → (∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs1)) ∧ ( aINV(asl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0 ∧ astep(asl.last, aa, as1) → aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl0, cal0) ∧ cstart(csl0[0]) ∧ csl0.last = cs2 → (∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as))) ∧ ( cstart(cs3) ∧ t(cs3, asl0.last) ∧ aINV(asl0.last) ∧ frag*(IOAut(astart, astep, aext))(asl0, aal0) ∧ astart(asl0[0]) ∧ asl0.last = as2 → astart(asl0.last)) ∧ ( frag*(IOAut(cstart, cstep, cext))(csl1, cal1) ∧ cstart(csl1[0]) ∧ csl1.last = cs4 ∧ cstep(csl1.last, ca0, cs5) ∧ t(cs5, asl1.last) ∧ aINV(asl1.last) ∧ frag*(IOAut(astart, astep, aext))(asl1, aal1) ∧ astart(asl1[0]) ∧ asl1.last = as3 → (∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)))

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  cstart(cs), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs

• Proof step 10:

  astart(as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

• Proof step 13:

  csl.last = cs0, cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs1

• Proof step 21:

  asl.last = as0, aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

• Proof step 36:

  csl0.last = cs2, cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

• Proof step 59:

  asl0.last = as2, aINV(asl0.last), astart(asl0[0]), cstart(cs3), frag*(IOAut(astart, astep, aext))(asl0, aal0), t(cs3, asl0.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ astart(asl0.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦

• Proof step 61:

  csl1.last = cs4, asl1.last = as3, aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(s ', []); (s) ⊦ a '[0] = a; (s) ⊦ a '.last = a; (s) Used terms: cs ', []

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

  astart(as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), frag*(IOAut(astart, astep, aext))(as ', []) ∧ astart(as '[0]) → aINV(as '.last), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

Used terms: as ', []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  aINV(as), astart(as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as

Rule argument

Additional information

Used simplifier rules: ⊦ a '.last = a; (s) ⊦ a '[0] = a; (s) ⊦ frag*(IOAut(start, step, ext))(s ', []); (s)

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(s ', []); (s) ⊦ a '[0] = a; (s) ⊦ a '.last = a; (s) Used terms: as ', []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ csl, cal. frag*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstart(csl[0]) ∧ csl.last = cs1

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 15:

  cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ frag*(IOAut(cstart, cstep, cext))(csl + cs1, cal + ca) ∧ cstart((csl + cs1)[0]) ∧ (csl + cs1).last = cs1

Rule argument

Additional information

Used terms: csl + cs1, cal + ca

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ frag*(IOAut(cstart, cstep, cext))(csl + cs1 ', cal + ca ') ∧ cstart((csl + cs1 ')[0])

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ (cstep(csl.last, ca, cs1) ∧ frag*(IOAut(cstart, cstep, cext))(csl, cal)) ∧ cstart((csl + cs1 ')[0])

Rule argument

Additional information

Used terms: cal, cs1, cext, csl, ca, cstart, cstep

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  cstart(csl[0]), cstep(csl.last, ca, cs1), frag*(IOAut(cstart, cstep, cext))(csl, cal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ cstart((csl + cs1 ')[0]), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: 0, csl, cs1 '

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 23:

  aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), frag*(IOAut(astart, astep, aext))(asl + as1, aal + aa) ∧ astart((asl + as1)[0]) → aINV((asl + as1).last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

Used terms: asl + as1, aal + aa

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), frag*(IOAut(astart, astep, aext))(asl + as1 ', aal + aa ') ∧ astart((asl + as1 ')[0]) → aINV(as1), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), (astep(asl.last, aa, as1) ∧ frag*(IOAut(astart, astep, aext))(asl, aal)) ∧ astart((asl + as1 ')[0]) → aINV(as1), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

Used terms: aal, as1, aext, asl, aa, astart, astep

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), astart((asl + as1 ')[0]) → aINV(as1), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  0 < # asl, aINV(asl.last), astart(asl[0]), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), astart(asl[0]) → aINV(as1), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as1) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) Used terms: 0, asl, as1 '

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  asl ≠ [], aINV(asl.last), aINV(as1), astart(asl.head), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 31:

  asl = as0 + asl0, asl ≠ [], aINV(as1), aINV(asl.last), astart(as0), astep(asl.last, aa, as1), frag*(IOAut(astart, astep, aext))(asl, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: asl, as0, asl0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  aINV(as1), aINV((as0 ' + asl0).last), astart(as0), astep((as0 ' + asl0).last, aa, as1), frag*(IOAut(astart, astep, aext))(as0 ' + asl0, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as1

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 33:

  aINV((as0 ' + asl0).last), aINV(as1), astart(as0), astep((as0 ' + asl0).last, aa, as1), frag*(IOAut(astart, astep, aext))(as0 ' + asl0, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ frag*(IOAut(astart, astep, aext))(as0 ' + asl0 + as1 ', aal + aa ') ∧ astart((as0 ' + asl0 + as1 ')[0]) ∧ (as0 ' + asl0 + as1 ').last = as1

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  aINV(as1), aINV((as0 ' + asl0).last), astart(as0), astep((as0 ' + asl0).last, aa, as1), frag*(IOAut(astart, astep, aext))(as0 ' + asl0, aal), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ frag*(IOAut(astart, astep, aext))(as0 ' + asl0 + as1 ', aal + aa '), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

Used terms: aal, as1, aext, as0 ' + asl0, aa, astart, astep

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 38:

  cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), frag*(IOAut(cstart, cstep, cext))(csl0, cal0) ∧ cstart(csl0[0]) → (∃ as. t(csl0.last, as) ∧ aINV(as)), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

Used terms: csl0, cal0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 40:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), exec*(IOAut(cstart, cstep, cext))(csl0, cal0), csl0.last = cs, move(IOAut(cstart, cstep, cext))(cs, el, cs0), t(cs0, as0), aINV(as0) ⊦ ∃ as. move(IOAut(astart, astep, aext))(as, el, as0) ∧ t(cs, as) ∧ aINV(as)

• Proof step 41:

  aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as), exec*(IOAut(cstart, cstep, cext))(csl0.head ', []) ∧ csl0.head '.last = csl0.head ∧ move(IOAut(cstart, cstep, cext))(csl0.head, cext !(⌜cal0⌝ ).l, csl0.last)

• Proof step 48:

  aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∃ as1. move(IOAut(astart, astep, aext))(as1, cext !(⌜cal0⌝ ).l, as) ∧ t(csl0.head, as1) ∧ aINV(as1) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

Used terms: [], cstep, cext !(⌜cal0⌝ ).l, t, astart, cext, cstart, csl0.head ', as, astep, csl0.last, csl0.head, aINV, aext

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

Lemma weak-lemma_3-15

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as), cstart(csl0.head) ∧ move(IOAut(cstart, cstep, cext))(csl0.head, cext !(cal0), csl0.last)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ a '.last = a; (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ a '[0] = a; (s) ⊦ frag*(IOAut(start, step, ext))(s ', []); (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 43:

  csl0 = cs0 + csl, csl0 ≠ [], aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as), cstart(cs0) ∧ move(IOAut(cstart, cstep, cext))(cs0, cext !(cal0), csl0.last)

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: csl0, cs0, csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  aINV(as), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t((cs0 ' + csl).last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ move(IOAut(cstart, cstep, cext))(cs0, cext !(cal0), (cs0 ' + csl).last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as0. t((cs0 ' + csl).last, as0) ∧ aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0)

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

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

• Proof step 46:

  aINV(as), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t((cs0 ' + csl).last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ al, sl. ¬(frag*(IOAut(cstart, cstep, cext))(sl, al) ∧ cs0 = sl[0] ∧ (cs0 ' + csl).last = sl.last ∧ IOAut(cstart, cstep, cext).ext !(al) = cext !(cal0)) ⊦ ∃ as0. t((cs0 ' + csl).last, as0) ∧ aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0)

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), cs0, cext !(cal0), (cs0 ' + csl).last

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  aINV(as), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t((cs0 ' + csl).last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ al, sl. ¬ frag*(IOAut(cstart, cstep, cext))(sl, al) ∨ cs0 ≠ sl[0] ∨ (sl[0] ' + csl).last ≠ sl.last ∨ cext !(al) ≠ cext !(cal0) ⊦ ∃ as0. t((cs0 ' + csl).last, as0) ∧ aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0)

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: cal0, cs0 ' + csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  aINV(as1), aINV(as), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), move(IOAut(astart, astep, aext))(as1, cext !(cal0), as), t(csl0.head, as1), t(csl0.last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 50:

  csl0 = cs0 + csl, csl0 ≠ [], aINV(as), aINV(as1), cstart(csl0[0]), frag*(IOAut(cstart, cstep, cext))(csl0, cal0), move(IOAut(astart, astep, aext))(as1, cext !(cal0), as), t(csl0.last, as), t(cs0, as1), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ ∃ as. t(csl0.last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

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: csl0, cs0, csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  aINV(as1), aINV(as), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), move(IOAut(astart, astep, aext))(as1, cext !(cal0), as), t(cs0, as1), t((cs0 ' + csl).last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as0. t((cs0 ' + csl).last, as0) ∧ aINV(as0) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as0)

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 52:

  aINV(as), aINV(as1), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), move(IOAut(astart, astep, aext))(as1, cext !(cal0), as), t((cs0 ' + csl).last, as), t(cs0, as1), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ t((cs0 ' + csl).last, as) ∧ aINV(as) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as)

Rule argument

Additional information

Used terms: as

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  aINV(as1), aINV(as), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), move(IOAut(astart, astep, aext))(as1, cext !(cal0), as), t(cs0, as1), t((cs0 ' + csl).last, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

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

• Proof step 55:

  aINV(as), aINV(as1), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t((cs0 ' + csl).last, as), t(cs0, as1), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∃ al, sl. frag*(IOAut(astart, astep, aext))(sl, al) ∧ as1 = sl[0] ∧ as = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = cext !(cal0) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), as1, cext !(cal0), as

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  aext !(aal) = cext !(cal0), aINV(asl[0]), aINV(asl.last), cstart(cs0), frag*(IOAut(astart, astep, aext))(asl, aal), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t(cs0, asl[0]), t((cs0 ' + csl).last, asl.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ asl0, aal. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ astart(asl0[0]) ∧ asl0.last = asl.last

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 57:

  aext !(aal) = cext !(cal0), aINV(asl.last), aINV(asl[0]), cstart(cs0), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), frag*(IOAut(astart, astep, aext))(asl, aal), t((cs0 ' + csl).last, asl.last), t(cs0, asl[0]), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as) ⊦ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = asl.last

Rule argument

Additional information

Used terms: asl, aal

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  aext !(aal) = cext !(cal0), aINV(asl[0]), aINV(asl.last), cstart(cs0), frag*(IOAut(astart, astep, aext))(asl, aal), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal0), t(cs0, asl[0]), t((cs0 ' + csl).last, asl.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ astart(asl[0]), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: cs0, asl[0]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  aINV(asl0.last), astart(asl0[0]), cstart(cs3), frag*(IOAut(astart, astep, aext))(asl0, aal0), t(cs3, asl0.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ astart(asl0.last), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: cs3, asl0.last

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ csl2, cal2, ca1, cs6, as4. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) ∧ cstep(csl2.last, ca1, cs6) ∧ t(cs6, as4) ∧ aINV(as4) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca1) = None ⊃ [];cext(ca1).get '), as4) ∧ t(csl2.last, as5)) ⊦ ∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 63:

  aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), frag*(IOAut(cstart, cstep, cext))(csl1, cal1) ∧ cstart(csl1[0]) ∧ cstep(csl1.last, ca0, cs5) ∧ t(cs5, asl1.last) ∧ aINV(asl1.last) → (∃ as5. aINV(as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as5)), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)

Rule argument

Additional information

Used terms: csl1, cal1, ca0, cs5, asl1.last

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs5, asl1.last), t(csl1.last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ as4. aINV(as4) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as4) ∧ move(IOAut(astart, astep, aext))(as4, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as4)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 65:

  aINV(as5), aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(csl1.last, as5), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ aINV(as5) ∧ (∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5) ∧ move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last) ∧ t(csl1.last, as5)

Rule argument

Additional information

Used terms: as5

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs5, asl1.last), t(csl1.last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 67:

  weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), exec*(IOAut(cstart, cstep, cext))(csl0, cal0), csl0.last = cs, move(IOAut(cstart, cstep, cext))(cs, el, cs0), t(cs0, as0), aINV(as0) ⊦ ∃ as. move(IOAut(astart, astep, aext))(as, el, as0) ∧ t(cs, as) ∧ aINV(as)

• Proof step 68:

  aINV(as5), aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(csl1.last, as5), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5, exec*(IOAut(cstart, cstep, cext))(csl1.head ', []) ∧ csl1.head '.last = csl1.head ∧ move(IOAut(cstart, cstep, cext))(csl1.head, cext !(⌜cal1⌝ ).l, csl1.last)

• Proof step 75:

  aINV(as5), aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(csl1.last, as5), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∃ as. move(IOAut(astart, astep, aext))(as, cext !(⌜cal1⌝ ).l, as5) ∧ t(csl1.head, as) ∧ aINV(as) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

Used terms: [], cstep, cext !(⌜cal1⌝ ).l, t, astart, cext, cstart, csl1.head ', as5, astep, csl1.last, csl1.head, aINV, aext

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

Lemma weak-lemma_3-15

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs5, asl1.last), t(csl1.last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5, cstart(csl1.head) ∧ move(IOAut(cstart, cstep, cext))(csl1.head, cext !(cal1), csl1.last)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ a '.last = a; (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ a '[0] = a; (s) ⊦ frag*(IOAut(start, step, ext))(s ', []); (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 70:

  csl1 = cs0 + csl, csl1 ≠ [], aINV(as5), aINV(asl1.last), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(csl1.last, as5), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5, cstart(cs0) ∧ move(IOAut(cstart, cstep, cext))(cs0, cext !(cal1), csl1.last)

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: csl1, cs0, csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs5, asl1.last), t((cs0 ' + csl).last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ move(IOAut(cstart, cstep, cext))(cs0, cext !(cal1), (cs0 ' + csl).last), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  aINV(as5), aINV(asl1.last), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t((cs0 ' + csl).last, as5), t(cs5, asl1.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ al, sl. ¬(frag*(IOAut(cstart, cstep, cext))(sl, al) ∧ cs0 = sl[0] ∧ (cs0 ' + csl).last = sl.last ∧ IOAut(cstart, cstep, cext).ext !(al) = cext !(cal1)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), cs0, cext !(cal1), (cs0 ' + csl).last

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs5, asl1.last), t((cs0 ' + csl).last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ al, sl. ¬ frag*(IOAut(cstart, cstep, cext))(sl, al) ∨ cs0 ≠ sl[0] ∨ (sl[0] ' + csl).last ≠ sl.last ∨ cext !(al) ≠ cext !(cal1) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: cal1, cs0 ' + csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  aINV(as), aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), move(IOAut(astart, astep, aext))(as, cext !(cal1), as5), t(csl1.head, as), t(cs5, asl1.last), t(csl1.last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 77:

  csl1 = cs0 + csl, csl1 ≠ [], aINV(as5), aINV(asl1.last), aINV(as), astart(asl1[0]), cstart(csl1[0]), cstep(csl1.last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(csl1, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as, cext !(cal1), as5), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(csl1.last, as5), t(cs5, asl1.last), t(cs0, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

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: csl1, cs0, csl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  aINV(as), aINV(asl1.last), aINV(as5), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), move(IOAut(astart, astep, aext))(as, cext !(cal1), as5), t(cs0, as), t(cs5, asl1.last), t((cs0 ' + csl).last, as5), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

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

• Proof step 80:

  aINV(as5), aINV(asl1.last), aINV(as), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), move(IOAut(astart, astep, aext))(as5, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t((cs0 ' + csl).last, as5), t(cs5, asl1.last), t(cs0, as), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∃ al, sl. frag*(IOAut(astart, astep, aext))(sl, al) ∧ as = sl[0] ∧ as5 = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = cext !(cal1) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = as5

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), as, cext !(cal1), as5

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  aext !(aal) = cext !(cal1), aINV(asl[0]), aINV(asl1.last), aINV(asl.last), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl, aal), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), move(IOAut(astart, astep, aext))(asl.last, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs0, asl[0]), t(cs5, asl1.last), t((cs0 ' + csl).last, asl.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦ ∃ asl0, aal. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ astart(asl0[0]) ∧ asl0.last = asl.last

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 82:

  aext !(aal) = cext !(cal1), aINV(asl.last), aINV(asl1.last), aINV(asl[0]), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(astart, astep, aext))(asl, aal), move(IOAut(astart, astep, aext))(asl.last, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t((cs0 ' + csl).last, asl.last), t(cs5, asl1.last), t(cs0, asl[0]), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)) ⊦ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ asl.last = asl.last

Rule argument

Additional information

Used terms: asl, aal

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  aext !(aal) = cext !(cal1), aINV(asl[0]), aINV(asl1.last), aINV(asl.last), astart(asl1[0]), cstart(cs0), cstep((cs0 ' + csl).last, ca0, cs5), frag*(IOAut(astart, astep, aext))(asl, aal), frag*(IOAut(astart, astep, aext))(asl1, aal1), frag*(IOAut(cstart, cstep, cext))(cs0 ' + csl, cal1), move(IOAut(astart, astep, aext))(asl.last, (cext(ca0) = None ⊃ [];cext(ca0).get '), asl1.last), t(cs0, asl[0]), t(cs5, asl1.last), t((cs0 ' + csl).last, asl.last), weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), ¬ astart(asl[0]), ∀ csl2, cal2. frag*(IOAut(cstart, cstep, cext))(csl2, cal2) ∧ cstart(csl2[0]) → (∃ as. t(csl2.last, as) ∧ aINV(as)), ∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as), ∀ asl2, aal2. frag*(IOAut(astart, astep, aext))(asl2, aal2) ∧ astart(asl2[0]) → aINV(asl2.last) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: cs0, asl[0]