never {    /* ! ( (((! g1) U (u1 || [] ! g1)) && []( o1 -> ((! g1) U (u1 || [] ! g1)))) )
 */
T0_init:
	if
	:: (! ((u1)) && (g1)) -> goto accept_S31
	:: (! ((u1))) -> goto T0_S31
	:: (! ((u1)) && (g1)) -> goto accept_all
	:: (! ((u1)) && (g1)) -> goto accept_S44
	:: (1) -> goto T0_S29
	fi;
accept_S31:
	if
	:: (! ((u1))) -> goto T0_S31
	:: (! ((u1)) && (g1)) -> goto accept_all
	:: (! ((u1)) && (g1)) -> goto T0_S44
	fi;
accept_S44:
	if
	:: ((g1)) -> goto accept_all
	:: (1) -> goto T0_S44
	fi;
T0_S31:
	if
	:: (! ((u1)) && (g1)) -> goto accept_S31
	:: (! ((u1))) -> goto T0_S31
	:: (! ((u1)) && (g1)) -> goto accept_all
	:: (! ((u1)) && (g1)) -> goto accept_S44
	fi;
T0_S44:
	if
	:: ((g1)) -> goto accept_all
	:: (1) -> goto T0_S44
	fi;
T0_S29:
	if
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_S31
	:: (! ((u1)) && (o1)) -> goto T0_S31
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_all
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_S44
	:: (1) -> goto T0_S29
	fi;
accept_all:
	skip
}