sgl_probe_depth
DefinitionDefinition code
import Definitions.Def_sgl_first_halt namespace SipserGacsLautemann theorem probe_depth_check : True := trivial end SipserGacsLautemann
import Definitions.Def_sgl_first_halt namespace SipserGacsLautemann theorem probe_depth_check : True := trivial end SipserGacsLautemann