fact: Fixpoint addInterAux (Ar1 Ar2 : rArray vM) (L : list rZ) {struct L} : rArray vM -> rArray vM * list rZ := fun Ar3 : rArray vM => match L with | nil => (Ar3, nil) | a :: L1 => match addInterAux Ar1 Ar2 L1 Ar3 with | (Ar3', L2) => match addEqMem Ar3' (rZPlus (valRz a)) (getEquivMin Ar1 Ar2 (valRz a)) with | triple Ar3'' b L2' => (Ar3'', appendRz L2 L2') end end end.
imports: Stalmarck(rZ) Stalmarck(OrderedListEq) Stalmarck(LetP) Coq(Relation_Definitions) Stalmarck(state) Stalmarck(restrictState) Stalmarck(ltState)