-ndefinition oct1 ≝ nat1.
-ndefinition oct2 ≝ nat2.
-ndefinition oct3 ≝ nat3.
-ndefinition oct4 ≝ nat4.
-ndefinition oct5 ≝ nat5.
-ndefinition oct6 ≝ nat6.
-ndefinition oct7 ≝ nat7.
+ndefinition oct1 ≝ S O.
+ndefinition oct2 ≝ S (S O).
+ndefinition oct3 ≝ S (S (S O)).
+ndefinition oct4 ≝ S (S (S (S O))).
+ndefinition oct5 ≝ S (S (S (S (S O)))).
+ndefinition oct6 ≝ S (S (S (S (S (S O))))).
+ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).