proposition: Lemma primRecRepresentable1 : forall (n : nat) (f : PrimRec n), Representable n (evalPrimRec n f) (primRecFormula n f).
proof: Proof. intros n f. elim f using PrimRec_PrimRecs_ind with (P0 := fun (n m : nat) (fs : PrimRecs n m) => RepresentablesHelp n m (primRecsFormula n m fs) /\ extEqualVector _ _ (FormulasToFuncs n m (primRecsFormula n m fs)) (evalPrimRecs n m fs) /\ Vector.t_rect (Formula * naryFunc n) (fun _ _ => Prop) True (fun (pair : Formula * naryFunc n) (m : nat) (v : Vector.t _ m) (rec : Prop) => (forall v : nat, In v (freeVarF (fst pair)) -> v <= n) /\ rec) m (primRecsFormula n m fs)). - apply succRepresentable. - apply zeroRepresentable. - intros n0 m l; simpl; apply projRepresentable. - simpl; intros n0 m g H h H0. decompose record H /r; intros H1 H3 H4. assert (H2: Representable n0 (evalComposeFunc n0 m (FormulasToFuncs n0 m (primRecsFormula n0 m g)) (evalPrimRec m h)) (composeSigmaFormula n0 n0 m (primRecsFormula n0 m g) (primRecFormula m h))) by (apply composeSigmaRepresentable; auto). induction H2 as (H2, H5); split. + assumption. + apply Representable_ext with (evalComposeFunc n0 m (FormulasToFuncs n0 m (primRecsFormula n0 m g)) (evalPrimRec m h)). * apply extEqualCompose. -- assumption. -- apply extEqualRefl. * assumption. - simpl in |- *. intros n0 g H h H0. apply primRecSigmaRepresentable; auto. - simpl; tauto. - simpl; intros n0 m p H p0 H0. decompose record H0 /r; intros H1 H3 H4; clear H0. repeat split; auto. + destruct H as [H H0]; auto. + apply extEqualRefl. + destruct H; auto. Qed.
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)