proposition: Lemma translatePrf f : forall axm:fol.Formulas LNN, Prf LNN axm f -> (forall g, In g axm -> mem _ U g) -> exists Axm : Formulas, (exists prf : Prf LNT Axm (LNN2LNT_formula f), (forall g : Formula, In g Axm -> mem _ V g)) /\ forall v, In v (freeVarListFormula LNT Axm) -> (In v (freeVarListFormula LNN axm)).
proof: Proof. intros x x0 H; 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]. - destruct (AxiomsOK A). + apply H; now constructor. + exists x; destruct H0 as [H0 H1]. split. * apply H0. * intros v H2; simpl; rewrite app_nil_r. apply H1, H2. - assert (H0: forall g : fol.Formula LNN, In g Axm2 -> mem (fol.Formula LNN) U g). { intros g H0; apply H; apply in_or_app; now right. } assert (H1: forall g : fol.Formula LNN, In g Axm1 -> mem (fol.Formula LNN) U g). { intros g H1; apply H; apply in_or_app; now left. } destruct (Hrecx0_0 H0) as [x [[x0 I0] Z0]]. destruct (Hrecx0_1 H1) as [x1 [[x2 I1] Z1]]. clear H0 H1; rename I0 into H0; rename I1 into H1. exists (x1 ++ x); simpl in x2; split. + exists (MP LNT _ _ _ _ x2 x0). intros g H2; induction (in_app_or _ _ _ H2); auto. + intros v H2; rewrite freeVarListFormulaApp. rewrite freeVarListFormulaApp in H2; apply in_or_app. destruct (in_app_or _ _ _ H2); auto with *. - destruct (Hrecx0 H) as [x [[x1 H0] Z]]; exists x. assert (H1: ~ In v (freeVarListFormula LNT x)) by firstorder. split. + exists (GEN LNT _ _ _ H1 x1) ; assumption. + assumption. - exists (nil (A:=Formula)); split. + exists (IMP1 LNT (LNN2LNT_formula A) (LNN2LNT_formula B)). contradiction. + contradiction. - exists (nil (A:=Formula)); split. * exists (IMP2 LNT (LNN2LNT_formula A) (LNN2LNT_formula B) (LNN2LNT_formula C)); contradiction. * contradiction. - exists (nil (A:=Formula)); split. * exists (CP LNT (LNN2LNT_formula A) (LNN2LNT_formula B)). contradiction. * contradiction. - assert (H0: SysPrf (Empty_set _) (LNN2LNT_formula (impH (forallH v A) (substF A v t)))). { simpl in |- *. apply impE with (impH (forallH v (LNN2LNT_formula A)) (substF (LNN2LNT_formula A) v (LNN2LNT_term t))). apply iffE1. apply (reduceImp LNT). apply iffRefl. apply iffSym. apply LNN2LNT_subFormula. exists (nil (A:=Formula)). exists (FA1 LNT (LNN2LNT_formula A) v (LNN2LNT_term t)). contradiction. } destruct H0 as [x H0]; exists x; split. + destruct H0 as [x0 H0]; exists x0. intros g H1; elim (H0 g H1). + intros v0 H1; destruct H0. * destruct x. -- assumption. -- assert (H2: In f (f::x)) by auto with *. elim (H0 f H2). - exists (nil (A:=Formula)). assert (H0: ~ In v (freeVarF (LNN2LNT_formula A))) by (intro H0; elim n; now apply LNN2LNT_freeVarF1). split. + exists (FA2 LNT (LNN2LNT_formula A) v H0); contradiction. + contradiction. - exists (nil (A:=Formula)); split. + exists (FA3 LNT (LNN2LNT_formula A) (LNN2LNT_formula B) v); contradiction. + contradiction. - exists (nil (A:=Formula)); split. + exists (EQ1 LNT); contradiction. + contradiction. - exists (nil (A:=Formula)); split. + exists (EQ2 LNT); contradiction. + contradiction. - exists (nil (A:=Formula)); split. + exists (EQ3 LNT); contradiction. + contradiction. - assert (H0: SysPrf (Empty_set _) (LNN2LNT_formula (AxmEq4 LNN R))). { induction R; simpl; repeat apply impI. apply impE with (iffH (translateLT (Tcons (var 2) (Tcons (var 0) (Tnil)))) (translateLT (Tcons (var 3) (Tcons (var 1) (Tnil))))). - apply impRefl. - repeat rewrite translateLT1; simpl; unfold newVar; simpl. apply impE with (iffH (existH 3 (equal (LNT.Plus (var 2) (LNT.Succ (var 3))) (var 0))) (existH 4 (equal (LNT.Plus (var 3) (LNT.Succ (var 4))) (var 1)))). + apply impRefl. + eapply iffTrans with (exH 4, (substF (v#2 + LNT.Succ v#3 = v#0)%nt 3 (v#4)))%nt. * apply (rebindExist LNT). simpl in |- *. intro H0; decompose sum H0. -- discriminate H1. -- discriminate H2. * apply (reduceExist LNT). intros (x, (H0, H1)). destruct H1 as [x H1| x H1]; [ destruct H1 as [x H1| x H1] | destruct H1 ]. -- elim H1. -- induction H1. simpl in H0. decompose sum H0. discriminate H1. discriminate H2. -- simpl in H0; decompose sum H0. discriminate H1. discriminate H2. -- repeat rewrite (subFormulaEqual LNT); simpl. apply iffI. ++ apply impI. apply eqTrans with (var 0). ** apply eqTrans with (LNT.Plus (var 2) (LNT.Succ (var 4))). apply eqPlus. apply eqSym. apply Axm. left. left. right. constructor. apply eqRefl. apply Axm. right; constructor. ** apply Axm; left; right; constructor. ++ apply impI. apply eqTrans with (var 1). ** apply eqTrans with (v#3 + LNT.Succ v#4)%nt. fold (LNT.Succ (var 4)) in |- *. fold (LNT.Plus (var 2) (LNT.Succ (var 4))) in |- *. apply eqPlus. apply Axm. left. left. right. constructor. apply eqRefl. apply Axm. right; constructor. ** apply eqSym. apply Axm; left; right; constructor. } destruct H0 as [x H0]; exists x. destruct H0 as [x0 H0]; split. + exists x0; intros g H1; elim (H0 g H1). + intros v H1; destruct x. * assumption. * assert (H2: In f (f::x)) by auto with *. elim (H0 _ H2). - replace (LNN2LNT_formula (AxmEq5 LNN f)) with (AxmEq5 LNT f). + exists (nil (A:=Formula)); split. * exists (EQ5 LNT f); contradiction. * contradiction. + induction f; reflexivity. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)