let n be Element of NAT ; :: thesis: ( n <= 3 implies n is State of U3(n)Turing )

assume A1: n <= 3 ; :: thesis: n is State of U3(n)Turing

the FStates of U3(n)Turing = SegM 3 by Def21;

hence n is State of U3(n)Turing by A1, Th1; :: thesis: verum

assume A1: n <= 3 ; :: thesis: n is State of U3(n)Turing

the FStates of U3(n)Turing = SegM 3 by Def21;

hence n is State of U3(n)Turing by A1, Th1; :: thesis: verum