- ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
- table_TM (S n) (〈t0,false〉::table) →
- match_in_table (〈s0,false〉::curconfig@[〈c0,false〉])
- (〈s1,false〉::newconfig@[〈c1,false〉]) mv (〈t0,false〉::table) →
+ ∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+ 0 < |table| → table_TM (S n) table →
+ match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
+ (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table →