The proofs that both will not happen at once look good, but they assume too much to be useful for the “at least one happens proof”. They assume that one of the xor components happens, which is what we’re supposed to be proving. Or am I missing something?
Could you try expanding on this reasoning that leads to at least one happening?
Meanwhile, I’ll try to tackle that proof from a different angle, I think you can prove the whole statement by proving these two implications:
1/ assume:
o \in unspent(reality(T_n))
o \not\in double_spent(T_n)
o \in I(t_{n+1})
o \not\in E(T_{n+1}) (the “other xor component” not being true)
then these should imply O(t_{n+1}) \subseteq E(t_{n+1})
2/ assume:
o \in unspent(reality(T_n))
o \not\in double_spent(T_n)
o \in I(t_{n+1})
O(t_{n+1}) \not\subseteq E(t_{n+1}) (the opposite “xor component” not being true)
then these should imply o \in E(T_{n+1})
Sadly, I can’t follow that through now, b/c in transit. If you could elaborate on your reasoning, I’ll delve into that a couple of days later or I’ll try to pick up with this method above.