This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 0 * y2 + 2 * x + 0 * y + 2 * x * y) % 4' (0, 39, 358, 359, 360, 361, 362, 363, 364, 365, 366, 367, 368, 369, 370, 371, 372, 3658, 3659, 3660, 3661, 3662, 3663, 3664, 3665, 3666, 3667, 3668, 3669, 3670, 3671, 3672, 3673, 3674, 3675, 3676, 3677, 3678, 3679, 3680, 3681, 3682, 3683, 3684, 3685, 3686, 3687, 3688, 3689, 3690, 3691, 3692, 3693, 3694, 3695, 3696, 3697, 3698, 3699, 3700, 3701, 3702, 3703, 3704, 3705, 3706, 3707, 3708, 3709, 3861, 3862, 3863, 3864, 3865, 3866, 3867, 3868, 3869, 3870, 3871, 3872, 3873, 3874, 3875, 3876, 3877, 3878, 3879, 3880, 3881, 3882, 3883, 3884, 3885, 3886, 3887, 3888, 3889, 3890, 3891, 3892, 3893, 3894, 3895, 3896, 3897, 3898, 3899, 3900, 3901, 3902, 3903, 3904, 3905, 3906, 3907, 3908, 3909, 3910, 3911, 3912, 4064, 4065, 4066, 4067, 4068, 4069, 4070, 4071, 4072, 4073, 4074, 4075, 4076, 4077, 4078, 4079, 4080, 4081, 4082, 4083, 4084, 4085, 4086, 4087, 4088, 4089, 4090, 4091, 4092, 4093, 4094, 4095, 4096, 4097, 4098, 4099, 4100, 4101, 4102, 4103, 4104, 4105, 4106, 4107, 4108, 4109, 4110, 4111, 4112, 4113, 4114, 4115, 4267, 4268, 4269, 4270, 4281, 4282, 4283, 4284, 4285, 4286, 4287, 4288, 4313, 4314, 4315, 4316, 4317, 4318, 4338, 4339, 4340, 4341, 4356, 4357, 4358, 4359, 4360, 4582, 4583, 4584, 4585, 4586, 4587, 4588, 4589, 4590, 4591, 4592, 4593, 4594, 4595, 4596, 4597, 4598, 4599, 4600, 4601, 4602, 4603, 4604, 4605, 4606, 4607, 4608, 4609, 4610, 4611, 4612, 4613, 4614, 4615, 4616, 4617, 4618, 4619, 4620, 4621, 4622, 4623, 4624, 4625, 4626, 4627, 4628, 4629, 4630, 4631, 4632, 4633, 4634, 4635, 4636, 4637, 4638, 4639, 4640, 4641, 4642, 4643, 4644, 4645, 4646, 4647, 4648, 4649, 4650, 4651, 4652, 4653, 4654, 4655, 4656, 4657, 4658, 4659, 4660, 4661, 4662, 4663, 4664, 4665, 4666, 4667, 4668, 4669, 4670, 4671, 4672, 4673, 4674, 4675, 4676, 4677, 4678, 4679, 4680, 4681, 4682, 4683, 4684, 4685, 4686, 4687, 4688, 4689, 4690, 4691, 4692, 4693)

The magma definition

def «FinitePoly 2 * x + 2 * x * y % 4» : Magma (Fin 4)

Equations

• «FinitePoly 2 * x + 2 * x * y % 4» = { op := MemoFinOp.opOfTable 570434048 }

The facts

theorem «Facts from FinitePoly 2 * x + 2 * x * y % 4» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation366 G ∧ Equation4271 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation255 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2441 G ∧ ¬Equation2644 G ∧ ¬Equation2847 G ∧ ¬Equation3050 G ∧ ¬Equation3253 G ∧ ¬Equation3456 G ∧ ¬Equation3712 G ∧ ¬Equation3714 G ∧ ¬Equation3721 G ∧ ¬Equation3722 G ∧ ¬Equation3724 G ∧ ¬Equation3725 G ∧ ¬Equation3748 G ∧ ¬Equation3749 G ∧ ¬Equation3751 G ∧ ¬Equation3752 G ∧ ¬Equation3759 G ∧ ¬Equation3761 G ∧ ¬Equation3915 G ∧ ¬Equation3917 G ∧ ¬Equation3918 G ∧ ¬Equation3925 G ∧ ¬Equation3927 G ∧ ¬Equation3928 G ∧ ¬Equation3951 G ∧ ¬Equation3952 G ∧ ¬Equation3954 G ∧ ¬Equation3955 G ∧ ¬Equation3961 G ∧ ¬Equation3962 G ∧ ¬Equation3964 G ∧ ⋯