Proof step 1 from proof forward-lem (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  exec*(IOAut(cstart, cstep, cext))(csl, cal), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦ ∃ asl, aal. r(asl.last, csl.last) ∧ exec*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Proof step 2 from proof forward-lem (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 3:

  exec*(IOAut(cstart, cstep, cext))(csl, cal), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ∃ as. astart(as) ∧ r(as, csl[0]) ⊦ ∃ asl, aal. r(asl.last, csl.last) ∧ exec*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = cext !(cal)

• Proof step 8:

  exec*(IOAut(cstart, cstep, cext))(csl, cal), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦ ∃ asl, aal. r(asl.last, csl.last) ∧ exec*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = cext !(cal), ∃ as. astart(as) ∧ r(as, csl[0])

Rule argument

Additional information

Used formulas: ∃ as. astart(as) ∧ r(as, csl[0])

Proof step 3 from proof forward-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

Proof step 4 from proof forward-lem (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Used terms: cstep, cext, as, aext, r, astart, cstart, cal, astep, csl

Proof step 5 from proof forward-lem (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof forward-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof forward-lem (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: asl, aal

Proof step 8 from proof forward-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

Proof step 9 from proof forward-lem (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

  cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ 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)) ⊦ ∃ asl, aal. r(asl.last, csl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal), ∃ as. astart(as) ∧ r(as, csl[0])

Rule argument

Additional information

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

Proof step 10 from proof forward-lem (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof forward-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), ∀ 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) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs0)) ⊦ ∃ as. astart(as) ∧ r(as, csl[0]), ∃ asl, aal. r(asl.last, csl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

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

Proof step 12 from proof forward-lem (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), cstart(csl[0]) → (∃ as. r(as, csl[0]) ∧ astart(as)), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs0)) ⊦ ∃ asl, aal. r(asl.last, csl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal), ∃ as. astart(as) ∧ r(as, csl[0])

Rule argument

Additional information

Used terms: csl[0]

Proof step 13 from proof forward-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  astart(as), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), r(as, csl[0]), ∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (∃ as0. move(IOAut(astart, astep, aext))(as, (cext(ca) = None ⊃ [];cext(ca).get '), as0) ∧ r(as0, cs0)) ⊦ ∃ as. astart(as) ∧ r(as, csl[0]), ∃ asl, aal. r(asl.last, csl.last) ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ astart(asl[0]) ∧ aext !(aal) = cext !(cal)

Rule argument

Additional information

Proof step 14 from proof forward-lem (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: as