enrich
   mon-lim-filter-count-old

with
   functions 
       max∞ : (Nat → Bool) → Natinf;
       leninv : Stream[Nat] → Natinf;
      comment: length of the inverse of a stuttering stream.;
   
   predicates 
       stutf : Stream[Nat];
       mon≤ : Stream[Nat];
       mon< : Stream[Nat];
   
   variables 
       np : Nat → Bool;
       nσ : Stream[Nat];
       n : Nat;
       m : Nat;
       nnf : Nat → Nat;
       nl : List[Nat];
       nσf : Nat → Stream[Nat];
       σf : Nat → Stream[A];
       nf : Nat → Nat;
       p : A → Bool;
       n∞ : Natinf;
   
   partial functions 
       min : Stream[Nat] × Nat → Nat with λ nσ, n. mon<(nσ);
      comment: defined for nonempty streams only.;
       inv : Stream[Nat] → Stream[Nat] with λ nσ. stutf(nσ);
      comment: inverse of a stuttering stream (strict monotonic).;
   
   axioms 
      maxinf-def: (max∞(np) = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(max∞(np).n)) ∧ (∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ ));
      comment: definition justified by theorem maxinf-skolemf;
      
      stutf-def: stutf(nσ) ↔ nσ ≠ [] ∧ nσ(0) = 0 ∧ (∀ n. ⌜n⌝  + ⌜1⌝  < # nσ → nσ(n + 1) = nσ(n) ∨ nσ(n + 1) = nσ(n) + 1);
      
      monle-def: mon≤(nσ) ↔ (∀ n. ⌜n⌝  + ⌜1⌝  < # nσ → nσ(n) ≤ nσ(n + 1));
      
      monls-def: mon<(nσ) ↔ (∀ n. ⌜n⌝  + ⌜1⌝  < # nσ → nσ(n) < nσ(n + 1));
      
      leninv-def: leninv(nσ) = max∞(λ n. n ≠ 0 → (∃ m. ⌜m⌝  < # nσ ∧ nσ(m) = n - 1 ∧ ¬(# nσ = ∞ ∧ (∀ m0. m < m0 → nσ(m0) = n - 1))));
      
      inv-def: 
        stutf(nσ)
      →   inv(nσ)
        = (leninv(nσ) = ∞
          ⊃ ⌜λ m. max∞(λ n. ⌜n⌝  < # nσ ∧ nσ(n) = m).n⌝ 
          ;⌜λ m. max∞(λ n. ⌜n⌝  < # nσ ∧ nσ(n) = m).n⌝ .take(leninv(nσ).n)
          );
      
      min-def: 
        mon<(nσ)
      → (nσ = []
        ⊃ min(nσ, n) = 0
        ;(# nσ ≠ ∞ ∧ nσ((# nσ).n - 1) < n
         ⊃ min(nσ, n) = (# nσ).n
         ;⌜min(nσ, n)⌝  < # nσ ∧ n ≤ nσ(min(nσ, n)) ∧ (∀ m. ⌜m⌝  < # nσ ∧ n ≤ nσ(m) → min(nσ, n) ≤ m)
         )
        );
      comment: Skolem function justified by theorems min-skolemf;
   
   
end enrich