#|
Copyright (C) 1994 by Alex Bronstein and Carolyn Talcott.  All Rights
Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by Alex Bronstein and Carolyn
Talcott.  All Rights Reserved."
NO WARRANTY
Alex Bronstein and Carolyn Talcott PROVIDE ABSOLUTELY NO WARRANTY.  THE EVENT
SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR
IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.
IN NO EVENT WILL Alex Bronstein or Carolyn Talcott BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
(INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "mlp" using the compiled version.

; bcdSbi.bm: = bcdS, but with integer bits instead of booleans on the wires.
;   LESSONS:
;    - the quality of the proofs is not degraded, we usually get the same
;      case splits, except sometime with one or two more cases.
;    - the timing is degraded by 50% on average, with a range of 20% to 300%
; So in general we should stick (or start) with a boolean model of 0 and 1,
; but if for some crucial reason we have to go numerical, it's no major
; disaster.
;
;;; CIRCUIT in SUGARED form:

#|
(setq sysd '(sy-BCDSBI (x)
(Y01 S bnot x)
(Y02 S bnot x)
(Y03 S bnot YR3)
(Y04 S bnot YR1)
(Y05 S bnot YR2)
(Y06 S bnot YR3)
(Y07 S bnot YR1)
(Y08 S bnot YR3)
(Y11 S band3 Y01 YR1 YR3)
(Y12 S band3 Y02 YR2 Y03)
(Y13 S band3 Y04 Y05 Y06)
(Y14 S band3 x Y07 Y08)
(Y15 S band3 x YR1 YR3)
(Y21 S bor Y11 Y12)
(Y22 S bor Y13 Y14)
(Y23 S bor YR2 Y15)
(YR1 R 0 Y21)
(YR2 R 0 Y22)
(YR3 R 0 Y23)
(Y31 S bnot YR1)
(Y32 S bnot YR2)
(Y41 S band4 x Y31 Y32 YR3)
(Yout S bnot Y41)
))
(setq bcdSbi '( |#
; this load entered by hand, because needed in the SPEC
; comb_band.bm: Binary And combinational element
; U7-DONE

Definition: band (u, v) = if (u = 0) ∨ (v = 0) then 0

else 1 endif

; Everything below generated by: (bmcomb 'band '() '(x y))

Definition: s-band (x, y) = if empty (x) then e

else a (s-band (p (x), p (y)), band (l (x), l (y))) endif

;; A2-Begin-S-BAND

Theorem: a2-empty-s-band empty (s-band (x, y)) = empty (x)

Theorem: a2-e-s-band (s-band (x, y) = e) = empty (x)

Theorem: a2-lp-s-band len (s-band (x, y)) = len (x)

Theorem: a2-lpe-s-band eqlen (s-band (x, y), x)

Theorem: a2-ic-s-band (len (x) = len (y)) → (s-band (i (c x, x), i (c y, y)) = i (band (c x, c y), s-band (x, y)))

Theorem: a2-lc-s-band (¬ empty (x)) → (l (s-band (x, y)) = band (l (x), l (y)))

Theorem: a2-pc-s-band p (s-band (x, y)) = s-band (p (x), p (y))

Theorem: a2-hc-s-band ((¬ empty (x)) ∧ (len (x) = len (y))) → (h (s-band (x, y)) = band (h (x), h (y)))

Theorem: a2-bc-s-band (len (x) = len (y)) → (b (s-band (x, y)) = s-band (b (x), b (y)))

Theorem: a2-bnc-s-band (len (x) = len (y)) → (bn (n, s-band (x, y)) = s-band (bn (n, x), bn (n, y)))

;; A2-End-S-BAND
; eof:comb_band.bm

; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_band3.bm: Binary And3 combinational element
; U7-DONE

Definition: band3 (u1 , u2 , u3 ) = if (u1 = 0) ∨ (u2 = 0) ∨ (u3 = 0) then 0

else 1 endif

; Everything below generated by: (bmcomb 'band3 '() '(x1 x2 x3))

Definition: s-band3 (x1 , x2 , x3 ) = if empty (x1 ) then e

else a (s-band3 (p (x1 ), p (x2 ), p (x3 )), band3 (l (x1 ), l (x2 ), l (x3 ))) endif

;; A2-Begin-S-BAND3

Theorem: a2-empty-s-band3 empty (s-band3 (x1 , x2 , x3 )) = empty (x1 )

Theorem: a2-e-s-band3 (s-band3 (x1 , x2 , x3 ) = e) = empty (x1 )

Theorem: a2-lp-s-band3 len (s-band3 (x1 , x2 , x3 )) = len (x1 )

Theorem: a2-lpe-s-band3 eqlen (s-band3 (x1 , x2 , x3 ), x1 )

Theorem: a2-ic-s-band3 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (s-band3 (i (c x1 , x1 ), i (c x2 , x2 ), i (c x3 , x3 ))

= i (band3 (c x1 , c x2 , c x3 ), s-band3 (x1 , x2 , x3 )))

Theorem: a2-lc-s-band3 (¬ empty (x1 )) → (l (s-band3 (x1 , x2 , x3 )) = band3 (l (x1 ), l (x2 ), l (x3 )))

Theorem: a2-pc-s-band3 p (s-band3 (x1 , x2 , x3 )) = s-band3 (p (x1 ), p (x2 ), p (x3 ))

Theorem: a2-hc-s-band3 ((¬ empty (x1 )) ∧ ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 )))) → (h (s-band3 (x1 , x2 , x3 )) = band3 (h (x1 ), h (x2 ), h (x3 )))

Theorem: a2-bc-s-band3 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (b (s-band3 (x1 , x2 , x3 )) = s-band3 (b (x1 ), b (x2 ), b (x3 )))

Theorem: a2-bnc-s-band3 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (bn (n, s-band3 (x1 , x2 , x3 )) = s-band3 (bn (n, x1 ), bn (n, x2 ), bn (n, x3 )))

;; A2-End-S-BAND3
; eof:comb_band3.bm
; comb_bor.bm: Binary Or combinational element
; U7-DONE

Definition: bor (u, v) = if (u = 0) ∧ (v = 0) then 0

else 1 endif

; Everything below generated by: (bmcomb 'bor '() '(x y))

Definition: s-bor (x, y) = if empty (x) then e

else a (s-bor (p (x), p (y)), bor (l (x), l (y))) endif

;; A2-Begin-S-BOR

Theorem: a2-empty-s-bor empty (s-bor (x, y)) = empty (x)

Theorem: a2-e-s-bor (s-bor (x, y) = e) = empty (x)

Theorem: a2-lp-s-bor len (s-bor (x, y)) = len (x)

Theorem: a2-lpe-s-bor eqlen (s-bor (x, y), x)

Theorem: a2-ic-s-bor (len (x) = len (y)) → (s-bor (i (c x, x), i (c y, y)) = i (bor (c x, c y), s-bor (x, y)))

Theorem: a2-lc-s-bor (¬ empty (x)) → (l (s-bor (x, y)) = bor (l (x), l (y)))

Theorem: a2-pc-s-bor p (s-bor (x, y)) = s-bor (p (x), p (y))

Theorem: a2-hc-s-bor ((¬ empty (x)) ∧ (len (x) = len (y))) → (h (s-bor (x, y)) = bor (h (x), h (y)))

Theorem: a2-bc-s-bor (len (x) = len (y)) → (b (s-bor (x, y)) = s-bor (b (x), b (y)))

Theorem: a2-bnc-s-bor (len (x) = len (y)) → (bn (n, s-bor (x, y)) = s-bor (bn (n, x), bn (n, y)))

;; A2-End-S-BOR
; eof:comb_bor.bm
; comb_band4.bm: Binary And4 combinational element
; U7-DONE

Definition: band4 (u1 , u2 , u3 , u4 ) = if (u1 = 0) ∨ (u2 = 0) ∨ (u3 = 0) ∨ (u4 = 0) then 0

else 1 endif

; Everything below generated by: (bmcomb 'band4 '() '(x1 x2 x3 x4))

Definition: s-band4 (x1 , x2 , x3 , x4 ) = if empty (x1 ) then e

else a (s-band4 (p (x1 ), p (x2 ), p (x3 ), p (x4 )), band4 (l (x1 ), l (x2 ), l (x3 ), l (x4 ))) endif

;; A2-Begin-S-BAND4

Theorem: a2-empty-s-band4 empty (s-band4 (x1 , x2 , x3 , x4 )) = empty (x1 )

Theorem: a2-e-s-band4 (s-band4 (x1 , x2 , x3 , x4 ) = e) = empty (x1 )

Theorem: a2-lp-s-band4 len (s-band4 (x1 , x2 , x3 , x4 )) = len (x1 )

Theorem: a2-lpe-s-band4 eqlen (s-band4 (x1 , x2 , x3 , x4 ), x1 )

Theorem: a2-ic-s-band4 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 )) ∧ (len (x3 ) = len (x4 ))) → (s-band4 (i (c x1 , x1 ), i (c x2 , x2 ), i (c x3 , x3 ), i (c x4 , x4 ))

= i (band4 (c x1 , c x2 , c x3 , c x4 ), s-band4 (x1 , x2 , x3 , x4 )))

Theorem: a2-lc-s-band4 (¬ empty (x1 )) → (l (s-band4 (x1 , x2 , x3 , x4 )) = band4 (l (x1 ), l (x2 ), l (x3 ), l (x4 )))

Theorem: a2-pc-s-band4 p (s-band4 (x1 , x2 , x3 , x4 )) = s-band4 (p (x1 ), p (x2 ), p (x3 ), p (x4 ))

Theorem: a2-hc-s-band4 ((¬ empty (x1 )) ∧ ((len (x1 ) = len (x2 ))

∧ (len (x2 ) = len (x3 )) ∧ (len (x3 ) = len (x4 ))))

→ (h (s-band4 (x1 , x2 , x3 , x4 )) = band4 (h (x1 ), h (x2 ), h (x3 ), h (x4 )))

Theorem: a2-bc-s-band4 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 )) ∧ (len (x3 ) = len (x4 ))) → (b (s-band4 (x1 , x2 , x3 , x4 )) = s-band4 (b (x1 ), b (x2 ), b (x3 ), b (x4 )))

Theorem: a2-bnc-s-band4 ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 )) ∧ (len (x3 ) = len (x4 ))) → (bn (n, s-band4 (x1 , x2 , x3 , x4 ))

= s-band4 (bn (n, x1 ), bn (n, x2 ), bn (n, x3 ), bn (n, x4 )))

;; A2-End-S-BAND4
; eof:comb_band4.bm
; comb_bnot.bm: Binary Not combinational element
; U7-DONE

Definition: bnot (u) = if u = 0 then 1

else 0 endif

; Everything below generated by: (bmcomb 'bnot '() '(x))

Definition: s-bnot (x) = if empty (x) then e

else a (s-bnot (p (x)), bnot (l (x))) endif

;; A2-Begin-S-BNOT

Theorem: a2-empty-s-bnot empty (s-bnot (x)) = empty (x)

Theorem: a2-e-s-bnot (s-bnot (x) = e) = empty (x)

Theorem: a2-lp-s-bnot len (s-bnot (x)) = len (x)

Theorem: a2-lpe-s-bnot eqlen (s-bnot (x), x)

Theorem: a2-ic-s-bnot s-bnot (i (c x, x)) = i (bnot (c x), s-bnot (x))

Theorem: a2-lc-s-bnot (¬ empty (x)) → (l (s-bnot (x)) = bnot (l (x)))

Theorem: a2-pc-s-bnot p (s-bnot (x)) = s-bnot (p (x))

Theorem: a2-hc-s-bnot (¬ empty (x)) → (h (s-bnot (x)) = bnot (h (x)))

Theorem: a2-bc-s-bnot b (s-bnot (x)) = s-bnot (b (x))

Theorem: a2-bnc-s-bnot bn (n, s-bnot (x)) = s-bnot (bn (n, x))

;; A2-End-S-BNOT
; eof:comb_bnot.bm

Definition: topor-sy-bcdsbi (ln) = if ln = 'y01 then 1

elseif ln = 'y02 then 1 elseif ln = 'y03 then 1 elseif ln = 'y04 then 1 elseif ln = 'y05 then 1 elseif ln = 'y06 then 1 elseif ln = 'y07 then 1 elseif ln = 'y08 then 1 elseif ln = 'y11 then 2 elseif ln = 'y12 then 2 elseif ln = 'y13 then 2 elseif ln = 'y14 then 2 elseif ln = 'y15 then 1 elseif ln = 'y21 then 3 elseif ln = 'y22 then 3 elseif ln = 'y23 then 2 elseif ln = 'yr1 then 0 elseif ln = 'yr2 then 0 elseif ln = 'yr3 then 0 elseif ln = 'y31 then 1 elseif ln = 'y32 then 1 elseif ln = 'y41 then 2 elseif ln = 'yout then 3 else 0 endif

Definition: sy-bcdsbi (ln, x) = if ln = 'y01 then s-bnot (x)

elseif ln = 'y02 then s-bnot (x) elseif ln = 'y03 then s-bnot (sy-bcdsbi ('yr3, x)) elseif ln = 'y04 then s-bnot (sy-bcdsbi ('yr1, x)) elseif ln = 'y05 then s-bnot (sy-bcdsbi ('yr2, x)) elseif ln = 'y06 then s-bnot (sy-bcdsbi ('yr3, x)) elseif ln = 'y07 then s-bnot (sy-bcdsbi ('yr1, x)) elseif ln = 'y08 then s-bnot (sy-bcdsbi ('yr3, x)) elseif ln = 'y11 then s-band3 (sy-bcdsbi ('y01, x),

sy-bcdsbi ('yr1, x), sy-bcdsbi ('yr3, x))

elseif ln = 'y12 then s-band3 (sy-bcdsbi ('y02, x),

sy-bcdsbi ('yr2, x),

sy-bcdsbi ('y03, x))

elseif ln = 'y13 then s-band3 (sy-bcdsbi ('y04, x),

sy-bcdsbi ('y05, x), sy-bcdsbi ('y06, x))

elseif ln = 'y14 then s-band3 (x, sy-bcdsbi ('y07, x), sy-bcdsbi ('y08, x)) elseif ln = 'y15 then s-band3 (x, sy-bcdsbi ('yr1, x), sy-bcdsbi ('yr3, x)) elseif ln = 'y21 then s-bor (sy-bcdsbi ('y11, x), sy-bcdsbi ('y12, x)) elseif ln = 'y22 then s-bor (sy-bcdsbi ('y13, x), sy-bcdsbi ('y14, x)) elseif ln = 'y23 then s-bor (sy-bcdsbi ('yr2, x), sy-bcdsbi ('y15, x)) elseif ln = 'yr1 then if empty (x) then e

else i (0, sy-bcdsbi ('y21, p (x))) endif elseif ln = 'yr2 then if empty (x) then e

else i (0, sy-bcdsbi ('y22, p (x))) endif elseif ln = 'yr3 then if empty (x) then e

else i (0, sy-bcdsbi ('y23, p (x))) endif elseif ln = 'y31 then s-bnot (sy-bcdsbi ('yr1, x)) elseif ln = 'y32 then s-bnot (sy-bcdsbi ('yr2, x)) elseif ln = 'y41 then s-band4 (x,

sy-bcdsbi ('y31, x), sy-bcdsbi ('y32, x), sy-bcdsbi ('yr3, x))

elseif ln = 'yout then s-bnot (sy-bcdsbi ('y41, x)) else sfix (x) endif

;; A2-Begin-SY-BCDSBI

Theorem: a2-empty-sy-bcdsbi empty (sy-bcdsbi (ln, x)) = empty (x)

Theorem: a2-e-sy-bcdsbi (sy-bcdsbi (ln, x) = e) = empty (x)

Theorem: a2-lp-sy-bcdsbi len (sy-bcdsbi (ln, x)) = len (x)

Theorem: a2-lpe-sy-bcdsbi eqlen (sy-bcdsbi (ln, x), x)

Theorem: a2-pc-sy-bcdsbi p (sy-bcdsbi (ln, x)) = sy-bcdsbi (ln, p (x))

;; A2-End-SY-BCDSBI
;;; Circuit CORRECTNESS /Paillet:
; BCD-bits defines a correct binary coded decimal, b0 is most-significant.

Definition: bcd-bits (b0 , b1 , b2 , b3 ) = ((b0 = 0) ∨ ((b1 = 0) ∧ (b2 = 0)))

; CORRECTNESS:
;;; WHAT PAILLET ACTUALLY PROVES:

Definition: sy-b2i (ln, x) = if ln = 'yr1

then if empty (x) then e

else i (0,

s-bor (s-band3 (s-bnot (p (x)), sy-b2i ('yr1, p (x)), sy-b2i ('yr3, p (x))),

s-band3 (s-bnot (p (x)), sy-b2i ('yr2, p (x)), s-bnot (sy-b2i ('yr3, p (x)))))) endif

elseif ln = 'yr2

then if empty (x) then e

else i (0,

s-bor (s-band3 (s-bnot (sy-b2i ('yr1, p (x))), s-bnot (sy-b2i ('yr2, p (x))), s-bnot (sy-b2i ('yr3, p (x)))),

s-band3 (p (x), s-bnot (sy-b2i ('yr1, p (x))), s-bnot (sy-b2i ('yr3, p (x)))))) endif

elseif ln = 'yr3

then if empty (x) then e

else i (0,

s-bor (sy-b2i ('yr2, p (x)), s-band3 (p (x), sy-b2i ('yr1, p (x)), sy-b2i ('yr3, p (x))))) endif

else sfix (x) endif

; B2 is just a GENERALIZED sysd, and our A2 lemmas should still be true:
; The following were generated by:
; (vp (bma2sysd-aux 'sy-b2i 'sy-b2i '(x) '(band3 bor band4 bnot)))
; with A2-PC preemptively disabled.
;; A2-Begin-SY-B2I

Theorem: a2-empty-sy-b2i empty (sy-b2i (ln, x)) = empty (x)

Theorem: a2-e-sy-b2i (sy-b2i (ln, x) = e) = empty (x)

Theorem: a2-lp-sy-b2i len (sy-b2i (ln, x)) = len (x)

Theorem: a2-lpe-sy-b2i eqlen (sy-b2i (ln, x), x)

;(PROVE-LEMMA A2-PC-SY-B2I (REWRITE)
;    (EQUAL (P (SY-B2I LN X)) (SY-B2I LN (P X)))
;    ((DISABLE S-BAND3 S-BOR S-BAND4 S-BNOT A2-IC-S-BAND3 A2-IC-S-BOR
;              A2-IC-S-BAND4 A2-IC-S-BNOT)))
;; A2-End-SY-B2I
; BCDS-is-B2i is the essence of this simplification.

Theorem: bcdsbi-is-b2i (sy-bcdsbi ('yr1, x) = sy-b2i ('yr1, x)) ∧ (sy-bcdsbi ('yr2, x) = sy-b2i ('yr2, x)) ∧ (sy-bcdsbi ('yr3, x) = sy-b2i ('yr3, x))

; at this point we should never need SY-BCDSBI anymore:

Event: Disable sy-bcdsbi.

; and also he does the expansion for Yout once and for all:
; Note: A-POSTERIORI analysis indicates that this lemma is not really useful
; to BM, which is usual, since it's just a non-recursive rewrite, and we might
; as well give the expand hint at the right place.

Theorem: bcdsbi-eq-yout sy-bcdsbi ('yout, x) = s-bnot (s-band4 (x,

s-bnot (sy-b2i ('yr1, x)), s-bnot (sy-b2i ('yr2, x)), sy-b2i ('yr3, x)))

;; SECOND, he proves things about his DEROULEMENTS:
; note: all thms below are "one-shot", i.e. disabled and enabled explicitely
; NOTE: at this point we express everything in terms of B2; obviously
;       with BCDSBI-IS-B2i we can carry everything over.  This follows Paillet.

Theorem: bcdsbi-paillet-1 (len (x) = 1) → ((l (sy-b2i ('yr1, x)) = 0)

∧ (l (sy-b2i ('yr2, x)) = 0) ∧ (l (sy-b2i ('yr3, x)) = 0))

Event: Disable bcdsbi-paillet-1.

Theorem: bcdsbi-paillet-1out (len (x) = 1) → (l (sy-bcdsbi ('yout, x)) = 1)

Event: Disable bcdsbi-paillet-1out.

Theorem: bcdsbi-paillet-2 (len (x) = 2) → ((l (sy-b2i ('yr1, x)) = 0)

∧ (l (sy-b2i ('yr2, x)) = 1) ∧ (l (sy-b2i ('yr3, x)) = 0))

Event: Disable bcdsbi-paillet-2.

Theorem: bcdsbi-paillet-2out (len (x) = 2) → (l (sy-bcdsbi ('yout, x)) = 1)

Event: Disable bcdsbi-paillet-2out.

; Note that the "bitp" hyp is not explicit in Paillet...

Theorem: bcdsbi-paillet-3 ((len (x) = 3) ∧ s-bitp (x)) → ((l (sy-b2i ('yr1, x)) = bnot (l (p (x))))

∧ (l (sy-b2i ('yr2, x)) = l (p (x))) ∧ (l (sy-b2i ('yr3, x)) = 1))

Event: Disable bcdsbi-paillet-3.

Theorem: bcdsbi-paillet-3out ((len (x) = 3) ∧ s-bitp (x)) → (l (sy-bcdsbi ('yout, x)) = 1)

Event: Disable bcdsbi-paillet-3out.

Theorem: bcdsbi-paillet-4 ((len (x) = 4) ∧ s-bitp (x)) → ((l (sy-b2i ('yr1, x)) = band (bnot (l (p (x))), bnot (l (p (p (x))))))

∧ (l (sy-b2i ('yr2, x)) = 0) ∧ (l (sy-b2i ('yr3, x))

= bor (l (p (p (x))), band (l (p (x)), bnot (l (p (p (x))))))))

Event: Disable bcdsbi-paillet-4.

; and his conclusion:

Theorem: bcdsbi-paillet-4out ((len (x) = 4) ∧ s-bitp (x)) → (l (sy-bcdsbi ('yout, x))

= bor (bnot (l (x)), band (bnot (l (p (x))), bnot (l (p (p (x)))))))

Event: Disable bcdsbi-paillet-4out.

; from which he leaves to the reader the real conclusion:

Theorem: bcdsbi-paillet-4out-correct ((len (x) = 4) ∧ s-bitp (x)) → (l (sy-bcdsbi ('yout, x))

= bobi (bcd-bits (l (x), l (p (x)), l (p (p (x))), l (p (p (p (x)))))))

Event: Disable bcdsbi-paillet-4out-correct.

; and the last "re-initialization" condition:

Theorem: bcdsbi-paillet-5 ((len (x) = 5) ∧ s-bitp (x)) → ((l (sy-b2i ('yr1, x)) = 0)

∧ (l (sy-b2i ('yr2, x)) = 0) ∧ (l (sy-b2i ('yr3, x)) = 0))

Event: Disable bcdsbi-paillet-5.

;;; WHAT I CAN PROVE! :

Theorem: bcdsbi-paillet-r-correct ((¬ empty (x)) ∧ s-bitp (x)) → ((l (sy-b2i ('yr1, x))

= if (len (x) mod 4) = 1 then 0 elseif (len (x) mod 4) = 2 then 0 elseif (len (x) mod 4) = 3 then bnot (l (p (x))) else band (bnot (l (p (x))), bnot (l (p (p (x))))) endif)

∧ (l (sy-b2i ('yr2, x))

= if (len (x) mod 4) = 1 then 0 elseif (len (x) mod 4) = 2 then 1 elseif (len (x) mod 4) = 3 then l (p (x)) else 0 endif)

∧ (l (sy-b2i ('yr3, x))

= if (len (x) mod 4) = 1 then 0 elseif (len (x) mod 4) = 2 then 0 elseif (len (x) mod 4) = 3 then 1 else bor (l (p (p (x))),

band (l (p (x)), bnot (l (p (p (x)))))) endif))

; and finally, the true, general correctness of Paillet#5 :

Theorem: bcdsbi-paillet-yout-correct ((¬ empty (x)) ∧ s-bitp (x)) → (l (sy-bcdsbi ('yout, x))

= if (len (x) mod 4) = 0 then bobi (bcd-bits (l (x), l (p (x)), l (p (p (x))), l (p (p (p (x)))))) else 1 endif)

; eof: bcdsbi.bm
;))

Index

a, 2, 4–6, 8 a2-bc-s-band, 3 a2-bc-s-band3, 4 a2-bc-s-band4, 7 a2-bc-s-bnot, 8 a2-bc-s-bor, 6 a2-bnc-s-band, 3 a2-bnc-s-band3, 5 a2-bnc-s-band4, 7 a2-bnc-s-bnot, 8 a2-bnc-s-bor, 6 a2-e-s-band, 3 a2-e-s-band3, 4 a2-e-s-band4, 6 a2-e-s-bnot, 8 a2-e-s-bor, 5 a2-e-sy-b2i, 12 a2-e-sy-bcdsbi, 10 a2-empty-s-band, 3 a2-empty-s-band3, 4 a2-empty-s-band4, 6 a2-empty-s-bnot, 8 a2-empty-s-bor, 5 a2-empty-sy-b2i, 12 a2-empty-sy-bcdsbi, 10 a2-hc-s-band, 3 a2-hc-s-band3, 4 a2-hc-s-band4, 7 a2-hc-s-bnot, 8 a2-hc-s-bor, 6 a2-ic-s-band, 3 a2-ic-s-band3, 4 a2-ic-s-band4, 7 a2-ic-s-bnot, 8 a2-ic-s-bor, 5 a2-lc-s-band, 3 a2-lc-s-band3, 4 a2-lc-s-band4, 7 a2-lc-s-bnot, 8 a2-lc-s-bor, 5 a2-lp-s-band, 3 a2-lp-s-band3, 4 a2-lp-s-band4, 6 a2-lp-s-bnot, 8 a2-lp-s-bor, 5 a2-lp-sy-b2i, 12 a2-lp-sy-bcdsbi, 10 a2-lpe-s-band, 3 a2-lpe-s-band3, 4 a2-lpe-s-band4, 7 a2-lpe-s-bnot, 8 a2-lpe-s-bor, 5 a2-lpe-sy-b2i, 12 a2-lpe-sy-bcdsbi, 11 a2-pc-s-band, 3 a2-pc-s-band3, 4 a2-pc-s-band4, 7 a2-pc-s-bnot, 8 a2-pc-s-bor, 6 a2-pc-sy-bcdsbi, 11

b, 3, 4, 6–8

band, 2, 3, 14, 15

band3, 4 band4, 6, 7 bcd-bits, 11, 14, 15 bcdsbi-eq-yout, 13 bcdsbi-is-b2i, 12 bcdsbi-paillet-1, 13 bcdsbi-paillet-1out, 13 bcdsbi-paillet-2, 13 bcdsbi-paillet-2out, 13 bcdsbi-paillet-3, 14 bcdsbi-paillet-3out, 14 bcdsbi-paillet-4, 14 bcdsbi-paillet-4out, 14 bcdsbi-paillet-4out-correct, 14 bcdsbi-paillet-5, 15 bcdsbi-paillet-r-correct, 15 bcdsbi-paillet-yout-correct, 15 bn, 3, 5–8 bnot, 7, 8, 14, 15 bobi, 14, 15 bor, 5, 6, 14, 15

e, 2–6, 8, 10–12 empty, 2–8, 10–12, 15 eqlen, 3–5, 7, 8, 11, 12

h, 3, 4, 6–8

i, 3–5, 7, 8, 10–12

l, 2–8, 13–15 len, 3–8, 10, 12–15

p, 2–8, 10–12, 14, 15

s-band, 2, 3 s-band3, 4, 5, 9–12 s-band4, 6, 7, 10, 13 s-bitp, 14, 15 s-bnot, 8–11, 13 s-bor, 5, 6, 10–12 sfix, 10, 12 sy-b2i, 11–15 sy-bcdsbi, 9–15

topor-sy-bcdsbi, 9