proposition: Lemma Tprf2T'prf : forall f : Formula, SysPrf T f -> folProof.SysPrf LNN T' (LNT2LNN_formula f).
proof: Proof. intros f H; unfold T'. apply (folLogic.sysExtend LNN) with (fun x : fol.Formula LNN => mem (fol.Formula LNT) T (LNN2LNT_formula x)). - intros x H0; right; assumption. - induction H as [x [x0 H]]; exists (map LNT2LNN_formula x). induction x0 as [A| Axm1 Axm2 A B x0_1 Hrecx0_1 x0_0 Hrecx0_0| Axm A v n x0 Hrecx0| A B| A B C| A B| A v t| A v n| A B v| | | | R| f]; simpl. + exists (AXM LNN (LNT2LNN_formula A)). intros g H0; unfold mem, Ensembles.In. induction H0 as [H0| H0]. * rewrite <- H0; rewrite LNT2LNT_formula; apply H; auto with datatypes. * induction H0. + assert (H0: forall g : fol.Formula LNT, In g Axm1 -> mem (fol.Formula LNT) T g) by auto with datatypes. assert (H1: forall g : fol.Formula LNT, In g Axm2 -> mem (fol.Formula LNT) T g) by auto with datatypes. induction (Hrecx0_0 H1) as [x H2]. induction (Hrecx0_1 H0) as [x0 H3]. clear Hrecx0_0 Hrecx0_1 H0 H1. assert (H0: map LNT2LNN_formula (Axm1 ++ Axm2) = map LNT2LNN_formula Axm1 ++ map LNT2LNN_formula Axm2). { generalize Axm1 Axm2; intros. induction Axm0 as [| a Axm0 HrecAxm0]; simpl in |- *. reflexivity. rewrite HrecAxm0. reflexivity. } rewrite H0. exists (MP LNN (map LNT2LNN_formula Axm1) (map LNT2LNN_formula Axm2) (LNT2LNN_formula A) (LNT2LNN_formula B) x0 x). intros g H1; induction (in_app_or _ _ _ H1); auto. + induction (Hrecx0 H) as [x H0]. assert (H1: ~ In v (freeVarListFormula LNN (map LNT2LNN_formula Axm))). { clear x0 H Hrecx0 x H0. intros H; apply n; clear n. induction Axm as [| a Axm HrecAxm]. - auto. - simpl in H |- *; apply in_or_app. induction (in_app_or _ _ _ H). + left; rewrite <- (LNT2LNT_formula a). now apply LNN2LNT_freeVarF2. + auto. } exists (GEN LNN (map LNT2LNN_formula Axm) (LNT2LNN_formula A) v H1 x); auto. + exists (IMP1 LNN (LNT2LNN_formula A) (LNT2LNN_formula B)). tauto. + exists (IMP2 LNN (LNT2LNN_formula A) (LNT2LNN_formula B) (LNT2LNN_formula C)). tauto. + exists (CP LNN (LNT2LNN_formula A) (LNT2LNN_formula B)). tauto. + rewrite LNT2LNN_subFormula. exists (FA1 LNN (LNT2LNN_formula A) v (LNT2LNN_term t)). tauto. + rewrite <- LNT2LNN_freeVarF in n. exists (FA2 LNN (LNT2LNN_formula A) v n). tauto. + exists (FA3 LNN (LNT2LNN_formula A) (LNT2LNN_formula B) v). tauto. + exists (EQ1 LNN). tauto. + exists (EQ2 LNN). tauto. + exists (EQ3 LNN). tauto. + induction R. + induction f; simpl. * exists (EQ5 LNN Languages.Plus_). tauto. * exists (EQ5 LNN Languages.Times_). tauto. * exists (EQ5 LNN Languages.Succ_). tauto. * exists (EQ5 LNN Languages.Zero_). tauto. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith Lia) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(NNtheory) hydras.Ackermann(NN2PA) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)