never {    /* !([]!(term && (e1szGT0 || e2szGT0)))
 */
T0_init:
	if
	:: ((((e1szGT0) && (term)) || ((e2szGT0) && (term)))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}