IndisputableMonolith.LedgerPostingAdjacency

declarations in this module (43)

• def AccountRS L35
• instance accountRS_atomicTick L48
• abbrev LedgerState L58
• abbrev phiVec L60
• abbrev parity L63
• inductive Side L68
• def post L74
• lemma phiVec_post_debit L84
• lemma phiVec_post_credit L93
• lemma phiVec_coordAtomicStep_of_post L104
• theorem parity_oneBitDiff_of_post L133
• def PostingStep L143
• theorem postingStep_oneBitDiff L146
• def ledgerL1Cost L154
• def MonotoneLedger L159
• def LegalAtomicTick L163
• def ledgerJlogCost L169
• theorem ledgerJlogCost_nonneg L173
• lemma ledgerJlogCost_post L183
• lemma intCast_ne_zero_of_ne_zero L243
• lemma jlog_lt_jlog_of_one_lt L246
• theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 L253
• theorem ledgerL1Cost_eq_zero_iff L611
• lemma post_monotone L664
• lemma ledgerL1Cost_post L687
• theorem legalAtomicTick_of_post L748
• theorem postingStep_implies_legalAtomicTick L752
• lemma int_natAbs_eq_one_of_nonneg L757
• lemma int_eq_of_natAbs_eq_zero L773
• lemma exists_unique_of_sum_univ_eq_one L776
• theorem legalAtomicTick_implies_PostingStep L810
• theorem postingStep_iff_legalAtomicTick L924
• theorem minCost_monotoneStep_implies_postingStep L930
• theorem minJlogCost_monotoneStep_implies_postingStep L969
• theorem legalAtomicTick_oneBitDiff L994
• def accountAt L1002
• lemma postedAt_accountAt L1005
• def stepAt L1012
• lemma stepAt_isPostingStep L1016
• theorem stepAt_oneBitDiff L1020
• abbrev PostInstr L1027
• def run L1030
• theorem run_step_oneBitDiff L1036