proposition: Lemma wellFormedTermCorrect1 : forall t : Term, wellFormedTerm (codeTerm t) = 1.
proof: Proof. intros t; 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)). elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => wellFormedTerms (codeTerms ts) = 1); simpl. - intro n; unfold codeTerm, wellFormedTerm, wellFormedTermTerms. fold A; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; unfold A at 1; repeat rewrite cPairProjections1; simpl; reflexivity. - intros f t0 H; replace (codeTerm (apply f t0)) with (cPair (S (cf f)) (codeTerms t0)); [ idtac | reflexivity ]. unfold wellFormedTerm, wellFormedTermTerms; fold A. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; unfold A at 1. repeat rewrite cPairProjections1. rewrite evalStrongRecHelp1. simpl; rewrite codeArityFIsCorrect1, cPairProjections2; simpl. rewrite lengthTerms, Nat.eqb_refl; simpl. rewrite Nat.add_comm; simpl; apply H. rewrite cPairProjections2; apply cPairLt2. - 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. - intros n t0 H t1 H0; unfold wellFormedTerms, wellFormedTermTerms. fold A; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; unfold A at 1; rewrite cPairProjections1; rewrite cPairProjections2. replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. repeat rewrite evalStrongRecHelp1. + simpl; rewrite cPairProjections1. rewrite cPairProjections2. unfold wellFormedTerm, wellFormedTermTerms in H. unfold A; rewrite H. unfold wellFormedTerms, wellFormedTermTerms in H0; rewrite H0. 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)