IndisputableMonolith.RRF.Hypotheses.EightTick

declarations in this module (19)

• abbrev Phase L33
• def lock_start L38
• def lock_end L40
• def balance_start L42
• def balance_end L44
• def isLock L47
• def isBalance L50
• theorem lock_balance_partition L53
• theorem lock_balance_disjoint L58
• def next L63
• def prev L66
• theorem next_prev L68
• theorem prev_next L71
• structure TickedTrace L79
• class EightTickHypothesis L89
• structure LockPhasePrediction L100
• structure EightTickFalsifier L111
• def validAlternativePeriods L122
• def strongFalsifier L125