IndisputableMonolith.CrossDomain.CognitiveStateSpace

declarations in this module (19)

• inductive Sense L27
• inductive Emotion L31
• inductive MemorySystem L35
• theorem senseCount L39
• theorem emotionCount L40
• theorem memorySystemCount L41
• abbrev CognitiveState L43
• theorem cognitiveStateCount L45
• theorem senseProj_surj L49
• theorem emotionProj_surj L53
• theorem memoryProj_surj L58
• theorem notCollapsedToSense L63
• theorem notCollapsedToEmotion L66
• theorem notCollapsedToMemory L70
• theorem notCollapsedToPair1 L75
• theorem notCollapsedToPair2 L81
• theorem notCollapsedToPair3 L87
• structure CognitiveStateSpaceCert L93
• def cognitiveStateSpaceCert L104