∀x. ⟨x+0⟩=x ∀x. ∀y. ⟨x+y⟩=⟨y+x⟩ ∀x. ∀y. ∀z. ⟨x+⟨y+z⟩⟩=⟨⟨x+y⟩+z⟩ ∀x. ¬∀y. ¬⟨x+y⟩=0 ∀x. ⟨x⋅1⟩=x ∀x. ∀y. ⟨x⋅y⟩=⟨y⋅x⟩ ∀x. ∀y. ∀z. ⟨x⋅⟨y⋅z⟩⟩=⟨⟨x⋅y⟩⋅z⟩ ∀x. (¬x=0 → ¬∀y. ¬⟨x⋅y⟩=1) ¬1=0 ∀x. ∀y. ∀z. ⟨x⋅⟨y+z⟩⟩=⟨⟨x⋅y⟩+⟨x⋅z⟩⟩ ∀x. (¬x<0 → (¬x=0 → 0