IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic

declarations in this module (18)

• inductive DistinctionAct L23
• inductive Side L28
• structure Endpoint L34
• inductive Trace L47
• def step L55
• def append L59
• theorem append_empty L63
• theorem append_extend L67
• theorem empty_append L71
• theorem append_assoc L79
• def Extends L87
• theorem extends_refl L91
• theorem extends_trans L96
• def orbitTrace L105
• def length L110
• theorem length_empty L114
• theorem length_extend L118
• theorem length_orbitTrace L123