Proof step 1 from proof bwtrueinv-aux (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(bwsim(cioaut, aioaut, t) ↔ bwsim(cioaut, aioaut, t, λ cs. true, λ as. true)) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cINV, cstep, cext), ¬(bwsim(cioaut, aioaut, t) ↔ bwsim(cioaut, aioaut, t, λ cs. true, λ as. true)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬(bwsim(IOAut(cINV, cstep, cext), aioaut, t) ↔ bwsim(IOAut(cINV, cstep, cext), aioaut, t, λ cs. true, λ as. true)) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(aINV, astep, aext), ¬(bwsim(IOAut(cINV, cstep, cext), aioaut, t) ↔ bwsim(IOAut(cINV, cstep, cext), aioaut, t, λ cs. true, λ as. true)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬(bwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t) ↔ bwsim(IOAut(cINV, cstep, cext), IOAut(aINV, astep, aext), t, λ cs. true, λ as. true)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

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

Rule argument

Additional information

Used terms: astep, aINV, t, aext, cINV, cstep, λ as. true, cext, λ cs. true

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ∀ cs. ∃ as. t(cs, as), ∀ cs, as. cINV(cs) ∧ t(cs, as) → aINV(as), ∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)) ⊦ (∃ as. t(cs, as)) ∧ (cINV(cs0) ∧ t(cs0, as) → aINV(as)) ∧ (cstep(cs1, ca, cs2) ∧ t(cs2, as0) → (∃ as1. move(IOAut(aINV, astep, aext))(as1, cext !(ca '), as0) ∧ t(cs1, as1)))

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

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

• Proof step 15:

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

• Proof step 16:

  cstep(cs1, ca, cs2), t(cs2, as0), ∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)), ∀ cs, as. cINV(cs) ∧ t(cs, as) → aINV(as), ∀ cs. ∃ as. t(cs, as) ⊦ ∃ as1. move(IOAut(aINV, astep, aext))(as1, cext !(ca '), as0) ∧ t(cs1, as1)

Rule argument

Additional information

Proof step 12 from proof bwtrueinv-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used terms: cs

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: as

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: cs0, as

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

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 17:

  cstep(cs1, ca, cs2), t(cs2, as0), cstep(cs1, ca, cs2) ∧ t(cs2, as0) → (∃ as. move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0) ∧ t(cs1, as)), ∀ cs. ∃ as. t(cs, as), ∀ cs, as. cINV(cs) ∧ t(cs, as) → aINV(as), ∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)) ⊦ ∃ as1. move(IOAut(aINV, astep, aext))(as1, cext !(ca '), as0) ∧ t(cs1, as1)

Rule argument

Additional information

Used terms: cs1, ca, cs2, as0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  cstep(cs1, ca, cs2), move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0), t(cs2, as0), t(cs1, as), ∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(aINV, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)), ∀ cs, as. cINV(cs) ∧ t(cs, as) → aINV(as), ∀ cs. ∃ as. t(cs, as) ⊦ ∃ as1. move(IOAut(aINV, astep, aext))(as1, cext !(ca '), as0) ∧ t(cs1, as1)

Rule argument

Additional information

Proof step 18 from proof bwtrueinv-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: as