AG ((p0.pc=L1) -> AF (p0.pc=L12)) ;
AG ((p1.pc=L1) -> AF (p1.pc=L12)) ;
AG ((p0.pc=L12) -> AF (p0.pc=L16)) ;
AG ((p1.pc=L12) -> AF (p1.pc=L16)) ;
AG (!(p0.pc=L12) + !(p1.pc=L12)) ;