Package hardware-bus: Hardware bus devices

Information

Files

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

Defined Constants

• Hardware
  • Bus
    • Bus.and2
    • Bus.and3
    • Bus.case1
    • Bus.connect
    • Bus.delay
    • Bus.lift2
    • Bus.lift3
    • Bus.majority3
    • Bus.not
    • Bus.or2
    • Bus.or3
    • Bus.reverse
    • Bus.wire
    • Bus.xor2
    • Bus.xor3

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.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.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

⊦ 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

⊦ ∀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

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

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

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

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

⊦ ∀i w. ¬Bus.wire Bus.nil i 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

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

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

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

⊦ ∀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

⊦ ∀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 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

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

⊦ ∀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

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

⊦ ∀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 y t. Bus.delay x y ⇒ Bus.signal y (t + 1) = Bus.signal x t

⊦ ∀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

⊦ ∀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

⊦ ∀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₁ 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₂)

⊦ ∀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

⊦ ∀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)

⊦ ∀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

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

⊦ ∀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

⊦ ∀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 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)

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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 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)

⊦ ∀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₂)

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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₂)

⊦ ∀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)

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

⊦ ∀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

External Type Operators

• →
• bool
• Data
  • List
    • list
• Hardware
  • bus
  • wire
• Number
  • Natural
    • natural

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • []
• Hardware
  • and2
  • and3
  • case1
  • connect
  • delay
  • ground
  • majority3
  • not
  • or2
  • or3
  • signal
  • xor2
  • xor3
  • Bus
    • Bus.append
    • Bus.ground
    • Bus.nil
    • Bus.signal
    • Bus.single
    • Bus.sub
    • Bus.width
• Number
  • Natural
    • *
    • +
    • <
    • ≤
    • ↑
    • bit0
    • bit1
    • fromBool
    • suc
    • zero
    • Bits
      • Bits.bit
      • Bits.bound
      • Bits.cons
      • Bits.head
      • Bits.shiftLeft
      • Bits.tail
      • Bits.toNatural

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ Bus.ground 0 = Bus.nil

⊦ Bus.width Bus.nil = 0

⊦ bit0 0 = 0

⊦ Bits.toNatural [] = 0

⊦ ∀x. connect x x

⊦ ⊥ ⇔ ∀p. p

⊦ fromBool ⊤ = 1

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀a. ∃x. x = a

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

⊦ ∀x. ∃y. connect x y

⊦ ∀x. ∃y. delay x y

⊦ ∀x. ∃y. not x y

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

⊦ Bus.ground 1 = Bus.single ground

⊦ ∀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

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

⊦ ∀n. ¬(suc n = 0)

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

⊦ ∀n. 0 + n = n

⊦ ∀n. Bits.bound n 0 = 0

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

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

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

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

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

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

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

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

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

⊦ ∀m. suc m = m + 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊦ ∀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. m ≤ n ⇔ ∃d. n = m + d

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

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

⊦ ∀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)

⊦ ∀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₃

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

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

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

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

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

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

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

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

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

⊦ ∀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

⊦ ∀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)