proposition: Lemma NN82PA : SysPrf PA (LNN2LNT_formula NN8).
proof: Proof. replace (LNN2LNT_formula NN8) with (allH 1 0, translateLT (Tcons v#0 (Tcons (S_ v#1) Tnil)) -> translateLT (Tcons v#0 (Tcons v#1 Tnil)) \/ v#0 = v#1)%nt; simpl. - repeat rewrite translateLT1; simpl. unfold newVar; simpl; fold (Succ (v#3))%nt. fold (Succ (v#1))%nt; fold (v#0 + LNT.Succ v#3)%nt. fold (exH 3, v#0 + LNT.Succ v#3 = LNT.Succ v#1)%nt. fold (exH 3, v#0 + LNT.Succ v#3 = v#1)%nt. apply forallI. + apply closedPA. + apply forallI. * apply closedPA. * apply impI. apply existSys. -- apply closedPA. -- simpl; intro H. repeat (elim H; clear H; [ discriminate | intros ]); auto. -- eapply orE. ++ apply sysWeaken. apply paZeroOrSucc. ++ apply impI; apply orI2. apply impE with (LNT.Succ v#0 = LNT.Succ v#1)%nt. ** repeat simple apply sysWeaken. apply pa2. ** 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; apply impI. apply existSys. intros (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. repeat (elim H; clear H; [ discriminate | intros ]); auto. intros H; simpl in H. repeat (elim H; clear H; [ discriminate | intros ]); auto. apply orI1. apply existI with (var 4). rewrite (subFormulaEqual LNT). simpl; apply impE with (LNT.Succ (v#0 + LNT.Succ v#4) = LNT.Succ v#1)%nt. repeat simple apply sysWeaken. apply pa2. apply eqTrans with (v#0 + LNT.Succ v#3)%nt. apply eqTrans with (v#0 + LNT.Succ (LNT.Succ v#4))%nt. 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. - reflexivity. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(subAll folReplace folProp folLogic3 NN LNN2LNT) hydras.Ackermann(NewNotations)