proposition: Lemma codeFreeVarTermsCorrect (n : nat) (ts : Terms n): codeFreeVarTerms (codeTerms ts) = codeList (freeVarTs ts).
proof: Proof. induction ts as [| n t ts Hrects]. - simpl; unfold codeTerms, codeFreeVarTerms, codeFreeVarTermTerms. unfold evalStrongRec; simpl. repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - unfold freeVarTs; fold (freeVarT t); fold (freeVarTs ts). rewrite <- codeAppCorrect. rewrite <- Hrects. rewrite <- codeFreeVarTermCorrect; clear Hrects. unfold codeTerms; fold (codeTerm t); fold (codeTerms ts). generalize (codeTerm t) (codeTerms ts). clear t ts. intros n0 n1; unfold codeFreeVarTerms at 1; unfold codeFreeVarTermTerms. unfold evalStrongRec in |- *. set (g := fun t0 recs : nat => cPair (switchPR (car t0) (cdr (codeNth (t0 - S (cdr t0)) recs)) (S (cPair (cdr t0) 0))) (switchPR t0 (codeApp (car (codeNth (t0 - S (car (pred t0))) recs)) (cdr (codeNth (t0 - S (cdr (pred t0))) recs))) 0)). unfold evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc; unfold g at 1. + rewrite (evalStrongRecHelp1 g (S (cPair n0 n1)) (car (pred (S (cPair n0 n1))))). * rewrite (evalStrongRecHelp1 g (S (cPair n0 n1)) (cdr (pred (S (cPair n0 n1))))). -- simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. -- simpl; rewrite cPairProjections2. apply Compat815.le_lt_n_Sm. apply cPairLe2. * simpl; rewrite cPairProjections1. apply Nat.lt_succ_r. apply cPairLe1. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)