#define p (done == 0)
#define q (load == 0)
#define r (load == 1)
#define s ((in1 == a) && (in2 == b))
#define t (done == 1)
#define u (a == ((quo * b) + rem))

/* []  (p  -> q)  -> []  ((r  && s)  -> <>  (t  && u)) */