enrich
   streamseq-mon-lim
with
   functions 
       lift : (List[A] → Bool) → Stream[A] → Bool;
      comment: lifts predicate on lists to predicate on streams;
       lift : (List[S] × List[A] → Bool) → Stream[S] × Stream[A] → Bool;
      comment: lifts predicate on pair of lists to predicate on streams;
       pcont : (Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool;
      comment: continuous function on a subset of streams;
       pcont : (Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool;
      comment: continuous function on a subset of traces;
       pmon : (Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool;
      comment: monotone function on a subset of streams;
       pmon : (List[A] → Bool) → (List[A] → List[B]) → Bool;
      comment: monotone function on a subset of lists;
       pmon : (Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool;
      comment: monotone function on a subset of all pairs of streams;
       pmon : (List[S] × List[A] → Bool) → (List[S] × List[A] → List[B]) → Bool;
      comment: monotone function on a subset of streams;
       ppbd : (Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool;
      comment: preservesboundedness on a subset of streams;
       ppbd : (Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool;
      comment: preservesboundedness on a subset of streams;
       lifted : (List[A] → Bool) → (List[A] → List[B]) × (Stream[A] → Stream[B]) → Bool;
      comment: on a subset of lists, continuous stream function is a lifted version of the monotone list function;
       lifted : (List[S] × List[A] → Bool) → (List[S] × List[A] → List[B]) × (Stream[S] × Stream[A] → Stream[B]) → Bool;
      comment: on a subset of traces, continuous stream function is a lifted version of the monotone list function;
   
   predicates 
       mon : (Stream[A] → Stream[B]);
      comment: monotone function on streams;
       mon : (Stream[S] × Stream[A] → Stream[B]);
      comment: monotone function on a pair of streams;
       mon : (List[A] → List[B]);
      comment: monotone function on lists;
       pbd : (Stream[A] → Stream[B]);
      comment: preservesboundedness;
       pbd : (Stream[S] × Stream[A] → Stream[B]);
      comment: preservesboundedness on a pairs of streams;
       cont : (Stream[A] → Stream[B]);
      comment: continuous function;
       cont : (Stream[S] × Stream[A] → Stream[B]);
      comment: continuous function on traces;
       mon : (List[S] × List[A] → List[B]);
      comment: monontone when the list of states is always one bigger than the list of actions;
       pfxclosed : (Stream[A] → Bool);
      comment: a prefix-closed set of streams;
       pfxclosed : (List[A] → Bool);
      comment: a prefix-closed set of lists;
       pfxclosed : (Stream[S] × Stream[A] → Bool);
      comment: a prefix-closed set of streams;
       pfxclosed : (List[S] × List[A] → Bool);
      comment: a prefix-closed set of lists;
   
   variables 
       f : Stream[A] → Stream[B];
       lf : List[A] → List[B];
       al : List[A];
       sl : List[S];
       a : A;
       af : Nat → A;
       sf : Nat → S;
       bl : List[B];
       bf : Nat → B;
       b : B;
       α : Stream[A];
       β : Stream[B];
       n : Nat;
       m : Nat;
       σ : Stream[S];
       αf : Nat → Stream[A];
       alf : Nat → List[A];
       σf : Nat → Stream[S];
       trf : List[S] × List[A] → List[B];
       βf : Stream[S] × Stream[A] → Stream[B];
       αp : Stream[A] → Bool;
       alp : List[A] → Bool;
       trp : Stream[S] × Stream[A] → Bool;
       trlp : List[S] × List[A] → Bool;
       slf : Nat → List[S];
   
   partial functions 
       lift : (List[A] → List[B]) → Stream[A] → Stream[B] with λ lf. λ α. mon(lf);
      comment: lifts a monotone function on lists to a continuous one on streams;
       lift : (List[S] × List[A] → List[B]) → Stream[S] × Stream[A] → Stream[B] with λ trf. λ σ, α. mon(trf);
      comment: lifts a monotone function on two lists to a continuous one on two streams;
   
   axioms 
      lifted-def: lifted(alp)(lf, f) ↔ (∀ α. lift(alp)(α) → lift(lf)(α) = f(α));
      used for: s, ls;
      
      liftedtr-def: lifted(trlp)(trf, βf) ↔ (∀ σ, α. lift(trlp)(σ, α) → lift(trf)(σ, α) = βf(σ, α));
      used for: s, ls;
      
      pfxclosed-def: pfxclosed(αp) ↔ (∀ α1, α2. αp(α2) ∧ α1 ⊑ α2 → αp(α1));
      
      pfxclosedl-def: pfxclosed(alp) ↔ (∀ al1, al2. alp(al2) ∧ al1 ⊑ al2 → alp(al1));
      
      pdfclosedtr-def: 
      pfxclosed(trp) ↔ (∀ σ1, σ2, α1, α2. trp(σ2, α2) ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ # σ1 = # α1 + ⌜1⌝  ∧ # σ2 = # α2 + ⌜1⌝  → trp(σ1, α1));
      
      pdfclosedtrl-def: 
        pfxclosed(trlp)
      ↔ (∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1));
      
      lift-pred-fin: lift(alp)(⌜al⌝ ) ↔ alp(al);
      used for: s, ls;
      
      lift-pred-inf: lift(alp)(⌜af⌝ ) ↔ (∀ n. alp(af.take(n)));
      used for: s, ls;
      
      lift-trp-fin: lift(trlp)(⌜sl⌝ , ⌜al⌝ ) ↔ trlp(sl, al);
      used for: s, ls;
      
      lift-not-trp-fininf: ¬ lift(trlp)(⌜sl⌝ , ⌜af⌝ );
      used for: s, ls;
      
      lift-not-trp-inffin: ¬ lift(trlp)(⌜sf⌝ , ⌜al⌝ );
      used for: s, ls;
      
      lift-trp-inf: lift(trlp)(⌜sf⌝ , ⌜af⌝ ) ↔ (∀ n. trlp(sf.take(n + 1), af.take(n)));
      used for: s, ls;
      
      montrl-def: 
      mon(trf) ↔ (∀ sl1, al1, sl2, al2. # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 ∧ al1 ⊑ al2 ∧ sl1 ⊑ sl2 → trf(sl1, al1) ⊑ trf(sl2, al2));
      
      montrl-relative-def: 
        pmon(trlp)(trf)
      ↔ (∀ sl1, al1, sl2, al2. 
             # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 ∧ al1 ⊑ al2 ∧ sl1 ⊑ sl2 ∧ trlp(sl1, al1) ∧ trlp(sl2, al2)
           → trf(sl1, al1) ⊑ trf(sl2, al2));
      
      montr-def: mon(βf) ↔ (∀ σ1, α1, σ2, α2. # σ1 = # α1 + ⌜1⌝  ∧ # σ2 = # α2 + ⌜1⌝  ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 → βf(σ1, α1) ⊑ βf(σ2, α2));
      used for: ls;
      
      montr-relative-def: 
        pmon(trp)(βf)
      ↔ (∀ σ1, α1, σ2, α2. 
           # σ1 = # α1 + ⌜1⌝  ∧ # σ2 = # α2 + ⌜1⌝  ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ trp(σ1, α1) ∧ trp(σ2, α2) → βf(σ1, α1) ⊑ βf(σ2, α2));
      used for: ls;
      
      monl-def: mon(lf) ↔ (∀ al1, al2. al1 ⊑ al2 → lf(al1) ⊑ lf(al2));
      
      monl-relative-def: pmon(alp)(lf) ↔ (∀ al1, al2. alp(al1) ∧ alp(al2) ∧ al1 ⊑ al2 → lf(al1) ⊑ lf(al2));
      
      mon-def: mon(f) ↔ (∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2));
      used for: ls;
      
      mon-relative-def: pmon(αp)(f) ↔ (∀ α1, α2. αp(α1) ∧ αp(α2) ∧ α1 ⊑ α2 → f(α1) ⊑ f(α2));
      used for: ls;
      
      cont-def: cont(f) ↔ mon(f) ∧ pbd(f);
      used for: ls;
      
      cont-relative-def: pcont(αp)(f) ↔ pmon(αp)(f) ∧ ppbd(αp)(f);
      used for: ls;
      
      conttr-def: cont(βf) ↔ mon(βf) ∧ pbd(βf);
      used for: ls;
      
      conttr-relative-def: pcont(trp)(βf) ↔ pmon(trp)(βf) ∧ ppbd(trp)(βf);
      used for: ls;
      
      pbd-def: pbd(f) ↔ (∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ );
      
      pbd-relative-def: ppbd(αp)(f) ↔ (∀ af, bl. αp(⌜af⌝ ) → ((∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ ));
      
      pbdtr-def: pbd(βf) ↔ (∀ sf, af, bl. (∀ n. βf(⌜sf.take(n + 1)⌝ , ⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ βf(⌜sf⌝ , ⌜af⌝ ) ⊑ ⌜bl⌝ );
      
      pbdtr-relative-def: 
      ppbd(trp)(βf) ↔ (∀ sf, af, bl. trp(⌜sf⌝ , ⌜af⌝ ) → ((∀ n. βf(⌜sf.take(n + 1)⌝ , ⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ βf(⌜sf⌝ , ⌜af⌝ ) ⊑ ⌜bl⌝ ));
      
      lift-fin: lift(lf)(⌜al⌝ ) = ⌜lf(al)⌝ ;
      used for: s, ls;
      
      lift-inf: lift(lf)(⌜af⌝ ) = lim(⌜λ n. ⌜lf(af.take(n))⌝ ⌝ );
      used for: s, ls;
      
      lifttr-fin: lift(trf)(⌜sl⌝ , ⌜al⌝ ) = ⌜trf(sl, al)⌝ ;
      used for: s, ls;
      
      lifttr-inf: lift(trf)(⌜sf⌝ , ⌜af⌝ ) = lim(⌜λ n. ⌜trf(sf.take(n + 1), af.take(n))⌝ ⌝ );
      used for: s, ls;
   
   theorems 
      lift-pcont: pmon(alp)(lf) → pcont(lift(alp))(lift(lf));
      
      lifttr-pcont: pmon(trlp)(trf) → pcont(lift(trlp))(lift(trf));
      
      lift-cont: mon(lf) → cont(lift(lf));
      
      lifttr-cont: mon(trf) → cont(lift(trf));
      
      monl-equiv: mon(lf) ↔ (∀ af. mon(⌜λ n. ⌜lf(af.take(n))⌝ ⌝ ));
      
      cont-thm: cont(f) ∧ mon(⌜αf⌝ ) → lim(⌜λ n. f(αf(n))⌝ ) = f(lim(⌜αf⌝ ));
      
      montrl-equiv: mon(trf) ↔ (∀ sf, af. mon(⌜λ n. ⌜trf(sf.take(n + 1), af.take(n))⌝ ⌝ ));
      
      conttr-thm: 
      cont(βf) ∧ mon(⌜σf⌝ ) ∧ mon(⌜αf⌝ ) ∧ (∀ n. # σf(n) = # αf(n) + ⌜1⌝ ) → lim(⌜λ n. βf(σf(n), αf(n))⌝ ) = βf(lim(⌜σf⌝ ), lim(⌜αf⌝ ));
   
   
end enrich