|
|
|---|
|
|
|
|---|
Proof by simultaneous induction for certain invariants.
As discussed in unequivocal-dags-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 is used, elsewhere, to prove theorems showing that individual invariants (among that set) hold in reachable states.