proposition: Lemma codeSubTermsCorrect : forall (n : nat) (ts : Terms n) (v : nat) (s : Term), codeSubTerms (codeTerms ts) v (codeTerm s) = codeTerms (substTs ts v s).
proof: Proof. set (g := fun t0 recs v0 s0 : nat => cPair (switchPR (car t0) (cPair (car t0) (cdr (codeNth (t0 - S (cdr t0)) recs))) (switchPR (charFunction 2 Nat.eqb (cdr t0) v0) s0 t0)) (switchPR t0 (S (cPair (car (codeNth (t0 - S (car (pred t0))) recs)) (cdr (codeNth (t0 - S (cdr (pred t0))) recs)))) 0)). intros n ts v s; induction ts as [| n t ts Hrects]. - simpl; unfold codeTerms, codeSubTerms, codeSubTermTerms, evalStrongRec. simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - simpl; transitivity (S (cPair (codeTerm (substT t v s)) (codeTerms (substTs ts v s)))). + rewrite <- Hrects, <- codeSubTermCorrect. replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))). * generalize (codeTerm t) (codeTerms ts). clear Hrects ts t n; intros n n0. unfold codeSubTerms at 1; unfold codeSubTermTerms; fold g. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. unfold pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g at 1; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. assert (H: extEqual _ (evalComposeFunc 2 1 (Vector.cons _ (evalStrongRecHelp 2 g (S (cPair n n0))) 0 (Vector.nil _)) (fun b : nat => codeNth (S (cPair n n0) - S n) b)) (evalStrongRec 2 g n)). { apply (evalStrongRecHelp2 2). apply Compat815.le_lt_n_Sm. apply cPairLe1. } simpl in H; rewrite H; clear H. assert (H: extEqual _ (evalComposeFunc 2 1 (Vector.cons _ (evalStrongRecHelp 2 g (S (cPair n n0))) 0 (Vector.nil _)) (fun b : nat => codeNth (S (cPair n n0) - S n0) b)) (evalStrongRec 2 g n0)). { apply (evalStrongRecHelp2 2). apply Compat815.le_lt_n_Sm. apply cPairLe2. } simpl in H; rewrite H; clear H. simpl; reflexivity. * reflexivity. + reflexivity. Qed.
imports: hydras.Ackermann(primRec cPair folProp code extEqualNat) Coq(Arith) hydras(Compat815) NewNotations