initial
assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])