initial
assume (= [uut_0] [uut_1])