IndisputableMonolith.Foundation.OptionAEmpiricalProtocol

declarations in this module (22)

• structure ProtocolSpec L24
• def protocolSpec L31
• def ProtocolFalsifiable L38
• theorem protocolFalsifiable_all L42
• def ProtocolMatches L48
• theorem protocolSpec_matches L53
• theorem uniqueProtocolSpec L58
• theorem protocolSpec_injective L68
• theorem protocolSpec_eq_iff L74
• theorem protocolSpec_ne_of_ne L83
• theorem c1_c3_protocol_distinct L88
• theorem c3_c5_protocol_distinct L92
• theorem c5_c8_protocol_distinct L96
• def EmpiricallyCovered L102
• theorem empiricallyCovered L105
• theorem c1_protocol L108
• theorem c3_protocol L112
• theorem c5_protocol L116
• theorem c8_protocol L120
• theorem c3_uniqueProtocol L124
• structure EmpiricalProtocolCert L128
• def empiricalProtocolCert L142