set St = SegM 3;
reconsider qF = 3 as Element of SegM 3 by Th1;
reconsider p0 = 0 as Element of SegM 3 by Th1;
set Sym = {0 ,1};
take TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) ; :: thesis: ( the Symbols of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = {0 ,1} & the FStates of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = SegM 3 & the Tran of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = U3(n)Tran & the InitS of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = 0 & the AcceptS of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = 3 )
thus ( the Symbols of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = {0 ,1} & the FStates of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = SegM 3 & the Tran of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = U3(n)Tran & the InitS of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = 0 & the AcceptS of TuringStr(# {0 ,1},(SegM 3),U3(n)Tran ,p0,qF #) = 3 ) ; :: thesis: verum