proposition: Lemma codeInCorrect (a : nat) (l : list nat) : codeIn a (codeList l) = match In_dec eq_nat_dec a l with | left _ => 1 | right _ => 0 end.
proof: Proof. induction l as [| a0 l Hrecl]; simpl in |- *. - unfold codeIn, evalStrongRec; simpl; now rewrite cPairProjections1. - unfold codeIn, evalStrongRec; unfold evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp. unfold evalList in |- *. set (f := fun n Hrecs p1 : nat => switchPR n (switchPR (charFunction 2 Nat.eqb (cPairPi1 (pred n)) p1) 1 (codeNth (n - S (cPairPi2 (pred n))) Hrecs)) 0) in *. set (m := cPairPi2 (pred (S (cPair a0 (codeList l))))) in *. set (n := S (cPair a0 (codeList l))) in *. simpl in |- *. repeat rewrite cPairProjections1. destruct (eq_nat_dec a0 a) as [a1 | b]. + rewrite a1, Nat.eqb_refl; reflexivity. + rewrite nat_eqb_false; simpl. assert (H: extEqual _ (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 f n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 f m)). { apply (evalStrongRecHelp2 1). unfold m, n; simpl. rewrite cPairProjections2. apply Compat815.le_lt_n_Sm. apply cPairLe2. } simpl in H; rewrite H. unfold codeIn in Hrecl. move f after Hrecl; fold f in Hrecl. unfold m, n in |- *. simpl in |- *. rewrite cPairProjections2. rewrite Hrecl. clear H f Hrecl. induction (In_dec eq_nat_dec a l) as [a1 | ?]; try reflexivity. assumption. Qed.
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)