From Coq Require Import Arith Lia Ensembles List.

From hydras.Ackermann Require Import folProp subAll folLogic3 Languages.
From hydras.Ackermann Require Export LNN.
From hydras Require Import Compat815 NewNotations.
Import NNnotations.

Section NN.

Definition NN1 := (allH 0, S_ v#0 ≠ Zero)%fol.

Definition NN2 := (allH 1 0, S_ v#0 = S_ v#1 → v#0 = v#1)%fol.

Definition NN3 := (allH 0, v#0 + Zero = v#0)%fol.

Definition NN4 := (allH 1 0, v#0 + S_ v#1 = S_ (v#0 + v#1))%fol.

Definition NN5 := (allH 0, v#0 × Zero = Zero)%fol.

Definition NN6 := (allH 1 0, v#0 × S_ v#1 = v#0 × v#1 + v#0)%fol.

Definition NN7 := (allH 0, ¬ v#0 < Zero)%fol.

Definition NN8 :=
 (allH 1 0, v#0 < Succ(v#1) → v#0 < v#1 ∨ v#0 = v#1)%fol.

Definition NN9 := (allH 1 0, v#0 < v#1 ∨ v#0 = v#1 ∨ v#1 < v#0)%fol.

Definition NN := SetEnum NN1 NN2 NN3 NN4 NN5 NN6 NN7 NN8 NN9.

Lemma closedNN1 : ClosedSystem LNN NN.

Lemma closedNN : ∀ v : nat, ¬ In_freeVarSys LNN v NN.

Lemma nn1 (a : Term) : SysPrf NN (S_ a ≠ Zero)%fol.

Lemma nn2 (a b : Term): SysPrf NN (S_ a = S_ b → a = b)%fol.

Lemma nn3 (a : Term): SysPrf NN (a + Zero = a)%fol.

Lemma nn4 (a b : Term) : SysPrf NN (a + S_ b = S_ (a + b))%fol.

Lemma nn5 ( a : Term) : SysPrf NN (a × Zero = Zero)%fol.

Lemma nn6 (a b : Term):
  SysPrf NN (a × Succ b = a × b + a)%fol.

Lemma nn7 (a : Term): SysPrf NN (¬ (a <Zero))%fol.

Lemma nn8 (a b : Term) : SysPrf NN (a < Succ b → a < b ∨ a = b)%fol.

Lemma nn9 (a b : Term): SysPrf NN (a < b ∨ a = b ∨ b < a)%fol.

End NN.