Proof step 4 from proof monls-mon-implies-monls (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  mon(nσf), ∀ n. mon<(nσf(n)), ∀ n. nσf(n) ⊑ lim(nσf), ∀ m. ¬ # lim(nσf) < ⌜m⌝ → (∃ n. lim(nσf) to m ⊑ nσf(n)) ⊦ mon<(lim(nσf))

Rule argument

Additional information