IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic

declarations in this module (23)

• structure TracePredicate L23
• def top L31
• def bottom L38
• def and L45
• def or L52
• def imp L62
• def not L70
• def all L76
• def exists_ L84
• theorem top_intro L91
• theorem and_intro L95
• theorem and_left L100
• theorem and_right L105
• theorem or_inl L110
• theorem or_inr L115
• theorem imp_elim L120
• theorem not_elim L127
• theorem all_intro L134
• theorem all_elim L139
• theorem exists_intro L144
• theorem persists L149
• structure TraceLogicCertificate L157
• theorem trace_logic_certificate L197