definition R_uni_step_true ≝ λt1,t2.
∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
table_TM (S n) (〈t0,false〉::table) →
definition R_uni_step_true ≝ λt1,t2.
∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
table_TM (S n) (〈t0,false〉::table) →