IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination

declarations in this module (20)

• class mass L90
• theorem unit_fugacity_forced_after_erasure L94
• theorem three_fugacities_collapse_on_posting_mu L107
• theorem three_fugacities_collapse_via_characterCost L118
• theorem unit_fugacity_forced_by_surface_and_kindTotals L148
• theorem a17_lands_in_a14_elimination L166
• theorem erasure_and_unit_fugacity_compose_to_mu L185
• theorem erasure_and_full_posting_force_gibbsSize L214
• theorem erasure_and_a17_compose_to_mu_no_fugacity L244
• theorem widening_blocked_by_non_sizeWeight_posting L266
• theorem widening_blocked_without_naming_mu L284
• theorem widening_blocked_without_kindTotals L297
• theorem fugacity_elimination_verdict L320
• structure FugacityEliminationIndex L341
• def fugacityEliminationIndex L353
• theorem index_elimination L360
• theorem index_three_fugacities L361
• theorem index_a17_widening L362
• theorem index_composition L363
• theorem index_flag_unmoved L366