|
|
|---|
|
|
|
|---|
Proof by simultaneous induction for certain invariants.
As discussed in unequivocal-accepted-certificates-def-and-init and in nonforking-blockchains-def-and-init, these key invariants are proved by simultaneous induction. There are many other invariants involved, all of which are are proved to be preserved, through any sequence of events (via events-next), by simultaneous induction, in invariants-of-events-next. This theorem can be used to prove theorems showing that individual invariants (among that set) hold in reachable states.