proposition: Lemma codeNoDupCorrect (l : list nat) : codeNoDup (codeList l) = codeList (List.nodup eq_nat_dec l).
proof: Proof. unfold codeNoDup; set (g := fun l0 recs : nat => switchPR l0 (switchPR (codeIn (cPairPi1 (pred l0)) (codeNth (l0 - S (cPairPi2 (pred l0))) recs)) (codeNth (l0 - S (cPairPi2 (pred l0))) recs) (S (cPair (cPairPi1 (pred l0)) (codeNth (l0 - S (cPairPi2 (pred l0))) recs)))) 0) in *. induction l as [| a l Hrecl]. - simpl in |- *. unfold evalStrongRec; simpl; now rewrite cPairProjections1. - simpl; unfold evalStrongRec; unfold evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *. unfold g at 1 in |- *. repeat rewrite evalStrongRecHelp1; unfold pred in |- *. repeat rewrite cPairProjections1 || rewrite cPairProjections2. + rewrite Hrecl; rewrite codeInCorrect. destruct (In_dec Nat.eq_dec a (List.nodup Nat.eq_dec l)). destruct (in_dec Nat.eq_dec a l). * reflexivity. * rewrite nodup_In in i; contradiction. * destruct (in_dec Nat.eq_dec a l). -- rewrite nodup_In in n. contradiction. -- reflexivity. + simpl; apply Compat815.le_lt_n_Sm. apply cPairLe2A. Qed.
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)