File tree Expand file tree Collapse file tree 1 file changed +9
-5
lines changed
Expand file tree Collapse file tree 1 file changed +9
-5
lines changed Original file line number Diff line number Diff line change @@ -78,11 +78,15 @@ we say `#3` reads `#2`, which together forms the below modification order
7878#3 ≤ #2 ≤ #3
7979</pre ></blockquote >
8080<p >
81- According to the second bullet of the definition of the (non-strict) total order, we can get `#3` ≤ `#3`,
82- which is also valid according to the first bullet. Then we instead use the third bullet to claim `#3` = `#2`
83- in that valid total order. However, `#3` and `#2` are different modifications, so that the total order is
84- not possible, which is quite indirect. It's a bit overcomplicated for reasoning.
85- The definition of single total order says
81+ According to the second bullet of the definition of the (non-strict) total order, we can get `#3 = #3`,
82+ which is also valid according to the first bullet. Then we instead use the third bullet to claim
83+ `#3 = #2` in that valid total order. However, when we get `#3 = #2` according to the non-strict total
84+ order in the above example, it's unclear what `=` means here, since we didn't define what `=` means
85+ between two modifications in the modification order. Whether the total order is valid depends on how
86+ `=` intended to mean for two modifications in a non-strict total order. This is quite indirect and
87+ is a bit overcomplicated for reasoning.
88+ <p />
89+ The definition of strict single total order says
8690</p >
8791<blockquote style =" border-left: 3px solid #ccc;padding-left: 15px;" >
8892<p >
You can’t perform that action at this time.
0 commit comments