Write UCLID5 code to complete the following task.

> Consider the circuit diagram of the sequential circuit with input variable x, output variable y, and register r. The output variable y is given by the negation of x xor r. The register evaluation r changes according to the circuit function next_r = x OR r. Note that once the register evaluation is [r = 1], r keeps that value. Model the circuit behaviour with a transition system where each state corresponds to an evaluation of x and r, and the initial valuation of r is 0. There are two initial states: S1: x=0, r=0 S2: x=1, r=0  Write an LTL property that checks that the output bit y is set infinitely often. You may use auxiliary variables. Use the variable names x, y and r.

Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
