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