Theorem SD-3. A simpler basis for set difference.

\{ \begin{matrix}x − (y − x) = x \\ x − (x − y) = y − (y − x) \end{matrix} \} ⇒

{(x − y) − z = (x − z) − (y − z) ⇔ (x − y) − z = (x − z) − y}.

Proof (⇒) found by Otter 3.0.4 on gyro at 2.72 seconds.

3,2 x − (y − x) = x 4 x − (x − y) = y − (y − x) 5 (x − y) − z = (x − z) − (y − z) 6 (A − C) − B ≠ (A − B) − C

7  (x − y) − (z − y) = (x − z) − y  [flip 5]
8  (x − y) − y = x − y  [2 → 2]
11,10  (x − y) − (x − y) = y − y  [8 → 4 :3]
12  (x − y) − ((x − y) − x) = x − (y − (y − x))  [4 → 4, flip]
19,18  (x − (x − y)) − (y − (y − x)) = x − x  [4 → 10 :11]
20  x − x = y − y  [4 → 10 :19,11]
35  (A − B) − (C − B) ≠ (A − B) − C  [5 → 6]
46,45  x − (y − y) = x  [20 → 4 :3]
53  (x − x) − y = x − x  [45 → 2]
83,82  ((x − y) − z) − y = (x − y) − (z − y)  [8 → 7, flip]
98,97  (x − y) − x = x − x  [53 → 7, flip]
104  x − (y − (y − x)) = x − y  [12 :98,46, flip]
120  (x − (y − z)) − y = x − y  [97 → 7 :46, flip]
154  (x − y) − (x − (y − z)) = z − z  [120 → 97 :11,11]
359  x − (x − ((y − x) − z)) = z − z  [2 → 154]
569  x − (x − ((y − x) − z)) = x − x  [104 → 359 :11,11,11]
627  (x − y) − (z − y) = (x − y) − z  [569 → 104 :46,83, flip]
629  □  [627,35]

Proof (⇐) found by Otter 3.0.4 on gyro at 20.60 seconds.

3,2 x − (y − x) = x 4 x − (x − y) = y − (y − x) 5 (x − y) − z = (x − z) − y 6 (A − B) − C ≠ (A − C) − (B − C)

7  (A − C) − (B − C) ≠ (A − B) − C  [flip 6]
8  (x − y) − y = x − y  [2 → 2]
11,10  (x − y) − (x − y) = y − y  [8 → 4 :3]
19,18  ((x − y) − z) − y = (x − y) − z  [8 → 5, flip]
21  (x − (x − y)) − z = (y − z) − (y − x)  [4 → 5]
22  (x − y) − (z − x) = x − y  [2 → 5, flip]
29  (x − y) − (x − z) = (z − (z − x)) − y  [flip 21]
33,32  (x − y) − ((x − z) − y) = z − (z − (x − y))  [5 → 4]

34  x − ((y − x) − z) = x  [5 → 2]
50  x − x = y − y  [34 → 4 :19,11]
55,54  x − (y − y) = x  [50 → 34]
57  (x − x) − y = (z − y) − z  [50 → 5]
61  (x − y) − x = (z − z) − y  [flip 57]
67,66  (x − x) − y = x − x  [54 → 2]
68  (x − y) − x = z − z  [61 :67]
75  x − (x − (x − y)) = x − y  [68 → 4 :55, flip]
103,102 ((x − y) − z) − (u − (x − z)) = (x − z) − y  [5 → 22]

767 (x − y) − ((z − (z − x)) − y) = (x − z) − ((x − z) − (x − y))

[29 → 4]

841 (x − (x − y)) − ((x − (x − y)) − (x − z)) = y − (y − (x − z))

[75 → 32 :33, flip]

2094,2093 (x − y) − (x − (x − z)) = (x − y) − z  [75 → 102 :103, flip]
2125,2124 (x − y) − ((x − y) − (x − z)) = (x − y) − z  [29 → 102 :19]
2130,2129 (x − (x − y)) − z = y − (y − (x − z))  [841 :2125]
2132  (x − y) − (z − y) = (x − z) − y  [767 :2130,2094,2125]
2133  □  [2132,7]