nrryuya.icon > The decoupled "mutually recursive definition of states and messages" are only handled in the definition of full node and not in the safety and non-triviality proofs
Non-triviality = the existence of a protocol property$ Pfor which there is a protocol state$ \sigma_1that is decided on$ Pand another protocol state$ \sigma_2that is decided on$ ¬P
"In our generalization efforts, we found that non-triviality precisely captures the notion of non-local confluence in the abstract rewriting system literature"
Strong non-triviality = for every protocol state s1, there exists a protocol state s2 that is s1’s next state and a protocol state s3 that is s1’s future state, such that s1 and s3 share a common future, but s2 and s3 do not
Proved by full/light node specification but not only by abstract definition