proposition: Lemma T'prf2Tprf : forall f : fol.Formula LNN, folProof.SysPrf LNN T' f -> SysPrf T (LNN2LNT_formula f).
proof: Proof. assert (freeVarPA : forall x : Formulas, (forall g : fol.Formula LNT, In g x -> mem (fol.Formula LNT) PA g) -> forall v : nat, In v (freeVarListFormula LNT x) -> False). { intros x H v H0; induction x as [| a x Hrecx]. - apply H0. - simpl in H0; induction (in_app_or _ _ _ H0) as [H1 | H1]. + apply (closedPA v); exists a; auto with datatypes. + auto with datatypes. } intros f [x [x0 H]]; unfold SysPrf, folProof.SysPrf. assert (H0: exists Axm : fol.Formulas LNT, (forall v : nat, In v (freeVarListFormula _ Axm) -> In v (freeVarListFormula _ x)) /\ ex (fun _ : Prf LNT Axm (LNN2LNT_formula f) => forall g : fol.Formula LNT, In g Axm -> mem (fol.Formula LNT) T g)). { 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. - assert (H0: mem (fol.Formula LNN) T' A) by auto with datatypes. repeat induction H0. + exists (PA1 :: nil); split. * auto. * exists (AXM _ PA1); intros g H0. apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0. repeat (right; constructor) || left. -- elim H0. + exists (PA2 :: nil); split. * auto. * exists (AXM _ PA2); intros g H0; apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0. repeat (right; constructor) || left. -- elim H0. + exists (PA3 :: nil); split. * auto. * exists (AXM _ PA3); intros g H0; apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0; repeat (right; constructor) || left. -- elim H0. + exists (PA4 :: nil); split. * auto. * exists (AXM _ PA4); intros g H0; apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0. repeat (right; constructor) || left. -- elim H0. + exists (PA5 :: nil); split. * auto. * exists (AXM _ PA5); intros g H0; apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0. repeat (right; constructor) || left. -- elim H0. + exists (PA6 :: nil); split. * auto. * exists (AXM _ PA6); intros g H0; apply extendsPA. induction H0 as [H0| H0]. -- rewrite <- H0; repeat (right; constructor) || left. -- elim H0. + assert (H0: SysPrf PA (LNN2LNT_formula NN7)) by apply NN72PA. induction H0 as [x [x0 H0]]; exists x; split. * intros v H1; apply (freeVarPA x H0 v H1). * exists x0; intros g H1. apply extendsPA. fold mem; auto. + assert (H0: SysPrf PA (LNN2LNT_formula NN8)) by apply NN82PA. induction H0 as [x [x0 H0]]; exists x; split. intros v H1; apply (freeVarPA x H0 v H1). exists x0; intros g H1. apply extendsPA. fold mem; auto. + assert (H0:SysPrf PA (LNN2LNT_formula NN9)) by apply NN92PA. induction H0 as [x [x0 H0]]; exists x; split. intros v H1; apply (freeVarPA x H0 v H1). exists x0; intros g H1; apply extendsPA. fold mem; auto. + exists (LNN2LNT_formula x :: nil); split. * simpl; repeat rewrite app_nil_r. apply (LNN2LNT_freeVarF1 x). * exists (AXM _ (LNN2LNT_formula x)). intros g H1; induction H1 as [H1| H1]. -- unfold mem, Ensembles.In in H0. rewrite H1 in H0. apply H0. -- elim H1. - assert (H0: forall g : fol.Formula LNN, In g Axm1 -> mem (fol.Formula LNN) T' g) by auto with datatypes. assert (H1: forall g : fol.Formula LNN, In g Axm2 -> mem (fol.Formula LNN) T' g) by auto with datatypes. induction (Hrecx0_1 H0) as [x H2]. induction (Hrecx0_0 H1) as [x0 H3]. induction H2 as [H2 H4]. induction H3 as [H3 H5]. induction H4 as [x1 H4]. induction H5 as [x2 H5]. clear Hrecx0_1 H0 Hrecx0_0 H1. exists (x ++ x0); split. + repeat rewrite freeVarListFormulaApp. intros v H0; induction (in_app_or _ _ _ H0); auto with datatypes. + simpl in x1; exists (MP _ _ _ _ _ x1 x2). intros g H0; induction (in_app_or _ _ _ H0); auto. - assert (H0: forall g : fol.Formula LNN, In g Axm -> mem (fol.Formula LNN) T' g) by auto. induction (Hrecx0 H0) as [x H1]. clear Hrecx0 H0. induction H1 as [H0 H1]. induction H1 as [x1 H1]. exists x; split. + assumption. + assert (H2: ~ In v (freeVarListFormula LNT x)) by auto. exists (GEN _ _ _ _ H2 x1); assumption. - exists (nil (A:=Formula)); split. + auto. + exists (IMP1 _ (LNN2LNT_formula A) (LNN2LNT_formula B)). simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (IMP2 _ (LNN2LNT_formula A) (LNN2LNT_formula B) (LNN2LNT_formula C)). simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (CP _ (LNN2LNT_formula A) (LNN2LNT_formula B)). simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + assert (H0: SysPrf (Empty_set _) (impH (forallH v (LNN2LNT_formula A)) (LNN2LNT_formula (substF A v t)))). { apply impTrans with (substF (LNN2LNT_formula A) v (LNN2LNT_term t)). apply impI. apply forallE. apply Axm; right; constructor. apply iffE2. apply LNN2LNT_subFormula. } induction H0 as [x [x0 H0]]. induction x as [| a x Hrecx]. * exists x0; simpl; tauto. * assert (H1: mem (fol.Formula LNT) (Empty_set (fol.Formula LNT)) a) by auto with datatypes. induction H1. - exists (nil (A:=Formula)); split. + auto. + assert (H0: ~ In v (freeVarF (LNN2LNT_formula A))). { intros H0; apply n. apply LNN2LNT_freeVarF1. assumption. } exists (FA2 _ (LNN2LNT_formula A) v H0); simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (FA3 _ (LNN2LNT_formula A) (LNN2LNT_formula B) v). simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (EQ1 LNT); simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (EQ2 LNT); simpl; tauto. - exists (nil (A:=Formula)); split. + auto. + exists (EQ3 LNT); simpl; tauto. - assert (H0: SysPrf (Empty_set Formula) (LNN2LNT_formula (AxmEq4 LNN R))). { apply translateProof with (Empty_set (fol.Formula LNN)). unfold ClosedSystem in |- *. intros v f H0; induction H0. - intros f H0; induction H0. - exists (nil (A:=fol.Formula LNN)). exists (EQ4 LNN R). simpl; tauto. } induction H0 as [x [x0 H0]]. exists x; split. + intros v H1; induction (In_freeVarListFormulaE _ _ _ H1) as [x1 [H2 H3]]. assert (H4: mem (fol.Formula LNT) (Empty_set Formula) x1) by auto. induction H4. + exists x0; intros g H1. assert (H2: mem (fol.Formula LNT) (Empty_set Formula) g) by auto. induction H2. - assert (H0: SysPrf (Empty_set Formula) (LNN2LNT_formula (AxmEq5 LNN f))). { apply translateProof with (Empty_set (fol.Formula LNN)). - unfold ClosedSystem; intros v f0 H0; induction H0. - intros f0 H0; induction H0. - exists (nil (A:=fol.Formula LNN)). exists (EQ5 LNN f). simpl; tauto. } induction H0 as [x [x0 H0]]; exists x; split. + intros v H1; induction (In_freeVarListFormulaE _ _ _ H1) as [x1 [H2 H3]]. assert (H4: mem (fol.Formula LNT) (Empty_set Formula) x1) by auto. induction H4. + exists x0. intros g H1. assert (H2: mem (fol.Formula LNT) (Empty_set Formula) g) by auto. induction H2. } induction H0 as [x1 [H0 H1]]; now exists x1. 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)