
$$(3^{\circ})\quad\langle x,s\rangle\ \mapsto\ \left\{\begin{array}{ll}\langle s(x),s\rangle&\mbox{if$x$is defined in$s$}\\ \langle[v_{1},\ldots,v_{n}],s\ \biguplus(x\mapsto[v_{1},\ldots,v_{n}])\rangle&\mbox{otherwise($v_{i}$'s are fresh}\\ \end{array}\right.$$

If, for a variable x, the second case of the above rule has been applied, x **gets the status**
symbolic and independent **(and is represented by a vector of propositional formulae).** In other words, this status is associated to each variable that **is for the first time used not on** the left hand side of an assignment operator. For example, if a variable nX **was not defined**
beforehand, after the statement nY=nX;**, both variables are to be represented by the same** sequence of propositional variables, but nX will internally have the status independent**, while**
nY will have the status dependent. Variables with the status symbolic and independent are those that should be determined in order to solve the given problem.

Example 5.1. **Let us consider the specification for the trivial problem from Example 3.1:**
nv = nu+1; assert(nv==2);
The variable nu **is used for the first time within the first command, so it is symbolic**
(internally represented by a vector of propositional formulae) and independent. The variable nv **becomes symbolic and dependent (it depends on** nu).

Since in ursa **expressions (numerical and Boolean) may be represented in symbolic**
propositional form, the rule (4) is replaced by the following four rules:
(4'a) hi1 ⋄ i2, si 7→ hi, si (where i **equals** i1 ⋄ i2) (4'b) hi ⋄ [f
′1
, . . . , f′n
], si 7→ h[f1**, . . . , f**n] ⋄ [f
′1
, . . . , f′n
], si
(where [f1, . . . , fn**] is a binary representation of** i)
(4'c) h[f1, . . . , fn] ⋄ i, si 7→ h[f1**, . . . , f**n] ⋄ [f
′1
, . . . , f′n], si
(where [f
′1
, . . . , f′n**] is a binary representation of** i)
(4'd) h[f1**, . . . , f**n] ⋄ [f
′1
, . . . , f′n], s**i 7→ h**[f
′′
1
, . . . , f′′
n], si where, in the last rule, [f
′′
1
, . . . , f′′
n
] is a vector of propositional formulae corresponding to
[f1**, . . . , f**n] ⋄ [f
′1
, . . . , f′n**], assuming that all numerical expressions are considered unsigned**4 and all arithmetic operations are performed modulo 2n. For example, assuming that numbers are represented by vectors of length 2 (i.e., n **= 2), the rule (4'd) for the operator + is**
as follows:
h[f1, f2**] + [**f
′1
, f′2
], s**i 7→ h**[(f1 ⊕ f
′1
) ⊕ (f2 ∧ f
′2
), f2 ⊕ f
′2
], si