Package hardware: Hardware devices

Information

name	hardware
version	1.64
description	Hardware devices
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool function list natural natural-bits pair set stream
show	Data.Bool Data.List Data.Pair Data.Stream Function Hardware Number.Natural Set

Files

Package tarball hardware-1.64.tgz
Theory source file hardware.thy (included in the package tarball)

Defined Type Operators

Hardware
- bus
- wire

Defined Constants

Hardware
- adder2
- adder3
- and2
- and3
- bus
- case1
- connect
- counter
- delay
- eventCounter
- ground
- majority3
- not
- or2
- or3
- pipe
- power
- pulse
- signal
- signals
- sticky
- wire
- xor2
- xor3
- Bus
  - Bus.adder2
  - Bus.adder3
  - Bus.adder4
  - Bus.and2
  - Bus.and3
  - Bus.append
  - Bus.case1
  - Bus.connect
  - Bus.delay
  - Bus.ground
  - Bus.lift2
  - Bus.lift3
  - Bus.majority3
  - Bus.multiplier
  - Bus.nil
  - Bus.not
  - Bus.or2
  - Bus.or3
  - Bus.pipe
  - Bus.power
  - Bus.reverse
  - Bus.signal
  - Bus.single
  - Bus.sub
  - Bus.width
  - Bus.wire
  - Bus.wires
  - Bus.xor2
  - Bus.xor3
- SumCarry
  - SumCarry.multiplier
  - SumCarry.shiftRight

Theorems

⊦ Bus.connect Bus.nil Bus.nil

⊦ Bus.delay Bus.nil Bus.nil

⊦ Bus.not Bus.nil Bus.nil

⊦ Bus.reverse Bus.nil Bus.nil

⊦ Bus.nil = bus []

⊦ Bus.connect = Bus.lift2 connect

⊦ Bus.delay = Bus.lift2 delay

⊦ Bus.not = Bus.lift2 not

⊦ Bus.and2 = Bus.lift3 and2

⊦ Bus.or2 = Bus.lift3 or2

⊦ Bus.xor2 = Bus.lift3 xor2

⊦ Bus.ground 0 = Bus.nil

⊦ Bus.power 0 = Bus.nil

⊦ Bus.width Bus.nil = 0

⊦ Bus.and2 Bus.nil Bus.nil Bus.nil

⊦ Bus.or2 Bus.nil Bus.nil Bus.nil

⊦ Bus.xor2 Bus.nil Bus.nil Bus.nil

⊦ ∀x. Bus.connect x x

⊦ ∀x. connect x x

⊦ ∀t. signal power t

⊦ ground = wire (replicate ⊥)

⊦ power = wire (replicate ⊤)

⊦ Bus.adder2 Bus.nil Bus.nil Bus.nil Bus.nil

⊦ Bus.and3 Bus.nil Bus.nil Bus.nil Bus.nil

⊦ Bus.majority3 Bus.nil Bus.nil Bus.nil Bus.nil

⊦ Bus.or3 Bus.nil Bus.nil Bus.nil Bus.nil

⊦ Bus.xor3 Bus.nil Bus.nil Bus.nil Bus.nil

⊦ ∀t. ¬signal ground t

⊦ ∀r. Bus.lift2 r Bus.nil Bus.nil

⊦ ∀x. ∃y. Bus.connect x y

⊦ ∀x. ∃y. Bus.delay x y

⊦ ∀x. ∃y. Bus.not x y

⊦ ∀x. ∃y. connect x y

⊦ ∀x. ∃y. delay x y

⊦ ∀x. ∃y. not x y

⊦ ∀x. ∃y. pulse x y

⊦ Bus.ground 1 = Bus.single ground

⊦ Bus.power 1 = Bus.single power

⊦ Bus.adder3 Bus.nil Bus.nil Bus.nil Bus.nil Bus.nil

⊦ ∀x. bus (Bus.wires x) = x

⊦ ∀x. Bus.append Bus.nil x = x

⊦ ∀x. Bus.append x Bus.nil = x

⊦ ∀w. Bus.reverse (Bus.single w) (Bus.single w)

⊦ ∀w. wire (signals w) = w

⊦ ∀s. Bus.case1 s Bus.nil Bus.nil Bus.nil

⊦ ∀n. Bus.width (Bus.ground n) = n

⊦ ∀n. Bus.width (Bus.power n) = n

⊦ ∀t. Bus.signal Bus.nil t = []

⊦ ∀l. Bus.wires (bus l) = l

⊦ ∀s. signals (wire s) = s

⊦ ∀r. Bus.lift3 r Bus.nil Bus.nil Bus.nil

⊦ ∀x. Bus.width x = length (Bus.wires x)

⊦ ∀w. signal w = nth (signals w)

⊦ ∀s. Bus.case1 s = Bus.lift3 (case1 s)

⊦ ∀w. Bus.width (Bus.single w) = 1

⊦ ∀t. fromBool (signal ground t) = 0

⊦ ∀t. Bits.toNatural (Bus.signal Bus.nil t) = 0

⊦ ∀i w. ¬Bus.wire Bus.nil i w

⊦ ∀x y. ∃z. and2 x y z

⊦ ∀x y. ∃z. or2 x y z

⊦ ∀x y. ∃z. xor2 x y z

⊦ ∀w. Bus.single w = bus (w :: [])

⊦ ∀x. connect ground x ⇒ not power x

⊦ ∀x. connect power x ⇒ not ground x

⊦ ∀n. Bus.ground n = bus (replicate ground n)

⊦ ∀n. Bus.power n = bus (replicate power n)

⊦ ∀t. fromBool (signal power t) = 1

⊦ ∀x. Bus.width x = 0 ⇔ x = Bus.nil

⊦ ∀x t. length (Bus.signal x t) = Bus.width x

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.ground n) t) = 0

⊦ ∀n. Bus.ground (suc n) = Bus.append (Bus.single ground) (Bus.ground n)

⊦ ∀n. Bus.power (suc n) = Bus.append (Bus.single power) (Bus.power n)

⊦ ∀w x y. ∃z. and3 w x y z

⊦ ∀s x y. ∃z. case1 s x y z

⊦ ∀w x y. ∃z. majority3 w x y z

⊦ ∀w x y. ∃z. or3 w x y z

⊦ ∀w x y. ∃z. xor3 w x y z

⊦ ∀x y. ∃s c. adder2 x y s c

⊦ ∀x y. connect ground y ⇒ and2 ground x y

⊦ ∀x y. connect ground y ⇒ and2 x ground y

⊦ ∀x y. connect power y ⇒ or2 power x y

⊦ ∀x y. connect power y ⇒ or2 x power y

⊦ ∀x y. connect x y ⇒ and2 power x y

⊦ ∀x y. connect x y ⇒ and2 x power y

⊦ ∀x y. connect x y ⇒ or2 ground x y

⊦ ∀x y. connect x y ⇒ or2 x ground y

⊦ ∀x y. connect x y ⇒ xor2 ground x y

⊦ ∀x y. connect x y ⇒ xor2 x ground y

⊦ ∀x y. not x y ⇒ xor2 power x y

⊦ ∀x y. not x y ⇒ xor2 x power y

⊦ ∀n t. Bus.signal (Bus.ground n) t = replicate ⊥ n

⊦ ∀n t. Bus.signal (Bus.power n) t = replicate ⊤ n

⊦ ∀s t. signal (wire s) t ⇔ nth s t

⊦ ∀w₁ w₂. Bus.single w₁ = Bus.single w₂ ⇔ w₁ = w₂

⊦ ∀x y. Bus.connect (Bus.single x) (Bus.single y) ⇔ connect x y

⊦ ∀x y. Bus.delay (Bus.single x) (Bus.single y) ⇔ delay x y

⊦ ∀x y. Bus.not (Bus.single x) (Bus.single y) ⇔ not x y

⊦ ∀w₁ w₂. Bus.single w₁ = Bus.single w₂ ⇒ w₁ = w₂

⊦ ∀r. (∀w. r w w) ⇒ ∀x. Bus.lift2 r x x

⊦ ∀x y. Bus.append x y = bus (Bus.wires x @ Bus.wires y)

⊦ ∀x y. Bus.width (Bus.append x y) = Bus.width x + Bus.width y

⊦ ∀x y. Bus.sub x 0 (Bus.width x) y ⇔ y = x

⊦ ∀x. Bus.width x = 1 ⇔ ∃w. x = Bus.single w

⊦ ∀w t. Bus.signal (Bus.single w) t = signal w t :: []

⊦ ∀w t.
Bits.toNatural (Bus.signal (Bus.single w) t) = fromBool (signal w t)

⊦ ∀m n. Bus.ground (m + n) = Bus.append (Bus.ground m) (Bus.ground n)

⊦ ∀m n. Bus.power (m + n) = Bus.append (Bus.power m) (Bus.power n)

⊦ ∀x i w. Bus.wire x i w ⇒ i < Bus.width x

⊦ ∀x t. Bus.signal x t = map (λw. signal w t) (Bus.wires x)

⊦ ∀x i. i < Bus.width x ⇒ ∃w. Bus.wire x i w

⊦ ∀x y z. ∃s c. adder3 x y z s c

⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.and2 x y z

⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.or2 x y z

⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.xor2 x y z

⊦ ∀x y z. and2 x y z ⇒ case1 x y ground z

⊦ ∀x y z. and2 x y z ⇒ majority3 x y ground z

⊦ ∀x y z. or2 x y z ⇒ case1 x power y z

⊦ ∀x y z. or2 x y z ⇒ or3 x y ground z

⊦ ∀x y z. xor2 x y z ⇒ xor3 x y ground z

⊦ ∀r w x. Bus.lift2 r (Bus.single w) (Bus.single x) ⇔ r w x

⊦ ∀r. (∀w. r w w w) ⇒ ∀x. Bus.lift3 r x x x

⊦ ∀x y z. Bus.append (Bus.append x y) z = Bus.append x (Bus.append y z)

⊦ ∀x y t. Bus.connect x y ⇒ Bus.signal y t = Bus.signal x t

⊦ ∀w x v. Bus.wire (Bus.append (Bus.single w) x) 0 v ⇔ v = w

⊦ ∀x y t. connect x y ⇒ (signal y t ⇔ signal x t)

⊦ ∀x y. connect x y ⇔ ∀t. signal y t ⇔ signal x t

⊦ ∀w₁ w₂. (∀t. signal w₁ t ⇔ signal w₂ t) ⇔ w₁ = w₂

⊦ ∀w₁ w₂. (∀t. signal w₁ t ⇔ signal w₂ t) ⇒ w₁ = w₂

⊦ ∀r. (∀xi. ∃yi. r xi yi) ⇒ ∀x. ∃y. Bus.lift2 r x y

⊦ ∀x k n y. Bus.sub x k n y ⇒ Bus.width y = n

⊦ ∀x y z. Bus.sub (Bus.append x y) 0 (Bus.width x) z ⇔ z = x

⊦ ∀x i w. Bus.wire x i w ⇔ Bus.sub x i 1 (Bus.single w)

⊦ ∀x y z.
Bus.and2 (Bus.single x) (Bus.single y) (Bus.single z) ⇔ and2 x y z

⊦ ∀x y z. Bus.or2 (Bus.single x) (Bus.single y) (Bus.single z) ⇔ or2 x y z

⊦ ∀x y z.
Bus.xor2 (Bus.single x) (Bus.single y) (Bus.single z) ⇔ xor2 x y z

⊦ ∀x y t. not x y ⇒ (signal y t ⇔ ¬signal x t)

⊦ ∀x y. not x y ⇔ ∀t. signal y t ⇔ ¬signal x t

⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃s c. Bus.adder2 x y s c

⊦ ∀s x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.case1 s x y z

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.power n) t) = 2 ↑ n - 1

⊦ ∀x y z. Bus.sub (Bus.append x y) (Bus.width x) (Bus.width y) z ⇔ z = y

⊦ ∀x y t. Bus.signal (Bus.append x y) t = Bus.signal x t @ Bus.signal y t

⊦ ∀x y n. Bus.connect x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀x y n. Bus.delay x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀x y n. Bus.not x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀x y n. Bus.reverse x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀x y. Bus.connect x y ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n

⊦ ∀x y. Bus.delay x y ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n

⊦ ∀x y. Bus.not x y ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n

⊦ ∀x y. Bus.reverse x y ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n

⊦ ∀w i v. Bus.wire (Bus.single w) i v ⇔ i = 0 ∧ v = w

⊦ ∀n k w. Bus.wire (Bus.ground n) k w ⇔ k < n ∧ w = ground

⊦ ∀x k n y. Bus.sub x k n y ⇒ k + n ≤ Bus.width x

⊦ ∀x k n. k + n ≤ Bus.width x ⇒ ∃y. Bus.sub x k n y

⊦ ∀x y s c. adder2 x y s c ⇒ adder3 x y ground s c

⊦ ∀x y t. Bus.delay x y ⇒ Bus.signal y (t + 1) = Bus.signal x t

⊦ ∀x y k. Bus.sub x k 0 y ⇔ k ≤ Bus.width x ∧ y = Bus.nil

⊦ ∀x n y. Bus.width x = n ∧ Bus.connect x y ⇒ Bus.or2 x (Bus.ground n) y

⊦ ∀x n y. Bus.width x = n ∧ Bus.connect x y ⇒ Bus.xor2 x (Bus.ground n) y

⊦ ∀w x t.
Bus.signal (Bus.append (Bus.single w) x) t =
signal w t :: Bus.signal x t

⊦ ∀x y t. delay x y ⇒ (signal y (t + 1) ⇔ signal x t)

⊦ ∀x y. delay x y ⇔ ∀t. signal y (t + 1) ⇔ signal x t

⊦ ∀r x y.
Bus.lift2 r (Bus.ground (Bus.width x)) y ⇔
Bus.lift2 (λx y. r ground y) x y

⊦ ∀x i w₁ w₂. Bus.wire x i w₁ ∧ Bus.wire x i w₂ ⇒ w₁ = w₂

⊦ ∀w x i v.
Bus.wire (Bus.append (Bus.single w) x) (suc i) v ⇔ Bus.wire x i v

⊦ ∀r w x y.
Bus.lift3 r (Bus.single w) (Bus.single x) (Bus.single y) ⇔ r w x y

⊦ ∀x n y.
Bus.width x = n ∧ Bus.connect (Bus.ground n) y ⇒
Bus.and2 x (Bus.ground n) y

⊦ ∀x y z n. Bus.and2 x y z ∧ Bus.width x = n ⇒ Bus.width z = n

⊦ ∀x y z n. Bus.or2 x y z ∧ Bus.width x = n ⇒ Bus.width z = n

⊦ ∀x y z n. Bus.xor2 x y z ∧ Bus.width x = n ⇒ Bus.width z = n

⊦ ∀x y i w. Bus.wire (Bus.append x y) (Bus.width x + i) w ⇔ Bus.wire y i w

⊦ ∀s x y z.
Bus.case1 s (Bus.single x) (Bus.single y) (Bus.single z) ⇔
case1 s x y z

⊦ ∀x y z xn. not x xn ∧ and2 xn y z ⇒ case1 x ground y z

⊦ ∀w d wd t. pipe w d wd ⇒ (signal wd (t + d) ⇔ signal w t)

⊦ ∀r x y n. Bus.lift2 r x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀r x y. Bus.lift2 r x y ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n

⊦ ∀x y s c. Bus.adder2 x y s c ⇔ Bus.xor2 x y s ∧ Bus.and2 x y c

⊦ ∀x₁ x₂ y₁ y₂.
Bus.connect x₁ y₁ ∧ Bus.connect x₂ y₂ ⇒
Bus.connect (Bus.append x₁ x₂) (Bus.append y₁ y₂)

⊦ ∀x₁ x₂ y₁ y₂.
Bus.delay x₁ y₁ ∧ Bus.delay x₂ y₂ ⇒
Bus.delay (Bus.append x₁ x₂) (Bus.append y₁ y₂)

⊦ ∀x₁ x₂ y₁ y₂.
Bus.not x₁ y₁ ∧ Bus.not x₂ y₂ ⇒
Bus.not (Bus.append x₁ x₂) (Bus.append y₁ y₂)

⊦ ∀x₁ x₂ y₁ y₂.
Bus.reverse x₁ y₂ ∧ Bus.reverse x₂ y₁ ⇒
Bus.reverse (Bus.append x₁ x₂) (Bus.append y₁ y₂)

⊦ ∀x y s c. adder2 x y s c ⇔ xor2 x y s ∧ and2 x y c

⊦ ∀x y s c.
Bus.adder2 (Bus.single x) (Bus.single y) (Bus.single s)
(Bus.single c) ⇔ adder2 x y s c

⊦ ∀w x y z.
Bus.and3 (Bus.single w) (Bus.single x) (Bus.single y) (Bus.single z) ⇔
and3 w x y z

⊦ ∀w x y z.
Bus.majority3 (Bus.single w) (Bus.single x) (Bus.single y)
(Bus.single z) ⇔ majority3 w x y z

⊦ ∀w x y z.
Bus.or3 (Bus.single w) (Bus.single x) (Bus.single y) (Bus.single z) ⇔
or3 w x y z

⊦ ∀w x y z.
Bus.xor3 (Bus.single w) (Bus.single x) (Bus.single y) (Bus.single z) ⇔
xor3 w x y z

⊦ ∀k n x. Bus.sub Bus.nil k n x ⇔ k = 0 ∧ n = 0 ∧ x = Bus.nil

⊦ ∀x y n z.
Bus.width x = n ∧ Bus.and2 x y z ⇒ Bus.majority3 x y (Bus.ground n) z

⊦ ∀x y n z. Bus.width x = n ∧ Bus.or2 x y z ⇒ Bus.or3 x y (Bus.ground n) z

⊦ ∀x y n z.
Bus.width x = n ∧ Bus.xor2 x y z ⇒ Bus.xor3 x y (Bus.ground n) z

⊦ ∀x y i w.
i < Bus.width x ⇒ (Bus.wire (Bus.append x y) i w ⇔ Bus.wire x i w)

⊦ ∀x y z t. and2 x y z ⇒ (signal z t ⇔ signal x t ∧ signal y t)

⊦ ∀x y z t. or2 x y z ⇒ (signal z t ⇔ signal x t ∨ signal y t)

⊦ ∀x y z. and2 x y z ⇔ ∀t. signal z t ⇔ signal x t ∧ signal y t

⊦ ∀x y z. or2 x y z ⇔ ∀t. signal z t ⇔ signal x t ∨ signal y t

⊦ ∀x y. pulse x y ⇔ ∃xd xn. delay x xd ∧ not xd xn ∧ and2 x xn y

⊦ ∀x y s c n. Bus.adder2 x y s c ∧ Bus.width x = n ⇒ Bus.width s = n

⊦ ∀x y s c n. Bus.adder2 x y s c ∧ Bus.width x = n ⇒ Bus.width c = n

⊦ ∀w x y z n. Bus.and3 w x y z ∧ Bus.width w = n ⇒ Bus.width z = n

⊦ ∀w x y z n. Bus.majority3 w x y z ∧ Bus.width w = n ⇒ Bus.width z = n

⊦ ∀w x y z n. Bus.or3 w x y z ∧ Bus.width w = n ⇒ Bus.width z = n

⊦ ∀w x y z n. Bus.xor3 w x y z ∧ Bus.width w = n ⇒ Bus.width z = n

⊦ ∀w x y z. Bus.and3 w x y z ⇔ ∃wx. Bus.and2 w x wx ∧ Bus.and2 wx y z

⊦ ∀w x y z. Bus.or3 w x y z ⇔ ∃wx. Bus.or2 w x wx ∧ Bus.or2 wx y z

⊦ ∀w x y z. Bus.xor3 w x y z ⇔ ∃wx. Bus.xor2 w x wx ∧ Bus.xor2 wx y z

⊦ ∀x k n y z. Bus.sub x k n y ∧ Bus.sub x k n z ⇒ y = z

⊦ ∀s x y z n. Bus.case1 s x y z ∧ Bus.width x = n ⇒ Bus.width z = n

⊦ ∀w x y z. and3 w x y z ⇔ ∃wx. and2 w x wx ∧ and2 wx y z

⊦ ∀w x y z. or3 w x y z ⇔ ∃wx. or2 w x wx ∧ or2 wx y z

⊦ ∀w x y z. xor3 w x y z ⇔ ∃wx. xor2 w x wx ∧ xor2 wx y z

⊦ ∀r x y z n. Bus.lift3 r x y z ∧ Bus.width x = n ⇒ Bus.width z = n

⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.and3 w x y z

⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.majority3 w x y z

⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.or3 w x y z

⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.xor3 w x y z

⊦ ∀xh xt yh yt.
Bus.connect (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) ⇔ connect xh yh ∧ Bus.connect xt yt

⊦ ∀xh xt yh yt.
Bus.delay (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) ⇔ delay xh yh ∧ Bus.delay xt yt

⊦ ∀xh xt yh yt.
Bus.not (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) ⇔ not xh yh ∧ Bus.not xt yt

⊦ ∀w₁ w₂ x₁ x₂.
Bus.append (Bus.single w₁) x₁ = Bus.append (Bus.single w₂) x₂ ⇔
w₁ = w₂ ∧ x₁ = x₂

⊦ ∀x y z t. xor2 x y z ⇒ (signal z t ⇔ ¬(signal x t ⇔ signal y t))

⊦ ∀x y z. xor2 x y z ⇔ ∀t. signal z t ⇔ ¬(signal x t ⇔ signal y t)

⊦ ∀n x.
Bus.width x = suc n ⇔
∃w y. x = Bus.append (Bus.single w) y ∧ Bus.width y = n

⊦ ∀n i k x. Bus.sub (Bus.ground n) i k x ⇔ i + k ≤ n ∧ x = Bus.ground k

⊦ ∀n i k x. Bus.sub (Bus.power n) i k x ⇔ i + k ≤ n ∧ x = Bus.power k

⊦ ∀x y k n z.
Bus.sub (Bus.append x y) (Bus.width x + k) n z ⇔ Bus.sub y k n z

⊦ ∀x y t.
    Bits.toNatural (Bus.signal (Bus.append x y) t) =
    Bits.toNatural (Bus.signal x t) +
    Bits.shiftLeft (Bits.toNatural (Bus.signal y t)) (Bus.width x)

⊦ ∀x y i xi yi.
Bus.connect x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ connect xi yi

⊦ ∀x y i xi yi.
Bus.delay x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ delay xi yi

⊦ ∀x y i xi yi. Bus.not x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ not xi yi

⊦ ∀x k n y t.
    Bus.sub x k n y ⇒
    Bits.shiftLeft (Bits.toNatural (Bus.signal y t)) k ≤
    Bits.toNatural (Bus.signal x t)

⊦ ∀x y z s c n. Bus.adder3 x y z s c ∧ Bus.width x = n ⇒ Bus.width s = n

⊦ ∀x y z s c n. Bus.adder3 x y z s c ∧ Bus.width x = n ⇒ Bus.width c = n

⊦ ∀x y z.
Bus.and2 x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀x y z.
Bus.or2 x y z ⇒ ∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀x y z.
Bus.xor2 x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀x i w t.
Bus.wire x i w ∧ signal w t ⇒ 2 ↑ i ≤ Bits.toNatural (Bus.signal x t)

⊦ ∀x y z s c.
Bus.adder3 x y z s c ⇔ Bus.xor3 x y z s ∧ Bus.majority3 x y z c

⊦ ∀x y z.
Bus.width x = Bus.width y ∧ Bus.width x = Bus.width z ⇒
∃s c. Bus.adder3 x y z s c

⊦ ∀x y n s c.
Bus.width x = n ∧ Bus.adder2 x y s c ⇒
Bus.adder3 x y (Bus.ground n) s c

⊦ ∀w x i xi t.
Bus.pipe w x ∧ Bus.wire x i xi ⇒ (signal xi (t + i) ⇔ signal w t)

⊦ ∀x y z s c. adder3 x y z s c ⇔ xor3 x y z s ∧ majority3 x y z c

⊦ ∀x y z s c.
Bus.adder3 (Bus.single x) (Bus.single y) (Bus.single z) (Bus.single s)
(Bus.single c) ⇔ adder3 x y z s c

⊦ ∀r x₁ x₂ y₁ y₂.
Bus.lift2 r x₁ y₁ ∧ Bus.lift2 r x₂ y₂ ⇒
Bus.lift2 r (Bus.append x₁ x₂) (Bus.append y₁ y₂)

⊦ ∀x k n y i w. Bus.sub x k n y ∧ Bus.wire y i w ⇒ Bus.wire x (k + i) w

⊦ ∀r s x y. (∀xi yi. r xi yi ⇒ s xi yi) ∧ Bus.lift2 r x y ⇒ Bus.lift2 s x y

⊦ ∀r x n y.
Bus.lift3 r x (Bus.ground n) y ⇔
Bus.width x = n ∧ Bus.lift2 (λx y. r x ground y) x y

⊦ ∀x k n y t.
    Bus.sub x k n y ⇒
    Bits.toNatural (Bus.signal y t) =
    Bits.bound (Bits.shiftRight (Bits.toNatural (Bus.signal x t)) k) n

⊦ ∀x y t. pulse x y ⇒ (signal y (t + 1) ⇔ ¬signal x t ∧ signal x (t + 1))

⊦ ∀r xh xt yh yt.
Bus.lift2 r (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) ⇔ r xh yh ∧ Bus.lift2 r xt yt

⊦ ∀r.
(∀xi yi. ∃zi. r xi yi zi) ⇒
∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.lift3 r x y z

⊦ ∀r x y i xi yi.
Bus.lift2 r x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ r xi yi

⊦ ∀x y k n z.
k + n ≤ Bus.width x ⇒
(Bus.sub (Bus.append x y) k n z ⇔ Bus.sub x k n z)

⊦ ∀s x y z t.
Bus.case1 s x y z ⇒
Bus.signal z t = if signal s t then Bus.signal x t else Bus.signal y t

⊦ ∀s x y z.
Bus.case1 s x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀s x y z t.
case1 s x y z ⇒
(signal z t ⇔ if signal s t then signal x t else signal y t)

⊦ ∀s x y z.
case1 s x y z ⇔
∀t. signal z t ⇔ if signal s t then signal x t else signal y t

⊦ ∀r x y z.
Bus.lift3 r x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀x y k n xs ys.
Bus.connect x y ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ⇒
Bus.connect xs ys

⊦ ∀x y k n xs ys.
Bus.delay x y ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ⇒ Bus.delay xs ys

⊦ ∀x y k n xs ys.
Bus.not x y ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ⇒ Bus.not xs ys

⊦ ∀x k n y.
Bus.sub x k n y ⇔
k + n ≤ Bus.width x ∧ y = bus (take n (drop k (Bus.wires x)))

⊦ ∀x w y k n.
Bus.wire x k w ∧ Bus.sub x (suc k) n y ⇒
Bus.sub x k (suc n) (Bus.append (Bus.single w) y)

⊦ ∀ld xs xc xb.
SumCarry.shiftRight ld xs xc xb ⇒
∃r. Bus.width xs = r + 1 ∧ Bus.width xc = r + 1

⊦ ∀w x y z t.
and3 w x y z ⇒ (signal z t ⇔ signal w t ∧ signal x t ∧ signal y t)

⊦ ∀w x y z t.
or3 w x y z ⇒ (signal z t ⇔ signal w t ∨ signal x t ∨ signal y t)

⊦ ∀w x y z t.
xor3 w x y z ⇒ (signal z t ⇔ signal w t ⇔ signal x t ⇔ signal y t)

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂.
Bus.and2 x₁ y₁ z₁ ∧ Bus.and2 x₂ y₂ z₂ ⇒
Bus.and2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂.
Bus.or2 x₁ y₁ z₁ ∧ Bus.or2 x₂ y₂ z₂ ⇒
Bus.or2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂.
Bus.xor2 x₁ y₁ z₁ ∧ Bus.xor2 x₂ y₂ z₂ ⇒
Bus.xor2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀x j m y k n z. Bus.sub x j m y ∧ Bus.sub y k n z ⇒ Bus.sub x (j + k) n z

⊦ ∀n x t.
(∀i xi. Bus.wire x i xi ⇒ (signal xi t ⇔ Bits.bit n i)) ⇒
Bits.toNatural (Bus.signal x t) = Bits.bound n (Bus.width x)

⊦ ∀x k n y i w.
Bus.sub x k n y ⇒ (Bus.wire y i w ⇔ i < n ∧ Bus.wire x (k + i) w)

⊦ ∀x y j yj.
Bus.reverse x y ∧ Bus.wire y j yj ⇒
∃i. i + (j + 1) = Bus.width x ∧ Bus.wire x i yj

⊦ ∀r x y k n xs ys.
Bus.lift2 r x y ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ⇒
Bus.lift2 r xs ys

⊦ ∀x y z k m n.
Bus.sub x k m y ∧ Bus.sub x (k + m) n z ⇒
Bus.sub x k (m + n) (Bus.append y z)

⊦ ∀xh xt yh yt zh zt.
    Bus.and2 (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt) ⇔
    and2 xh yh zh ∧ Bus.and2 xt yt zt

⊦ ∀xh xt yh yt zh zt.
Bus.or2 (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)
(Bus.append (Bus.single zh) zt) ⇔ or2 xh yh zh ∧ Bus.or2 xt yt zt

⊦ ∀xh xt yh yt zh zt.
    Bus.xor2 (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt) ⇔
    xor2 xh yh zh ∧ Bus.xor2 xt yt zt

⊦ ∀ld w x.
sticky ld w x ⇔
∃p q r. case1 ld ground p q ∧ or2 w q r ∧ delay r p ∧ connect r x

⊦ ∀x y s c.
    Bus.adder2 x y s c ⇒
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧ Bus.width s = n ∧ Bus.width c = n

⊦ ∀w x y z.
    Bus.and3 w x y z ⇒
    ∃n.
      Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀w x y z.
    Bus.majority3 w x y z ⇒
    ∃n.
      Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀w x y z.
    Bus.or3 w x y z ⇒
    ∃n.
      Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀w x y z.
    Bus.xor3 w x y z ⇒
    ∃n.
      Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n

⊦ ∀w d wd.
    pipe w d wd ⇔
    ∃x x₀.
      Bus.width x = d + 1 ∧ Bus.wire x d x₀ ∧ Bus.pipe w x ∧ connect x₀ wd

⊦ ∀r s x y z.
(∀xi yi zi. r xi yi zi ⇒ s xi yi zi) ∧ Bus.lift3 r x y z ⇒
Bus.lift3 s x y z

⊦ ∀w x y z s c n.
Bus.adder4 w x y z s c ∧ Bus.width w = n + 1 ⇒ Bus.width c = n + 1

⊦ ∀s x₁ x₂ y₁ y₂ z₁ z₂.
Bus.case1 s x₁ y₁ z₁ ∧ Bus.case1 s x₂ y₂ z₂ ⇒
Bus.case1 s (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀r x₁ x₂ y₁ y₂ z₁ z₂.
Bus.lift3 r x₁ y₁ z₁ ∧ Bus.lift3 r x₂ y₂ z₂ ⇒
Bus.lift3 r (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀w x y z s c n.
Bus.adder4 w x y z s c ∧ Bus.width w = n + 1 ⇒ Bus.width s = n + 2

⊦ ∀x y z i xi yi zi.
Bus.and2 x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒
and2 xi yi zi

⊦ ∀x y z i xi yi zi.
Bus.or2 x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒
or2 xi yi zi

⊦ ∀x y z i xi yi zi.
Bus.xor2 x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒
xor2 xi yi zi

⊦ ∀x y i xi yi xt yt.
Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.signal x xt = Bus.signal y yt ⇒
(signal xi xt ⇔ signal yi yt)

⊦ ∀x j m y k n z.
Bus.sub x j m y ⇒ (Bus.sub y k n z ⇔ k + n ≤ m ∧ Bus.sub x (j + k) n z)

⊦ ∀r xh xt yh yt zh zt.
    Bus.lift3 r (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt) ⇔
    r xh yh zh ∧ Bus.lift3 r xt yt zt

⊦ ∀x y s c t.
    Bus.adder2 x y s c ⇒
    Bits.toNatural (Bus.signal x t) + Bits.toNatural (Bus.signal y t) =
    Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)

⊦ ∀w x y z.
    Bus.majority3 w x y z ⇔
    ∃wx wy xy.
      Bus.and2 w x wx ∧ Bus.and2 w y wy ∧ Bus.and2 x y xy ∧
      Bus.or3 wx wy xy z

⊦ ∀s xh xt yh yt zh zt.
    Bus.case1 s (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt) ⇔
    case1 s xh yh zh ∧ Bus.case1 s xt yt zt

⊦ ∀x y s c t.
    adder2 x y s c ⇒
    fromBool (signal x t) + fromBool (signal y t) =
    fromBool (signal s t) + 2 * fromBool (signal c t)

⊦ ∀w x y z.
majority3 w x y z ⇔
∃wx wy xy. and2 w x wx ∧ and2 w y wy ∧ and2 x y xy ∧ or3 wx wy xy z

⊦ ∀x₁ x₂ y₁ y₂ s₁ s₂ c₁ c₂.
    Bus.adder2 x₁ y₁ s₁ c₁ ∧ Bus.adder2 x₂ y₂ s₂ c₂ ⇒
    Bus.adder2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append s₁ s₂)
      (Bus.append c₁ c₂)

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.and3 w₁ x₁ y₁ z₁ ∧ Bus.and3 w₂ x₂ y₂ z₂ ⇒
    Bus.and3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.majority3 w₁ x₁ y₁ z₁ ∧ Bus.majority3 w₂ x₂ y₂ z₂ ⇒
    Bus.majority3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.or3 w₁ x₁ y₁ z₁ ∧ Bus.or3 w₂ x₂ y₂ z₂ ⇒
    Bus.or3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.xor3 w₁ x₁ y₁ z₁ ∧ Bus.xor3 w₂ x₂ y₂ z₂ ⇒
    Bus.xor3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀s r.
(∀x y z. s x z ⇒ r x y z) ⇒
∀x y z. Bus.width x = Bus.width y ∧ Bus.lift2 s x z ⇒ Bus.lift3 r x y z

⊦ ∀r x y z i xi yi zi.
Bus.lift3 r x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire z i zi ⇒ r xi yi zi

⊦ ∀s x y z i xi yi zi.
Bus.case1 s x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire z i zi ⇒ case1 s xi yi zi

⊦ ∀r x y.
    Bus.lift2 r x y ⇔
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧
      ∀i xi yi. Bus.wire x i xi ∧ Bus.wire y i yi ⇒ r xi yi

⊦ ∀x y z k n xs ys zs.
Bus.and2 x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.and2 xs ys zs

⊦ ∀x y z k n xs ys zs.
Bus.or2 x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.or2 xs ys zs

⊦ ∀x y z k n xs ys zs.
Bus.xor2 x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.xor2 xs ys zs

⊦ ∀x y k n xs ys xt yt.
Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.signal x xt = Bus.signal y yt ⇒ Bus.signal xs xt = Bus.signal ys yt

⊦ ∀x y z s c.
    Bus.adder3 x y z s c ⇒
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n ∧
      Bus.width s = n ∧ Bus.width c = n

⊦ ∀w x y z.
    ¬(Bus.width w = 0) ∧ Bus.width w = Bus.width x ∧
    Bus.width w = Bus.width y ∧ Bus.width w = Bus.width z ⇒
    ∃s c. Bus.adder4 w x y z s c

⊦ ∀w x y z t.
    majority3 w x y z ⇒
    (signal z t ⇔
     signal w t ∧ signal x t ∨ signal w t ∧ signal y t ∨
     signal x t ∧ signal y t)

⊦ ∀xh xt yh yt sh st ch ct.
    Bus.adder2 (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single sh) st)
      (Bus.append (Bus.single ch) ct) ⇔
    adder2 xh yh sh ch ∧ Bus.adder2 xt yt st ct

⊦ ∀wh wt xh xt yh yt zh zt.
    Bus.and3 (Bus.append (Bus.single wh) wt)
      (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)
      (Bus.append (Bus.single zh) zt) ⇔
    and3 wh xh yh zh ∧ Bus.and3 wt xt yt zt

⊦ ∀wh wt xh xt yh yt zh zt.
    Bus.majority3 (Bus.append (Bus.single wh) wt)
      (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)
      (Bus.append (Bus.single zh) zt) ⇔
    majority3 wh xh yh zh ∧ Bus.majority3 wt xt yt zt

⊦ ∀wh wt xh xt yh yt zh zt.
    Bus.or3 (Bus.append (Bus.single wh) wt) (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt) ⇔
    or3 wh xh yh zh ∧ Bus.or3 wt xt yt zt

⊦ ∀wh wt xh xt yh yt zh zt.
    Bus.xor3 (Bus.append (Bus.single wh) wt)
      (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)
      (Bus.append (Bus.single zh) zt) ⇔
    xor3 wh xh yh zh ∧ Bus.xor3 wt xt yt zt

⊦ ∀x y.
    Bus.reverse x y ⇔
    Bus.width x = Bus.width y ∧
    ∀i j xi yj.
      i + (j + 1) = Bus.width x ∧ Bus.wire x i xi ∧ Bus.wire y j yj ⇒
      xi = yj

⊦ ∀s x y z k n xs ys zs.
Bus.case1 s x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.case1 s xs ys zs

⊦ ∀r x y z k n xs ys zs.
Bus.lift3 r x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.lift3 r xs ys zs

⊦ ∀x y z s c t.
    Bus.adder3 x y z s c ⇒
    Bits.toNatural (Bus.signal x t) +
    (Bits.toNatural (Bus.signal y t) + Bits.toNatural (Bus.signal z t)) =
    Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)

⊦ ∀x y z s c t.
    adder3 x y z s c ⇒
    fromBool (signal x t) +
    (fromBool (signal y t) + fromBool (signal z t)) =
    fromBool (signal s t) + 2 * fromBool (signal c t)

⊦ ∀x y s c i xi yi si ci.
Bus.adder2 x y s c ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire s i si ∧ Bus.wire c i ci ⇒ adder2 xi yi si ci

⊦ ∀w x y z i wi xi yi zi.
Bus.and3 w x y z ∧ Bus.wire w i wi ∧ Bus.wire x i xi ∧
Bus.wire y i yi ∧ Bus.wire z i zi ⇒ and3 wi xi yi zi

⊦ ∀w x y z i wi xi yi zi.
Bus.majority3 w x y z ∧ Bus.wire w i wi ∧ Bus.wire x i xi ∧
Bus.wire y i yi ∧ Bus.wire z i zi ⇒ majority3 wi xi yi zi

⊦ ∀w x y z i wi xi yi zi.
Bus.or3 w x y z ∧ Bus.wire w i wi ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire z i zi ⇒ or3 wi xi yi zi

⊦ ∀w x y z i wi xi yi zi.
Bus.xor3 w x y z ∧ Bus.wire w i wi ∧ Bus.wire x i xi ∧
Bus.wire y i yi ∧ Bus.wire z i zi ⇒ xor3 wi xi yi zi

⊦ ∀ld w x t k.
(∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧ sticky ld w x ⇒
(signal x (t + k) ⇔ ∃i. i ≤ k ∧ signal w (t + i))

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂ s₁ s₂ c₁ c₂.
    Bus.adder3 x₁ y₁ z₁ s₁ c₁ ∧ Bus.adder3 x₂ y₂ z₂ s₂ c₂ ⇒
    Bus.adder3 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)
      (Bus.append s₁ s₂) (Bus.append c₁ c₂)

⊦ ∀x k n y.
    Bus.sub x k n y ⇒
    ∃d p q.
      Bus.width x = k + (n + d) ∧ Bus.sub x 0 k p ∧ Bus.sub x (k + n) d q ∧
      x = Bus.append p (Bus.append y q)

⊦ ∀r p.
    p Bus.nil Bus.nil ∧
    (∀xh xt yh yt.
       r xh yh ∧ Bus.lift2 r xt yt ∧ p xt yt ⇒
       p (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)) ⇒
    ∀x y. Bus.lift2 r x y ⇒ p x y

⊦ ∀x y s c k n xs ys ss cs.
Bus.adder2 x y s c ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub s k n ss ∧ Bus.sub c k n cs ⇒ Bus.adder2 xs ys ss cs

⊦ ∀w x y z k n ws xs ys zs.
Bus.and3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.and3 ws xs ys zs

⊦ ∀w x y z k n ws xs ys zs.
Bus.majority3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.majority3 ws xs ys zs

⊦ ∀w x y z k n ws xs ys zs.
Bus.or3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.or3 ws xs ys zs

⊦ ∀w x y z k n ws xs ys zs.
Bus.xor3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.xor3 ws xs ys zs

⊦ ∀xh xt yh yt zh zt sh st ch ct.
    Bus.adder3 (Bus.append (Bus.single xh) xt)
      (Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt)
      (Bus.append (Bus.single sh) st) (Bus.append (Bus.single ch) ct) ⇔
    adder3 xh yh zh sh ch ∧ Bus.adder3 xt yt zt st ct

⊦ ∀w x y z s c t.
    Bus.adder4 w x y z s c ⇒
    Bits.toNatural (Bus.signal w t) +
    (Bits.toNatural (Bus.signal x t) +
     (Bits.toNatural (Bus.signal y t) + Bits.toNatural (Bus.signal z t))) =
    Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)

⊦ ∀ld xb ys yc zb zs zc.
    Bus.multiplier ld xb ys yc zb zs zc ⇒
    ∃r.
      Bus.width ys = r + 1 ∧ Bus.width yc = r + 1 ∧ Bus.width zs = r + 1 ∧
      Bus.width zc = r + 1

⊦ ∀ld xs xc d ys yc zb zs zc.
    SumCarry.multiplier ld xs xc d ys yc zb zs zc ⇔
    ∃xb ldd xbd.
      SumCarry.shiftRight ld xs xc xb ∧ pipe ld d ldd ∧ pipe xb d xbd ∧
      Bus.multiplier ldd xbd ys yc zb zs zc

⊦ ∀r x y z.
    Bus.lift3 r x y z ⇔
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n ∧
      ∀i xi yi zi.
        Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒ r xi yi zi

⊦ ∀x y z s c i xi yi zi si ci.
    Bus.adder3 x y z s c ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
    Bus.wire z i zi ∧ Bus.wire s i si ∧ Bus.wire c i ci ⇒
    adder3 xi yi zi si ci

⊦ ∀w x.
    Bus.pipe w x ⇔
    ∃r xp x₀ x₁ x₂.
      Bus.width x = r + 1 ∧ Bus.width xp = r ∧ Bus.wire x 0 x₀ ∧
      Bus.sub x 0 r x₁ ∧ Bus.sub x 1 r x₂ ∧ connect w x₀ ∧
      Bus.connect xp x₂ ∧ Bus.delay x₁ xp

⊦ ∀x ld xs xc xb t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    SumCarry.shiftRight ld xs xc xb ⇒ (signal xb (t + k) ⇔ Bits.bit x k)

⊦ ∀n ld nb dn t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal nb t) + (n + 2) =
    2 ↑ Bus.width nb + Bus.width nb ∧ counter ld nb dn ⇒
    (signal dn (t + k) ⇔ n < k)

⊦ ∀x y z s c k n xs ys zs ss cs.
    Bus.adder3 x y z s c ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
    Bus.sub z k n zs ∧ Bus.sub s k n ss ∧ Bus.sub c k n cs ⇒
    Bus.adder3 xs ys zs ss cs

⊦ ∀r p.
    p Bus.nil Bus.nil Bus.nil ∧
    (∀xh xt yh yt zh zt.
       r xh yh zh ∧ Bus.lift3 r xt yt zt ∧ p xt yt zt ⇒
       p (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)
         (Bus.append (Bus.single zh) zt)) ⇒
    ∀x y z. Bus.lift3 r x y z ⇒ p x y z

⊦ ∀w x y z s c.
    Bus.adder4 w x y z s c ⇒
    ∃n.
      Bus.width w = n + 1 ∧ Bus.width x = n + 1 ∧ Bus.width y = n + 1 ∧
      Bus.width z = n + 1 ∧ Bus.width s = n + 2 ∧ Bus.width c = n + 1

⊦ ∀n ld nb inc dn t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal nb t) + n = 2 ↑ Bus.width nb ∧
    eventCounter ld nb inc dn ⇒
    (signal dn (t + k) ⇔
     n ≤ size { i. i | 0 < i ∧ i + Bus.width nb ≤ k ∧ signal inc (t + i) })

⊦ ∀x y ld xb ys yc zb zs zc t k.
    (∀i.
       i ≤ k ⇒
       (signal ld (t + i) ⇔ i = 0) ∧ (signal xb (t + i) ⇔ Bits.bit x i) ∧
       (Bits.bit x i ⇒
        Bits.toNatural (Bus.signal ys (t + i)) +
        2 * Bits.toNatural (Bus.signal yc (t + i)) = y)) ∧
    Bus.multiplier ld xb ys yc zb zs zc ⇒
    Bits.cons (signal zb (t + k))
      (Bits.toNatural (Bus.signal zs (t + k)) +
       2 * Bits.toNatural (Bus.signal zc (t + k))) =
    Bits.shiftRight (Bits.bound x (k + 1) * y) k

⊦ ∀x y ld xs xc d ys yc zb zs zc t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    (∀i.
       i ≤ d + k ∧ d ≤ i ∧ i ≤ Bus.width xs + (d + 1) ⇒
       Bits.toNatural (Bus.signal ys (t + i)) +
       2 * Bits.toNatural (Bus.signal yc (t + i)) = y) ∧
    SumCarry.multiplier ld xs xc d ys yc zb zs zc ⇒
    Bits.cons (signal zb (t + (d + k)))
      (Bits.toNatural (Bus.signal zs (t + (d + k))) +
       2 * Bits.toNatural (Bus.signal zc (t + (d + k)))) =
    Bits.shiftRight (Bits.bound x (k + 1) * y) k

⊦ ∀ld xs xc xb.
    SumCarry.shiftRight ld xs xc xb ⇔
    ∃r sp sq sr cp cq cr xs₀ xs₁ sq₀ sq₁ sq₂ sq₃ cp₀ cp₁ cq₀ cq₁.
      Bus.width xs = r + 1 ∧ Bus.width xc = r + 1 ∧ Bus.width sp = r ∧
      Bus.width sq = r + 1 ∧ Bus.width sr = r ∧ Bus.width cp = r + 1 ∧
      Bus.width cq = r + 1 ∧ Bus.width cr = r + 1 ∧ Bus.wire xs 0 xs₀ ∧
      Bus.sub xs 1 r xs₁ ∧ Bus.wire sq 0 sq₀ ∧ Bus.sub sq 0 r sq₁ ∧
      Bus.sub sq 1 r sq₂ ∧ Bus.wire sq r sq₃ ∧ Bus.sub cp 0 r cp₀ ∧
      Bus.wire cp r cp₁ ∧ Bus.sub cq 0 r cq₀ ∧ Bus.wire cq r cq₁ ∧
      Bus.adder2 sp cp₀ sq₁ cq₀ ∧ connect cp₁ sq₃ ∧ connect ground cq₁ ∧
      case1 ld xs₀ sq₀ xb ∧ Bus.case1 ld xs₁ sq₂ sr ∧
      Bus.case1 ld xc cq cr ∧ Bus.delay sr sp ∧ Bus.delay cr cp

⊦ ∀ld nb dn.
    counter ld nb dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr nb₀ nb₁ cp₀ cp₁ cp₂ cq₀ cq₁ cr₀ cr₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r ∧
      Bus.width cr = r + 1 ∧ Bus.wire nb 0 nb₀ ∧ Bus.sub nb 1 r nb₁ ∧
      Bus.wire cp 0 cp₀ ∧ Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧
      Bus.wire cq 0 cq₀ ∧ Bus.sub cq 1 r cq₁ ∧ Bus.wire cr 0 cr₀ ∧
      Bus.sub cr 1 r cr₁ ∧ not cp₀ cq₀ ∧ Bus.adder2 sp cp₁ sq cq₁ ∧
      or2 dp cp₂ dq ∧ Bus.case1 ld nb₁ sq sr ∧ case1 ld nb₀ cq₀ cr₀ ∧
      Bus.case1 ld (Bus.ground r) cq₁ cr₁ ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

⊦ ∀w x y z s c.
    Bus.adder4 w x y z s c ⇔
    ∃n p q z₀ z₁ s₀ s₁ s₂ c₀ c₁ p₀ p₁ q₁ q₂.
      Bus.width w = n + 1 ∧ Bus.width x = n + 1 ∧ Bus.width y = n + 1 ∧
      Bus.width z = n + 1 ∧ Bus.width s = n + 2 ∧ Bus.width c = n + 1 ∧
      Bus.width p = n + 1 ∧ Bus.width q = n + 1 ∧ Bus.wire z 0 z₀ ∧
      Bus.sub z 1 n z₁ ∧ Bus.wire s 0 s₀ ∧ Bus.sub s 1 n s₁ ∧
      Bus.wire s (n + 1) s₂ ∧ Bus.wire c 0 c₀ ∧ Bus.sub c 1 n c₁ ∧
      Bus.wire p 0 p₀ ∧ Bus.sub p 1 n p₁ ∧ Bus.sub q 0 n q₁ ∧
      Bus.wire q n q₂ ∧ Bus.adder3 w x y p q ∧ adder2 p₀ z₀ s₀ c₀ ∧
      Bus.adder3 p₁ q₁ z₁ s₁ c₁ ∧ connect q₂ s₂

⊦ ∀ld nb inc dn.
    eventCounter ld nb inc dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr sp₀ sp₁ cp₀ cp₁ cp₂ sq₀ sq₁ cq₀ cq₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r + 1 ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r + 1 ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r + 1 ∧
      Bus.width cr = r + 1 ∧ Bus.wire sp 0 sp₀ ∧ Bus.sub sp 1 r sp₁ ∧
      Bus.wire sq 0 sq₀ ∧ Bus.sub sq 1 r sq₁ ∧ Bus.wire cp 0 cp₀ ∧
      Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧ Bus.wire cq 0 cq₀ ∧
      Bus.sub cq 1 r cq₁ ∧ xor2 inc sp₀ sq₀ ∧ and2 inc sp₀ cq₀ ∧
      Bus.adder2 sp₁ cp₁ sq₁ cq₁ ∧ or2 dp cp₂ dq ∧ Bus.case1 ld nb sq sr ∧
      Bus.case1 ld (Bus.ground (r + 1)) cq cr ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

⊦ ∀ld xb ys yc zb zs zc.
    Bus.multiplier ld xb ys yc zb zs zc ⇔
    ∃r sp sq sr cp cq cr yos yoc ps pc sq₀ sq₁ sr₀ sr₁ cq₀ cq₁ cr₀ cr₁ yos₀
      yos₁ yoc₀ yoc₁ pc₀ pc₁ pc₂ pc₃.
      Bus.width ys = r + 1 ∧ Bus.width yc = r + 1 ∧ Bus.width zs = r + 1 ∧
      Bus.width zc = r + 1 ∧ Bus.width sp = r + 1 ∧ Bus.width sq = r + 1 ∧
      Bus.width sr = r + 1 ∧ Bus.width cp = r + 1 ∧ Bus.width cq = r + 1 ∧
      Bus.width cr = r + 1 ∧ Bus.width yos = r + 1 ∧
      Bus.width yoc = r + 1 ∧ Bus.width ps = r ∧ Bus.width pc = r + 1 ∧
      Bus.wire sq 0 sq₀ ∧ Bus.sub sq 1 r sq₁ ∧ Bus.sub sr 0 r sr₀ ∧
      Bus.wire sr r sr₁ ∧ Bus.sub cq 0 r cq₀ ∧ Bus.wire cq r cq₁ ∧
      Bus.sub cr 0 r cr₀ ∧ Bus.wire cr r cr₁ ∧ Bus.wire yos 0 yos₀ ∧
      Bus.sub yos 1 r yos₁ ∧ Bus.sub yoc 0 r yoc₀ ∧ Bus.wire yoc r yoc₁ ∧
      Bus.wire pc 0 pc₀ ∧ Bus.sub pc 0 r pc₁ ∧ Bus.sub pc 1 r pc₂ ∧
      Bus.wire pc r pc₃ ∧ Bus.case1 ld (Bus.ground (r + 1)) sp sq ∧
      Bus.case1 ld (Bus.ground (r + 1)) cp cq ∧
      Bus.case1 xb ys (Bus.ground (r + 1)) yos ∧
      Bus.case1 xb yc (Bus.ground (r + 1)) yoc ∧ adder2 sq₀ yos₀ zb pc₀ ∧
      Bus.adder3 sq₁ cq₀ yos₁ ps pc₂ ∧ Bus.adder3 yoc₀ ps pc₁ sr₀ cr₀ ∧
      adder3 yoc₁ cq₁ pc₃ sr₁ cr₁ ∧ Bus.connect sr zs ∧ Bus.connect cr zc ∧
      Bus.delay sr sp ∧ Bus.delay cr cp

External Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×
- Stream
  - stream
Number
- Natural
  - natural
Set
- set

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - drop
  - length
  - map
  - replicate
  - take
- Pair
  - ,
  - fst
  - snd
- Stream
  - fromFunction
  - nth
  - replicate
Function
- ∘
Number
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - fromBool
  - max
  - minimal
  - suc
  - zero
  - Bits
    - Bits.bit
    - Bits.bound
    - Bits.cons
    - Bits.head
    - Bits.shiftLeft
    - Bits.shiftRight
    - Bits.tail
    - Bits.toNatural
    - Bits.width
Set
- ∅
- disjoint
- finite
- fromPredicate
- image
- insert
- ∩
- ∈
- size
- ⊆
- ∪

Assumptions

⊦ ⊤

⊦ finite ∅

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ fromBool ⊥ = 0

⊦ Bits.toNatural [] = 0

⊦ size ∅ = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ fromPredicate (λx. ⊥) = ∅

⊦ fromBool ⊤ = 1

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ ∀n. n ≤ suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀a. ∃x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀x. replicate x 0 = []

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀m. m - 0 = m

⊦ ∀n. Bits.bound n 0 = 0

⊦ ∀k. Bits.shiftLeft 0 k = 0

⊦ ∀n. Bits.shiftRight n 0 = n

⊦ ∀l. [] @ l = l

⊦ ∀l. l @ [] = l

⊦ ∀l. drop 0 l = l

⊦ ∀l. take 0 l = []

⊦ ∀f. map f [] = []

⊦ ∀f. nth (fromFunction f) = f

⊦ (∘) = λf g x. f (g x)

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀b. Bits.cons b 0 = fromBool b

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀n. Bits.bit n 0 ⇔ Bits.head n

⊦ ∀k. Bits.toNatural (replicate ⊥ k) = 0

⊦ ∀m. m * 1 = m

⊦ ∀m. 1 * m = m

⊦ ∀l. take (length l) l = l

⊦ ∀l. Bits.width (Bits.toNatural l) ≤ length l

⊦ ∀m n. m ≤ m + n

⊦ ∀m n. n ≤ m + n

⊦ ∀n k. Bits.bound n k ≤ n

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀x. size (insert x ∅) = 1

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀b. fromBool b = 0 ⇔ ¬b

⊦ ∀b. Bits.toNatural (b :: []) = fromBool b

⊦ ∀m. suc m = m + 1

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. suc n - 1 = n

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

⊦ ∀a n. nth (replicate a) n = a

⊦ ∀x n. length (replicate x n) = n

⊦ ∀h t. Bits.head (Bits.cons h t) ⇔ h

⊦ ∀h t. Bits.tail (Bits.cons h t) = t

⊦ ∀b. fromBool b = if b then 1 else 0

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

⊦ ∀n. Bits.bound n 1 = fromBool (Bits.head n)

⊦ ∀l. length l = 0 ⇔ l = []

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀m n. m < n ⇒ m ≤ n

⊦ ∀m n. m + n - m = n

⊦ ∀m n. m + n - n = m

⊦ ∀n k. Bits.bound (Bits.shiftLeft n k) k = 0

⊦ ∀s x. finite (insert x s) ⇔ finite s

⊦ ∀f l. length (map f l) = length l

⊦ ∀p x. x ∈ fromPredicate p ⇔ p x

⊦ ∅ = { x. x | ⊥ }

⊦ ∀n. Bits.cons ⊥ n = 2 * n

⊦ ∀l. Bits.toNatural l < 2 ↑ length l

⊦ ∀h t. length (h :: t) = suc (length t)

⊦ ∀n i. Bits.bit n i ⇔ Bits.head (Bits.shiftRight n i)

⊦ ∀n i. Bits.bit n i ⇒ i < Bits.width n

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

⊦ ∀m n. m < suc n ⇔ m ≤ n

⊦ ∀m n. suc m ≤ n ⇔ m < n

⊦ ∀m. m = 0 ∨ ∃n. m = suc n

⊦ ∀l₁ l₂. drop (length l₁) (l₁ @ l₂) = l₂

⊦ ∀l₁ l₂. take (length l₁) (l₁ @ l₂) = l₁

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀n. Bits.shiftLeft n 1 = 2 * n

⊦ ∀k. Bits.shiftLeft 1 k = 2 ↑ k

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀x y. x ∈ insert y ∅ ⇔ x = y

⊦ ∀h t. (h :: []) @ t = h :: t

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural t)

⊦ ∀n i. Bits.bit n (suc i) ⇔ Bits.bit (Bits.tail n) i

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀n k. Bits.shiftRight n (suc k) = Bits.tail (Bits.shiftRight n k)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀n k. Bits.width (Bits.shiftLeft n k) ≤ Bits.width n + k

⊦ ∀m n. m < m + n ⇔ 0 < n

⊦ ∀m n. n < m + n ⇔ 0 < m

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀k n. Bits.shiftLeft n k = 0 ⇔ n = 0

⊦ ∀m n. m + n ≤ m ⇔ n = 0

⊦ ∀m n. n + m ≤ m ⇔ n = 0

⊦ ∀n k. Bits.bound (Bits.bound n k) k = Bits.bound n k

⊦ ∀s t. disjoint s t ⇔ s ∩ t = ∅

⊦ ∀s t. finite t ∧ s ⊆ t ⇒ finite s

⊦ ∀n. finite { m. m | m ≤ n }

⊦ ∀x n. replicate x (suc n) = x :: replicate x n

⊦ ∀m n. m ↑ suc n = m * m ↑ n

⊦ ∀n k. Bits.shiftLeft n (suc k) = Bits.cons ⊥ (Bits.shiftLeft n k)

⊦ ∀n k. Bits.shiftLeft n (suc k) = Bits.shiftLeft (Bits.cons ⊥ n) k

⊦ ∀n k. Bits.bound n k = n ⇔ Bits.width n ≤ k

⊦ ∀n k. Bits.shiftRight n k = 0 ⇔ Bits.width n ≤ k

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ ∀p a. (∃x. x = a ∧ p x) ⇔ p a

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

⊦ ∀n k. Bits.bound n k + Bits.shiftLeft (Bits.shiftRight n k) k = n

⊦ ∀n l. n ≤ length l ⇒ length (take n l) = n

⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d

⊦ ∀k. Bits.toNatural (replicate ⊤ k) = 2 ↑ k - 1

⊦ ∀f x n. map f (replicate x n) = replicate (f x) n

⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t

⊦ ∀p q. (∀x. p ⇒ q x) ⇔ p ⇒ ∀x. q x

⊦ ∀n k.
Bits.bound n (suc k) =
Bits.cons (Bits.head n) (Bits.bound (Bits.tail n) k)

⊦ ∀a b. a ⊆ b ∧ finite b ⇒ size a ≤ size b

⊦ ∀p q. (∀x. p x ⇒ q) ⇔ (∃x. p x) ⇒ q

⊦ ∀p q. (∃x. p x) ⇒ q ⇔ ∀x. p x ⇒ q

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀k n₁ n₂. Bits.shiftLeft (n₁ * n₂) k = n₁ * Bits.shiftLeft n₂ k

⊦ ∀m n p. m + n = m + p ⇔ n = p

⊦ ∀p m n. m + p = n + p ⇔ m = n

⊦ ∀k n₁ n₂. Bits.shiftLeft n₁ k = Bits.shiftLeft n₂ k ⇔ n₁ = n₂

⊦ ∀m n p. m + n < m + p ⇔ n < p

⊦ ∀m n p. n + m < p + m ⇔ n < p

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

⊦ ∀k n₁ n₂. Bits.shiftLeft n₁ k ≤ Bits.shiftLeft n₂ k ⇔ n₁ ≤ n₂

⊦ ∀m n p. m < n ∧ n < p ⇒ m < p

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀l₁ l₂ l₃. l₁ @ l₂ @ l₃ = (l₁ @ l₂) @ l₃

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇔ s₁ = s₂

⊦ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

⊦ ∀p x. (∀y. p y ⇔ y = x) ⇒ (select) p = x

⊦ ∀f g l. map (f ∘ g) l = map f (map g l)

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n

⊦ ∀m n. Bits.width (m + n) ≤ max (Bits.width m) (Bits.width n) + 1

⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

⊦ ∀l₁ l₂.
Bits.toNatural (l₁ @ l₂) =
Bits.toNatural l₁ + Bits.shiftLeft (Bits.toNatural l₂) (length l₁)

⊦ ∀f h t. map f (h :: t) = f h :: map f t

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀n l. n ≤ length l ⇒ n + length (drop n l) = length l

⊦ ∀p x. x ∈ { y. y | p y } ⇔ p x

⊦ ∀x y s. x ∈ insert y s ⇔ x = y ∨ x ∈ s

⊦ ∀x m n. replicate x (m + n) = replicate x m @ replicate x n

⊦ ∀p q r. p ∧ (q ∨ r) ⇔ p ∧ q ∨ p ∧ r

⊦ ∀p q r. (p ∨ q) ∧ r ⇔ p ∧ r ∨ q ∧ r

⊦ ∀m n p. max n p ≤ m ⇔ n ≤ m ∧ p ≤ m

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀m n p. (m + n) * p = m * p + n * p

⊦ ∀k n₁ n₂.
Bits.shiftLeft (n₁ + n₂) k = Bits.shiftLeft n₁ k + Bits.shiftLeft n₂ k

⊦ ∀n j k.
Bits.bound (Bits.shiftLeft n k) (j + k) =
Bits.shiftLeft (Bits.bound n j) k

⊦ ∀n₁ n₂ k.
Bits.shiftRight (n₁ + Bits.shiftLeft n₂ k) k =
Bits.shiftRight n₁ k + n₂

⊦ ∀n. size { m. m | m ≤ n } = n + 1

⊦ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

⊦ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

⊦ ∀f l₁ l₂. map f (l₁ @ l₂) = map f l₁ @ map f l₂

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀n k.
Bits.bound n (suc k) =
Bits.bound n k + Bits.shiftLeft (fromBool (Bits.bit n k)) k

⊦ ∀p q. (∃x. p x ∨ q x) ⇔ (∃x. p x) ∨ ∃x. q x

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

⊦ ∀m n k.
Bits.bound (Bits.bound m k + Bits.bound n k) k = Bits.bound (m + n) k

⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n

⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m

⊦ ∀y s f. y ∈ image f s ⇔ ∃x. y = f x ∧ x ∈ s

⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p

⊦ ∀h₁ h₂ t₁ t₂. h₁ :: t₁ = h₂ :: t₂ ⇔ h₁ = h₂ ∧ t₁ = t₂

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

⊦ ∀h₁ h₂ t₁ t₂. Bits.cons h₁ t₁ = Bits.cons h₂ t₂ ⇔ (h₁ ⇔ h₂) ∧ t₁ = t₂

⊦ ∀l n. length l = suc n ⇔ ∃h t. l = h :: t ∧ length t = n

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀m n l. m + n ≤ length l ⇒ drop (m + n) l = drop m (drop n l)

⊦ ∀l₁ l1' l₂ l2'. length l₁ = length l1' ∧ l₁ @ l₂ = l1' @ l2' ⇒ l₁ = l1'

⊦ ∀l₁ l1' l₂ l2'. length l₂ = length l2' ∧ l₁ @ l₂ = l1' @ l2' ⇒ l₂ = l2'

⊦ ∀s t. finite s ∧ finite t ∧ disjoint s t ⇒ size (s ∪ t) = size s + size t

⊦ ∀m n l. m + n ≤ length l ⇒ take (m + n) l = take m l @ take n (drop m l)

⊦ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ finite s ⇒
size (image f s) = size s