fact: Fixpoint mi_of_term k (t : bterm k) : mint (S k) := match t with | BVar ip => let zero_int := Vconst (zero_matrix dim dim) (S k) in let args_int := Vreplace zero_int (le_lt_S ip) (id_matrix dim) in mkMatrixInt (@zero_vec dim) args_int | BFun f v => let f_int := trsInt f in let args_int := Vmap (@mi_of_term k) v in let args_int' := Vmap2 (@mat_matrixInt_prod (S k)) (args f_int) args_int in let res_const := add_vectors (Vcons (const f_int) (Vmap (@const A matrix dim (S k)) args_int')) in let res_args := combine_matrices (Vmap (@args A matrix dim (S k)) args_int') in mkMatrixInt res_const res_args end.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)