fact: Fixpoint primRecFormula (n : nat) (f : PrimRec n) {struct f} : Formula := match f with | succFunc => succFormula | zeroFunc => zeroFormula | projFunc n m _ => projFormula m | composeFunc n m g h => composeSigmaFormula n n m (primRecsFormula n m g) (primRecFormula m h) | primRecFunc n g h => primRecSigmaFormula n (primRecFormula n g) (primRecFormula (S (S n)) h) end with primRecsFormula (n m : nat) (fs : PrimRecs n m) {struct fs} : Vector.t (Formula * naryFunc n) m := match fs in (PrimRecs n m) return (Vector.t (Formula * naryFunc n) m) with | PRnil n => Vector.nil _ | PRcons n m f fs' => Vector.cons (Formula * naryFunc n) (primRecFormula n f, evalPrimRec n f) m (primRecsFormula n m fs') end.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)