+
+definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
+ mk_tape B (map ?? f (left ? t))
+ (option_map ?? f (current ? t))
+ (map ?? f (right ? t)).
+
+definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+ [tape_map ?? bit (ctape ?? c);
+ midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
+ midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
+ ].
+