Let $G$ be a graph over $32$ nodes $($namely$,$ node $0,$cdots, node $31).$ For all $0i,j31,$ there is

an edge from node $i$ to node $j$ iff $(i+3)\%32=j\%32$ or $(i+8)\%32=j\%32.(\%$ is the modular

operator in C; e$.$g$.,35\%32=3.)$ A node $i$ is even if $i$ is an even number. A node $i$ is prime if $i$

is a prime number. In particular, we define $[$even$]$ as the set $\{0,2,4,6,$cdots,$30\}$ and $[$prime$]$ as the

set $\{3,5,7,11,13,17,19,23,29,31\}.$ We use $R$ to denote the set of all edges in $G.$

$($graded on correctness and clarity. If you use explicit graph search such as DFS$,$ you receive

$0.)($coding in Python$)$ Every finite set can be coded as a BDD$.$ Please write a Python program

to decide whether the following is true:

$($StatementA$)$ for each node $u$ in $[$prime$],$ there is a node $v$ in $[$even$]$ such that $u$ can reach $v$

in a positive even number of steps.

Your code shall implement the following steps.

step$3\mathrm{.}1.$ Obtain BDDs $RR,$EVEN,PRIME for the finite sets $R,[$even$],[$prime$],$ respectively.

Pay attention to the use of BDD variables in your BDDs$.$ Your code shall also verify the following

test cases:

$RR(27,3)$ is true;

$RR(16,20)$ is false;

EVEN$(14)$ is true;

EVEN$(13)$ is false;

PRIME$(7)$ is true;

PRIME$(2)$ is false.

step$3\mathrm{.}2.$ Compute BDD $RR2$ for the set $R$@$R,$ from BDD $RR.$ Herein, $RR2$ encodes the set of

node pairs such that one can reach the other in two steps. Your code shall also verify the following

test cases:

$RR2(27,6)$ is true;

$RR2(27,9)$ is false.

step$3\mathrm{.}3.$ Compute the transitive closure RR$2$star of $RR2.$ Herein, RR$2$star encodes the set of

all node pairs such that one can reach the other in a positive even number of steps.

step$3\mathrm{.}4.$ Here comes the most difficult part. We first StatementA formally:

AAu.$(PRIME(u)$EEv.$(EVEN(v{)}^{{?}^{?}}RR2$star$(u,v))).$

There are two quantifiers in StatementA: one is "for each", and the other is "there is$".$ First,

from what you have learned from math$216($discrete math$),$ "for each" can be expressed through

"there is$".$ Second, "there is$"$ can be implemented using existential quantifier elimination method

$BDD.$smoothing $().$ As a result, the entire StatementA is a BDD without free variables and hence

it is either true or false. Return the truth value.

Many students find methods BDD$.$compose $()$ and BDD$.$smoothing $()$ are quite useful in the pack$-$

age. Please do in Python and Pyeda