proposition: Lemma codeOpenCorrect (f : Formula): codeOpen (codeFormula f) = codeFormula (open f).
proof: Proof. unfold codeOpen, open; set (g := fun f recs : nat => switchPR (car f) (switchPR (pred (car f)) (switchPR (pred (pred (car f))) (switchPR (pred (pred (pred (car f)))) f (codeNth (f - S (cdr (cdr f))) recs)) f) f) f). induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl; unfold evalStrongRec. - simpl ; unfold g ; repeat rewrite cPairProjections1 || rewrite cPairProjections2; reflexivity. - simpl in |- *; unfold g at 1 in |- *; repeat rewrite cPairProjections1 || rewrite cPairProjections2; reflexivity. - simpl in |- *; unfold g at 1 in |- *; repeat rewrite cPairProjections1 || rewrite cPairProjections2; reflexivity. - simpl in |- *; unfold g at 1 in |- *; repeat rewrite cPairProjections1 || rewrite cPairProjections2; reflexivity. - unfold evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. unfold g at 1; repeat rewrite evalStrongRecHelp1. unfold pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. + simpl; apply Hrecf. + eapply Nat.le_lt_trans. * apply cPairLe2A. * rewrite cPairProjections2. apply cPairLt2. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)