Boolean Ring

Has Zero Divisors

βˆƒ(p,q∈Aβˆ’Zero:pβ‰ q:pβŠ—q=Zero)\exists(p,q \in A - \text{Zero}: p \neq q : p \otimes q = \text{Zero})

BooleanRingβ€…β€ŠAβ€…β€ŠβŠ—β€…β€ŠβŠ•β€…β€ŠZeroβ€…β€ŠOne\textbf{BooleanRing} \; A \; \otimes \; \oplus \; \text{Zero} \; \text{One}


sig A {
  , tms: A->A
  , pls: A->A
}

sig Zero, One in A {}

has_zero_divisors: check {
  { BooleanRing[A,tms,pls,Zero,One]
    #A > 2
  } implies {
    some disj p,q: A-Zero {
      tms[p,q] = Zero
    }
  }
} for 10

Last updated