proposition: Lemma codeFreeVarTermCorrect (t: Term) : codeFreeVarTerm (codeTerm t) = codeList (freeVarT t).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => codeFreeVarTerms (codeTerms ts) = codeList (freeVarTs ts)); intros. - simpl; unfold codeTerm, codeFreeVarTerm, codeFreeVarTermTerms, evalStrongRec in |- *. simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. simpl; reflexivity. - unfold freeVarT; fold (freeVarTs t0). rewrite <- H; clear H. unfold codeTerm; fold (codeTerms t0). generalize (codeTerms t0). intros n; unfold codeFreeVarTerm, codeFreeVarTermTerms. set (g := fun t1 recs : nat => cPair (switchPR (car t1) (cdr (codeNth (t1 - S (cdr t1)) recs)) (S (cPair (cdr t1) 0))) (switchPR t1 (codeApp (car (codeNth (t1 - S (car (pred t1))) recs)) (cdr (codeNth (t1 - S (cdr (pred t1))) recs))) 0)). unfold evalStrongRec, evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp. unfold compose2 in |- *. unfold evalComposeFunc in |- *. unfold g at 1 in |- *. repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold codeF. rewrite (evalStrongRecHelp1 g (cPair (S (cf f)) n) n). + simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold codeFreeVarTerms; unfold codeFreeVarTermTerms. fold g; reflexivity. + apply cPairLt2. - simpl; unfold codeTerms, codeFreeVarTerms, codeFreeVarTermTerms. unfold evalStrongRec; simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - unfold freeVarTs; fold (freeVarT t0); fold (freeVarTs t1); rewrite <- codeAppCorrect. rewrite <- H; rewrite <- H0; clear H H0. unfold codeTerms. fold (codeTerm t0); fold (codeTerms t1). generalize (codeTerm t0) (codeTerms t1). clear t0 t1. intros n0 n1; unfold codeFreeVarTerms at 1 in |- *. unfold codeFreeVarTermTerms in |- *. 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)) in *. 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 Compat815.le_lt_n_Sm. apply cPairLe1. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)