fact: Fixpoint comp_limit (r : rseq) (env : list Rseq_with_limit) : option rseq_limit := match r with | rseq_cst r => Return (finite r) | rseq_var n => Bind (nth_error env n) (fun x => Return (proj1_sig (projT2 x))) | rseq_opp r => Bind (comp_limit r env) (fun l => Some (rseq_limit_opp l)) | rseq_plus rl rr => Bind (comp_limit rl env) (fun ll => Bind (comp_limit rr env) (fun lr => rseq_limit_add ll lr)) | rseq_minus rl rr => Bind (comp_limit rl env) (fun ll => Bind (comp_limit rr env) (fun lr => rseq_limit_add ll (rseq_limit_opp lr))) end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics