proposition: Lemma listable_space : {L : list space | forall x, In x L}.
proof: Proof. have : {L' | forall (d : direction) (t : bool) (m : TM.move), In (d, t, m) L'}. { exists (list_prod (list_prod [go_left; go_right] [true; false]) [TM.Lmove; TM.Rmove; TM.Nmove]). move=> [] [] [] /=; tauto. } move=> [L' HL']. exists ( flat_map (fun '(q, (d, t, m)) => [space_base q; space_read q; space_move q d t; space_test q d t; space_write q t m]) (list_prod (elem (TM.state M)) L')). move=> []. - move=> q. apply /in_flat_map. exists (q, (go_left, true, TM.Lmove)) => /=. split; last tauto. apply /in_prod; by [apply: elem_spec|]. - move=> q. apply /in_flat_map. exists (q, (go_left, true, TM.Lmove)) => /=. split; last tauto. apply /in_prod; by [apply: elem_spec|]. - move=> q d t. apply /in_flat_map. exists (q, (d, t, TM.Lmove)) => /=. split; last tauto. apply /in_prod; by [apply: elem_spec|]. - move=> q d t. apply /in_flat_map. exists (q, (d, t, TM.Lmove)) => /=. split; last tauto. apply /in_prod; by [apply: elem_spec|]. - move=> q a m. apply /in_flat_map. exists (q, (go_left, a, m)) => /=. split; last tauto. apply /in_prod; by [apply: elem_spec|]. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun