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