; The design team has found what they consider to be a show$-$stopping

; problem. They are not happy. They are complanining that the compiler

; is highly inefficient. They presented their analysis in a high$-$level

; meeting and management agrees. By EOD Tuesday, they want a compiler

; that never includes constants in its output and don't try to be

; smart by replacing constants with something even more

; complicated. See the lecture notes on constant propagation. Your

; job is to get this working. After a compiler team meeting, here is

; the plan.

;

; You decide to start by defining the type of the output the compiler

; should generate. It is based on NorFm but it is more restrictive, as

; it does not allow constants nested in formulas. Here is the

; definition.

; Helper data type

$($defdata NorNCFm

$($oneof var

$($list NorNCFm $\text{'}!$v NorNCFm$)))$

; no nested constants.

$($defdata NorCPFm

$($oneof bool NorNCFm$))$

; The first thing you decide to do is to see if you can come up with a

; formula of type NorFm such that the minimal formula of type NorCPFm

; is smaller $($less operators$).$

$($defconst $*$NorFM$-$large$*$ XXX$)$

$($check $($NorFMp $*$NorFM$-$large$*))$

$($defconst $*$NorCPFm$-$small$*$ XXX$)$

$($check $($NorCPFmp $*$NorCPFm$-$small$*))$

; Use ACL$2$s to check that the above two formulas are logically

; equivalent by transforming them into equivalent ACL$2$s formulas

; manually. This is an example of reduction. See the example below.

"Property $8"$

$($property XXX$)$

; For example, here is how you can check that $($a $!$v b$)$