Proof step 1 from proof mon-repla (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α), ¬ mon(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ ) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ mon(σσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ[n] ⊑ σσ[n + 1])

• 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α), ∃ n. ¬ ( ⌜n⌝ + ⌜1⌝ < # ⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ → ⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ [n] ⊑ ⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ [n + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. ⌜repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα) ⌝ ⌝

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

A spec-lemma

Proof step 4 from proof mon-repla (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(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: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ a + σ = ⌜a '⌝ + σ; (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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ 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 + σ = ⌜a '⌝ + σ; (s) ⊦ a + x = a ' + x; (s) Used terms: aren, ren, ext, s, as, astep, paf, n, astart, step, aext, cstart, cren, cstep, aα, start, aσ, pcsf, cext, cs

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

Lemma repla-mon