IndisputableMonolith.Verification.BornRuleRouteB

declarations in this module (17)

• structure RouteBHyp L20
• def hSub L29
• theorem hSub_zero L31
• theorem hSub_one L34
• theorem hSub_cont L37
• theorem hSub_split L40
• theorem hSub_additive L60
• theorem additive_nat_mul L74
• theorem additive_nat_zero L89
• theorem additive_zero_on_unit L96
• theorem additive_zero_on_nonneg L142
• def gDev L167
• theorem hSub_eq_id L169
• theorem born_rule_route_B L183
• theorem modulus_multiplicativity L189
• structure RouteBCert L198
• theorem route_B_certified L202