proposition: Fact pos_list_split n p : exists l r, pos_list n = l++p::r /\ length l = pos2nat p.
proof: Proof. induction p as [ n | n p (l & r & H1 & H2) ]. + exists nil, (map pos_nxt (pos_list n)); auto. + exists (pos0::map pos_nxt l), (map pos_nxt r); split; simpl. * rewrite H1, map_app; simpl; auto. * rewrite map_length, H2; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)