Proof step 1 from proof simpleforward-is-forward-aux (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  simplefwsim(cioaut, aioaut, r, aabs), ¬ fwsim(cioaut, aioaut, r) ⊦

Rule argument

Additional information

Proof step 2 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cstart, cstep, cext), simplefwsim(cioaut, aioaut, r, aabs), ¬ fwsim(cioaut, aioaut, r) ⊦

Rule argument

Additional information

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

Proof step 3 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  simplefwsim(IOAut(cstart, cstep, cext), aioaut, r, aabs), ¬ fwsim(IOAut(cstart, cstep, cext), aioaut, r) ⊦

Rule argument

Additional information

Proof step 4 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(astart, astep, aext), simplefwsim(IOAut(cstart, cstep, cext), aioaut, r, aabs), ¬ fwsim(IOAut(cstart, cstep, cext), aioaut, r) ⊦

Rule argument

Additional information

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

Proof step 5 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  simplefwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, aabs), ¬ fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦

Rule argument

Additional information

Proof step 6 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ simplefwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, aabs) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0))) ∧ (∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)))

• Proof step 8:

  ¬ fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)), ∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)) ⊦

Rule argument

Additional information

Used terms: cstep, cext, aext, r, astart, cstart, astep, aabs

Proof step 7 from proof simpleforward-is-forward-aux (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  ∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), (∃ cs. ¬(cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)))) ∨ (∃ cs, ca, cs0, as. ¬(r(as, cs) ∧ cstep(cs, ca, cs0) → (∃ as0. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ r(as0, cs0)))) ⊦

Rule argument

Additional information

Used terms: cstep, cext, aext, r, astart, cstart, astep

Proof step 9 from proof simpleforward-is-forward-aux (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)), ∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ¬(cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∨ ¬(r(as, cs0) ∧ cstep(cs0, ca, cs1) → (∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1))) ⊦

Rule argument

Additional information

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

Proof step 11 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  cstart(cs), ∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as. r(as, cs) ∧ astart(as)

• Proof step 13:

  cstep(cs0, ca, cs1), r(as, cs0), ∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 12 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: cs

Proof step 13 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  cstep(cs0, ca, cs1), r(as, cs0), (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Used terms: ca

Proof step 14 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

  cstep(cs0, ca, cs1), r(as, cs0), r(as, cs0) ∧ cstep(cs0, ca, cs1) → (aabs(ca) = None ⊃ r(as, cs1);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs1)), (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Used terms: cs0, ca, cs1, as

Proof step 15 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  cstep(cs0, ca, cs1), r(as, cs0), (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)), (aabs(ca) = None ⊃ r(as, cs1);astep(as, aabs(ca).get, as0) ∧ r(as0, cs1)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 16 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

  aabs(ca) = None, cext(ca) = None, cstep(cs0, ca, cs1), r(as, cs0), (aabs(ca) = None ⊃ r(as, cs1);astep(as, aabs(ca).get, as0) ∧ r(as0, cs1)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

• Proof step 19:

  cext(ca) = aext(aabs(ca).get), aabs(ca) ≠ None, cstep(cs0, ca, cs1), r(as, cs0), (aabs(ca) = None ⊃ r(as, cs1);astep(as, aabs(ca).get, as0) ∧ r(as0, cs1)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 17 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  aabs(ca) = None, cext(ca) = None, cstep(cs0, ca, cs1), r(as, cs0), r(as, cs1), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, [], as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 18 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ move(IOAut(start, step, ext))(s, [], s); (s) Used terms: as

Proof step 19 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  cext(ca) = aext(aabs(ca).get), aabs(ca) ≠ None, astep(as, aabs(ca).get, as0), cstep(cs0, ca, cs1), r(as, cs0), r(as0, cs1), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Proof step 20 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  aabs(ca) = Some(aa), cext(ca) = aext(aa), aabs(ca) ≠ None, astep(as, aa, as0), cstep(cs0, ca, cs1), r(as0, cs1), r(as, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: aabs(ca), aa

Proof step 21 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  aabs(ca) = Some(aa), cext(ca) = aext(aa), astep(as, aa, as0), cstep(cs0, ca, cs1), r(as0, cs1), r(as, cs0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ as0. move(IOAut(astart, astep, aext))(as, (aext(aa) = None ⊃ [];aext(aa).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s)

Proof step 22 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 23:

  aabs(ca) = Some(aa), cext(ca) = aext(aa), astep(as, aa, as0), cstep(cs0, ca, cs1), r(as, cs0), r(as0, cs1), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ move(IOAut(astart, astep, aext))(as, (aext(aa) = None ⊃ [];aext(aa).get '), as0) ∧ r(as0, cs1)

Rule argument

Additional information

Used terms: as0

Proof step 23 from proof simpleforward-is-forward-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  aabs(ca) = Some(aa), cext(ca) = aext(aa), astep(as, aa, as0), cstep(cs0, ca, cs1), r(as0, cs1), r(as, cs0), ¬ move(IOAut(astart, astep, aext))(as, (aext(aa) = None ⊃ [];aext(aa).get '), as0), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦

Rule argument

Additional information

Proof step 24 from proof simpleforward-is-forward-aux (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

  ⊦ step(s, a, s0) → move(IOAut(start, step, ext))(s, ext !(a '), s0)

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) Used terms: as, aext, aa, astart, as0, astep

Proof step 25 from proof simpleforward-is-forward-aux (previous step) (back to tree)

A spec-lemma