LISA MP+oo+oo { a = 1; x = 2; } P0 | P1 ; w[once] a 3 | r[once] r1 x ; w[once] x 4 | r[once] r2 a ; exists (1:r1 = 4 /\ 1:r2 = 1)
C11 equivalent: c11-prop-src/mp+o-o+o-o.litmus