proposition: Lemma lengthTerms : forall (n : nat) (ts : Terms n), codeLength (codeTerms ts) = n.
proof: Proof. intros n ts; induction ts as [| n t ts Hrects]. - reflexivity. - replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. unfold codeLength, evalStrongRec, evalComposeFunc, evalOneParamList, evalList. set (A := fun n0 Hrecs : nat => switchPR n0 (S (codeNth (n0 - S (cPairPi2 (pred n0))) Hrecs)) 0). rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; unfold A at 1; rewrite evalStrongRecHelp1. + simpl; rewrite cPairProjections1, cPairProjections2. now f_equal. + generalize (cPair (codeTerm t) (codeTerms ts)). simpl; intros n0; apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 n0) (cPairPi2 n0)). * apply cPairLe2. * rewrite cPairProjections; apply le_n. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)