Proof step 1 from proof repla-mon (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, (s, cs) + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n + 1), paf.take(n + 1), ⌜as '⌝ + aσ, aα)⌝ ⊦

Rule argument

Additional information

Proof step 2 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n + 1), paf.take(n + 1), ⌜as '⌝ + aσ, aα)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 3 from proof repla-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 +1), paf.take(n0 +1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 +1 + 1), paf.take(n0 +1 + 1), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart, astep, aext, as, aσ, aα, start, cstart, step, cstep, ren, cren, ext, cext, s, cs, pcsf, paf, aren. ¬ ( frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ∧ ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0), paf.take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: repla-base: ⊦ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = []; Nat freely generated by 0, +1;; ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ nf.take(0) = []; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜[]⌝ = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ nf.take(1) = nf(0) '; (s) ⊦ [] ⊑ σ; (s)

Proof step 4 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(2 + n0), paf.take(2 + n0), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

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 ⊦ m +1 = m + 1; (s)

Proof step 5 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ nf.take(n + 2) = nf(0) + (λ n. nf(n + 1)).take(n + 1)

• Proof step 7:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (pcsf(0) + (λ n. pcsf(n + 1)).take(n0 + 1)), paf.take(2 + n0), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: pcsf, n0

Proof step 6 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf.take(2 + n0), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

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

Proof step 8 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ nf.take(n + 2) = nf(0) + (λ n. nf(n + 1)).take(n + 1)

• Proof step 10:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: paf, n0

Proof step 9 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n0 + 1), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 11 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n)

• Proof step 13:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (pcsf(0) + (λ n. pcsf(n + 1)).take(n0)), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: pcsf, n0

Proof step 12 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0), paf.take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

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

Proof step 14 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n)

• Proof step 16:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: paf, n0

Proof step 15 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 17 from proof repla-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 18:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf(0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 18 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 19 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ⌜nf⌝ = nf(0) + ⌜λ n. nf(n + 1)⌝

• Proof step 21:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , paf(0) + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: paf

Proof step 20 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 22 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ fragω(IOAut(start, step, ext))(s ' + sf, af) ↔ step(s, af(0), sf(0)) ∧ fragω(IOAut(start, step, ext))(sf, λ n. af(n + 1))

• Proof step 24:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), pcsf(0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜pcsf⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: (s, cs), Π(ext, cext, ren, cren), Π(start, cstart), pcsf, paf, Π(step, cstep, ren, cren, ext, cext)

Proof step 23 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ ⌜nf⌝ = nf(0) + ⌜λ n. nf(n + 1)⌝

• Proof step 26:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), pcsf(0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + (pcsf(0) + ⌜λ n. pcsf(n + 1)⌝ ), ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: pcsf

Proof step 25 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  (s0, cs0) = pcsf(0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 27 from proof repla-mon (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  (s0, cs0) = pcsf(0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

• Proof step 90:

  (s0, cs0) = pcsf(0), pcsf ≠ (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used formulas: pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1))

Proof step 28 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  (s0, cs0) = pcsf(0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 29 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), pa, (ls0, rs0)) ↔ rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ pa = lren(la) ∧ ¬ cod(rren)(pa)) ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ pa = rren(ra) ∧ ¬ cod(lren)(pa)) ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ pa = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ pa = rren(ra))

• Proof step 31:

  (s0, cs0) = pcsf(0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ , cs = cs0 ∧ (∃ la. step(s, la, s0) ∧ paf(0) = ren(la) ∧ ¬ cod(cren)(paf(0))) ∨ s = s0 ∧ (∃ ra. cstep(cs, ra, cs0) ∧ paf(0) = cren(ra) ∧ ¬ cod(ren)(paf(0))) ∨ (∃ la, ra. step(s, la, s0) ∧ ext(la) ≠ None ∧ paf(0) = ren(la) ∧ cstep(cs, ra, cs0) ∧ cext(ra) ≠ None ∧ paf(0) = cren(ra)) ⊦

Rule argument

Additional information

Used terms: cext, paf(0), cs, cstep, ren, ext, cren, cs0, step, s, s0

Proof step 30 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  (s0, cs0) = pcsf(0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ , cs = cs0 ∧ step(s, a, s0) ∧ paf(0) = ren(a) ∧ ¬ cod(cren)(paf(0)) ∨ s = s0 ∧ cstep(cs, ca, cs0) ∧ paf(0) = cren(ca) ∧ ¬ cod(ren)(paf(0)) ∨ step(s, a0, s0) ∧ ext(a0) ≠ None ∧ paf(0) = ren(a0) ∧ cstep(cs, ca0, cs0) ∧ cext(ca0) ≠ None ∧ paf(0) = cren(ca0) ⊦

Rule argument

Additional information

Proof step 32 from proof repla-mon (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 33:

  (s0, cs0) = pcsf(0), cs = cs0, paf(0) = ren(a), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(cren)(paf(0)), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

• Proof step 38:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), s = s0, cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(paf(0)), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

• Proof step 45:

  (s0, cs0) = pcsf(0), paf(0) = ren(a0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 33 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (s0, cs0) = pcsf(0), paf(0) = ren(a), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs0) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜ren(a) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(cren)(ren(a)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: repla-rec-addS: ⊦ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα) = ren(a) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ + σ1 ⊑ ⌜x⌝ + σ2 ↔ σ1 ⊑ σ2; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s)

Proof step 34 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 35:

  ⊦ Πok(lext, rext, lren, rren) ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs) ' + psf, paf) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs) '⌝ + ⌜psf⌝ , lren(la) + ⌜paf⌝ ) = πra(lstep, rstep, lren, rren, ⌜(ls0, rs) '⌝ + ⌜psf⌝ , ⌜paf⌝ )

• Proof step 36:

  (s0, cs0) = pcsf(0), paf(0) = ren(a), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs0) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜ren(a) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(cren)(ren(a)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , Πok(ext, cext, ren, cren) ∧ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + (λ n. pcsf(n + 1)), λ n. paf(n + 1)) → πra(step, cstep, ren, cren, ⌜(s, cs0) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ren(a) + ⌜λ n. paf(n + 1)⌝ ) = πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: cext, cs0, cstart, cstep, λ n. pcsf(n + 1), ren, ext, cren, a, step, start, λ n. paf(n + 1), s, s0

Proof step 35 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  (s0, cs0) = pcsf(0), paf(0) = ren(a), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), πra(step, cstep, ren, cren, ⌜(s, cs0) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜ren(a) '⌝ + ⌜λ n. paf(n + 1)⌝ ) = πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(cren)(ren(a)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 37 from proof repla-mon (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: astart, astep, aext, as, aσ, aα, start, cstart, step, cstep, ren, cren, ext, cext, s0, cs0, λ n. pcsf(n + 1), λ n. paf(n + 1), aren

Proof step 38 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: repla-rec-skip: ⊦ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα) = repla (step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); a: ⊦ (x + y) + z = x + y + z; from specification list append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 39 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 40:

  ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls, rs0) ' + psf, paf) ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls, rs0) '⌝ + ⌜psf⌝ , rren(ra) + ⌜paf⌝ ) = ⌜ra '⌝ + πra(lstep, rstep, lren, rren, (ls, rs0) + ⌜psf⌝ , ⌜paf⌝ )

• Proof step 41:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + (λ n. pcsf(n + 1)), λ n. paf(n + 1)) ∧ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , cren(ca) + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca '⌝ + πra(step, cstep, ren, cren, (s0, cs0) + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: cext, cs, cstart, cstep, λ n. pcsf(n + 1), ca, ren, ext, cren, cs0, step, start, λ n. paf(n + 1), s0

Proof step 40 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 42 from proof repla-mon (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 43:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ¬ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∨ ¬ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + (λ n. pcsf(n + 1)), λ n. paf(n + 1)) ∨ ¬ nounsharedextR(cren, cext, ren) ∨ ¬ Πok(ext, cext, ren, cren) ∨ ¬ cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα) ∨ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ ⊦

Rule argument

Additional information

Used terms: astart, astep, aext, as, aσ, aα, start, cstart, step, cstep, ren, cren, ext, cext, s0, cs0, λ n. pcsf(n + 1), λ n. paf(n + 1), aren

Proof step 43 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s0, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ¬ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα)⌝ , ¬ cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 44 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nounsharedextR-notcodren-internal: ⊦ ¬ cod(ren)(cren(ca)) ∧ nounsharedextR(cren, cext, ren) → (cext(ca) = None ↔ true); ⊦ ext !(⌜a '⌝ + α) = ext(a) + ext !(α); (s) ⊦ oe + β = (oe = None ⊃ [];⌜oe.get '⌝ ) + β; (s) ⊦ [] + σ = σ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 45 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 46 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 47:

  pa = rren(ra) ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs0) ' + psf, paf) ∧ lstep(ls, la, ls0) ∧ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , pa + ⌜paf⌝ ) = ⌜ra '⌝ + πra(lstep, rstep, lren, rren, ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , ⌜paf⌝ )

• Proof step 48:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + (λ n. pcsf(n + 1)), λ n. paf(n + 1)) ∧ step(s, a0, s0) ∧ cstep(cs, ca0, cs0) ∧ ren(a0) = cren(ca0) → πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ren(a0) + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca0 '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: cext, ren(a0), cs, cstart, cstep, λ n. pcsf(n + 1), ca0, ren, ext, cren, a0, cs0, step, start, λ n. paf(n + 1), s, s0

Proof step 47 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca0) '⌝ + ⌜λ n. paf(n + 1)⌝ ) = ⌜ca0 '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜cren(ca0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 49 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 50:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), cext !(⌜ca0 '⌝ + πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 50 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  (s0, cs0) = pcsf(0), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜cext(ca0).get '⌝ + cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ext(a) ≠ None → ext !(⌜a '⌝ + α) = ⌜ext(a).get '⌝ + ext !(α); (s)

Proof step 51 from proof repla-mon (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 52:

  (s0, cs0) = pcsf(0), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜e '⌝ + cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: cext(ca0), e

Proof step 52 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  (s0, cs0) = pcsf(0), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜e '⌝ + cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

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

Proof step 53 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 55:

  (s0, cs0) = pcsf(0), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0), ∃ σ1. (⌜e '⌝ + cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ))) + σ1 = aext !(aα) ⊦

Rule argument

Additional information

Used terms: ⌜e '⌝ + cext ! (πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )), aext !(aα)

Proof step 54 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  (s0, cs0) = pcsf(0), (⌜e '⌝ + cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ ))) + β = aext !(aα), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Proof step 56 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ ext !(α) = ⌜e '⌝ + β ↔ (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β)

• Proof step 58:

  (s0, cs0) = pcsf(0), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0), ∃ al, aa, α0. aα = ⌜al⌝ + ⌜aa '⌝ + α0 ∧ aext(aa) = Some(e) ∧ aext !(⌜al⌝ ) = [] ∧ aext !(α0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: e, cext ! (πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext, aα

Proof step 57 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 58 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 59 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 60:

  ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ cren(ca) = ren(a) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ n = # aal → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα)

• Proof step 61:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), step(s, a0, s0) ∧ cstep(cs, ca0, cs0) ∧ cren(ca0) = ren(a0) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca0) = aext(aa) ∧ # aal = # aal → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), ren(a0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) = aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), (⌜as '⌝ + aσ).drop(# aal + 1), aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used terms: aren, ren, cstep, cext, aa, s, aext, aα0, ca0, a0, (λ n. paf(n + 1)).take(n0), cren, aal, (λ n. pcsf(n + 1)).take(n0), cs0, s0, cs, # aal, ⌜as '⌝ + aσ, step

Proof step 60 from proof repla-mon (previous step) (back to tree)

Lemma repla-rec-addboth

Proof step 61 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) = aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), cren(ca0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 62 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 63:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Proof step 63 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 64:

  ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ cren(ca) = ren(a) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ n = # aal → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα)

• Proof step 65:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), step(s, a0, s0) ∧ cstep(cs, ca0, cs0) ∧ cren(ca0) = ren(a0) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca0) = aext(aa) ∧ # aal = # aal → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), ren(a0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) = aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), (⌜as '⌝ + aσ).drop(# aal + 1), aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used terms: aren, ren, cstep, cext, aa, s, aext, aα0, ca0, a0, (λ n. paf(n + 1)).take(n0 + 1), cren, aal, (λ n. pcsf(n + 1)).take(n0 + 1), cs0, s0, cs, # aal, ⌜as '⌝ + aσ, step

Proof step 64 from proof repla-mon (previous step) (back to tree)

Lemma repla-rec-addboth

Proof step 65 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) = aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), cren(ca0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 66 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 67:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Proof step 67 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s1, cs1, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s1, cs1) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s1, cs1) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0) ⊑ repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s1, cs1) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0) ⊦

Rule argument

Additional information

Proof step 68 from proof repla-mon (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 69:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ∨ ¬ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + (λ n. pcsf(n + 1)), λ n. paf(n + 1)) ∨ ¬ nounsharedextR(cren, cext, ren) ∨ ¬ Πok(ext, cext, ren, cren) ∨ ¬ cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα0) ∨ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊦

Rule argument

Additional information

Used terms: astart, astep, aext, aσ[# aal], aσ.drop(# aal + 1), aα0, start, cstart, step, cstep, ren, cren, ext, cext, s0, cs0, λ n. pcsf(n + 1), λ n. paf(n + 1), aren

Proof step 69 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ∨ ¬ cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα0) ∨ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊦

Rule argument

Additional information

Proof step 70 from proof repla-mon (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 71:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

• Proof step 80:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

• Proof step 83:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

Rule argument

Additional information

Proof step 71 from proof repla-mon (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 72:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ∧ ¬ # α < ⌜n⌝ → (frag(IOAut(start, step, ext))(σ.drop(n), α.drop(n)) ↔ true)

• Proof step 73:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0) ∧ ¬ #(⌜aal⌝ + ⌜aa '⌝ + aα0) < ⌜# aal + 1⌝ → (frag(IOAut(astart, astep, aext))((⌜as '⌝ + aσ).drop(# aal + 1), (⌜aal⌝ + ⌜aa '⌝ + aα0).drop(# aal + 1)) ↔ true) ⊦

Rule argument

Additional information

Used terms: aext, ⌜aal⌝ + ⌜aa '⌝ + aα0, astart, ⌜as '⌝ + aσ, # aal + 1, astep

Proof step 72 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag(IOAut(astart, astep, aext))(aσ.drop(# aal), aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜a '⌝ + σ).drop(1) = σ; (s) ⊦ (⌜x⌝ + σ).drop(m + # x) = σ.drop(m); (s) ⊦ n + 0 = n; (s) ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ¬ n∞ + n∞1 < n∞1; (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 74 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ ⌜n⌝ < # σ → σ.drop(n) = σ[n] + σ.drop(n + 1)

• Proof step 76:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(aσ.drop(# aal), aα0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜# aal⌝ < # aσ, ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s) Used terms: aσ, # aal

Proof step 75 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 78:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, #(⌜as '⌝ + aσ) = #(⌜aal⌝ + ⌜aa '⌝ + aα0) + ⌜1⌝ , (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(aσ.drop(# aal), aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜# aal⌝ < # aσ, ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ n. ⌜n⌝ < #(⌜aal⌝ + ⌜aa '⌝ + aα0) → astep((⌜as '⌝ + aσ)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], (⌜as '⌝ + aσ)[n +1]) ⊦

Rule argument

Additional information

Used terms: aext, ⌜aal⌝ + ⌜aa '⌝ + aα0, astart, ⌜as '⌝ + aσ, astep

Proof step 77 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 78 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], # aσ = ⌜1⌝ + ⌜# aal⌝ + # aα0, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(aσ.drop(# aal), aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜# aal⌝ < # aσ, ¬ frag(IOAut(astart, astep, aext))(⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ n. ¬ ⌜# aal⌝ + # aα0 < ⌜n⌝ → astep((⌜as '⌝ + aσ)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], aσ[n]) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ m +1 = m + 1; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ n < m → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ n∞1 = ⌜m - n⌝ + n∞2); (s) ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; (s)

Proof step 79 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ ¬ n∞ + n∞1 < n∞1; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf

Proof step 80 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 82:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ aal.map(aren) + aren(aa) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ σ1. cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + σ1 ≠ aext !(aα0) ⊦

Rule argument

Additional information

Used terms: cext ! (πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )), aext !(aα0)

Proof step 81 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 82 from proof repla-mon (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β

Proof step 83 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x ⊑ b ' + y ↔ a = b ∧ x ⊑ y; (ws) ⊦ x + y ⊑ x + z ↔ y ⊑ z; (s)

Proof step 84 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ ⌜n⌝ < # σ → σ.drop(n) = σ[n] + σ.drop(n + 1)

• Proof step 86:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, ⌜aal⌝ + ⌜aa '⌝ + aα0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ ⌜# aal⌝ < # aσ, ¬ repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s) Used terms: aσ, # aal

Proof step 85 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 88:

  aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, aext !(aal) = [], #(⌜as '⌝ + aσ) = #(⌜aal⌝ + ⌜aa '⌝ + aα0) + ⌜1⌝ , (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ ⌜# aal⌝ < # aσ, ¬ repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ n. ⌜n⌝ < #(⌜aal⌝ + ⌜aa '⌝ + aα0) → astep((⌜as '⌝ + aσ)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], (⌜as '⌝ + aσ)[n +1]) ⊦

Rule argument

Additional information

Used terms: aext, ⌜aal⌝ + ⌜aa '⌝ + aα0, astart, ⌜as '⌝ + aσ, astep

Proof step 87 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  aext !(aal) = [], aext !(aα0) = cext !(πra(step, cstep, ren, cren, ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜λ n. paf(n + 1)⌝ )) + β, # aσ = ⌜1⌝ + ⌜# aal⌝ + # aα0, (s0, cs0) = pcsf(0), aext(aa) = Some(e), cext(ca0) = Some(e), paf(0) = cren(ca0), pcsf = (s0, cs0) ' + (λ n. pcsf(n + 1)), ren(a0) = cren(ca0), ext(a0) ≠ None, cstep(cs, ca0, cs0), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), ⌜aσ[# aal] '⌝ + aσ.drop(# aal + 1), aα0), ¬ ⌜# aal⌝ < # aσ, ¬ repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), (λ n. paf(n + 1)).take(n0), aσ.drop(# aal), aα0) ⊑ repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1), aσ.drop(# aal), aα0), ∀ n. ¬ ⌜# aal⌝ + # aα0 < ⌜n⌝ → astep((⌜as '⌝ + aσ)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], aσ[n]) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ m +1 = m + 1; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ n < m → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ n∞1 = ⌜m - n⌝ + n∞2); (s) ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; (s)

Proof step 89 from proof repla-mon (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ ¬ n∞ + n∞1 < n∞1; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf

Proof step 90 from proof repla-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

  ⊦ x + nf = (λ n. (n < # x ⊃ x[n];nf(n - # x)))

• Proof step 92:

  (s0, cs0) = pcsf(0), pcsf ≠ (λ n. (n < # (s0, cs0) ' ⊃ (s0, cs0) '[n];pcsf((n - # (s0, cs0) ') + 1))), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used terms: (s0, cs0) ', λ n. pcsf(n + 1)

Proof step 91 from proof repla-mon (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof repla-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  (s0, cs0) = pcsf(0), pcsf(n) ≠ (n = 0 ⊃ (s0, cs0);pcsf((n - 1) + 1)), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ a '[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s)

Proof step 93 from proof repla-mon (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 94:

  (s0, cs0) = pcsf(0), n ≠ 0, pcsf(n) ≠ pcsf((n - 1) + 1), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, λ n. paf(n + 1)), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), paf(0), (s0, cs0)), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜λ n. pcsf(n + 1)⌝ , ⌜paf(0) '⌝ + ⌜λ n. paf(n + 1)⌝ )) ⊑ aext !(aα), ¬ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0), ⌜as '⌝ + aσ, aα) ⌝ ⊑ ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + (λ n. pcsf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1), ⌜as '⌝ + aσ, aα) ⌝ , ∀ astart0, astep0, aext0, as0, aσ0, aα0, start0, cstart0, step0, cstep0, ren0, cren0, ext0, cext0, s0, cs0, pcsf0, paf0, aren0. ¬ frag(IOAut(astart0, astep0, aext0))(⌜as0 '⌝ + aσ0, aα0) ∨ ¬ fragω(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsf0, paf0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ cext0 !(πra(step0, cstep0, ren0, cren0, ⌜(s0, cs0) '⌝ + ⌜pcsf0⌝ , ⌜paf0⌝ )) ⊑ aext0 !(aα0) ∨ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0), paf0.take(n0), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊑ ⌜repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsf0.take(n0 + 1), paf0.take(n0 + 1), ⌜as0 '⌝ + aσ0, aα0)⌝ ⊦

Rule argument

Additional information

Proof step 94 from proof repla-mon (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, n1