:: deftheorem Def17 defines SuccTuring TURING_1:def 17 :
for b₁ being strict TuringStr holds
( b₁ = SuccTuring iff ( the Symbols of b₁ = {0,1} & the FStates of b₁ = SegM 4 & the Tran of b₁ = Succ_Tran & the InitS of b₁ = 0 & the AcceptS of b₁ = 4 ) );