proposition: Lemma codePAcorrect1 (f : Formula): codePA (codeFormula f) = true -> mem Formula PA f.
proof: Proof. intros H; destruct (PAdec f) as [H0 | H0]. - assumption. - unfold codePA, orRel, nat_rec, nat_rect in H. unfold PA; destruct (eq_nat_dec (codeFormula PA6) (codeFormula f)) as [a | b]. + rewrite a, Nat.eqb_refl in H. replace f with PA6. * right; constructor. * eapply codeFormulaInj; apply a. + left; rewrite nat_eqb_false in H. * clear b. destruct (eq_nat_dec (codeFormula PA5) (codeFormula f)) as [a | b]. -- rewrite a, Nat.eqb_refl in H. replace f with PA5. ++ right; constructor. ++ eapply codeFormulaInj; apply a. -- left. rewrite nat_eqb_false in H. ++ clear b; destruct (eq_nat_dec (codeFormula PA4) (codeFormula f)) as [a | b]. ** rewrite a in H. rewrite Nat.eqb_refl in H. replace f with PA4. right; constructor. eapply codeFormulaInj. apply a. ** left. rewrite nat_eqb_false in H. clear b. induction (eq_nat_dec (codeFormula PA3) (codeFormula f)) as [a | b]. rewrite a in H. rewrite Nat.eqb_refl in H. replace f with PA3. right; constructor. eapply codeFormulaInj. apply a. left. rewrite nat_eqb_false in H. clear b. induction (eq_nat_dec (codeFormula PA2) (codeFormula f)) as [a | b]. rewrite a, Nat.eqb_refl in H. replace f with PA2. right; constructor. eapply codeFormulaInj. apply a. left. rewrite nat_eqb_false in H. clear b. induction (eq_nat_dec (codeFormula PA1) (codeFormula f)) as [a | b]. rewrite a, Nat.eqb_refl in H. replace f with PA1. right; constructor. eapply codeFormulaInj. apply a. left. rewrite nat_eqb_false in H. apply codeInductionSchemaCorrect2. simpl in H. assumption. assumption. assumption. assumption. assumption. ++ assumption. * assumption. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)