proposition: Lemma M_capped : Forall (fun '(_, n) => n < 4) M.
proof: Proof. apply /Forall_app. constructor; [|apply /Forall_app; constructor]; apply /Forall_forall. - move=> [[]] > /in_map_iff [?] [[? <-]] _; by do ? constructor. - move=> [[]] > /in_map_iff [?] [[? <-]] _; by do ? constructor. - move=> [[]]. + move=> [|[|[|[|?]]]]; [lia..|]. move=> /in_flat_map [[[]?]] > [_] /=; intuition congruence. + move=> n [|[|[|[|?]]]]; [lia..|]. move=> /in_flat_map [[[]?]] > [_] /=; intuition congruence. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun