never {    /* ! [] ( (p0 /\ p1) -> ((! p1) V (p0 \/ (! p1))) ) */
T0_init:
	if
	:: ((p0) && (p1)) -> goto T0_S4
	:: (1) -> goto T0_init
	fi;
T0_S4:
	if
	:: (! ((p0)) && (p1)) -> goto accept_all
	:: ((p1)) -> goto T0_S4
	fi;
accept_all:
	skip
}