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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

Proof step 2 from proof mon-pis (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])

Rule argument

Additional information

Used simplifier rules: pis-mon: ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n), paf.take(n + 1))⌝ ; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ ⌜n⌝ ≠ ∞; (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 ⊦ ⌜nf⌝ [n] = nf(n); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝

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

A spec-lemma