This file is generated from the following operator table: [[0,2,3,4,5,6,7,8,9,10,11,12,1],[2,1,11,7,9,4,8,0,3,12,6,5,10],[3,11,2,12,8,10,5,9,0,4,1,7,6],[4,7,12,3,1,9,11,6,10,0,5,2,8],[5,9,8,1,4,2,10,12,7,11,0,6,3],[6,4,10,9,2,5,3,11,1,8,12,0,7],[7,8,5,11,10,3,6,4,12,2,9,1,0],[8,0,9,6,12,11,4,7,5,1,3,10,2],[9,3,0,10,7,1,12,5,8,6,2,4,11],[10,12,4,0,11,8,2,1,6,9,7,3,5],[11,6,1,5,0,12,9,3,2,7,10,8,4],[12,5,7,2,6,0,1,10,4,3,8,11,9],[1,10,6,8,3,7,0,2,11,5,4,9,12]]
The magma definition
Equations
- One or more equations did not get rendered due to their size.
Instances For
The facts
theorem
«Facts from FinitePoly [[0,2,3,4,5,6,7,8,9,10,11,12,1],[2,1,11,7,9,4,8,0,3,12,6,5,10],[3,11,2,12,8,10,5,9,0,4,1,7,6],[4,7,12,3,1,9,11,6,10,0,5,2,8],[5,9,8,1,4,2,10,12,7,11,0,6,3],[6,4,10,9,2,5,3,11,1,8,12,0,7],[7,8,5,11,10,3,6,4,12,2,9,1,0],[8,0,9,6,12,11,4,7,5,1,3,10,2],[9,3,0,10,7,1,12,5,8,6,2,4,11],[10,12,4,0,11,8,2,1,6,9,7,3,5],[11,6,1,5,0,12,9,3,2,7,10,8,4],[12,5,7,2,6,0,1,10,4,3,8,11,9],[1,10,6,8,3,7,0,2,11,5,4,9,12]]» :
∃ (G : Type) (x : Magma G),
Equation1076 G ∧ Equation2531 G ∧ ¬Equation55 G ∧ ¬Equation65 G ∧ ¬Equation73 G ∧ ¬Equation118 G ∧ ¬Equation127 G ∧ ¬Equation160 G ∧ ¬Equation167 G ∧ ¬Equation209 G ∧ ¬Equation229 G ∧ ¬Equation261 G ∧ ¬Equation263 G ∧ ¬Equation274 G ∧ ¬Equation419 G ∧ ¬Equation429 G ∧ ¬Equation436 G ∧ ¬Equation437 G ∧ ¬Equation464 G ∧ ¬Equation466 G ∧ ¬Equation473 G ∧ ¬Equation474 G ∧ ¬Equation504 G ∧ ¬Equation513 G ∧ ¬Equation617 G ∧ ¬Equation632 G ∧ ¬Equation633 G ∧ ¬Equation640 G ∧ ¬Equation642 G ∧ ¬Equation669 G ∧ ¬Equation677 G ∧ ¬Equation679 G ∧ ¬Equation704 G ∧ ¬Equation826 G ∧ ¬Equation833 G ∧ ¬Equation845 G ∧ ¬Equation872 G ∧ ¬Equation879 G ∧ ¬Equation883 G ∧ ¬Equation917 G ∧ ¬Equation1026 G ∧ ¬Equation1029 G ∧ ¬Equation1039 G ∧ ¬Equation1045 G ∧ ¬Equation1046 G ∧ ¬Equation1075 G ∧ ¬Equation1085 G ∧ ¬Equation1086 G ∧ ¬Equation1110 G ∧ ⋯