proposition: Lemma wellFormedTermsCorrect1 (n : nat) (ts : Terms n): wellFormedTerms (codeTerms ts) = 1.
proof: Proof. set (A := fun t recs : nat => cPair (switchPR (cPairPi1 t) (charFunction 2 Nat.eqb (codeArityF (pred (cPairPi1 t))) (S (codeLength (cPairPi2 t))) * cPairPi2 (codeNth (t - S (cPairPi2 t)) recs)) 1) (switchPR t (cPairPi1 (codeNth (t - S (cPairPi1 (pred t))) recs) * cPairPi2 (codeNth (t - S (cPairPi2 (pred t))) recs)) 1)). induction ts as [| n t ts Hrects]. - unfold wellFormedTerms, wellFormedTermTerms; fold A. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1; unfold A; now rewrite cPairProjections2. - unfold wellFormedTerms, wellFormedTermTerms; fold A. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp; unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. unfold A at 1; rewrite cPairProjections1, cPairProjections2. replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. repeat rewrite evalStrongRecHelp1. + simpl; rewrite cPairProjections1, cPairProjections2. replace (cPairPi1 (evalStrongRec 0 A (codeTerm t))) with (wellFormedTerm (codeTerm t)). * rewrite (wellFormedTermCorrect1 t). unfold wellFormedTerms, wellFormedTermTerms in Hrects. unfold A; now rewrite Hrects. * reflexivity. + simpl; rewrite cPairProjections2. apply Nat.lt_succ_r. apply cPairLe2. + simpl; rewrite cPairProjections1; apply Nat.lt_succ_r. apply cPairLe1. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)