Package hardware-adder-def: Definition of hardware adder devices

Information

namehardware-adder-def
version1.10
descriptionDefinition of hardware adder devices
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-02-24
requiresbool
hardware-bus
hardware-wire
showData.Bool
Hardware

Files

Defined Constants

Theorems

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

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

⊦ ∀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 s c. adder3 x y z s c ⇔ xor3 x y z s ∧ majority3 x y z c

⊦ ∀ld xs xc xb.
    SumCarry.shiftRight ld xs xc xb ⇔
    ∃r sp sq sr cp cq cr xs0 xs1 sq0 sq1 sq2 sq3 cp0 cp1 cq0 cq1.
      Bus.width xs = Number.Natural.+ r 1 ∧
      Bus.width xc = Number.Natural.+ r 1 ∧ Bus.width sp = r ∧
      Bus.width sq = Number.Natural.+ r 1 ∧ Bus.width sr = r ∧
      Bus.width cp = Number.Natural.+ r 1 ∧
      Bus.width cq = Number.Natural.+ r 1 ∧
      Bus.width cr = Number.Natural.+ r 1 ∧ Bus.wire xs 0 xs0 ∧
      Bus.sub xs 1 r xs1 ∧ Bus.wire sq 0 sq0 ∧ Bus.sub sq 0 r sq1 ∧
      Bus.sub sq 1 r sq2 ∧ Bus.wire sq r sq3 ∧ Bus.sub cp 0 r cp0 ∧
      Bus.wire cp r cp1 ∧ Bus.sub cq 0 r cq0 ∧ Bus.wire cq r cq1 ∧
      Bus.adder2 sp cp0 sq1 cq0 ∧ connect cp1 sq3 ∧ connect ground cq1 ∧
      case1 ld xs0 sq0 xb ∧ Bus.case1 ld xs1 sq2 sr ∧
      Bus.case1 ld xc cq cr ∧ Bus.delay sr sp ∧ Bus.delay cr cp

⊦ ∀w x y z s c.
    Bus.adder4 w x y z s c ⇔
    ∃n p q z0 z1 s0 s1 s2 c0 c1 p0 p1 q1 q2.
      Bus.width w = Number.Natural.+ n 1 ∧
      Bus.width x = Number.Natural.+ n 1 ∧
      Bus.width y = Number.Natural.+ n 1 ∧
      Bus.width z = Number.Natural.+ n 1 ∧
      Bus.width s = Number.Natural.+ n 2 ∧
      Bus.width c = Number.Natural.+ n 1 ∧
      Bus.width p = Number.Natural.+ n 1 ∧
      Bus.width q = Number.Natural.+ n 1 ∧ Bus.wire z 0 z0 ∧
      Bus.sub z 1 n z1 ∧ Bus.wire s 0 s0 ∧ Bus.sub s 1 n s1 ∧
      Bus.wire s (Number.Natural.+ n 1) s2 ∧ Bus.wire c 0 c0 ∧
      Bus.sub c 1 n c1 ∧ Bus.wire p 0 p0 ∧ Bus.sub p 1 n p1 ∧
      Bus.sub q 0 n q1 ∧ Bus.wire q n q2 ∧ Bus.adder3 w x y p q ∧
      adder2 p0 z0 s0 c0 ∧ Bus.adder3 p1 q1 z1 s1 c1 ∧ connect q2 s2

External Type Operators

External Constants

Assumptions

⊦ ⊤

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