Shorter (but not necessarily more legible): ∀x∀y∀z: (R(x, 0, z)↔(x=z)) ∧ (R(x, Sy, z)↔R(Sx, y, z)).
Done!
Perfect!
Shorter (but not necessarily more legible): ∀x∀y∀z: (R(x, 0, z)↔(x=z)) ∧ (R(x, Sy, z)↔R(Sx, y, z)).
Done!
Perfect!