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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ≤F(cioaut, aioaut), ¬ C_≤T_A(cioaut, aioaut) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  cioaut = IOAut(cstart, cstep, cext), ≤F(cioaut, aioaut), ¬ C_≤T_A(cioaut, aioaut) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ≤F(IOAut(cstart, cstep, cext), aioaut), ¬ C_≤T_A(IOAut(cstart, cstep, cext), aioaut) ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  aioaut = IOAut(astart, astep, aext), ≤F(IOAut(cstart, cstep, cext), aioaut), ¬ C_≤T_A(IOAut(cstart, cstep, cext), aioaut) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ≤F(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)), ¬ C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ≤F(cioaut, aioaut) ↔ (∃ r. fwsim(cioaut, aioaut, r))

• Proof step 8:

  ¬ C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)), ∃ r. fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ⊦

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ C_≤T_A(cioaut, aioaut) ↔ (∀ β. trace(cioaut)(β) → trace(aioaut)(β))

• Proof step 11:

  fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ∃ β. ¬(trace(IOAut(cstart, cstep, cext))(β) → trace(IOAut(astart, astep, aext))(β)) ⊦

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), trace(IOAut(cstart, cstep, cext))(β), ¬ trace(IOAut(astart, astep, aext))(β) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ trace(IOAut(start, step, ext))(β) ↔ (∃ σ, α. β = ext !(α) ∧ exec(IOAut(start, step, ext))(σ, α))

• Proof step 14:

  fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(β), ∃ σ, α. β = cext !(α) ∧ exec(IOAut(cstart, cstep, cext))(σ, α) ⊦

Rule argument

Additional information

Used terms: cstart, cstep, cext, β

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)) ⊦

Rule argument

Additional information

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

Proof step 15 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 16:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n, as. ∃ asl. cstep(cσ[n], α[n], cσ[n + 1]) ∧ r(as, cσ[n]) → (∃ aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ # aal + 1 = # asl ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n] '⌝ ) ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as) ⊦

• Proof step 90:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)) ⊦ ∀ n, as. ∃ asl. cstep(cσ[n], α[n], cσ[n + 1]) ∧ r(as, cσ[n]) → (∃ aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ # aal + 1 = # asl ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n] '⌝ ) ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as)

Rule argument

Additional information

Used formulas: ∀ n, as. ∃ asl. cstep(cσ[n], α[n], cσ[n + 1]) ∧ r(as, cσ[n]) → (∃ aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ # aal + 1 = # asl ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n] '⌝ ) ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as)

Proof step 16 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 17:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n0] '⌝ ) ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Proof step 17 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 18:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n0] '⌝ ) ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∃ as. r(as, cσ[0]) ∧ astart(as) ⊦

• Proof step 87:

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n0] '⌝ ) ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ ∃ as. r(as, cσ[0]) ∧ astart(as)

Rule argument

Additional information

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

Proof step 18 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  astart(as), cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[0]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(α[n0]) = None ⊃ [];cext(α[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 19 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ∃ lf. lf(0) = a ' ∧ (∀ n. lf(n + 1) = nextl(n, lf(n).last))

• Proof step 21:

  astart(as), cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[0]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(α[n0]) = None ⊃ [];cext(α[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∃ lf. lf(0) = as ' ∧ (∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last)) ⊦

Rule argument

Additional information

Used terms: as, f_Nat_'as->List<'as>

Proof step 20 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  lf(0) = as ', astart(as), cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[0]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(α[n0]) = None ⊃ [];cext(α[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Proof step 22 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 23:

  cσ = ⌜csl⌝ , lf(0) = as ', astart(as), cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[0]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(α[n0]) = None ⊃ [];cext(α[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦

• Proof step 31:

  cσ = ⌜csf⌝ , lf(0) = as ', astart(as), cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[0]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(α[n0]) = None ⊃ [];cext(α[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 23 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  lf(0) = as ', 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]), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csl[n0], cal[n0], csl[n0 + 1]) ∧ r(as0, csl[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(cal[n0]) = None ⊃ [];cext(cal[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csl[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ trace(ioa)(⌜el⌝ ) ↔ trace*(ioa)(el); (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ ⌜x⌝ .l = x; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ⊦ frag(ioa)(⌜sl⌝ , α) ↔ frag*(ioa)(sl, α.l) ∧ finp(α); (s)

Proof step 24 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  lf(0) = as ', 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]), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)), ∀ n0, as0. cstep(csl[n0], cal[n0], csl[n0 + 1]) ∧ r(as0, csl[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(cal[n0]) = None ⊃ [];cext(cal[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csl[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∃ asl, aal. r(asl.last, csl.last) ∧ exec*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = cext !(cal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s) ⊦ IOAut(start, step, ext).start = start; (s) Used terms: cstep, cext, aext, r, astart, cstart, cal, astep, csl

Proof step 25 from proof forward-implies-leqrefine (previous step) (back to tree)

Lemma forward-lem

Proof step 26 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  aext !(aal) = cext !(cal), lf(0) = as ', astart(as), astart(asl[0]), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), frag*(IOAut(astart, astep, aext))(asl, aal), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csl[0]), r(asl.last, csl.last), ¬ trace*(IOAut(astart, astep, aext))(cext !(cal)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csl[n0], cal[n0], csl[n0 + 1]) ∧ r(as0, csl[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(cal[n0]) = None ⊃ [];cext(cal[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csl[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

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 27 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ trace*(IOAut(start, step, ext))(el) ↔ (∃ sl, al. el = ext !(al) ∧ exec*(IOAut(start, step, ext))(sl, al))

• Proof step 29:

  aext !(aal) = cext !(cal), lf(0) = as ', astart(asl[0]), astart(as), 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(as, csl[0]), ∀ n0, as0. cstep(csl[n0], cal[n0], csl[n0 + 1]) ∧ r(as0, csl[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(cal[n0]) = None ⊃ [];cext(cal[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csl[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ sl, al. ¬(cext !(cal) = aext !(al) ∧ exec*(IOAut(astart, astep, aext))(sl, al)) ⊦

Rule argument

Additional information

Used terms: astart, astep, aext, cext !(cal)

Proof step 28 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  aext !(aal) = cext !(cal), lf(0) = as ', astart(as), astart(asl[0]), cstart(csl[0]), frag*(IOAut(cstart, cstep, cext))(csl, cal), frag*(IOAut(astart, astep, aext))(asl, aal), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csl[0]), r(asl.last, csl.last), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csl[n0], cal[n0], csl[n0 + 1]) ∧ r(as0, csl[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(cal[n0]) = None ⊃ [];cext(cal[n0]).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csl[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ sl, al. cext !(cal) ≠ aext !(al) ∨ ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ ¬ astart(sl[0]) ⊦

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 30 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: asl, aal

Proof step 31 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ ⌜nf⌝ .f = nf; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ frag(ioa)(⌜sf⌝ , α) ↔ fragω(ioa)(sf, α.f) ∧ ¬ finp(α); (s)

Proof step 32 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 33:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦

• Proof step 74:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ []

Rule argument

Additional information

Used formulas: ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ []

Proof step 33 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 34:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last) ∧ aext !(⌜aal⌝ ) = cext !(⌜nf(n) '⌝ ) ∧ r(lf(n + 1).last, csf(n + 1)) ⊦

• Proof step 65:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ ∀ n. ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last) ∧ aext !(⌜aal⌝ ) = cext !(⌜nf(n) '⌝ ) ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Used formulas: ∀ n. ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last) ∧ aext !(⌜aal⌝ ) = cext !(⌜nf(n) '⌝ ) ∧ r(lf(n + 1).last, csf(n + 1))

Proof step 34 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 35:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(⌜f_Nat->List<'aa>(n0)⌝ ) = cext !(⌜nf(n0) '⌝ ) ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦

Rule argument

Additional information

Proof step 35 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 36:

  start(sf(0)), ∀ n. move(IOAut(start, step, ext))(sf(n), cext !(caf(n) '), sf(n + 1)) ⊦ trace(IOAut(start, step, ext))(cext !(⌜caf⌝ ))

• Proof step 37:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(⌜f_Nat->List<'aa>(n0)⌝ ) = cext !(⌜nf(n0) '⌝ ) ∧ r(lf(n0 + 1).last, csf(n0 + 1)) ⊦ astart(f_Nat_'as->List<'as>(0, lf(0).last).head) ∧ (∀ n. move(IOAut(astart, astep, aext)) (f_Nat_'as->List<'as>(n, lf(n).last).head, cext !(nf(n) '), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head))

Rule argument

Additional information

Used terms: cext, aext, astart, nf, λ n. f_Nat_'as->List<'as>(n, lf(n).last).head, astep

Proof step 36 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 37 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ astart(f_Nat_'as->List<'as>(0, as).head) ∧ move(IOAut(astart, astep, aext)) (f_Nat_'as->List<'as>(n, lf(n).last).head, (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head)

Rule argument

Additional information

Used simplifier rules: ⊦ a '.last = a; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 38 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 39:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)) ⊦

• Proof step 46:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ move(IOAut(astart, astep, aext)) (f_Nat_'as->List<'as>(n, lf(n).last).head, (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)) ⊦

Rule argument

Additional information

Proof step 39 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 40:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(0), nf(0), csf(0 + 1)) ∧ r(as, csf(0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(0, as), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(0, as) ∧ aext !(aal) = (cext(nf(0)) = None ⊃ [];cext(nf(0)).get ') ∧ r(f_Nat_'as->List<'as>(0, as).last, csf(0 + 1)) ∧ f_Nat_'as->List<'as>(0, as).head = as), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used terms: 0, as

Proof step 40 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(0), nf(0), csf(1)) → frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(0, as), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(0, as) ∧ aext !(aal) = (cext(nf(0)) = None ⊃ [];cext(nf(0)).get ') ∧ r(f_Nat_'as->List<'as>(0, as).last, csf(1)) ∧ f_Nat_'as->List<'as>(0, as).head = as, ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 41 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ cstep(csf(0), nf(0), csf(1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Proof step 42 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ fragω(ioa)(sf, af) ↔ (∀ n. ioa.step(sf(n), af(n), sf(n +1)))

• Proof step 44:

  lf(0) = as ', astart(as), cstart(csf(0)), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ cstep(csf(0), nf(0), csf(1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. IOAut(cstart, cstep, cext).step(csf(n), nf(n), csf(n +1)) ⊦

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), csf, nf

Proof step 43 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  lf(0) = as ', astart(as), cstart(csf(0)), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ astart(f_Nat_'as->List<'as>(0, as).head), ¬ cstep(csf(0), nf(0), csf(1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. cstep(csf(n), nf(n), csf(n + 1)) ⊦

Rule argument

Additional information

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

Proof step 45 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: 0

Proof step 46 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

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

• Proof step 48:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ al, sl. ¬ ( frag*(IOAut(astart, astep, aext))(sl, al) ∧ f_Nat_'as->List<'as>(n, lf(n).last).head = sl[0] ∧ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ')) ⊦

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), f_Nat_'as->List<'as>(n, lf(n).last).head, (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head

Proof step 47 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat->List<'aa>(n0)) ∧ # f_Nat->List<'aa>(n0) + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(f_Nat->List<'aa>(n0)) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(lf(n0 + 1).last, csf(n0 + 1)), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ f_Nat_'as->List<'as>(n, lf(n).last).head ≠ sl[0] ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ sl.last ∨ aext !(al) ≠ (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ⊦

Rule argument

Additional information

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

Proof step 49 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 50:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ f_Nat_'as->List<'as>(n, lf(n).last).head ≠ sl[0] ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ sl.last ∨ aext !(al) ≠ (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used terms: n

Proof step 50 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ al, sl. ¬ frag*(IOAut(astart, astep, aext))(sl, al) ∨ f_Nat_'as->List<'as>(n, lf(n).last).head ≠ sl[0] ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ sl.last ∨ aext !(al) ≠ aext !(f_Nat->List<'aa>(n)) ⊦

Rule argument

Additional information

Proof step 51 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 52:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ¬ frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)) ∨ f_Nat_'as->List<'as>(n, lf(n).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last)[0] ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last ∨ aext !(f_Nat->List<'aa>(n)) ≠ aext !(f_Nat->List<'aa>(n)) ⊦

Rule argument

Additional information

Used terms: f_Nat->List<'aa>(n), f_Nat_'as->List<'as>(n, lf(n).last)

Proof step 52 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], f_Nat_'as->List<'as>(n, lf(n).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last)[0] ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last ⊦

Rule argument

Additional information

Proof step 53 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ x ≠ [] → x[0] = x.head

• Proof step 55:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), f_Nat_'as->List<'as>(n, lf(n).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).head ∨ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: f_Nat_'as->List<'as>(n, lf(n).last)

Proof step 54 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦

Rule argument

Additional information

Proof step 56 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 57:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(n + 1), nf(n + 1), csf((n + 1) + 1)) ∧ r(lf(n + 1).last, csf(n + 1)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n + 1, lf(n + 1).last) ∧ aext !(aal) = (cext(nf(n + 1)) = None ⊃ [];cext(nf(n + 1)).get ') ∧ r(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).last, csf((n + 1) + 1)) ∧ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head = lf(n + 1).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Used terms: n + 1, lf(n + 1).last

Proof step 57 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(n + 1), nf(n + 1), csf(2 + n)) → frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n + 1, lf(n + 1).last) ∧ aext !(aal) = (cext(nf(n + 1)) = None ⊃ [];cext(nf(n + 1)).get ') ∧ r(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).last, csf(2 + n)) ∧ f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head = lf(n + 1).last, ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 58 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 59:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ cstep(csf(n + 1), nf(n + 1), csf(2 + n)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

• Proof step 63:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), aext !(aal) = (cext(nf(n + 1)) = None ⊃ [];cext(nf(n + 1)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), # aal + 1 = # f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head = lf(n + 1).last, lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), r(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).last, csf(2 + n)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦

Rule argument

Additional information

Proof step 59 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ fragω(ioa)(sf, af) ↔ (∀ n. ioa.step(sf(n), af(n), sf(n +1)))

• Proof step 61:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ cstep(csf(n + 1), nf(n + 1), csf(2 + n)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. IOAut(cstart, cstep, cext).step(csf(n), nf(n), csf(n +1)) ⊦

Rule argument

Additional information

Used terms: IOAut(cstart, cstep, cext), csf, nf

Proof step 60 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), lf(0) = as ', f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(lf(n + 1).last, csf(n + 1)), ¬ cstep(csf(n + 1), nf(n + 1), csf(2 + n)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ⊦

Rule argument

Additional information

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

Proof step 62 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic Used terms: n + 1

Proof step 63 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  aext !(aal) = (cext(nf(n + 1)) = None ⊃ [];cext(nf(n + 1)).get '), aext !(f_Nat->List<'aa>(n)) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), # f_Nat->List<'aa>(n) + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).head = lf(n + 1).last, lf(0) = as ', lf(n + 1).last ≠ f_Nat_'as->List<'as>(n, lf(n).last).last, f_Nat_'as->List<'as>(n, lf(n).last) ≠ [], astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last), aal), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), f_Nat->List<'aa>(n)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(f_Nat_'as->List<'as>(n + 1, lf(n + 1).last).last, csf(2 + n)), r(lf(n + 1).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦

Rule argument

Additional information

Proof step 64 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 65 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss)

Proof step 66 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 67:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(n), nf(n), csf(n + 1)) ∧ r(lf(n).last, csf(n)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, lf(n).last).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, lf(n).last).head = lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Used terms: n, lf(n).last

Proof step 67 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), cstep(csf(n), nf(n), csf(n + 1)) ∧ r(lf(n).last, csf(n)) → frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, lf(n).last).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, lf(n).last).head = lf(n).last, ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Proof step 68 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 69:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1)), cstep(csf(n), nf(n), csf(n + 1)) ∧ r(lf(n).last, csf(n))

• Proof step 71:

  aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), f_Nat_'as->List<'as>(n, lf(n).last).head = lf(n).last, lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(f_Nat_'as->List<'as>(n, lf(n).last).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Proof step 69 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  lf(0) = as ', astart(as), cstart(csf(0)), cstep(csf(n), nf(n), csf(n + 1)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ r(lf(n).last, csf(n)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ step(sf(n), af(n), sf(n + 1)) → (fragω(IOAut(start, step, ext))(sf, af) ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 70 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 71 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 72:

  aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), f_Nat_'as->List<'as>(n, lf(n).last).head = lf(n).last, lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(f_Nat_'as->List<'as>(n, lf(n).last).last, csf(n + 1)), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [] ⊦ frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(lf(n + 1).last, csf(n + 1))

Rule argument

Additional information

Used terms: aal

Proof step 72 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n, lf(n).last), f_Nat_'as->List<'as>(n, lf(n).last).head = lf(n).last, lf(0) = as ', astart(as), cstart(csf(0)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, lf(n).last), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), r(f_Nat_'as->List<'as>(n, lf(n).last).last, csf(n + 1)), ¬ r(lf(n + 1).last, csf(n + 1)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. r(lf(n).last, csf(n)) ∧ lf(n) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦

Rule argument

Additional information

Proof step 73 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n + 1

Proof step 74 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  lf(0) = as ', astart(as), cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, csf(0)), ¬ trace(IOAut(astart, astep, aext))(cext !(⌜nf⌝ )), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ r(lf(n).last, csf(n)) ∧ lf(n) ≠ []

Rule argument

Additional information

Proof step 75 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 76:

  lf(0) = as ', cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ r(lf(n).last, csf(n)) ∧ lf(n) ≠ []

Rule argument

Additional information

Proof step 76 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 77:

  lf(0) = as ', cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ lf, as, cstart, csf, cstep, cext, nf, r, astart, astep, aext, f_Nat_'as->List<'as>. lf(0) = as ' ∧ cstart(csf(0)) ∧ fragω(IOAut(cstart, cstep, cext))(csf, nf) ∧ r(as, csf(0)) ∧ (∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0)) ∧ (∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last)) → r(lf(n0).last, csf(n0)) ∧ lf(n0) ≠ [] ⊦ r(lf(n0 +1).last, csf(n0 +1)) ∧ lf(n0 +1) ≠ []

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ a '.last = a; (s) ⊦ a ' ≠ []; (s)

Proof step 77 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  lf(0) = as ', cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ lf0, as0, cstart0, csf0, cstep0, cext0, nf0, r0, astart0, astep0, aext0, f_Nat_'as->List<'as>0. lf0(0) = as0 ' ∧ cstart0(csf0(0)) ∧ fragω(IOAut(cstart0, cstep0, cext0))(csf0, nf0) ∧ r0(as0, csf0(0)) ∧ (∀ n, as1. cstep0(csf0(n), nf0(n), csf0(n + 1)) ∧ r0(as1, csf0(n)) → (∃ aal. frag*(IOAut(astart0, astep0, aext0))(f_Nat_'as->List<'as>0(n, as1), aal) ∧ aext0 !(aal) = (cext0(nf0(n)) = None ⊃ [];cext0(nf0(n)).get ') ∧ r0(f_Nat_'as->List<'as>0(n, as1).last, csf0(n + 1)) ∧ f_Nat_'as->List<'as>0(n, as1).head = as1)) ∧ (∀ n. lf0(n + 1) = f_Nat_'as->List<'as>0(n, lf0(n).last)) → r0(lf0(n0).last, csf0(n0)) ∧ lf0(n0) ≠ [] ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss)

Proof step 78 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 79:

  lf(0) = as ', cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), lf(0) = as ' ∧ cstart(csf(0)) ∧ fragω(IOAut(cstart, cstep, cext))(csf, nf) ∧ r(as, csf(0)) ∧ (∀ n, as1. cstep(csf(n), nf(n), csf(n + 1)) ∧ r(as1, csf(n)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, as1).head = as1)) ∧ (∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last)) → r(lf(n0).last, csf(n0)) ∧ lf(n0) ≠ [], ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Used terms: lf, as, cstart, csf, cstep, cext, nf, r, astart, astep, aext, f_Nat_'as->List<'as>

Proof step 79 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  lf(0) = as ', cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), ( cstep(csf(n), nf(n), csf(n + 1)) ∧ r(as1, csf(n)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, as1).head = as1)) → r(lf(n0).last, csf(n0)) ∧ lf(n0) ≠ [], ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Proof step 80 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 81:

  lf(0) = as ', cstart(csf(0)), cstep(csf(n), nf(n), csf(n + 1)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as1, csf(n)), r(as, csf(0)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, as1).head = as1, r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

• Proof step 84:

  lf(0) = as ', lf(n0) ≠ [], cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), r(lf(n0).last, csf(n0)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last), ∀ n0, as0. cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(as0, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, as0).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0) ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Proof step 81 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 82:

  lf(0) = as ', cstart(csf(0)), cstep(csf(n), nf(n), csf(n + 1)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as, csf(0)), r(as1, csf(n)), cstep(csf(n), nf(n), csf(n + 1)) ∧ r(as1, csf(n)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n, as1) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, as1).head = as1), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal) ∧ aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get ') ∧ r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)) ∧ f_Nat_'as->List<'as>(n, as1).head = as1, r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Used terms: n, as1

Proof step 82 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  aext !(aal) = (cext(nf(n)) = None ⊃ [];cext(nf(n)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n, as1), f_Nat_'as->List<'as>(n, as1).head = as1, lf(0) = as ', cstart(csf(0)), cstep(csf(n), nf(n), csf(n + 1)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(as1, csf(n)), r(as, csf(0)), r(f_Nat_'as->List<'as>(n, as1).last, csf(n + 1)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ ∃ aal0. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n, as1), aal0) ∧ aext !(aal0) = aext !(aal), r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Proof step 83 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: aal

Proof step 84 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 85:

  lf(0) = as ', lf(n0) ≠ [], cstart(csf(0)), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(lf(n0).last, csf(n0)), r(as, csf(0)), cstep(csf(n0), nf(n0), csf(n0 + 1)) ∧ r(lf(n0).last, csf(n0)) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last) ∧ aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get ') ∧ r(f_Nat_'as->List<'as>(n0, lf(n0).last).last, csf(n0 + 1)) ∧ f_Nat_'as->List<'as>(n0, lf(n0).last).head = lf(n0).last), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Used terms: n0, lf(n0).last

Proof step 85 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  aext !(aal) = (cext(nf(n0)) = None ⊃ [];cext(nf(n0)).get '), # aal + 1 = # f_Nat_'as->List<'as>(n0, lf(n0).last), f_Nat_'as->List<'as>(n0, lf(n0).last).head = lf(n0).last, lf(0) = as ', lf(n0) ≠ [], cstart(csf(0)), cstep(csf(n0), nf(n0), csf(n0 + 1)), frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, lf(n0).last), aal), fragω(IOAut(cstart, cstep, cext))(csf, nf), r(lf(n0).last, csf(n0)), r(as, csf(0)), r(f_Nat_'as->List<'as>(n0, lf(n0).last).last, csf(n0 + 1)), ∀ n. lf(n + 1) = f_Nat_'as->List<'as>(n, lf(n).last) ⊦ r(lf(n0 + 1).last, csf(n0 + 1)) ∧ lf(n0 + 1) ≠ []

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ step(sf(n), af(n), sf(n + 1)) → (fragω(IOAut(start, step, ext))(sf, af) ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 86 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n0

Proof step 87 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

  cstart(cσ[0]), frag(IOAut(cstart, cstep, cext))(cσ, α), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ n0, as0. cstep(cσ[n0], α[n0], cσ[n0 + 1]) ∧ r(as0, cσ[n0]) → (∃ aal. frag*(IOAut(astart, astep, aext))(f_Nat_'as->List<'as>(n0, as0), aal) ∧ # aal + 1 = # f_Nat_'as->List<'as>(n0, as0) ∧ aext !(⌜aal⌝ ) = cext !(⌜α[n0] '⌝ ) ∧ r(f_Nat_'as->List<'as>(n0, as0).last, cσ[n0 + 1]) ∧ f_Nat_'as->List<'as>(n0, as0).head = as0), ∀ 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)) ⊦ ∃ as. r(as, cσ[0]) ∧ astart(as)

Rule argument

Additional information

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

Proof step 88 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 89 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) Used terms: cσ[0]

Proof step 90 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), r(as, cσ[n]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ext !(a ') = (ext(a) = None ⊃ [];ext(a).get '); (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss)

Proof step 91 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

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

  cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), r(as, cσ[n]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ 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. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as

Rule argument

Additional information

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

Proof step 92 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 93 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 94:

  cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), r(as, cσ[n]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), r(as, cσ[n]) ∧ cstep(cσ[n], α[n], cσ[n + 1]) → (∃ as0. move(IOAut(astart, astep, aext))(as, cext !(α[n] '), as0) ∧ r(as0, cσ[n + 1])), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as

Rule argument

Additional information

Used terms: cσ[n], α[n], cσ[n + 1], as

Proof step 94 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), move(IOAut(astart, astep, aext))(as, (cext(α[n]) = None ⊃ [];cext(α[n]).get '), as0), r(as, cσ[n]), r(as0, cσ[n + 1]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as

Rule argument

Additional information

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

Proof step 95 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

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

• Proof step 97:

  cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), r(as0, cσ[n + 1]), r(as, cσ[n]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)), ∃ al, sl. frag*(IOAut(astart, astep, aext))(sl, al) ∧ as = sl[0] ∧ as0 = sl.last ∧ IOAut(astart, astep, aext).ext !(al) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ⊦ ∃ asl, aal. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = as

Rule argument

Additional information

Used terms: IOAut(astart, astep, aext), as, (cext(α[n]) = None ⊃ [];cext(α[n]).get '), as0

Proof step 96 from proof forward-implies-leqrefine (previous step) (back to tree)

A spec-lemma

Proof step 97 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get '), cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), frag*(IOAut(astart, astep, aext))(asl, aal), r(asl[0], cσ[n]), r(asl.last, cσ[n + 1]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ ∃ asl0, aal. frag*(IOAut(astart, astep, aext))(asl0, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl0.last, cσ[n + 1]) ∧ asl0.head = asl[0]

Rule argument

Additional information

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

Proof step 98 from proof forward-implies-leqrefine (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 99:

  aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get '), cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), frag*(IOAut(astart, astep, aext))(asl, aal), r(asl.last, cσ[n + 1]), r(asl[0], cσ[n]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get ') ∧ r(asl.last, cσ[n + 1]) ∧ asl.head = asl[0]

Rule argument

Additional information

Used terms: asl, aal

Proof step 99 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

  aext !(aal) = (cext(α[n]) = None ⊃ [];cext(α[n]).get '), asl.head ≠ asl[0], cstart(cσ[0]), cstep(cσ[n], α[n], cσ[n + 1]), frag(IOAut(cstart, cstep, cext))(cσ, α), frag*(IOAut(astart, astep, aext))(asl, aal), r(asl[0], cσ[n]), r(asl.last, cσ[n + 1]), ¬ trace(IOAut(astart, astep, aext))(cext !(α)), ∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)) ⊦

Rule argument

Additional information

Proof step 100 from proof forward-implies-leqrefine (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: asl, as0, asl0