Casper CBC: Safety
This is just a list of lemmas & theorem in Casper CBC safety.
https://gyazo.com/a6aed584ead32ce0053524a248ebce2f
https://gyazo.com/8b0a95540bc58d2db5aa717f4db6ab50
https://gyazo.com/b9ead39066b575296143720f614aac87
https://gyazo.com/8cdea4709bf4b7ff0f5c454786013a46
https://gyazo.com/8d91f3c0096bca2f729f90fd575bf180
https://gyazo.com/eac1d4cdeb6e9f5fb035045a83056996
https://gyazo.com/27349d739d8d8adf8d9a61fcac430eab
https://gyazo.com/8b2714232323e2f158099898bbf428d6
https://gyazo.com/48aadc09e36546856a3767c447eb3a87
nrryuya.icon > "n-party consensus" doesn't mean there are n validators which appeared at least once
https://gyazo.com/ee1e98fb9758e8325d23ff50f7dc9c12
nrryuya.icon > $ His a function which generates a property of protocol states from a property of consensus values
https://gyazo.com/410904b586d16590e80c014678cfcc26
https://gyazo.com/c090750a3a5202a5c7b61347e3d0a2f9
https://gyazo.com/d692fe5b9cf4b8dae0f67220c15cd92f
https://gyazo.com/a982db113ca2d7b3b7d94407eb537438
https://gyazo.com/7424964e6fd44c2333db787679ae58d9
nrryuya.icon > Again, the safety is "It is not possible for nodes to make inconsistent decisions".
The assumption "less than or equal t weight of validators are equivocating" is included in the definition of decided and not "used" to prove the safety.
Tips in proof
Theorem 4
https://gyazo.com/fccb07bd6300c660131f4001dd398529
nrryuya.icon > $ \forall p \in A, \ Decided \land \forall q \in B, \ Decided \Leftrightarrow \forall p \in A \cup B, Decided
Theorem 5
nrryuya.icon > Simply explained as follows.
1. Decided properties of states are consistent
States has common future as union set and decided properties of each state is True at the common future.
2.