fact: Fixpoint prog_map (Val: Set)(p: Prog Val)(n: NId)(c: Clock): Prog (InstValRec Val) := match p with | put _ k v p => put _ k (inst_val _ n (c + 1) v) (prog_map _ p n (c + 1)) | get _ k p => get _ k (fun v => prog_map _ (p (inst_val_val _ v)) n c) | skip _ => skip _ | fault _ => fault _ end.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)