Belnap circuits

References

• [N. D. Belnap, A Useful Four-Valued Logic][Belnap1977]
• [Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits][Ghica2025]

@[inline]

def Circuit.Belnap.and (w : Wires BelnapLevel 2) : Wires BelnapLevel 1

The AND wire-function on a pair of Belnap-valued wires.

Equations

• Circuit.Belnap.and w = #v[(Vector.get w 0).and (Vector.get w 1)]

@[simp]

theorem Circuit.Belnap.and_leq {a₁ a₂ b₁ b₂ : BelnapLevel} (h0 : a₁ ≤ b₁) (h1 : a₂ ≤ b₂) : a₁.and a₂ ≤ b₁.and b₂

@[simp]

theorem Circuit.Belnap.and_monotonic : Monotone and

@[inline]

def Circuit.Belnap.or (w : Wires BelnapLevel 2) : Wires BelnapLevel 1

The OR wire-function on a pair of Belnap-valued wires.

Equations

• Circuit.Belnap.or w = #v[(Vector.get w 0).or (Vector.get w 1)]

@[simp]

theorem Circuit.Belnap.or_leq {a₁ a₂ b₁ b₂ : BelnapLevel} (h0 : a₁ ≤ b₁) (h1 : a₂ ≤ b₂) : a₁.or a₂ ≤ b₁.or b₂

@[simp]

theorem Circuit.Belnap.or_monotonic : Monotone or

@[inline]

def Circuit.Belnap.not (w : Wires BelnapLevel 1) : Wires BelnapLevel 1

The NOT wire-function on a single Belnap-valued wire.

Equations

• Circuit.Belnap.not w = #v[(Vector.get w 0).not]

@[simp]

theorem Circuit.Belnap.not_leq {x y : BelnapLevel} (h : x ≤ y) : x.not ≤ y.not

@[simp]

theorem Circuit.Belnap.not_monotonic : Monotone not