proposition: Lemma wellFormedFormulaCorrect1 : forall f : Formula, wellFormedFormula (codeFormula f) = 1.
proof: Proof. intros f; set (A := fun f recs : nat => switchPR (cPairPi1 f) (switchPR (pred (cPairPi1 f)) (switchPR (pred (pred (cPairPi1 f))) (switchPR (pred (pred (pred (cPairPi1 f)))) (charFunction 2 Nat.eqb (codeArityR (pred (pred (pred (pred (cPairPi1 f)))))) (S (codeLength (cPairPi2 f))) * wellFormedTerms (cPairPi2 f)) (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) (codeNth (f - S (cPairPi2 f)) recs)) (codeNth (f - S (cPairPi1 (cPairPi2 f))) recs * codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) (wellFormedTerm (cPairPi1 (cPairPi2 f)) * wellFormedTerm (cPairPi2 (cPairPi2 f)))). unfold wellFormedFormula; fold A; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; intros; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList in |- *; rewrite computeEvalStrongRecHelp; unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *; simpl in |- *; unfold A at 1 in |- *; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. - simpl; repeat rewrite wellFormedTermCorrect1; reflexivity. - simpl; rewrite wellFormedTermsCorrect1. rewrite codeArityRIsCorrect1. rewrite lengthTerms. rewrite Nat.eqb_refl; reflexivity. - rewrite evalStrongRecHelp1 with (m := codeFormula f0). + rewrite evalStrongRecHelp1 with (m := codeFormula f1). * simpl; now rewrite Hrecf1, Hrecf0. * eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe1. + eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. - rewrite evalStrongRecHelp1 with (m := codeFormula f). + simpl; assumption. + apply cPairLt2. - rewrite evalStrongRecHelp1 with (m := codeFormula f). + simpl; assumption. + eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)