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

; ppltcpu.bm is our 1st pipelined CPU (on our way to SRC CPU):
;
; it's totally trivial and unrealistic: no jumps, and current values in
; (visible) register(s) can't be USED in instructions!  (i.e. NO LOOPS).
;
;;; (Sugared) Circuits:
#|
(setq sy-A '(SY-A (x)
(Ypc R 0 Ypcn)
(Ypcn S inc Ypc)

(Ypr S Up Ypc)
(Yi S Ui Ypr)
(Ye S Ue Yi)
(Yout R 0 Ye)
; and the cork for Ye:
(Yec1 R (UE (UI 0)) Ye)
(Yec R (UE 0) Yec1)
))
(setq sy-B '(SY-B (x)
(Ypc R 0 Ypcn)
(Ypcn S inc Ypc)
(Ypr S Up Ypc)
(Ypr2 R 0 Ypr)
(Yi S Ui Ypr2)
(Yi2 R 0 Yi)
(Ye S Ue Yi2)
(Yout R 0 Ye)
))
(setq ppltcpu '( |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_inc.bm: INCrement combinational element
; U7-DONE

Definition: inc (u) = (1 + u)

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

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

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

;; A2-Begin-S-INC

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-INC
; eof:comb_inc.bm
; comb_up.bm: Up combinational element (= fun1)
; U7-DONE
; arbitrary Char-Fun of arity 1:

Event: Introduce the function symbol up of one argument.

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

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

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

;; A2-Begin-S-UP

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UP
; eof:comb_up.bm
; comb_ui.bm: Ui combinational element (= fun1)
; U7-DONE
; arbitrary Char-Fun of arity 1:

Event: Introduce the function symbol ui of one argument.

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

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

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

;; A2-Begin-S-UI

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UI
; eof:comb_ui.bm
; comb_ue.bm: Ue combinational element (= fun1)
; U7-DONE
; arbitrary Char-Fun of arity 1:

Event: Introduce the function symbol ue of one argument.

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

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

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

;; A2-Begin-S-UE

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UE
; eof:comb_ue.bm

Definition: topor-sy-a (ln) = if ln = 'ypc then 0

elseif ln = 'ypcn then 1 elseif ln = 'ypr then 1 elseif ln = 'yi then 2 elseif ln = 'ye then 3 elseif ln = 'yout then 0 elseif ln = 'yec1 then 0 elseif ln = 'yec then 0 else 0 endif

Definition: sy-a (ln, x) = if ln = 'ypc

then if empty (x) then e

else i (0, sy-a ('ypcn, p (x))) endif elseif ln = 'ypcn then s-inc (sy-a ('ypc, x)) elseif ln = 'ypr then s-up (sy-a ('ypc, x)) elseif ln = 'yi then s-ui (sy-a ('ypr, x)) elseif ln = 'ye then s-ue (sy-a ('yi, x)) elseif ln = 'yout then if empty (x) then e

else i (0, sy-a ('ye, p (x))) endif elseif ln = 'yec1 then if empty (x) then e

else i (ue (ui (0)), sy-a ('ye, p (x))) endif elseif ln = 'yec then if empty (x) then e

else i (ue (0), sy-a ('yec1, p (x))) endif else sfix (x) endif

;; A2-Begin-SY-A

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

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

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

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

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

;; A2-End-SY-A

Definition: topor-sy-b (ln) = if ln = 'ypc then 0

elseif ln = 'ypcn then 1 elseif ln = 'ypr then 1 elseif ln = 'ypr2 then 0 elseif ln = 'yi then 1 elseif ln = 'yi2 then 0 elseif ln = 'ye then 1 elseif ln = 'yout then 0 else 0 endif

Definition: sy-b (ln, x) = if ln = 'ypc

then if empty (x) then e

else i (0, sy-b ('ypcn, p (x))) endif elseif ln = 'ypcn then s-inc (sy-b ('ypc, x)) elseif ln = 'ypr then s-up (sy-b ('ypc, x)) elseif ln = 'ypr2 then if empty (x) then e

else i (0, sy-b ('ypr, p (x))) endif elseif ln = 'yi then s-ui (sy-b ('ypr2, x)) elseif ln = 'yi2 then if empty (x) then e

else i (0, sy-b ('yi, p (x))) endif elseif ln = 'ye then s-ue (sy-b ('yi2, x)) elseif ln = 'yout then if empty (x) then e

else i (0, sy-b ('ye, p (x))) endif else sfix (x) endif

;; A2-Begin-SY-B

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

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

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

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

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

;; A2-End-SY-B
; SOME ANIMATION:
; (setq x5T (A (A (A (A (A (e) T) T) T) T) T))
;*(sy-A 'Yout x5t)
; (A (A (A (A (A (E) 0)
;      '(UE (UI (UP 0))))
;          '(UE (UI (UP 1))))
;       '(UE (UI (UP 2))))
;    '(UE (UI (UP 3))))
;*(sy-A 'Ye x5t)
; (A (A (A (A (A (E) '(UE (UI (UP 0))))
;             '(UE (UI (UP 1))))
;          '(UE (UI (UP 2))))
;       '(UE (UI (UP 3))))
;    '(UE (UI (UP 4))))
;*(sy-B 'Yout x5t)
; (A (A (A (A (A (E) 0)
;      '(UE 0))
;   '(UE (UI 0)))
;       '(UE (UI (UP 0))))
;    '(UE (UI (UP 1))))
;*(sy-B 'Ye x5t)
; (A (A (A (A (A (E) '(UE 0))
;      '(UE (UI 0)))
;          '(UE (UI (UP 0))))
;       '(UE (UI (UP 1))))
;    '(UE (UI (UP 2))))
;*
; THIS SHOWS that Yout is not PPL but YE is. Proof of PPL YE w/ cork:
; (UE 0) (UE (UI 0))
; NOTE: I should really find a way to prove such a thing without going
; back to the circuit and altering def... (w/ DECORK & CORK?)
; This takes care of the PC loop:

Theorem: eq-pc sy-b ('ypc, x) = sy-a ('ypc, x)

Theorem: eq-a-b sy-b ('ye, x) = sy-a ('yec, x)

; EQ-A-B2: this phrasing REMOVES the need for fiddling with the circuit:
; i.e. has the cork explicitely in thm.

Theorem: eq-a-b2 sy-b ('ye, x) = if empty (x) then e

else i (ue (0), if empty (p (x)) then e else i (ue (ui (0)), sy-a ('ye, p (p (x)))) endif) endif

; EQ-A-B3: this is a weaker but more legible version of the explicitely
; corked thm.

Theorem: eq-a-b3 (¬ empty (p (x))) → (sy-b ('ye, x) = i (ue (0), i (ue (ui (0)), sy-a ('ye, p (p (x))))))

; Leaving the circuit alone AND WITHOUT EXPLICITING the cork, we get:

Theorem: eq-a-b4 (¬ empty (p (x))) → (b (b (sy-b ('ye, x))) = sy-a ('ye, p (p (x))))

; eof: ppltcpu.bm
;))

Index

a, 2–4, 6 a2-bc-s-inc, 3 a2-bc-s-ue, 6 a2-bc-s-ui, 5 a2-bc-s-up, 4 a2-bnc-s-inc, 3 a2-bnc-s-ue, 6 a2-bnc-s-ui, 5 a2-bnc-s-up, 4 a2-e-s-inc, 2 a2-e-s-ue, 6 a2-e-s-ui, 5 a2-e-s-up, 4 a2-e-sy-a, 7 a2-e-sy-b, 8 a2-empty-s-inc, 2 a2-empty-s-ue, 6 a2-empty-s-ui, 5 a2-empty-s-up, 4 a2-empty-sy-a, 7 a2-empty-sy-b, 8 a2-hc-s-inc, 3 a2-hc-s-ue, 6 a2-hc-s-ui, 5 a2-hc-s-up, 4 a2-ic-s-inc, 3 a2-ic-s-ue, 6 a2-ic-s-ui, 5 a2-ic-s-up, 4 a2-lc-s-inc, 3 a2-lc-s-ue, 6 a2-lc-s-ui, 5 a2-lc-s-up, 4 a2-lp-s-inc, 3 a2-lp-s-ue, 6 a2-lp-s-ui, 5 a2-lp-s-up, 4 a2-lp-sy-a, 7 a2-lp-sy-b, 9 a2-lpe-s-inc, 3 a2-lpe-s-ue, 6 a2-lpe-s-ui, 5 a2-lpe-s-up, 4 a2-lpe-sy-a, 7 a2-lpe-sy-b, 9 a2-pc-s-inc, 3 a2-pc-s-ue, 6 a2-pc-s-ui, 5 a2-pc-s-up, 4 a2-pc-sy-a, 8 a2-pc-sy-b, 9

b, 3–6, 10 bn, 3–6

e, 2–8, 10 empty, 2–8, 10 eq-a-b, 10 eq-a-b2, 10 eq-a-b3, 10 eq-a-b4, 10 eq-pc, 10 eqlen, 3–7, 9

h, 3–6

i, 3–8, 10 inc, 2, 3

l, 2–6 len, 3–7, 9

p, 2–10

s-inc, 2, 3, 7, 8 s-ue, 6–8 s-ui, 4, 5, 7, 8 s-up, 3, 4, 7, 8 sfix, 7, 8 sy-a, 7, 8, 10 sy-b, 8–10

topor-sy-a, 7 topor-sy-b, 8

ue, 5–7, 10 ui, 4, 5, 7, 10 up, 3, 4