proposition: Lemma computeEvalStrongRecHelp : forall (n : nat) (f : naryFunc n.+2) (c : nat), evalStrongRecHelp n f c.+1 = compose2 n (evalStrongRecHelp n f c) (fun a0 : nat => evalComposeFunc n 2 (Vector.cons (naryFunc n) (f c a0) 1 (Vector.cons (naryFunc n) (evalConstFunc n a0) 0 (Vector.nil (naryFunc n)))) (fun a1 b0 : nat => S (cPair a1 b0))).
proof: Proof. intros n f c; unfold evalStrongRecHelp at 1 in |- *; simpl in |- *. fold (naryFunc n) in |- *. induction (eq_nat_dec n n.+1). - destruct (neq_succ_diag_r n a). - induction (eq_nat_dec n n). + replace (evalPrimRecFunc n (evalComposeFunc n 0 (Vector.nil (naryFunc n)) 0) (fun a0 a1 : nat => evalComposeFunc n 2 (Vector.cons (naryFunc n) (f a0 a1) 1 (Vector.cons (naryFunc n) (evalConstFunc n a1) 0 (Vector.nil (naryFunc n)))) (fun a2 b0 : nat => (cPair a2 b0).+1)) c) with (evalStrongRecHelp n f c). reflexivity. unfold evalStrongRecHelp at 1 in |- *. simpl in |- *. fold (naryFunc n) in |- *. induction (eq_nat_dec n n.+1). elim b; auto. induction (eq_nat_dec n n). * reflexivity. * elim b1; auto. + elim b0; auto. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction