take S = {[0,{},{}]}; :: thesis: ( S is with_halt & S is standard-ins )
thus ( S is with_halt & S is standard-ins ) ; :: thesis: verum