fact: Fixpoint comp_rseq (r : rseq) (env : list Rseq_with_limit) := match r with | rseq_cst r => Return (Rseq_constant r) | rseq_var n => Bind (nth_error env n) (fun un => Some (projT1 un)) | rseq_opp r => Bind (comp_rseq r env) (fun un => Some (Rseq_opp un)) | rseq_plus rl rr => Bind (comp_rseq rl env) (fun un => Bind (comp_rseq rr env) (fun vn => Some (Rseq_plus un vn))) | rseq_minus rl rr => Bind (comp_rseq rl env) (fun un => Bind (comp_rseq rr env) (fun vn => Some (Rseq_minus un vn))) end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics