:: deftheorem defines Succ_Tran TURING_1:def 16 :
Succ_Tran = (((((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);