proposition: Lemma NN92PA : SysPrf PA (LNN2LNT_formula NN9).
proof: Proof. replace (LNN2LNT_formula NN9) with (allH 1 0, LNN2LNT_formula ((v#0)%nt < (v#1)%nt)%fol \/ v#0 = v#1 \/ LNN2LNT_formula (v#1 < v#0)%fol)%nt; [ idtac | reflexivity ]. simpl in |- *. repeat rewrite translateLT1. simpl in |- *. unfold newVar in |- *. simpl in |- *. fold (LNT.Succ v#3)%nt in |- *. fold (v#0 + LNT.Succ v#3)%nt. fold (v#1 + LNT.Succ v#3)%nt. fold (exH 3, v#0 + LNT.Succ v#3 = v#1)%nt. fold (exH 3, v#1 + LNT.Succ v#3 = v#0)%nt. apply induct. - rewrite (subFormulaForall LNT). induction (eq_nat_dec 0 1). + discriminate a. + induction (In_dec eq_nat_dec 0 (freeVarT LNT.Zero)). * simpl in a. elim a. * rewrite (subFormulaOr LNT). apply forallI. apply closedPA. apply orI2. rewrite (subFormulaOr LNT). rewrite (subFormulaEqual LNT). simpl in |- *. eapply orE. -- apply paZeroOrSucc with (t := (v#0)%nt). -- apply impI. apply orI1. apply Axm; right; constructor. -- apply impI. apply orI2. unfold newVar in |- *. simpl in |- *. rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). ++ discriminate a. ++ induction (In_dec eq_nat_dec 3 (freeVarT LNT.Zero)). ** elim a. ** apply impE with (exH 3, v#0 = LNT.Succ v#3)%nt. { apply sysWeaken. apply impI. apply existSys. - apply closedPA. - unfold not in |- *; intros. simpl in H. induction H as [H| H]. + discriminate H. + contradiction. - apply existI with (v#3)%nt. repeat rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ v#3)%nt. + apply sysWeaken. apply eqTrans with (LNT.Succ v#3 + LNT.Zero)%nt. * apply paPlusSym with (a := LNT.Zero) (b := (LNT.Succ v#3)%nt). * apply pa3. + apply eqSym. apply Axm; right; constructor. } apply impE with (exH 1, v#0 = LNT.Succ v#1)%nt. { replace (v#0 = LNT.Succ v#3)%nt with (substF (v#0 = LNT.Succ v#1)%nt 1 (v#3)%nt). - apply iffE1. apply (rebindExist LNT). simpl in |- *. unfold not in |- *; intros. induction H as [H| H]. + discriminate H. + contradiction. - rewrite (subFormulaEqual LNT). reflexivity. } apply Axm; right; constructor. - apply forallI. + apply closedPA. + apply impI. rewrite (subFormulaForall LNT). induction (eq_nat_dec 0 1). * discriminate a. * induction (In_dec eq_nat_dec 0 (freeVarT (LNT.Succ v#1)%nt)). -- simpl in a. induction a as [H| H]. ++ discriminate H. ++ contradiction. -- rewrite (subFormulaOr LNT). apply sysWeaken. apply induct. ++ rewrite (subFormulaOr LNT). apply orI1. rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). ** discriminate a. ** induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ v#1)%nt)). { simpl in a. induction a as [H| H]. - elim b1; auto. - contradiction. } rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 0). { discriminate a. } induction (In_dec eq_nat_dec 3 (freeVarT LNT.Zero)). { simpl in a; contradiction. } apply existI with (v#1)%nt. repeat rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ v#1 + LNT.Zero)%nt. { apply paPlusSym with (a := LNT.Zero) (b := (LNT.Succ v#1)%nt). } apply pa3. ++ apply forallI. ** apply closedPA. ** apply impI; apply orSys. { rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). - discriminate a. - induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ (v#1))%nt)). + simpl in a. induction a as [H| H]. * elim b1; auto. * contradiction. + repeat rewrite (subFormulaOr LNT). rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 0). * discriminate a. * induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ (v#0))%nt)). -- simpl in a. induction a as [H| H]. ++ elim b3; auto. ++ contradiction. -- rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). ++ elim b1; auto. ++ induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ (v#1))%nt)). ** elim b2; auto. ** rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 0). { elim b3; auto. } induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ (v#0))%nt)). { elim b4; auto. } repeat rewrite (subFormulaEqual LNT); simpl in |- *. apply existSys. { apply closedPA. } simpl in |- *. unfold not in |- *; intros. decompose sum H; auto. eapply orE. apply sysWeaken. apply paZeroOrSucc with (t := (v#3)%nt). apply impI. apply orI2. apply orI1. apply eqTrans with (v#0 + LNT.Succ v#3)%nt. apply eqTrans with (LNT.Succ (v#0 + v#3))%nt. apply eqSucc. apply eqTrans with (v#0 + LNT.Zero)%nt. apply eqSym. repeat simple apply sysWeaken. apply pa3. apply eqPlus. apply eqRefl. apply eqSym. apply Axm; right; constructor. apply eqSym. repeat simple apply sysWeaken. apply pa4. apply Axm; left; right; constructor. unfold newVar in |- *. simpl in |- *. apply impI. apply orI1. apply existSys. unfold not in |- *; intros. induction H as (x, H); induction H as (H, H0). induction H0 as [x H0| x H0]. elim closedPA with 4. exists x. auto. induction H0. simpl in H. decompose sum H; discriminate H0 || discriminate H1. simpl in |- *. unfold not in |- *; intros. decompose sum H; discriminate H0 || discriminate H1. apply existI with (var 4). rewrite (subFormulaEqual LNT); simpl in |- *. apply eqTrans with (v#0 + LNT.Succ v#3)%nt. apply eqTrans with (v#0 + LNT.Succ (LNT.Succ v#4))%nt. apply eqTrans with (LNT.Succ (v#0 + LNT.Succ v#4))%nt. apply eqTrans with (LNT.Succ v#4 + LNT.Succ v#0)%nt. repeat simple apply sysWeaken. apply paPlusSym with (a := (LNT.Succ v#0)%nt) (b := (LNT.Succ v#4)%nt). repeat simple apply sysWeaken. eapply eqTrans. apply pa4. apply eqSucc. apply paPlusSym. repeat simple apply sysWeaken. apply eqSym. apply pa4. apply eqPlus. apply eqRefl. apply eqSucc. apply eqSym. apply Axm; right; constructor. apply Axm; left; right; constructor. } repeat rewrite (subFormulaOr LNT). apply orSys. apply orI2. apply orI2. rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). { discriminate a. } induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ v#1)%nt)). induction a as [H| H]. { elim b1; auto. } contradiction. rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 0). discriminate a. induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ v#0)%nt)). induction a as [H| H]. elim b3; auto. contradiction. apply existI with LNT.Zero. repeat rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ (LNT.Succ v#1 + LNT.Zero))%nt. apply sysWeaken. apply pa4 with (a := (LNT.Succ v#1)%nt) (b := LNT.Zero). apply eqTrans with (LNT.Succ (LNT.Succ v#1))%nt. apply eqSucc. apply sysWeaken. apply pa3. fold (LNT.Succ (v#0))%nt. apply eqSucc. apply eqSym. apply Axm; right; constructor. do 2 rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 1). discriminate a. induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ v#1)%nt)). induction a as [H| H]. elim b1; auto. contradiction. do 2 rewrite (subFormulaExist LNT). induction (eq_nat_dec 3 0). discriminate a. induction (In_dec eq_nat_dec 3 (freeVarT (LNT.Succ (v#0))%nt)). induction a as [H| H]. elim b3; auto. contradiction. apply orI2. apply orI2. apply existSys. apply closedPA. simpl in |- *. unfold not in |- *; intros. decompose sum H; auto. apply existI with (LNT.Succ v#3)%nt. repeat rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ (LNT.Succ v#1 + LNT.Succ v#3))%nt. apply sysWeaken. apply pa4 with (a := (LNT.Succ v#1)%nt) (b := (LNT.Succ v#3)%nt). fold (LNT.Succ v#0)%nt in |- *. apply eqSucc. apply Axm; right; constructor. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(subAll folReplace folProp folLogic3 NN LNN2LNT) hydras.Ackermann(NewNotations)