let n be Element of NAT ; :: thesis: ( n <= 4 implies n is State of ZeroTuring )

assume A1: n <= 4 ; :: thesis: n is State of ZeroTuring

the FStates of ZeroTuring = SegM 4 by Def19;

hence n is State of ZeroTuring by A1, Th1; :: thesis: verum

assume A1: n <= 4 ; :: thesis: n is State of ZeroTuring

the FStates of ZeroTuring = SegM 4 by Def19;

hence n is State of ZeroTuring by A1, Th1; :: thesis: verum