proposition: Lemma NN72PA : SysPrf PA (LNN2LNT_formula NN7).
proof: Proof. simpl; apply forallI. - apply closedPA. - rewrite translateLT1. set (nv := newVar (0 :: 2 :: 1 :: 0 :: nil)) in *. fold Zero%nt; fold (LNT.Succ (v#nv))%nt; fold (v#0 + (LNT.Succ v#nv))%nt. apply nnI, forallI. + apply closedPA. + apply impE with (LNT.Succ (v#0 + v#nv) <> LNT.Zero)%nt. * apply cp2, impI; apply eqTrans with (v#0 + LNT.Succ (v#nv))%nt. -- apply sysWeaken, eqSym, pa4. -- apply Axm; right; constructor. * apply pa1. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(subAll folReplace folProp folLogic3 NN LNN2LNT) hydras.Ackermann(NewNotations)