proposition: Lemma evalStrongRecHelp2 : forall (a : nat) (f : naryFunc a.+2) (n m : nat), m < n -> extEqual _ (evalComposeFunc _ 1 (Vector.cons _ (evalStrongRecHelp _ f n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - m.+1) b)) (evalStrongRec _ f m).
proof: Proof. intro a; fold (naryFunc a) in |- *. induction a as [| a Hreca]. - simpl in |- *. apply evalStrongRecHelp1. - simpl in |- *. intros f n m H c; fold (naryFunc a) in |- *. set (g := fun x y : nat => f x y c) in *. assert (H0: extEqual a (evalComposeFunc a 1 (Vector.cons (naryFunc a) (evalStrongRecHelp a g n) 0 (Vector.nil (naryFunc a))) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec a g m)) by (apply Hreca; auto). unfold g in H0; clear g Hreca. apply extEqualTrans with (evalStrongRec a (fun x y : nat => f x y c) m). + apply extEqualTrans with (evalComposeFunc a 1 (Vector.cons (naryFunc a) (evalStrongRecHelp a (fun x y : nat => f x y c) n) 0 (Vector.nil (naryFunc a))) (fun b : nat => codeNth (n - S m) b)). * apply extEqualCompose; unfold extEqualVector in |- *. simpl in |- *; repeat split. apply evalStrongRecHelpParam. apply extEqualRefl. * apply H0. + unfold evalStrongRec in |- *; simpl in |- *. fold (naryFunc a) in |- *; apply extEqualCompose. unfold extEqualVector in |- *; simpl in |- *; repeat split. * apply extEqualSym. apply evalStrongRecHelpParam. * apply extEqualRefl. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction